Extend witness grammar for type invariant
The proposal is to extend the current grammar for the by
construct.
Currently:
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
proposed:
type t = { ... } invariant { ... } by e
where all leaf of e
in result position have the shape { f1 = ...; f2 = ...}
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.