Syntax and validation for struct.new_desc

[tlively]

And struct.new_default_desc. Also update the valiation for struct.new and struct.new_default to require empty descriptors. Add an explanation of expansion to desctype to the validation conventions section and teach SpecTec about the new ExpandDesc relation to avoid errors during rendering.

[rossberg]

Heads-up: busy with POPL deadline, will review next week.

[tlively]

Sounds good, thanks for the heads up. I'll continue to upload PRs, but no rush on the reviews.

[rossberg]

Couple of nits below, but I think they are actually moot considering the following more important question:

I'm not sure why we need both Expand and ExpandDesc instead of merely modifying the existing Expand. As defined, Expand: deftype ~~ comptype and ExpandDesc: deftype ~~ comptype actually are equivalent (the latter pattern-matching describestype? descriptortype? as both empty).

(One motivation to have both might be to avoid a lot of clutter in the future, should we allow describes on more types than just structs — instead of matching describestype? descriptortype? all over the place, the existing Expand could be a shorthand building that in. However, in that case we'd need different notation, or rendered "deftype ≈ comptype" could ambiguously mean either expanding to a the underlying comptype via Expand, ignoring the desc clauses, or expanding to a desctype with empty desc clause via ExpandDesc.)

In addition, I think you missed a bunch of uses of Expand on structs in 7.1.

[tlively]

I'm not sure why we need both Expand and ExpandDesc instead of merely modifying the existing Expand. As defined, Expand: deftype ~~ comptype and ExpandDesc: deftype ~~ comptype actually are equivalent (the latter pattern-matching describestype? descriptortype? as both empty).

The point was to reduce clutter for instructions that don't care about the presence of descriptor or described types, which is almost all of them. I guess pattern-matching both as empty works out for everything that's not a struct, though, so in practice it might only be struct.get and struct.set that have extra clutter. I'm happy to do it that way if you want, but it seems more principled to have a separate expansion that we use only when we actually care about the descriptor or describes types.

[rossberg]

Yeah, I was wondering if that was the intention. That's fine, too, but for that you'll need to change the definition of Expand accordingly. Also, you need to differentiate both expansions by syntax to avoid the ambiguity after rendering that I mentioned above.

[tlively]

As defined, Expand: deftype ~~ comptype and ExpandDesc: deftype ~~ comptype actually are equivalent (the latter pattern-matching describestype? descriptortype? as both empty).

Actually, I don't think this is true. ExpandDesc (now Expand_desc) is defined with $expanddt_to_desctype and Expand is defined in terms of $expanddt, which now calls $expanddt_to_desctype and matches any descriptor or describes.

However, in that case we'd need different notation, or rendered "deftype ≈ comptype" could ambiguously mean either expanding to a the underlying comptype via Expand, ignoring the desc clauses, or expanding to a desctype with empty desc clause via ExpandDesc.)

Makes sense. Do you have a suggestion for the different notation? Maybe ≈_desc?

In addition, I think you missed a bunch of uses of Expand on structs in 7.1.

Not sure what this is referring to. There is no section 7.1.

[rossberg]

As defined, Expand: deftype ~~ comptype and ExpandDesc: deftype ~~ comptype actually are equivalent (the latter pattern-matching describestype? descriptortype? as both empty).

Actually, I don't think this is true. ExpandDesc (now Expand_desc) is defined with $expanddt_to_desctype and Expand is defined in terms of $expanddt, which now calls $expanddt_to_desctype and matches any descriptor or describes.

Ah, sorry, you're right, I missed that that change already happened in an earlier PR.

However, in that case we'd need different notation, or rendered "deftype ≈ comptype" could ambiguously mean either expanding to a the underlying comptype via Expand, ignoring the desc clauses, or expanding to a desctype with empty desc clause via ExpandDesc.)

Makes sense. Do you have a suggestion for the different notation? Maybe ≈_desc?

Yeah, that clashes a bit with ≈_C which we already use and where the subscript is an actual operand.

I would tend to use a different but appropriately related operator, perhaps Latex \sim (a single ~). But that would have to be added to SpecTec. I could do that, unless you want to give it a try yourself. :)

In addition, I think you missed a bunch of uses of Expand on structs in 7.1.

Not sure what this is referring to. There is no section 7.1.

File 7.1-*. But this comment was under the assumption that Expand was unchanged, so you can disregard it.