Commit 99bd1126 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch '265-transformation-apply-failed-unbound-variable' into 'master'

Resolve "Transformation apply failed: unbound variable"

Closes #265

See merge request !92
parents d4117286 c4a44c96
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
module Test2
inductive test int =
| test_bad: forall x.
let y = x in
let z = y in
test z
| test_good: forall x.
let z =
let y = x in
test z
goal g: test 0
module Test3
predicate test int
function f int : int
axiom H1 : forall x:int. let y = f x in test y
goal g1: test 42
axiom H2 : forall x:int. let y = f x in let z = f y in test z
goal g2: test 42
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="5">
<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 name="g.1" expl="apply premises">
<transf name="apply" arg1="H3" arg2="with" arg3="19">
<goal name="g.0" expl="apply premises">
<goal name="g.1" expl="apply premises">
<transf name="apply" arg1="H1" arg2="with" arg3="18">
<goal name="g.0" expl="apply premises">
<transf name="apply" arg1="H2" arg2="with" arg3="4">
<goal name="g.0" expl="apply premises">
<transf name="apply" arg1="H" arg2="with" arg3="3">
<goal name="g.0" expl="apply premises">
<theory name="Test2">
<goal name="g">
<transf name="apply" arg1="test_bad" arg2="with" arg3="23">
<goal name="g.0" expl="apply premises">
<theory name="Test3">
<goal name="g1">
<transf name="apply" arg1="H1" arg2="with" arg3="23">
<goal name="g1.0" expl="apply premises">
<goal name="g2">
<transf name="apply" arg1="H2" arg2="with" arg3="48">
<goal name="g2.0" expl="apply premises">
......@@ -38,6 +38,12 @@ let rewrite_subgoals = "rewrite premises"
(* Equality hypothesis generated by using [replace] *)
let replace_hypothesis = "equality hypothesis"
(* Printing substitution *)
let print_subst fmt (mvs: Term.term Mvs.t) =
Format.fprintf fmt "Print subst@.";
Mvs.iter (fun k e -> Format.fprintf fmt "key = %a, term = %a@."
Pretty.print_vs k Pretty.print_term e) mvs
(* Do as intros: introduce all premises of hypothesis pr and return a triple
(goal, list_premises, binded variables) *)
let intros f =
......@@ -161,15 +167,19 @@ let matching_with_terms ~trans_name lv llet_vs left_term right_term withed_terms
raise (Arg_trans_pattern (trans_name, p1, p2))
| Reduction_engine.NoMatch None -> raise (Arg_trans trans_name)
Debug.dprintf debug_matching
"subst after first first_order_matching:\n%a@." print_subst subst;
let subst_ty, subst =
let withed_terms = match withed_terms with None -> [] | Some l -> l in
let withed_terms = Opt.get_def [] withed_terms in
with_terms ~trans_name subst_ty subst lv 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:
......@@ -178,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
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)
h (List.rev new_lets)
h :: new_goals
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
......@@ -223,11 +237,15 @@ let apply pr withed_terms : Task.task Trans.tlist = (fun task ->
match matching_with_terms ~trans_name:"apply" lv llet_vs nt g withed_terms with
| exception e -> raise e
| subst_ty, subst ->
Debug.dprintf debug_matching "subst after matching with terms:\n%a@."
print_subst 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 new_goals = generate_new_subgoals ~subst ~subst_ty llet lp in
Debug.dprintf debug_matching "Printing new_goals to introduce:\n%a@."
(Pp.print_list Pp.newline Pretty.print_term) new_goals;
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)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment