Skip to content

GitLab

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

Fix issue #79 

For first_order_matching, adding a bound_vars set to disallow substitution
by terms containing bounded vars.
parent ce5c39a0
Hide whitespace changes
Inline Side-by-side
Showing with 185 additions and 112 deletions
src/transform/apply.ml
View file @ d8017e38
......@@ -208,7 +208,8 @@ let replace_subst lp lv f1 f2 withed_terms t =
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
| exception _e ->
Term.t_map_fold
(fun is_replaced t -> replace is_replaced f1 f2 t)
is_replaced t
| subst_ty, subst ->
......@@ -224,7 +225,7 @@ let replace_subst lp lv f1 f2 withed_terms t =
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")
| 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)
......
src/transform/reduction_engine.ml
View file @ d8017e38
......@@ -299,22 +299,44 @@ let rec_step_limit = ref 0
exception NoMatch of (term * term) option
exception NoMatchpat of (pattern * pattern) option
type matched = P of pattern | T of term
let rec open_branches acc_p acc_t tbl1 =
match tbl1 with
| hd :: tl ->
let (p, t) = t_open_branch hd in
open_branches (P p :: acc_p) (T t :: acc_t) tl
| [] -> (acc_p, acc_t)
let rec pattern_renaming (bound_vars, mt) p1 p2 =
match p1.pat_node, p2.pat_node with
| Pwild, Pwild ->
(bound_vars, mt)
| Pvar v1, Pvar v2 ->
begin
try
let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
let bound_vars = Mvs.add v2 v1 bound_vars in
(bound_vars, mt)
with
| Ty.TypeMismatch _ ->
raise (NoMatchpat (Some (p1, p2)))
end
| Papp (ls1, tl1), Papp (ls2, tl2) when ls_equal ls1 ls2 ->
List.fold_left2 pattern_renaming (bound_vars, mt) tl1 tl2
| Por (p1a, p1b), Por (p2a, p2b) ->
let (bound_vars, mt) =
pattern_renaming (bound_vars, mt) p1a p2a in
pattern_renaming (bound_vars, mt) p1b p2b
| Pas (p1, v1), Pas (p2, v2) ->
begin
try
let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
let bound_vars = Mvs.add v2 v1 bound_vars in
pattern_renaming (bound_vars, mt) p1 p2
with
| Ty.TypeMismatch _ ->
raise (NoMatchpat (Some (p1, p2)))
end
| _ -> raise (NoMatchpat (Some (p1, p2)))
let first_order_matching (vars : Svs.t) (largs : term list)
(args : term list) : Ty.ty Ty.Mtv.t * substitution =
let rec loop ((mt,mv) as sigma) largs args =
let rec loop bound_vars ((mt,mv) as sigma) largs args =
match largs,args with
| [],[] -> sigma
| T t1::r1, T t2::r2 ->
| t1::r1, t2::r2 ->
begin
(*
Format.eprintf "matching terms %a and %a...@."
......@@ -325,30 +347,26 @@ let first_order_matching (vars : Svs.t) (largs : term list)
begin
try let t = Mvs.find vs mv in
if t_equal t t2 then
loop sigma r1 r2
loop bound_vars sigma r1 r2
else
raise (NoMatch (Some (t1, t2)))
with Not_found ->
try
let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
loop (ts,Mvs.add vs t2 mv) r1 r2
let fv2 = t_vars t2 in
if Mvs.is_empty (Mvs.set_inter bound_vars fv2) then
loop bound_vars (ts,Mvs.add vs t2 mv) r1 r2
else
raise (NoMatch (Some (t1, t2)))
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2)))
end
| Tvar vs when Mvs.mem vs mv ->
begin
let t = Mvs.find vs mv in
if t_equal t t2 then
loop sigma r1 r2
else
raise (NoMatch (Some (t1, t2)))
end
| Tapp(ls1,args1) ->
begin
match t2.t_node with
| Tapp(ls2,args2) when ls_equal ls1 ls2 ->
let mt, mv = loop sigma
(List.rev_append (List.map (fun x -> T x) args1) r1)
(List.rev_append (List.map (fun x -> T x) args2) r2) in
let mt, mv = loop bound_vars sigma
(List.rev_append args1 r1)
(List.rev_append args2 r2) in
begin
try Ty.oty_match mt t1.t_ty t2.t_ty, mv
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2)))
......@@ -361,29 +379,30 @@ let first_order_matching (vars : Svs.t) (largs : term list)
| Tquant (q2, bv2) when q1 = q2 ->
let (vl1, _tl1, term1) = t_open_quant bv1 in
let (vl2, _tl2, term2) = t_open_quant bv2 in
let (mt, mv) =
try List.fold_left2 (fun (mt, mv) e1 e2 ->
let (bound_vars, term1, mt) =
try List.fold_left2 (fun (bound_vars, term1, mt) e1 e2 ->
let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
(mt, Mvs.add e1 (t_var e2) mv)) (mt, mv) vl1 vl2
let bound_vars = Mvs.add e2 e1 bound_vars in
(bound_vars,term1, mt)) (bound_vars,term1, mt) vl1 vl2
with Invalid_argument _ | Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1,t2)))
in
loop (mt, mv) (T term1 :: r1) (T term2 :: r2)
loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Tbinop (b1, t1_l, t1_r) ->
begin
match t2.t_node with
| Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
loop (mt, mv) (T t1_l :: T t1_r :: r1) (T t2_l :: T t2_r :: r2)
loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Tif (t11, t12, t13) ->
begin
match t2.t_node with
| Tif (t21, t22, t23) ->
loop (mt, mv) (T t11 :: T t12 :: T t13 :: r1)
(T t21 :: T t22 :: T t23 :: r2)
loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
(t21 :: t22 :: t23 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Tlet (td1, tb1) ->
......@@ -394,23 +413,27 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let (v2, tl2) = t_open_bound tb2 in
let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1,t2))) in
let mv = Mvs.add v1 (t_var v2) mv in
loop (mt, mv) (T td1 :: T tl1 :: r1) (T td2 :: T tl2 :: r2)
let bound_vars = Mvs.add v2 v1 bound_vars in
loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
| _ ->
raise (NoMatch (Some (t1, t2)))
end
(* We assume that patterns are well-formed (ie already typed)
and that it is not possible to have an occurence of a pattern
introduced variable into a branch that does not depend on this
pattern *)
| Tcase (ts1, tbl1) ->
begin
match t2.t_node with
| Tcase (ts2, tbl2) ->
let list_p1, list_t1 = open_branches [] [] tbl1 in
let list_p2, list_t2 = open_branches [] [] tbl2 in
loop sigma (T ts1 :: list_p1 @ list_t1 @ r1)
(T ts2 :: list_p2 @ list_t2 @ r2)
begin try
let (bound_vars, mt, l1, l2) =
List.fold_left2 (fun (bound_vars, mt, l1, l2) tb1 tb2 ->
let (p1, tb1) = t_open_branch tb1 in
let (p2, tb2) = t_open_branch tb2 in
let bound_vars, mt = pattern_renaming (bound_vars, mt) p1 p2 in
(bound_vars,mt, tb1 :: l1, tb2 :: l2)
) (bound_vars,mt, ts1 :: r1, ts2 :: r2) tbl1 tbl2 in
loop bound_vars (mt,mv) l1 l2
with Invalid_argument _ ->
raise (NoMatch (Some (t1, t2)))
end
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Teps tb1 ->
......@@ -421,83 +444,38 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let (v2, td2) = t_open_bound tb2 in
let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1,t2))) in
let mv = Mvs.add v1 (t_var v2) mv in
loop (mt, mv) (T td1 :: r1) (T td2 :: r2)
let bound_vars = Mvs.add v2 v1 bound_vars in
loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Tnot t1 ->
begin
match t2.t_node with
| Tnot t2 ->
loop sigma (T t1 :: r1) (T t2 :: r2)
loop bound_vars sigma (t1 :: r1) (t2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
| Tvar v1 ->
begin match t2.t_node with
| Tvar v2 ->
begin try
if vs_equal v1 (Mvs.find v2 bound_vars) then
loop bound_vars sigma r1 r2
else
raise (NoMatch (Some (t1, t2)))
with
Not_found -> assert false
end
| _ -> raise (NoMatch (Some (t1, t2)))
end
| (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
loop sigma r1 r2
| Tvar _ | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2)))
end
| P p1 :: r1, P p2 :: r2 ->
begin
match p1.pat_node with
| Pwild ->
begin
match p2.pat_node with
| Pwild -> loop sigma r1 r2
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
| Pvar v1 when Mvs.mem v1 mv ->
begin
match p2.pat_node with
| Pvar v2 ->
if t_equal (t_var v2) (Mvs.find v1 mv) then
loop (mt,mv) r1 r2
else
raise (NoMatch (Some (t_var v1, t_var v2)))
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
| Pvar v1 ->
begin
match p2.pat_node with
| Pvar v2 ->
let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
let mv = Mvs.add v1 (t_var v2) mv in
loop (mt, mv) r1 r2
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
| Papp (ls1, pl1) ->
begin
match p2.pat_node with
| Papp (ls2, pl2) ->
if ls_equal ls1 ls2 then
loop (mt, mv) ((List.map (fun x -> P x) pl1) @ r1)
((List.map (fun x -> P x) pl2) @ r2)
else
raise (NoMatchpat (Some (p1, p2)))
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
| Por (p11, p12) ->
begin
match p2.pat_node with
| Por (p21, p22) ->
loop (mt, mv) (P p11 :: P p12 :: r1) (P p21 :: P p22 :: r2)
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
| Pas (pa1, v1) ->
begin
match p2.pat_node with
| Pas (pa2, v2) ->
let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
let mv = Mvs.add v1 (t_var v2) mv in
loop (mt, mv) (P pa1 :: r1) (P pa2 :: r2)
| _ -> raise (NoMatchpat (Some (p1, p2)))
end
loop bound_vars sigma r1 r2
| Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2)))
end
| _ -> raise (NoMatch None)
in
loop (Ty.Mtv.empty, Mvs.empty)
(List.map (fun x -> T x) largs)
(List.map (fun x -> T x) args)
loop Mvs.empty (Ty.Mtv.empty, Mvs.empty) largs args
exception Irreducible
......
tests/demo-itp.mlw
View file @ d8017e38
......@@ -3,12 +3,55 @@ module ApplyRewrite
use import int.Int
(* Use apply H require some cases of quantifications in first_order_matching *)
goal g: (forall y. exists x. x <= y /\ y = 0) -> forall x. exists y. y <= x /\ x = 0
function f int int : int
use HighOrd
axiom H: forall x. (\z: int. x + z) = f x
goal g1: (\toto. 42 + toto) = f 42
axiom Ha: forall x. (\z: int. x + z) 2 = 2
goal g3: (\toto. 42 + toto) 2 = 2
goal g2: (\y. y + y) = f 24
end
module A
use import int.Int
use HighOrd
function f int: int
axiom H: forall y. exists x. f x = x + y
goal g1: exists x. f x = x + 42
goal g: (\y. f y) 0 = 3
constant b: bool
axiom Ha: forall y. if b = true then let x = 3 in f x = x + y else false
goal ga: if b = true then let z = 3 in f z = z + 42 else false
goal gb: if b = true then let z = 453 in f z = z + 42 else false
end
module Soundness
use import int.Int
use HighOrd
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (\x. f0 x y z) <-> y = z
meta rewrite prop A
lemma Fail : p (\x. f0 x x x)
lemma Absurd : false
end
module TestCEX
......
tests/demo-itp/why3session.xml
View file @ d8017e38
......@@ -10,10 +10,61 @@
<prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../demo-itp.mlw">
<theory name="ApplyRewrite" proved="true" sum="06c28a672d2fbb0de6998078f2cfe895">
<goal name="g" proved="true">
<theory name="ApplyRewrite" sum="a5d903eba2570fb4645483c4ff500ebb">
<goal name="g1" proved="true">
<transf name="apply" proved="true" arg1="H">
</transf>
<transf name="rewrite" proved="true" arg1="H">
<goal name="g1.0" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="g3" proved="true">
<transf name="apply" proved="true" arg1="Ha">
</transf>
</goal>
<goal name="g2">
<transf name="compute_specified" >
<goal name="g2.0">
</goal>
</transf>
</goal>
</theory>
<theory name="A" sum="1abc5293356c4003ce35806f735459dc">
<goal name="g1" proved="true">
<transf name="apply" proved="true" arg1="H">
</transf>
</goal>
<goal name="g">
</goal>
<goal name="ga" proved="true">
<transf name="apply" proved="true" arg1="Ha">
</transf>
</goal>
<goal name="gb">
</goal>
</theory>
<theory name="Soundness" sum="198ba2949deb2335512120811dfebfc6">
<goal name="A" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="Fail">
<transf name="assert" arg1="(forall y:int, z:int. y = z -&gt; p (\ x:int. f0 x y z))">
<goal name="Fail.0" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="Fail.1">
<transf name="compute_specified" >
<goal name="Fail.1.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="Absurd" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="TestCEX" sum="55ceea8b24a88c1829a53af2c814f1a6">
......
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