Commit f431ccc7 authored by Sylvain Dailler's avatar Sylvain Dailler

Handle use of let bindings for apply/rewrite

This also adds an mli file for apply.
parent 38e8eba5
......@@ -2,6 +2,18 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file name="../185_apply.mlw" proved="true">
<file name="../185_apply.mlw">
<theory name="Ex1">
<goal name="g">
</goal>
</theory>
<theory name="Ex2">
<goal name="g">
</goal>
</theory>
<theory name="Ex3">
<goal name="g">
</goal>
</theory>
</file>
</why3session>
......@@ -41,19 +41,18 @@ let replace_hypothesis = "equality hypothesis"
(* 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 =
let rec intros_aux lp lv llet f =
match f.t_node with
| Tbinop (Timplies, f1, f2) ->
intros_aux (f1 :: lp) lv f2
intros_aux (f1 :: lp) lv llet f2
| Tquant (Tforall, fq) ->
let vsl, _, fs = t_open_quant fq in
intros_aux lp (lv @ vsl) fs
intros_aux lp (lv @ vsl) llet fs
| Tlet (t, tb) ->
let vs, t2 = t_open_bound tb in
let f = t_equ (t_var vs) t in
intros_aux (f :: lp) ([vs] @ lv) t2
| _ -> (lp, lv, f) in
intros_aux [] [] f
intros_aux lp lv ((vs, t) :: llet) t2
| _ -> (lp, lv, llet, f) in
intros_aux [] [] [] f
let term_decl d =
match d.td_node with
......@@ -67,10 +66,14 @@ let term_decl d =
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
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
......@@ -89,11 +92,14 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
^ " terms missing:", slv))
| _ (* when diff = 0 *) ->
let new_subst_ty, new_subst =
(* TODO Here we match on a list of variable against a list of terms. It
is probably possible to use a simplified version. But don't forget
to unify type variables. (Same comment as at top of this function) *)
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_term2 (trans_name, t1, t2))
raise (Arg_trans_term2 (trans_name^":matching", 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;
......@@ -128,14 +134,15 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
(* 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 matching_with_terms ~trans_name lv llet_vs left_term right_term withed_terms =
let slv = List.fold_left (fun acc v -> Svs.add v acc) llet_vs lv in
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_term2 (trans_name, t1, t2))
raise (Arg_trans_term2 (trans_name^":no_match", t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
......@@ -149,6 +156,39 @@ let matching_with_terms ~trans_name slv lv left_term right_term withed_terms =
in
subst_ty, subst
let generate_new_subgoals ~subst_ty ~subst llet lp =
let new_lets, new_goals =
List.fold_left (fun (new_lets, new_goals) (v,t) ->
match Mvs.find v subst with
| t' ->
(* [v -> t'] appears in subst. So we want to create two new goals:
G1: t = t'
G2: h
*)
let t' = t_ty_subst subst_ty subst t' in
let t = t_ty_subst subst_ty subst t in
(new_lets, (t_equ t' t) :: new_goals)
| exception Not_found ->
((v,t) :: new_lets, new_goals)
)
([], []) llet
in
let add_lets_subst new_goals h =
let h = t_ty_subst subst_ty subst h in
let freevars = t_freevars Mvs.empty h in
let h =
List.fold_left (fun h (v, t) ->
if Mvs.mem v freevars then
let t = t_ty_subst subst_ty subst t in
t_let t (t_close_bound v h)
else
h)
h (List.rev new_lets)
in
h :: new_goals
in
List.fold_left add_lets_subst new_goals lp
(* 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
......@@ -167,20 +207,25 @@ let apply pr withed_terms : Task.task Trans.tlist = Trans.store (fun task ->
| (_, t) -> t
| exception Not_found -> raise (Arg_pr_not_found pr)
in
let (lp, lv, nt) = intros t in
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
let (lp, lv, llet, nt) = intros t in
let llet_vs = List.fold_left (fun acc (vs, _) -> Svs.add vs acc) Svs.empty llet in
match matching_with_terms ~trans_name:"apply" lv llet_vs nt g withed_terms with
| exception e -> raise e
| subst_ty, subst ->
let inst_nt = t_ty_subst subst_ty subst nt in
(* Safety guard: we check that the goal was indeed the instantiated
hypothesis *)
if (Term.t_equal_nt_na inst_nt g) then
let nlp = List.map (t_ty_subst subst_ty subst) lp in
List.map (fun ng ->
let pr = create_prsymbol (gen_ident "G") in
Task.add_decl task
(create_goal ~expl:apply_subgoals pr ng)) nlp
let new_goals = generate_new_subgoals ~subst ~subst_ty llet lp in
let create_goal h =
let pr = create_prsymbol (gen_ident ?loc:g.t_loc "G") in
Task.add_decl task (create_goal ~expl:apply_subgoals pr h)
in
List.map create_goal new_goals
else
raise (Arg_trans_term2 ("apply", inst_nt, g)))
(* This should never happen *)
assert false
)
let replace rev f1 f2 t =
match rev with
......@@ -191,23 +236,23 @@ let replace rev f1 f2 t =
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 withed_terms t =
let replace_subst lp lv llet 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 *)
(* 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
(* Generate the list of variables that are here from let bindings *)
let llet_svs =
List.fold_left (fun acc (v, _) -> Svs.add v acc)
Svs.empty llet
in
(* 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
match matching_with_terms ~trans_name:"rewrite" lv llet_svs f1 t (Some withed_terms) with
| exception _e ->
Term.t_map_fold
(fun is_replaced t -> replace is_replaced f1 f2 t)
......@@ -221,13 +266,14 @@ let replace_subst lp lv f1 f2 withed_terms t =
is_replaced t
end
in
let is_replaced, t =
replace None f1 f2 t in
replace None f1 f2 t
in
match is_replaced with
| None -> raise (Arg_trans "rewrite: no term matching the given pattern")
| Some(subst_ty,subst) ->
(List.map (t_ty_subst subst_ty subst) lp, t)
let new_goals = generate_new_subgoals ~subst ~subst_ty llet lp in
(new_goals, t)
let rewrite_in rev with_terms h h1 =
let found_eq =
......@@ -237,7 +283,7 @@ let rewrite_in rev with_terms h h1 =
Trans.fold_decl (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 lp, lv, llet, 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 *)
......@@ -246,19 +292,21 @@ let rewrite_in rev with_terms h h1 =
(* 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
Some (lp, lv, llet, 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_error "rewrite")
| Some (lp, lv, t1, t2) ->
| None -> raise (Arg_error "rewrite") (* Should not happen *)
| Some (lp, lv, llet, t1, t2) ->
Trans.fold_decl (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 with_terms t in
let lp, new_term = replace_subst lp lv llet 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
......@@ -314,7 +362,7 @@ let rewrite_list opt rev with_terms hl h1 =
fold_decl (fun d ((acclp,accterm) as 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 lp, lv, llet, 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 *)
......@@ -325,9 +373,10 @@ let rewrite_list opt rev with_terms hl h1 =
| _ -> raise (Arg_bad_hypothesis ("rewrite", f))) in
let new_lp, new_term =
if opt
then try replace_subst lp lv t1 t2 with_terms accterm
then try replace_subst lp lv llet t1 t2 with_terms accterm
with Arg_trans _ -> acc
else replace_subst lp lv t1 t2 with_terms accterm in
else
replace_subst lp lv llet t1 t2 with_terms accterm in
new_lp@acclp, new_term
| _ -> acc) (lp, term) in
let do_all = List.fold_left (fun acc h -> Trans.bind acc (do_h h)) found_term hl in
......@@ -378,13 +427,6 @@ let rewrite_list with_terms rev opt hl h1 =
in
Trans.bind (find_target_prop h1) (rewrite_list opt (not rev) with_terms hl)
(* This function is used to detect when we found the hypothesis/goal we want
to replace/unfold into. *)
let detect_prop pr k h =
match h with
| None -> k = Pgoal
| Some h -> Ident.id_equal pr.pr_name h.pr_name && (k = Paxiom || k = Pgoal)
let detect_prop_list pr k hl =
match hl with
| None -> k = Pgoal
......
val intros: Term.term ->
Term.term list * Term.vsymbol list * (Term.vsymbol * Term.term) list * Term.term
(* intros returns a tuple containing:
- list of premises of the term,
- list of universally quantified variables at head of the terms,
- list of let-binding at head of the term,
- the term without premises/let-binding and forall variables at head.
*)
val rewrite_list: Term.term list option -> bool -> bool -> Decl.prsymbol list ->
Decl.prsymbol option -> Task.task list Trans.trans
(* [rewrite_list with_terms rev opt hl h1]
@param opt: If set, all the rewritings are optional
@param rev: If set, all the rewritings are from right to left
@param with_terms: A list of terms to instantiate variables that cannot be
matched (TODO this probably does not work: remove this argument ?)
@param hl: list of rewrite hypothesis
@param h1: hypothesis to rewrite in
*)
val term_decl: Theory.tdecl -> Term.term
(* Return the term associated to a prop declaration or raise an error in every
other cases *)
......@@ -605,7 +605,9 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task -
| (_, t) -> t
| exception Not_found -> raise (Exit "lemma not found")
in
let (lp, lv, rt) = Apply.intros l in
(* TODO solve llet assert *)
let (lp, lv, llet, rt) = Apply.intros l in
assert (llet = []);
let nt = Args_wrapper.build_naming_tables task in
let crc = nt.Trans.coercion in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
......@@ -664,7 +666,9 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
Debug.dprintf debug_refl "new post@.";
Debug.dprintf debug_refl "post: %a, %a@."
Pretty.print_vs vres Pretty.print_term p;
let (lp, lv, rt) = Apply.intros p in
(* TODO solve this llet assert *)
let (lp, lv, llet, rt) = Apply.intros p in
assert (llet = []);
let lv = lv @ args in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
Debug.dprintf debug_refl "computing args@.";
......
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