Note that this is incomplete in the case of desugared/scopelang because we only
have typing for expressions yet, and the scope/program structure is different.
The code allows passing an environment of types for scope/subscope variables in
order to resolve `ELocation` terms, but that's unused until we implement
scopelang typing at the scope level.
This moves dcalc/typing.ml to shared_ast, and generalises the input type, but
without yet implementing the extra cases (these are all `assert false`): it's
just a first step.
Also add some safeguards against bad propagation of types (e.g. checking the
arrow type of functions upon application); partly disabled at the moment since
they don't pass yet but that'll be further work.
- don't print variable id on type variables, there should be no ambiguity
- print "array" as "collection" to match the language
- print just "collection" for "'a collection", which makes sense english-wise
The issue was coming from Bindlib: it stores variable bindings as closures, so
`Bindlib.box_apply f bx` actually delays the application of `f` until the term
is substituted or unboxed (likely long after we are out of the `try..with`
block).
The proposed fix is to make sure we run the wrapper outside of bindlib
applications, on explicitely unboxed terms.
This PR extends PR #331, by avoiding hard failures when pretty-printing
a Z3 model when generating a counterexample.
#331 added some Z3 variables to encode EMatch nodes that are only used
internally in the encoding, and do not correspond to any source
variable. When trying to retrieve the source variable corresponding to
this Z3 variable for pretty-printing purposes (stored in a map in the
context, called ctx.z3_vars), we thus had a hard OCaml failure due to a
Not_found exception.
This PR fixes this by ignoring internal variables during pretty-printing
of the counterexample. It also adds some unit tests for #331, although,
since counterexample generation is disabled in tests/, this specific
issue would not have been caught.
Fixes#332
Now that #272 was merged and that type information is available at every
AST node, this PR improves the Z3 encoding of pattern matching in the
verification backend. To do so, it implements the second solution
presented in #241.
Fixes#241
