Commit d144bf12 authored by Sylvain Dailler's avatar Sylvain Dailler

apply: need to substitute let values in newly generated goals

Add test
parent 2d518596
module Test
predicate p int
function f int: int
axiom H: forall x. let y = f x in let z = f y in p z
axiom H2: forall x. let y = f x in let z = f y in let a = f z in p a
axiom H1: forall x. let y = x in let z = y in p z
axiom H3: forall x. let y = f x in x = y -> let z = f y in let a = f z in p a
axiom H4: forall x. (let v = x in f v = x) -> let z = f x in let a = f z in p a
goal g: p 17
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file>
<path name=".."/>
<path name="265_apply.mlw"/>
<theory name="Test">
<goal name="g">
<transf name="apply" arg1="H4" arg2="with" arg3="22">
<goal name="g.0" expl="apply premises">
</goal>
<goal name="g.1" expl="apply premises">
</goal>
</transf>
<transf name="apply" arg1="H3" arg2="with" arg3="19">
<goal name="g.0" expl="apply premises">
</goal>
<goal name="g.1" expl="apply premises">
</goal>
</transf>
<transf name="apply" arg1="H1" arg2="with" arg3="18">
<goal name="g.0" expl="apply premises">
</goal>
</transf>
<transf name="apply" arg1="H2" arg2="with" arg3="4">
<goal name="g.0" expl="apply premises">
</goal>
</transf>
<transf name="apply" arg1="H" arg2="with" arg3="3">
<goal name="g.0" expl="apply premises">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -176,8 +176,10 @@ let matching_with_terms ~trans_name lv llet_vs left_term right_term withed_terms
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) ->
(* Here the substitution is updated in order for the let values to not contain
any let-introduced-variables. *)
let subst_ty, subst, new_lets, new_goals =
List.fold_left (fun (subst_ty, subst, 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:
......@@ -186,27 +188,31 @@ let generate_new_subgoals ~subst_ty ~subst llet lp =
*)
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)
(subst_ty, subst, new_lets, (t_equ t' t) :: new_goals)
| exception Not_found ->
((v,t) :: new_lets, new_goals)
let t = t_ty_subst subst_ty subst t in
(subst_ty, Mvs.add v t subst, (v,t) :: new_lets, new_goals)
)
([], []) llet
(subst_ty, subst, [], []) 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 =
(* All the remaining freevars are originally let-binded. We rebind them
with a correct let. *)
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)
(* Small optimization with t_let_simp instead of t_let *)
t_let_simp 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
List.fold_left add_lets_subst [] (new_goals @ lp)
(* Apply:
1) takes the hypothesis and introduce parts of it to keep only the last
......
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