Commit b7c18ad8 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Trying to regroup transformations with arguments into several files instead

of having everything in case.ml.
parent e256e3be
......@@ -200,7 +200,8 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry \
args_wrapper case \
args_wrapper generic_arg_trans_utils case apply intros \
ind_itp destruct cut \
eliminate_literal
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 smtv2_cvc_ce coq\
......
......@@ -225,13 +225,13 @@ let get_exception_message ses id fmt e =
match e with
| Controller_itp.Noprogress ->
Format.fprintf fmt "Transformation made no progress\n"
| Case.Arg_trans_type (s, ty1, ty2) ->
| Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %a \n %a"
s (print_type ses id) ty1 (print_type ses id) ty2
| Case.Arg_trans_term (s, t1, t2) ->
| Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
Format.fprintf fmt "Error in transformation %s during unification of following two terms:\n %a \n %a" s
(print_term ses id) t1 (print_term ses id) t2
| Case.Arg_trans (s) ->
| Generic_arg_trans_utils.Arg_trans (s) ->
Format.fprintf fmt "Error in transformation function: %s \n" s
| Args_wrapper.Arg_hyp_not_found (s) ->
Format.fprintf fmt "Following hypothesis was not found: %s \n" s
......
open Trans
open Term
open Decl
open Theory
open Task
open Args_wrapper
open Reduction_engine
open Generic_arg_trans_utils
(** This file contains transformations with arguments that acts on specific
declarations to refine them (rewrite, replace, apply, unfold, subst...) *)
let debug_matching = Debug.register_info_flag "print_match"
~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
(* Do as intros: introduce all premises of hypothesis pr and return a triple
(goal, list_premises, binded variables) *)
let intros f =
let rec intros_aux lp lv f =
match f.t_node with
| Tbinop (Timplies, f1, f2) ->
intros_aux (f1 :: lp) lv f2
| Tquant (Tforall, fq) ->
let vsl, _, fs = t_open_quant fq in
intros_aux lp (List.fold_left (fun v lv -> Svs.add lv v) lv vsl) fs
| _ -> (lp, lv, f) in
intros_aux [] Svs.empty f
let term_decl d =
match d.td_node with
| Decl ({d_node = Dprop (_pk, _pr, t)}) -> t
| _ -> raise (Arg_trans "term_decl")
let pr_prsymbol pr =
match pr with
| Decl {d_node = Dprop (_pk, pr, _t)} -> Some pr
| _ -> None
(* Looks for the hypothesis name and return it. If not found return None *)
let find_hypothesis (name:Ident.ident) task =
let ndecl = ref None in
let _ = task_iter (fun x -> if (
match (pr_prsymbol x.td_node) with
| None -> false
| Some pr -> Ident.id_equal pr.pr_name name) then ndecl := Some x) task in
!ndecl
(* Apply:
1) takes the hypothesis and introduce parts of it to keep only the last
element of the implication. It gathers the premises and variables in a
list.
2) try to find a good substitution for the list of variables so that last
element of implication is equal to the goal.
3) generate new goals corresponding to premises with variables instantiated
with values found in 2).
*)
let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
let name = pr.pr_name in
let g, task = Task.task_separate_goal task in
let g = term_decl g in
let d = find_hypothesis name task in
if d = None then raise (Arg_hyp_not_found "apply");
let d = Opt.get d in
let t = term_decl d in
let (lp, lv, nt) = intros t in
let (_ty, subst) = try first_order_matching lv [nt] [g] with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2
else ()); raise (Arg_trans_term ("apply", t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2
else ()); raise (Arg_trans_pattern ("apply", p1, p2))
| Reduction_engine.NoMatch None -> raise (Arg_trans ("apply"))
in
let inst_nt = t_subst subst nt in
if (Term.t_equal_nt_nl inst_nt g) then
let nlp = List.map (t_subst subst) lp in
let lt = List.map (fun ng -> Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (gen_ident "G")) ng)) nlp in
lt
else
raise (Arg_trans_term ("apply", inst_nt, g)))
let replace rev f1 f2 t =
match rev with
| true -> replace_in_term f1 f2 t
| false -> replace_in_term f2 f1 t
(* Generic fold to be put in Trans ? TODO *)
let fold (f: decl -> 'a -> 'a) (acc: 'a): 'a Trans.trans =
Trans.fold (fun t acc -> match t.task_decl.td_node with
| Decl d -> f d acc
| _ -> acc) acc
(* - If f1 unifiable to t with substitution s then return s.f2 and replace every
occurences of s.f1 with s.f2 in the rest of the term
- Else call recursively on subterms of t *)
(* If a substitution s is found then new premises are computed as e -> s.e *)
let replace_subst lp lv f1 f2 t =
(* is_replced is common to the whole execution of replace_subst. Once an
occurence is found, it changes to Some (s) so that only one instanciation
is rewrritten during execution *)
(* Note that we can't use an accumulator to do this *)
let is_replaced = ref None in
let rec replace lv f1 f2 t : Term.term =
match !is_replaced with
| Some subst -> replace_in_term (t_subst subst f1) (t_subst subst f2) t
| None ->
begin
let fom = try Some (first_order_matching lv [f1] [t]) with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2
else ()); None
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2
else ()); None
| Reduction_engine.NoMatch None -> None in
(match fom with
| None -> t_map (fun t -> replace lv f1 f2 t) t
| Some (_ty, subst) ->
let sf1 = t_subst subst f1 in
if (Term.t_equal sf1 t) then
begin
is_replaced := Some subst;
t_subst subst f2
end
else
replace lv f1 f2 t)
end in
let t = t_map (replace lv f1 f2) t in
match !is_replaced with
| None -> raise (Arg_trans "matching/replace")
| Some subst ->
(List.map (t_subst subst) lp, t)
let rewrite_in rev h h1 =
let found_eq =
(* Used to find the equality we are rewriting on *)
fold (fun d acc ->
match d.d_node with
| Dprop (Paxiom, pr, t) when Ident.id_equal pr.pr_name h.pr_name ->
let lp, lv, f = intros t in
let t1, t2 = (match f.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Support to rewrite from the right *)
if rev then (t1, t2) else (t2, t1)
| _ -> raise (Arg_bad_hypothesis ("rewrite", f))) in
Some (lp, lv, t1, t2)
| _ -> acc) None in
(* Return instantiated premises and the hypothesis correctly rewritten *)
let lp_new found_eq =
match found_eq with
| None -> raise (Arg_hyp_not_found "rewrite")
| Some (lp, lv, t1, t2) ->
fold (fun d acc ->
match d.d_node with
| Dprop (p, pr, t)
when (Ident.id_equal pr.pr_name h1.pr_name &&
(p = Paxiom || p = Pgoal)) ->
let lp, new_term = replace_subst lp lv t1 t2 t in
Some (lp, create_prop_decl p pr new_term)
| _ -> acc) None in
(* Pass the premises as new goals. Replace the former toberewritten
hypothesis to the new rewritten one *)
let recreate_tasks lp_new =
match lp_new with
| None -> raise (Arg_trans "recreate_tasks")
| Some (lp, new_term) ->
let trans_rewriting =
Trans.decl (fun d -> match d.d_node with
| Dprop (p, pr, _t)
when (Ident.id_equal pr.pr_name h1.pr_name &&
(p = Paxiom || p = Pgoal)) ->
[new_term]
| _ -> [d]) None in
let list_par =
List.map
(fun e ->
Trans.decl (fun d -> match d.d_node with
| Dprop (p, pr, _t)
when (Ident.id_equal pr.pr_name h1.pr_name &&
p = Paxiom) ->
[d]
| Dprop (Pgoal, _, _) ->
[create_prop_decl Pgoal (Decl.create_prsymbol (gen_ident "G")) e]
| _ -> [d] )
None) lp in
Trans.par (trans_rewriting :: list_par) in
(* Composing previous functions *)
Trans.bind (Trans.bind found_eq lp_new) recreate_tasks
let find_target_prop h : prsymbol trans =
Trans.store (fun task ->
match h with
| Some pr -> pr
| None -> Task.task_goal task)
let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
(* Replace occurences of t1 with t2 in h *)
let replace t1 t2 h =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace", t1, t2))
else
(* Create a new goal for equality of the two terms *)
let g = Decl.create_prop_decl Decl.Pgoal (create_prsymbol (gen_ident "G")) (t_app_infer ps_equ [t1; t2]) in
let ng = Trans.goal (fun _ _ -> [g]) in
let g = Trans.decl (fun d ->
match d.d_node with
| Dprop (p, pr, t) when (Ident.id_equal pr.pr_name h.pr_name && (p = Paxiom || p = Pgoal)) ->
[create_prop_decl p pr (replace true t1 t2 t)]
| _ -> [d]) None in
Trans.par [g; ng]
let subst to_subst =
let found_eq =
fold (fun d acc ->
match d.d_node with
| Dprop (Paxiom, pr, t) ->
let acc = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when ls_equal ls to_subst ->
Some (pr, t1, t2)
| _, Tapp (ls, []) when ls_equal ls to_subst ->
Some (pr, t2, t1)
| _ -> acc
end
| _ -> acc) in
acc
| _ -> acc) None in
let subst found_eq =
match found_eq with
| None -> raise (Arg_trans "subst") (* TODO change exception *)
| Some (pr_eq, t1, t2) ->
begin
Trans.decl (fun d ->
match d.d_node with
(* Remove equality over which we subst *)
| Dprop (Paxiom, pr, _t) when pr_equal pr pr_eq ->
[]
(* Replace in all hypothesis *)
| Dprop (kind, pr, t) ->
[create_prop_decl kind pr (t_replace t1 t2 t)]
(* TODO should replace every occurences of t1 everywhere *)
| _ -> [d]) None
end
in
Trans.bind found_eq subst
let t_replace_app unf ls_defn t =
let (vl, tls) = ls_defn in
match t.t_node with
| Tapp (ls, tl) when ls_equal unf ls ->
let mvs =
List.fold_left2 (fun acc (v: vsymbol) (t: term) ->
Mvs.add v t acc) Mvs.empty vl tl in
t_subst mvs tls
| _ -> t
let rec t_ls_replace ls ls_defn t =
t_replace_app ls ls_defn (t_map (t_ls_replace ls ls_defn) t)
let unfold unf h =
let r = ref None in
Trans.decl
(fun d ->
match d.d_node with
(* Do not work on mutually recursive functions *)
| Dlogic [(ls, ls_defn)] when ls_equal ls unf ->
r := Some (open_ls_defn ls_defn);
[d]
| Dprop (k, pr, t) when pr_equal h pr ->
begin
match !r with
| None -> [d]
| Some ls_defn ->
let t = t_ls_replace unf ls_defn t in
let new_decl = create_prop_decl k pr t in
[new_decl]
end
| _ -> [d]) None
let () = wrap_and_register ~desc:"unfold ls pr: unfold logic symbol ls in hypothesis pr. Experimental." (* TODO *)
"unfold"
(Tlsymbol (Tprsymbol Ttrans)) unfold
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Tlsymbol Ttrans) subst
let () = wrap_and_register
~desc:"replace <term1> <term2> <name> replaces occcurences of term1 by term2 in prop name"
"replace"
(Tterm (Tterm (Tprsymbol Ttrans_l))) replace
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite
(* register_transform_with_args_l *)
(* ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
(* "rewrite" *)
(* (wrap_l (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite) *)
let () = wrap_and_register
~desc:"apply <prop> applies prop to the goal" "apply"
(Tprsymbol Ttrans_l) apply
This diff is collapsed.
open Term
open Decl
open Ty
open Generic_arg_trans_utils
open Args_wrapper
(** This file contains transformations with arguments that adds/removes
declarations from the context *)
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
let cut t name =
let name =
match name with
| Some name -> name
| None -> "h"
in
let h = Decl.create_prsymbol (gen_ident name) in
let g_t = Decl.create_prop_decl Decl.Pgoal h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
let goal = Trans.add_decls [h_t] in
Trans.par [goal; goal_cut]
(* From task [delta |- G] , build the tasks [delta] |- t] and [delta, t | - G] *)
let assert_tac t name =
let name =
match name with
| Some name -> name
| None -> "h"
in
let h = Decl.create_prsymbol (gen_ident name) in
let g_t = Decl.create_prop_decl Decl.Pgoal h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
let goal = Trans.add_decls [h_t] in
Trans.par [goal_cut; goal]
(* from task [delta, name1, name2, ... namen |- G] build the task [delta |- G] *)
let remove_list name_list =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (k, pr, _) when
(k != Pgoal &&
List.exists
(fun x -> match x with
| Tsprsymbol x -> Ident.id_equal pr.pr_name x.pr_name
| _ -> false
)
name_list) ->
[]
| Dparam ls when
(List.exists
(fun x -> match x with
| Tslsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list) ->
[]
| Dlogic dl when
(* also remove all dependant recursive declarations (as expected) *)
List.exists
(fun (ls, _) -> List.exists
(fun x -> match x with
| Tslsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list)
dl ->
[]
| Dind il when
(* also remove all dependant inductive declarations (as expected) *)
List.exists
(fun (ls, _) -> List.exists
(fun x -> match x with
| Tslsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list)
(snd il) ->
[]
| Dtype ty when
(List.exists
(fun x -> match x with
| Tstysymbol x -> Ident.id_equal ty.ts_name x.ts_name
| _ -> false
)
name_list) ->
[]
| Ddata tyl when
(* also remove all dependant recursive declarations (as expected) *)
List.exists
(fun (ty, _) -> List.exists
(fun x -> match x with
| Tstysymbol x -> Ident.id_equal ty.ts_name x.ts_name
| _ -> false
)
name_list)
tyl ->
[]
| _ -> [d])
None
(* from task [delta, name1, name2, ... namen |- G] build the task [name1, name2, ... namen |- G] *)
let clear_but (l: prsymbol list) =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (Paxiom, pr, _t) when List.mem pr l ->
[d]
| Dprop (Paxiom, _pr, _t) ->
[]
| _ -> [d]) None
let use_th th =
Trans.add_tdecls [Theory.create_use th]
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument"
"clear_but"
(Tprlist Ttrans) clear_but
let () = wrap_and_register
~desc:"cut <term> [name] makes a cut with hypothesis 'name: term'"
"cut"
(Tformula (Topt ("as",Tstring Ttrans_l))) cut
let () = wrap_and_register
~desc:"cut <term> [name] makes an assert with hypothesis 'name: term'"
"assert"
(Tformula (Topt ("as",Tstring Ttrans_l))) assert_tac
let () = wrap_and_register
~desc:"remove <prop list>: removes a list of hypothesis given by their names separated with ','. Example: remove_list a,b,c "
"remove"
(Tlist Ttrans) (fun l -> remove_list l)
let () = wrap_and_register
~desc:"use_th <theory> imports the theory" "use_th"
(Ttheory Ttrans) use_th
open Term
open Decl
open Args_wrapper
open Generic_arg_trans_utils
(** This file contains transformations with arguments that eliminates logic
connectors (instantiate, destruct, destruct_alg). *)
let create_constant ty =
let fresh_name = Ident.id_fresh "x" in
let ls = create_lsymbol fresh_name [] (Some ty) in
(ls, create_param_decl ls)
let rec return_list list_types type_subst =
match list_types with
| [] -> []
| hd :: tl ->
create_constant (Ty.ty_inst type_subst hd) :: return_list tl type_subst
let my_ls_app_inst ls ty =
match ls.ls_value, ty with
| Some _, None -> raise (PredicateSymbolExpected ls)
| None, Some _ -> raise (FunctionSymbolExpected ls)
| Some vty, Some ty -> Ty.ty_match Ty.Mtv.empty vty ty
| None, None -> Ty.Mtv.empty
let rec build_decls cls x =
match cls with
| [] -> []
| (cs, _) :: tl ->
let type_subst = my_ls_app_inst cs x.t_ty in
let l = return_list cs.ls_args type_subst in
let ht = t_equ x
(t_app cs (List.map (fun x -> t_app_infer (fst x) []) l) x.t_ty) in
let h = Decl.create_prsymbol (gen_ident "h") in
let new_hyp = Decl.create_prop_decl Decl.Paxiom h ht in
((List.map snd l) @ [new_hyp]) :: build_decls tl x
(* This tactic acts on a term of algebraic type. It introduces one
new goal per constructor of the type and introduce corresponding
variables. It also introduce the equality between the term and
its destruction in the context.
*)
let destruct_alg (x: term) : Task.task Trans.tlist =
let ty = x.t_ty in
let r = ref [] in
match ty with
| None -> raise (Cannot_infer_type "destruct")
| Some ty ->
begin
match ty.Ty.ty_node with
| Ty.Tyvar _ -> raise (Cannot_infer_type "destruct")
| Ty.Tyapp (ts, _) ->
Trans.decl_l (fun d ->
match d.d_node with
| Ddata dls ->
(try
(let cls = List.assoc ts dls in
r := build_decls cls x;
[[d]]
)
with Not_found -> [[d]])
| Dprop (Pgoal, _, _) ->
if !r = [] then [[d]] else List.map (fun x -> x @ [d]) !r
| _ -> [[d]]) None
end
(* Destruct the head term of an hypothesis if it is either
conjunction, disjunction or exists *)
let destruct pr : Task.task Trans.tlist =
Trans.decl_l (fun d ->
match d.d_node with
| Dprop (Paxiom, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
begin
match ht.t_node with
| Tbinop (Tand, t1, t2) ->
let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
[[new_decl1;new_decl2]]
| Tbinop (Tor, t1, t2) ->
let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
[[new_decl1];[new_decl2]]
| Tquant (Texists, tb) ->
begin
let (vsl, tr, te) = Term.t_open_quant tb in
match vsl with
| x :: tl ->
let ls = create_lsymbol (Ident.id_clone x.vs_name) [] (Some x.vs_ty) in
let tx = fs_app ls [] x.vs_ty in
let x_decl = create_param_decl ls in
(try
let part_t = t_subst_single x tx te in
let new_t = t_quant_close Texists tl tr part_t in
let new_pr = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl = create_prop_decl Paxiom new_pr new_t in
[[d; x_decl; new_decl]]
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("destruct_exists", ty1, ty2)))
| [] -> raise (Arg_trans ("destruct_exists"))
end