- 17 Oct, 2014 1 commit
-
-
Andrei Paskevich authored
-
- 16 Oct, 2014 2 commits
-
-
Andrei Paskevich authored
- hide the closure variable - split t_app_beta into t_func_app_beta, which returns terms, and t_pred_app_beta which returns formulas Also: - check for non-recursivity in t_open_lambda - implement t_is_lambda via t_open_lambda (less efficient, but the correct code without opening would be horrendous) - drop t_app_lambda, subsumed by t_[func|pred]_app_beta - support nested lambdas in t_[func|pred]_app_beta
-
Andrei Paskevich authored
Two points for discussion: - t_lambda accepts both terms and formulas for the body. Thus, t_open_lambda, t_app_lambda, and t_app_beta can all return a term or a formula, depending on what is inside the lambda term. The caller should not forget to check. We could, in principle, always return a term (bool-typed when needed), which would exclude a possible run-time error, but then a caller who expects a formula, would have to recognize the results of the form [if f then True else False], before blindly attaching [== True] to them. Maybe still worth it: it's better if a forgotten check leads to an inefficient formula than to a type-checking error. - t_lambda takes a preid which will be the binding variable in the produced epsilon. This permits us to give names to our lambdas if we want it (what for?) and to give locations to intermediate terms inside the epsilon. Overall, it's not very useful and can probably be removed.
-
- 11 Oct, 2014 1 commit
-
-
Martin Clochard authored
-
- 10 Oct, 2014 1 commit
-
-
Martin Clochard authored
-
- 08 Oct, 2014 1 commit
-
-
Martin Clochard authored
-
- 06 Oct, 2014 1 commit
-
-
Martin Clochard authored
-
- 04 Oct, 2014 2 commits
-
-
Martin Clochard authored
-
Martin Clochard authored
-
- 03 Oct, 2014 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Martin Clochard authored
-
- 26 Sep, 2014 4 commits
-
-
Martin Clochard authored
-
Martin Clochard authored
-
MARCHE Claude authored
-
Martin Clochard authored
-
- 24 Sep, 2014 3 commits
-
-
Andrei Paskevich authored
-
Martin Clochard authored
-
Martin Clochard authored
-
- 23 Sep, 2014 1 commit
-
-
Martin Clochard authored
-
- 22 Sep, 2014 4 commits
-
-
Andrei Paskevich authored
"Never be clever for the sake of being clever." Glenn Gould The type-checking benefits of separation of the ity and region types are more important than the weight of extra functions to manipulate a second type.
-
Andrei Paskevich authored
these generalize numerous type-specific X_all and X_any functions. These are now defined as [Util.all X_fold] or [Util.any X_fold].
-
Jean-Christophe Filliâtre authored
-
Martin Clochard authored
-
- 20 Sep, 2014 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 19 Sep, 2014 3 commits
-
-
Jean-Christophe Filliâtre authored
moved from map.why to bv.why + new theories BV31, BV63, and BV64 modules mach.int.Int32 etc. now have to_bv / of_bv routines ocaml driver identify integers and bit vectors and makes use of operations such as land
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 18 Sep, 2014 11 commits
-
-
MARCHE Claude authored
(no yet displayed in IDE)
-
MARCHE Claude authored
-
Martin Clochard authored
-
Léon Gondelman authored
-
Léon Gondelman authored
-
Léon Gondelman authored
-
Léon Gondelman authored
-
Léon Gondelman authored
-
Martin Clochard authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-