Commit 35418b73 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

fixes #19

Adding a new tactic apply_with which allows to give an ordered list of
terms to instantiate variables that are not found by apply. Same for
rewrite with rewrite_with. These tactics will be merged with apply/rewrite
when detached are implemented. This needs to be tested extensively.
Also, print terms with their types in errors.
parent 9e77f483
module Issue19
module I19_simplint
use import int.Int
......@@ -6,26 +6,50 @@ module Issue19
goal g: 0 < 2
(* we want to do
apply H with 1
to generate two new goals "0 < 1" and "1 < 2"
end
*)
module I19_simplpoly
type t
predicate r t t
axiom trans: forall x y z. r x y -> r y z -> r x z
constant a:t
constant b:t
constant c:t
axiom a1: r a b
axiom a2: r b c
goal test: r a c
end
module I19_simplpoly2
type t
type t'
predicate r 'a t t
axiom trans: forall a:'a. forall a':'a. forall x y z. r a x y -> r a y z -> r a' x z
constant a:t
constant b:t
constant c:t
axiom trans_eq: forall x y z. r 4 x y -> r 5 y z -> a = z
axiom a1: forall x:'a. r x a b
axiom a2: forall x:'a. r x b c
(* apply trans 1,b,b does not work *)
goal test: r 1 a c
(* apply trans with b *)
end
\ No newline at end of file
end
......@@ -88,6 +88,11 @@ let print_term s id fmt t =
let print_type s id fmt t =
let module P = (val (p s id)) in P.print_ty fmt t
let print_opt_type s id fmt t =
match t with
| None -> Format.fprintf fmt "bool"
| Some t -> print_type s id fmt t
let print_ts s id fmt t =
let module P = (val (p s id)) in P.print_ts fmt t
......@@ -215,13 +220,15 @@ let get_exception_message ses id e =
| Generic_arg_trans_utils.Arg_trans s ->
Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
Pp.sprintf "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, Loc.dummy_position, ""
Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
(print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty
(print_term ses id) t2 (print_opt_type ses id) t2.Term.t_ty,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_pattern (s, pa1, pa2) ->
Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
s (print_pat ses id) pa1 (print_pat ses id) pa2, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
Pp.sprintf "Error in transformation %s during unification of the following types:\n %a \n %a"
s (print_type ses id) ty1 (print_type ses id) ty2, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_bad_hypothesis ("rewrite", _t) ->
Pp.sprintf "Not a rewrite hypothesis", Loc.dummy_position, ""
......
......@@ -34,9 +34,9 @@ let intros f =
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
intros_aux lp (lv @ vsl) fs
| _ -> (lp, lv, f) in
intros_aux [] Svs.empty f
intros_aux [] [] f
let term_decl d =
match d.td_node with
......@@ -57,6 +57,95 @@ let find_hypothesis (name:Ident.ident) task =
| Some pr -> Ident.id_equal pr.pr_name name) then ndecl := Some x) task in
!ndecl
(* [with_terms subst_ty subst lv wt]: Takes the list of variables in lv that are
not part of the substitution and try to match them with the list of values
from wt (ordered). *)
(* TODO we could use something simpler than first_order_matching here. *)
let with_terms ~trans_name subst_ty subst lv withed_terms =
Debug.dprintf debug_matching "Calling with_terms@.";
(* Get the list of variables of lv that are not in subst. *)
let lv, slv = List.fold_left (fun (acc, accs) v ->
match (Mvs.find v subst) with
| _ -> acc, accs
| exception Not_found -> t_var v :: acc, Svs.add v accs) ([], Svs.empty) lv
in
let lv = List.rev lv in
(* Length checking for nice errors *)
let diff = Svs.cardinal slv - List.length withed_terms in
match diff with
| _ when diff < 0 ->
Debug.dprintf debug_matching "Too many withed terms@.";
raise (Arg_trans (trans_name ^ ": the last " ^
string_of_int diff
^ " terms in with are useless"))
| _ when diff > 0 ->
Debug.dprintf debug_matching "Not enough withed terms@.";
raise (Arg_trans (trans_name ^ ": there are " ^
string_of_int diff
^ " terms missing"))
| _ (* when diff = 0 *) ->
let new_subst_ty, new_subst =
try first_order_matching slv lv withed_terms with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term (trans_name, t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2;
raise (Arg_trans_pattern (trans_name, p1, p2))
| Reduction_engine.NoMatch None ->
Debug.dprintf debug_matching "with_terms: No match@.";
raise (Arg_trans trans_name)
in
let subst_ty = Ty.Mtv.union
(fun _x y z ->
if Ty.ty_equal y z then
Some y
else
raise (Arg_trans_type (trans_name ^ ": ", y, z)))
subst_ty new_subst_ty
in
let subst =
Mvs.union (fun _x y z ->
if Term.t_equal_nt_nl y z then
Some y
else
raise (Arg_trans_term (trans_name ^ ": ", y, z)))
subst new_subst
in
subst_ty, subst
(* This function first try to match left_term and right_term with a substitution
on lv/slv. It then tries to fill the holes with the list of withed_terms.
trans_name is used for nice error messages. Errors are returned when the size
of withed_terms is incorrect.
*)
(* TODO Having both slv and lv is redundant but we need both an Svs and the
order of elements: to be improved.
*)
let matching_with_terms ~trans_name slv lv left_term right_term withed_terms =
let (subst_ty, subst) =
try first_order_matching slv [left_term] [right_term] with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term (trans_name, t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2;
raise (Arg_trans_pattern (trans_name, p1, p2))
| Reduction_engine.NoMatch None -> raise (Arg_trans trans_name)
in
let subst_ty, subst =
let withed_terms = match withed_terms with None -> [] | Some l -> l in
with_terms ~trans_name subst_ty subst lv withed_terms
in
subst_ty, subst
(* 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
......@@ -66,7 +155,7 @@ let find_hypothesis (name:Ident.ident) task =
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 apply pr withed_terms : 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
......@@ -75,33 +164,17 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
let d = Opt.get d in
let t = term_decl d in
let (lp, lv, nt) = intros t in
let (subst_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
Svs.iter
(fun v ->
try ignore (Mvs.find v subst)
with Not_found ->
raise (Arg_trans ("no instance found for " ^ v.vs_name.Ident.id_string)))
lv;
let inst_nt = t_ty_subst subst_ty subst nt in
if (Term.t_equal_nt_nl inst_nt g) then
let nlp = List.map (t_ty_subst subst_ty 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 slv = List.fold_left (fun acc v -> Svs.add v acc) Svs.empty lv in
match matching_with_terms ~trans_name:"apply" slv lv nt g withed_terms with
| exception e -> raise e
| subst_ty, subst ->
let inst_nt = t_ty_subst subst_ty subst nt in
if (Term.t_equal_nt_nl inst_nt g) then
let nlp = List.map (t_ty_subst subst_ty subst) lp in
List.map (fun ng -> Task.add_decl task
(create_prop_decl Pgoal (create_prsymbol (gen_ident "G")) ng)) nlp
else
raise (Arg_trans_term ("apply", inst_nt, g)))
let replace rev f1 f2 t =
match rev with
......@@ -118,52 +191,48 @@ let fold (f: decl -> 'a -> 'a) (acc: 'a): 'a Trans.trans =
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 =
let replace_subst lp lv f1 f2 withed_terms 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_ty,subst) ->
replace_in_term (t_ty_subst subst_ty subst f1) (t_ty_subst subst_ty 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 (subst_ty, subst) ->
let sf1 = t_ty_subst subst_ty subst f1 in
if (Term.t_equal sf1 t) then
begin
is_replaced := Some (subst_ty,subst);
t_ty_subst subst_ty 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
(* first_order_matching requires an Svs but we still need the order in
with_terms. *)
let slv = List.fold_left (fun acc v -> Svs.add v acc) Svs.empty lv in
let rec replace is_replaced f1 f2 t : _ * Term.term =
match is_replaced with
| Some(subst_ty,subst) ->
is_replaced, replace_in_term (t_ty_subst subst_ty subst f1) (t_ty_subst subst_ty subst f2) t
| None ->
begin
(* Catch any error from first_order_matching or with_terms. *)
match matching_with_terms ~trans_name:"rewrite" slv lv f1 t (Some withed_terms) with
| exception _ -> Term.t_map_fold
(fun is_replaced t -> replace is_replaced f1 f2 t)
is_replaced t
| subst_ty, subst ->
let sf1 = t_ty_subst subst_ty subst f1 in
if (Term.t_equal_nt_nl sf1 t) then
Some (subst_ty, subst), t_ty_subst subst_ty subst f2
else
t_map_fold (fun is_replaced t -> replace is_replaced f1 f2 t)
is_replaced t
end
in
let is_replaced, t =
t_map_fold (fun is_replaced t -> replace is_replaced f1 f2 t) None t in
match is_replaced with
| None -> raise (Arg_trans "matching/replace")
| Some(subst_ty,subst) ->
(List.map (t_ty_subst subst_ty subst) lp, t)
(List.map (t_ty_subst subst_ty subst) lp, t)
let rewrite_in rev h h1 =
let rewrite_in rev with_terms h h1 =
let found_eq =
(* Used to find the equality we are rewriting on *)
(* TODO here should fold with a boolean stating if we found equality yet to
not go through all possible hypotheses *)
fold (fun d acc ->
match d.d_node with
| Dprop (Paxiom, pr, t) when Ident.id_equal pr.pr_name h.pr_name ->
......@@ -185,7 +254,7 @@ let rewrite_in rev h h1 =
| 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
let lp, new_term = replace_subst lp lv t1 t2 with_terms t in
Some (lp, create_prop_decl p pr new_term)
| _ -> acc) None in
(* Pass the premises as new goals. Replace the former toberewritten
......@@ -224,7 +293,13 @@ let find_target_prop h : prsymbol trans =
| Some pr -> pr
| None -> Task.task_goal task)
let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
let rewrite with_terms rev h h1 =
let with_terms =
match with_terms with
| None -> []
| Some l -> l
in
Trans.bind (find_target_prop h1) (rewrite_in (not rev) with_terms h)
(* This function is used to detect when we found the hypothesis/goal we want
to replace/unfold into. *)
......@@ -489,7 +564,12 @@ let () = wrap_and_register
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
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) (rewrite None)
let _ = wrap_and_register
~desc:"rewrite_with [<-] <name> [in] <name2> with <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite_with"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol (Topt ("with", Ttermlist Ttrans_l))))))) (fun rev h h1opt term_list -> rewrite term_list rev h h1opt)
(* register_transform_with_args_l *)
(* ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
......@@ -498,4 +578,14 @@ let _ = wrap_and_register
let () = wrap_and_register
~desc:"apply <prop> applies prop to the goal" "apply"
(Tprsymbol Ttrans_l) apply
(Tprsymbol Ttrans_l) (fun x -> apply x None)
let () = wrap_and_register
~desc:"apply_with <prop> <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply_with"
(* TODO ideally apply and apply_with should be the same tactic but with an
(Toptbool "with") inside it. This cannot currently be done because the change
would probably makes proof using apply detached. And detached are not handled
yet.
*)
(Tprsymbol (Ttermlist Ttrans_l)) (fun x y -> apply x (Some y))
......@@ -309,6 +309,7 @@ let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
| Tstring t -> t
| Tformula t -> t
| Ttheory t -> t
| Ttermlist t -> t
| _ -> assert false
type _ trans_typ_is_l = Yes : (task list) trans_typ_is_l | No : task trans_typ_is_l
......@@ -484,6 +485,9 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
pr_list in
let arg = Some pr_list in
wrap_to_store t' (f arg) tail env tables task
| Ttermlist t' ->
let term_list = parse_and_type_list ~as_fmla:false s' tables in
wrap_to_store t' (f (Some term_list)) tail env tables task
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
| Topt (_, t'), _ ->
......
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