Commit 9c20cd7c authored by Andrei Paskevich's avatar Andrei Paskevich

"eliminate_epsilon" added in drivers

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.
parent a8b30bac
......@@ -126,6 +126,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
encoding_guards encoding_tags encoding_twin \
encoding_sort simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eliminate_epsilon \
eval_match instantiate_predicate smoke_detector
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
......
......@@ -22,6 +22,7 @@ transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "simplify_formula"
......
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
transformation "eliminate_let"
......
......@@ -7,6 +7,7 @@ time "why3cpulimit time : %s s"
(* À discuter *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_projections"
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -24,6 +24,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -17,6 +17,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
......
......@@ -6,6 +6,7 @@ valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_epsilon"
transformation "eliminate_projections"
transformation "simplify_formula"
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
transformation "eliminate_epsilon"
(*transformation "eliminate_if"*)
transformation "eliminate_let"
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -30,6 +30,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
transformation "eliminate_let"
......
......@@ -12,6 +12,8 @@ transformation "eliminate_mutual_recursion"
(* though we could do better, we only use recursion on one argument *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_epsilon"
(* PVS only has simple patterns *)
transformation "compile_match"
transformation "eliminate_projections"
......
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition" (*_func*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "discriminate"
transformation "encoding_smt"
......
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
......
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -9,6 +9,7 @@ transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "discriminate"
transformation "encoding_smt"
......
......@@ -9,6 +9,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Ident
open Term
open Decl
let rec lift_f acc t = match t.t_node with
| (Tapp (ps, [t1; {t_node = Teps fb}])
| Tapp (ps, [{t_node = Teps fb}; t1]))
when ls_equal ps ps_equ ->
let vs, f = t_open_bound fb in
lift_f acc (t_let_close_simp vs t1 f)
| Teps fb ->
let vl = Mvs.keys (t_vars t) in
let vs, f = t_open_bound fb in
let (abst,axml), f = lift_f acc f in
let tyl = List.map (fun x -> x.vs_ty) vl in
let ls = create_fsymbol (id_clone vs.vs_name) tyl vs.vs_ty in
let t = t_app ls (List.map t_var vl) t.t_ty in
let f = t_forall_close_merge vl (t_subst_single vs t f) in
let id = id_derive (vs.vs_name.id_string ^ "_def") vs.vs_name in
let ax = create_prop_decl Paxiom (create_prsymbol id) f in
(create_param_decl ls :: abst, ax :: axml), t
| _ ->
t_map_fold lift_f acc t
let lift_l (acc,dl) (ls,ld) =
let vl, t, close = open_ls_defn_cb ld in
match t.t_node with
| Teps fb ->
let vs, f = t_open_bound fb in
let (abst,axml), f = lift_f acc f in
let t = t_app ls (List.map t_var vl) t.t_ty in
let f = t_forall_close_merge vl (t_subst_single vs t f) in
let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
let ax = create_prop_decl Paxiom (create_prsymbol id) f in
(create_param_decl ls :: abst, ax :: axml), dl
| _ ->
let acc, t = lift_f acc t in
acc, close ls vl t :: dl
let lift_d d = match d.d_node with
| Dlogic dl ->
let (abst,axml), dl = List.fold_left lift_l (([],[]),[]) dl in
if dl = [] then List.rev_append abst (List.rev axml) else
let d = create_logic_decl (List.rev dl) in
let add_ax (axml1, axml2) ax =
if Sid.disjoint ax.d_syms d.d_news
then ax :: axml1, axml2 else axml1, ax :: axml2 in
let axml1, axml2 = List.fold_left add_ax ([],[]) axml in
List.rev_append abst (axml1 @ d :: axml2)
| _ ->
let (abst,axml), d = decl_map_fold lift_f ([],[]) d in
List.rev_append abst (List.rev_append axml [d])
let eliminate_epsilon = Trans.decl lift_d None
let () = Trans.register_transform "eliminate_epsilon" eliminate_epsilon
~desc:"Eliminate@ lambda-terms@ and@ other@ comprehension@ forms."
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val eliminate_epsilon : Task.task Trans.trans
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment