Commit e5724510 authored by Johannes Kanig's avatar Johannes Kanig

different variant for epsilon-lifting

parent aa573b15
......@@ -17,39 +17,51 @@
(* *)
(**************************************************************************)
open Close_epsilon
open Term
open Theory
open Task
let rec term acc t =
match t.t_node with
| Teps fb ->
let fv = Svs.elements (t_freevars Svs.empty t) in
let x, f = f_open_bound fb in
let acc, f = form acc f in
let tys = List.map (fun x -> x.vs_ty) fv in
let xs = Ident.id_derive "epsilon" x.vs_name in
let xl = create_fsymbol xs tys x.vs_ty in
let acc = add_decl acc (Decl.create_logic_decl [xl,None]) in
let axs =
Decl.create_prsymbol (Ident.id_derive "epsilon_def" x.vs_name) in
let xlapp = t_app xl (List.map (fun x -> t_var x) fv) t.t_ty in
let f = f_forall_close_merge fv (f_subst_single x xlapp f) in
let acc = add_decl acc (Decl.create_prop_decl Decl.Paxiom axs f) in
acc, xlapp
| _ -> t_map_fold term form acc t
type lift_kind =
(* | Goal (* prove the existence of a witness *) *)
| Implied (* require the existence of a witness in an axiom *)
| Implicit (* do not require a witness *)
and form acc f = f_map_fold term form acc f
let lift kind =
let rec term acc t =
match t.t_node with
| Teps fb ->
let fv = Svs.elements (t_freevars Svs.empty t) in
let x, f = f_open_bound fb in
let acc, f = form acc f in
let tys = List.map (fun x -> x.vs_ty) fv in
let xs = Ident.id_derive "epsilon" x.vs_name in
let xl = create_fsymbol xs tys x.vs_ty in
let acc = add_decl acc (Decl.create_logic_decl [xl,None]) in
let axs =
Decl.create_prsymbol (Ident.id_derive ("epsilon_def") x.vs_name) in
let xlapp = t_app xl (List.map (fun x -> t_var x) fv) t.t_ty in
let f =
match kind with
(* assume that lambdas always exist *)
| Implied when not (is_lambda t) ->
f_forall_close_merge fv
(f_implies (f_exists_close [x] [] f) (f_subst_single x xlapp f))
| _ -> f_subst_single x xlapp f
in
let acc = add_decl acc (Decl.create_prop_decl Decl.Paxiom axs f) in
acc, xlapp
| _ -> t_map_fold term form acc t
and form acc f = f_map_fold term form acc f in
fun th acc ->
let th = th.task_decl in
match th.td_node with
| Decl d ->
let acc, d = Decl.decl_map_fold term form acc d in
add_decl acc d
| _ -> add_tdecl acc th
let lift th acc =
let th = th.task_decl in
match th.td_node with
| Decl d ->
let acc, d = Decl.decl_map_fold term form acc d in
add_decl acc d
| _ -> add_tdecl acc th
let lift_epsilon = Trans.fold lift None
let lift_epsilon = Trans.fold (lift Implicit) None
let () = Trans.register_transform "lift_epsilon" lift_epsilon
......
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