This improves on #121 by adding as simple kind system that separates format types from value types.
Expression evaluation can only return a value type, not a format type. In particular variables can only evaluate to values, not formats. This makes it impossible to put a format in a record or a tuple or pattern match on formats or anything like that.
Let bindings work for value types, let name := expr in format behaves as you would expect.
Dynamic bindings compile a dynamic format: dynamic name := format in format will compile the specified dynamic format to a decoder that can be applied by name.
Compiled decoders live in the scope, stored in a ScopeEntry that is either a value or a decoder.
As far as I can tell this scheme is sound and seems a lot easier to prove that it's sound.
This improves on #121 by adding as simple kind system that separates format types from value types.
Expression evaluation can only return a value type, not a format type. In particular variables can only evaluate to values, not formats. This makes it impossible to put a format in a record or a tuple or pattern match on formats or anything like that.
Let bindings work for value types,
let name := expr in formatbehaves as you would expect.Dynamic bindings compile a dynamic format:
dynamic name := format in formatwill compile the specified dynamic format to a decoder that can be applied by name.Compiled decoders live in the scope, stored in a ScopeEntry that is either a value or a decoder.
As far as I can tell this scheme is sound and seems a lot easier to prove that it's sound.