Commit dd57b9de authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents b89ed0ef 25acc03a
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 (fun x -> f0 x y z) <-> y = z
meta rewrite lemma A
(* compute_specified should not solve this goal.
0 = 0 was added so that compute_specified progress on this goal even when
not unsound.
*)
lemma Fail : 0 = 0 /\ p (fun x -> f0 x x x)
lemma Absurd : false
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="4">
<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../79_compute_unsound.mlw">
<theory name="Soundness" sum="aa1c41b51a76f536179c52b8dcf8a473">
<goal name="A" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Fail">
<transf name="compute_specified" >
<goal name="Fail.0">
</goal>
</transf>
</goal>
<goal name="Absurd" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -881,12 +881,10 @@ end
(* -- send the task -- *)
let task_of_id d id do_intros show_full_context loc =
let task,tables =
if do_intros then get_task d.cont.controller_session id
else
let task = get_raw_task d.cont.controller_session id in
let tables = Args_wrapper.build_naming_tables task in
task,tables
let task,tables = get_task d.cont.controller_session id in
let task =
if do_intros then task else
get_raw_task d.cont.controller_session id
in
(* This function also send source locations associated to the task *)
let loc_color_list = if loc then get_locations task else [] in
......@@ -924,7 +922,7 @@ end
Pp.string_of (Model_parser.print_model_human ?me_name_trans:None)
res.Call_provers.pr_model
in
result ^ "\n\n" ^ ce_result
result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
| None -> "Result of the prover not available.\n"
in
P.notify (Task (nid, prover_text ^ prover_ce, list_loc))
......
......@@ -1090,6 +1090,8 @@ let load_theory session parent_name old_provers acc th =
List.iter2
(load_goal session old_provers (Theory mth))
th.Xml.elements goals;
let proved = bool_attribute "proved" th false in
Hid.add session.th_state thname proved;
mth::acc
| s ->
Warning.emit "[Warning] Session.load_theory: unexpected element '%s'@."
......
......@@ -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)
......
......@@ -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
......
......@@ -202,7 +202,7 @@ let rec num_lines s acc tr =
(color_of_status ~dark:true) (th_proved s th)
name;
if th_proved s th then
fprintf fmt "fully verified in (TODO)%%.02f s"
fprintf fmt "fully verified" (*TODO in %%.02f s*)
else fprintf fmt "not fully verified";
fprintf fmt "</span></h2>@\n";
......
module Naming
use import int.Int
constant x : int
goal G : forall x:int. x >= 0 -> x = 0
end
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 : 0 = 0 /\ p (\x. f0 x x x)
lemma Absurd : false
end
module TestCEX
......
......@@ -10,11 +10,66 @@
<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="Naming" sum="887148d0be0266efa5001ad2fedbe72e">
<goal name="G">
</goal>
</theory>
<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="aa1c41b51a76f536179c52b8dcf8a473">
<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">
<goal name="g">
......
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