This PR implements a grammar definition construct and specifies Wasm's binary grammars. See Language.md and spec for details. For now, grammars are simply erased when elaborating into the IL, I doubt we'll do something smart with them anytime soon.
However, this required another extension to the DSL:
Integers. While at it, and in order to deal with floats later, I generalised numbers to a hierarchy nat<int<rat<real. Subsumption is explicit in the IL using SubE (could also introduce a separate expression form if folks prefer).
As a consequence, Overloading. Required a rewrite of expression elaboration to a more properly bidirectional approach. In the IL, numeric operators are now annotated with their type.
Spec'ing the binary format also required tweaking and fixing some corners I had previously cut in the spec itself:
Introduction of type indices and corresponding rules (previously we had inlined all function types).
Introduction of block types (previously just were an inlined function type as well).
Refined abstract syntax of load/stores to use memop.
rossberg
commented
11 months ago
This PR implements a
grammardefinition construct and specifies Wasm's binary grammars. See Language.md and spec for details. For now, grammars are simply erased when elaborating into the IL, I doubt we'll do something smart with them anytime soon.However, this required another extension to the DSL:
Integers. While at it, and in order to deal with floats later, I generalised numbers to a hierarchy nat<int<rat<real. Subsumption is explicit in the IL using SubE (could also introduce a separate expression form if folks prefer).
As a consequence, Overloading. Required a rewrite of expression elaboration to a more properly bidirectional approach. In the IL, numeric operators are now annotated with their type.
Spec'ing the binary format also required tweaking and fixing some corners I had previously cut in the spec itself:
Introduction of type indices and corresponding rules (previously we had inlined all function types).
Introduction of block types (previously just were an inlined function type as well).
Refined abstract syntax of load/stores to use memop.
Fixing the abstract syntax of SELECT.