 08 Mar, 2016 2 commits


Andrei Paskevich authored
also, remove the "material_type_arg" meta for (>), hardcoded now in Eliminate_algebraic

Andrei Paskevich authored

 01 Feb, 2016 1 commit


Daisuke Ishii authored
add Bool theory support.

 20 Aug, 2015 1 commit


Andrei Paskevich authored
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 letfunctions). 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?).

 20 Jan, 2014 1 commit


Andrei Paskevich authored
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 epsilonterms 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. lambdacalculus.

 06 Aug, 2013 1 commit


Andrei Paskevich authored

 19 Nov, 2012 2 commits


Daisuke Ishii authored

Daisuke Ishii authored
