Spec new encoding from #3

[bvisness]

This is producing an error that I don't know how to resolve. I have tried the following conditions:

• if nm_e = "" (fails with many flavors of "expression's type char* does not match type text")
• if |nm_e| = 0 (fails with "expression's type name does not match type (_)*")
• if ||nm_e|| = 0 (fails with "type error: undeclared grammar nm_e")
• if ||Bname|| = 0 (works, but clearly shouldn't because there are two occurrences of Bname in the grammar rule!)

It really seems like both of the first two options should work. Surely char* should be able to match text, and surely name (which is defined as char*) should match (_)*.

[rossberg]

Ah, I'm afraid the text type is for meta-level strings, which are a completely separate universe from Wasm strings or sequences. Sorry for misleading you in my earlier comment!

See my suggestion below for how you can express an empty Wasm string (as an empty sequence of codepoints).

Your second version should have worked as well, though. I'll have to investigate.

The latter two refer to the length of the binary encoding, so are not what we want here. This notation is not currently interpreted by SpecTec, so type checking may be a bit too loose.

[rossberg]

LGTM modulo fix.