except for modules/impset.mlw (because of Fset) and modules/mach/*
(because of program cloning), the standard library now typechecks.
This is still very much the work in progress. Many functions and
predicates have still to be converted to "let function" and
"let predicate". Here are some TODOs:
- do not require the return type for "val predicate", "val lemma", etc.
- do not require explicit variant for "let rec" if the code passes
the termination check in Decl (see list.why)
- what should become "val ghost function" and what should stay just
"function" (see array.mlw, matrix.mlw, string.mlw, etc)?
- some defined functions in algebra.why and relations.why had to be
removed, so that they can be implemented with "let function" in
int.mlw (since they are defined, they cannot be instantiated with
let-functions). This seems too restrictive. One way out would be
to authorise instantiation of defined functions (with a VC).
- should we keep the keyword "model"? reuse of "abstract" in types
breaks syntax coloring ("abstract" requires closing "end" in
programs but not in types; maybe we can drop that "end" again?).
Currently, the builtin theory why3.HighOrd (or just HighOrd) must
be explicitly "use"-d. However, the type (HighOrd.func 'a 'b) can
be written ('a -> 'b), and the type (HighOrd.pred 'a) can be written
('a -> bool), and the application operation (HighOrd.(@)) can be
written as the usual juxtaposition. Thus, normally, you do not have
to write the qualifiers. The builtin theory why3.Bool (or just Bool)
is needed for "bool". The names "HighOrd", "func", "pred", and "(@)"
are not yet fixed and may change.
"eliminate_epsilon" tries to be smart when a lambda (or some other
comprehension form) occurs under equality or at the top of a definition.
We could go even further and replace (\ x . t) s with t[x <- s], without
lifting the lambda. I'm not sure it's worth it: we rarely write redexes
manually. They can and will appear through inlining, though.
Anyone who wants to construct epsilon-terms directly using the API
should remember that these are not Hilbert's epsilons: by writing
an epsilon term, you postulate the existence (though not necessarily
uniqueness) of the described object, and "eliminate_epsilon" will
happily convert it to an axiom expressing this existence. We only
use epsilons to write comprehensions whose soundness is guaranteed
by a background theory, e.g. lambda-calculus.
also, avoid the "encoding_sort" transformation, if it can be done
directly in the printer.
On the same example as in the previous commits, this gives 5x
acceleration together with some memory usage reduction.
in a series of tests on available examples, lightweight polymorphism
encoding techniques combined with a more agressive generation of
monomorphic instances (via Discriminate) show better results than
our earlier defaults.
In the same commit:
- remove Encoding_explicit (unsound), Encoding_decoexp (too naive),
and Encoding_instantiate (subsumed by Discriminate)
- rename Encoding_decorate to Encoding_tags_full and Encoding_guard
to Encoding_guards_full
- move Encoding_guards_full specific functions from Libencoding to
Encoding_guards_full
- do not apply type protection in "encoding_tptp" and remove
Protect_finite which is not needed anymore.
What was its purpose in the first place? Integers are protected
in Simplify anyway and then we can simply forget the difference
between the infinite sorts (as we do in encoding_tptp).
