Add signature for alloctypes

[ShinWonho]

Hello, I am currently working on converting the DSL you wrote in wasm3 into AL to demonstrate the generality of the SpecTec approach. Fortunately, most of them seem to be converted well with just a few minor adjustments. However, one part that isn't converted properly is the allocmodule, as there is no allocation for the type of module instance. Fortunately, just defining the signature of the alloctypes function was enough to successfully complete the conversion of allocmodule. Now, I'm trying to define the body of the alloctypes function. But there is a typo in the gc proposal, making it hard to comprehend, and it is defined differently in function reference proposal. So, I'm having difficulty understanding how alloctype* should be defined. Could you please provide some guidance on the definition?

• allocating type in gc proposal

  

• allocating type in function reference proposal

(Perhaps 'alloctypes' is not a critical component for execution. If that's the case, please kindly inform me, and we can postpone its body.)

[rossberg]

Oops, indeed the DSL spec is missing the alloctypes function.

The GC proposal adds recursive types, so the definition becomes quite a bit more complicated than it still is in the function refs proposal: it has to first "roll up" the types, which substitutes the type indices internal to the recursion, and then it has to do a regular substitution for the others, which all must be defined before the recursion we currently looking at (hence the [0:x_i] on the right).

I don't think there is a typo in the spec (other than the wrong bracket), but it is a bit hard to read in the way it's trying to avoid a recursion. Please see #40 for a more readable formulation.

[ShinWonho]

Thank you for the quick answer! Now, I get it.