Commit e8d63c35 authored by MARCHE Claude's avatar MARCHE Claude

shape of a term

parent 23c89c14
* marks an incompatible change
o [Session] prover versions are stored in database. A proof is
marked obsolete if it was made by a prover with another version
than the current.
version 0.70, July 6, 2011
==========================
......@@ -77,3 +81,8 @@ version 0.63, Dec 21, 2010
==========================
o first public release. See release notes in manual
# Emacs parameters
Local Variables:
mode: text
End:
......@@ -430,7 +430,7 @@ install_local: bin/why3config
ifeq (@enable_ide@,yes)
IDE_FILES = xml session gconfig newmain
IDE_FILES = xml termcode session gconfig newmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -490,7 +490,7 @@ endif
# Replayer
###############
REPLAYER_FILES = xml session replay
REPLAYER_FILES = xml termcode session replay
REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))
......@@ -854,6 +854,9 @@ test-api: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
test-shape: src/why3.cma src/ide/termcode.cmo
ocaml -I src/ -I src/ide/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
bts12244: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
......
<!ELEMENT why3session (file*)>
<!ELEMENT why3session (prover*, file*)>
<!ATTLIST why3session name CDATA #REQUIRED>
<!ELEMENT prover EMPTY>
<!ATTLIST prover id CDATA #REQUIRED>
<!ATTLIST prover name CDATA #REQUIRED>
<!ATTLIST prover version CDATA #REQUIRED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ATTLIST file verified CDATA #REQUIRED>
......@@ -16,6 +21,7 @@
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
<!ATTLIST goal sum CDATA #REQUIRED>
<!ATTLIST goal shape CDATA #IMPLIED>
<!ATTLIST goal expanded CDATA #IMPLIED>
<!ELEMENT proof (result|undone)>
......
......@@ -253,6 +253,12 @@ let all_files : file list ref = ref []
let get_all_files () = !all_files
let current_env = ref None
let current_provers = ref Util.Mstr.empty
let project_dir = ref ""
let get_provers () = !current_provers
(************************)
(* saving state on disk *)
(************************)
......@@ -288,8 +294,9 @@ let opt lab fmt = function
| Some s -> fprintf fmt "%s=\"%s\" " lab s
let rec save_goal fmt g =
fprintf fmt "@\n@[<v 1><goal name=\"%s\" %asum=\"%s\" proved=\"%b\" expanded=\"%b\">"
g.goal_name (opt "expl") g.goal_expl g.checksum g.proved g.goal_expanded;
fprintf fmt "@\n@[<v 1><goal name=\"%s\" %asum=\"%s\" proved=\"%b\" expanded=\"%b\" shape=\"%s\">"
g.goal_name (opt "expl") g.goal_expl g.checksum g.proved g.goal_expanded
(Termcode.t_shape_buf (Task.task_goal_fmla (get_task g)));
Hashtbl.iter (save_proof_attempt fmt) g.external_proofs;
Hashtbl.iter (save_trans fmt) g.transformations;
fprintf fmt "@]@\n</goal>"
......@@ -307,16 +314,22 @@ let save_theory fmt t =
fprintf fmt "@]@\n</theory>"
let save_file fmt f =
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\" expanded=\"%b\">" f.file_name f.file_verified f.file_expanded;
fprintf fmt "@\n@[<v 1><file name=\"%s\" verified=\"%b\" expanded=\"%b\">"
f.file_name f.file_verified f.file_expanded;
List.iter (save_theory fmt) f.theories;
fprintf fmt "@]@\n</file>"
let save_prover fmt p =
fprintf fmt "@\n@[<v 1><prover id=\"%s\" name=\"%s\" version=\"%s\"/>@]"
p.prover_id p.prover_name p.prover_version
let save fname =
let ch = open_out fname in
let fmt = formatter_of_out_channel ch in
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
fprintf fmt "@[<v 1><why3session name=\"%s\">" fname;
Util.Mstr.iter (fun _ d -> save_prover fmt d) (get_provers ());
List.iter (save_file fmt) (get_all_files());
fprintf fmt "@]@\n</why3session>";
fprintf fmt "@.";
......@@ -729,11 +742,6 @@ let raw_add_file f exp =
!notify_fun any;
mfile
let current_env = ref None
let current_provers = ref Util.Mstr.empty
let project_dir = ref ""
let get_provers () = !current_provers
let read_file fn =
let fn = Filename.concat !project_dir fn in
......@@ -1093,13 +1101,18 @@ let int_attribute field r def =
int_of_string (List.assoc field r.Xml.attributes)
with Not_found | Invalid_argument _ -> def
let string_attribute field r =
try
List.assoc field r.Xml.attributes
with Not_found ->
eprintf "[Error] missing required attribute '%s' from element '%s'@."
field r.Xml.name;
assert false
let load_result r =
match r.Xml.name with
| "result" ->
let status =
try List.assoc "status" r.Xml.attributes
with Not_found -> assert false
in
let status = string_attribute "status" r in
let answer =
match status with
| "valid" -> Call_provers.Valid
......@@ -1109,8 +1122,9 @@ let load_result r =
| "failure" -> Call_provers.Failure ""
| "highfailure" -> Call_provers.Failure ""
| s ->
eprintf "Session.load_result: unexpected status '%s'@." s;
assert false
eprintf
"[Warning] Session.load_result: unexpected status '%s'@." s;
Call_provers.Failure ""
in
let time =
try float_of_string (List.assoc "time" r.Xml.attributes)
......@@ -1123,11 +1137,10 @@ let load_result r =
}
| "undone" -> Undone
| s ->
eprintf "Session.load_result: unexpected element '%s'@." s;
assert false
eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
Undone
let rec load_goal ~env parent acc g =
let rec load_goal ~env ~old_provers parent acc g =
match g.Xml.name with
| "goal" ->
let gname =
......@@ -1144,25 +1157,29 @@ let rec load_goal ~env parent acc g =
in
let exp = bool_attribute "expanded" g true in
let mg = raw_add_goal parent gname expl sum None exp in
List.iter (load_proof_or_transf ~env mg) g.Xml.elements;
List.iter (load_proof_or_transf ~env ~old_provers mg) g.Xml.elements;
mg::acc
| s ->
eprintf "Session.load_goal: unexpected element '%s'@." s;
assert false
eprintf "[Warning] Session.load_goal: unexpected element '%s'@." s;
acc
and load_proof_or_transf ~env mg a =
and load_proof_or_transf ~env ~old_provers mg a =
match a.Xml.name with
| "proof" ->
let prover =
try List.assoc "prover" a.Xml.attributes
with Not_found -> assert false
in
let p =
let prover_obsolete,p =
try
Detected_prover (Util.Mstr.find prover !current_provers)
let p = Util.Mstr.find prover !current_provers in
try
let (n,v) = Util.Mstr.find prover old_provers in
(p.prover_name <> n || p.prover_version <> v), Detected_prover p
with Not_found ->
true, Detected_prover p
with Not_found ->
Undetected_prover prover
true, Undetected_prover prover
in
let res = match a.Xml.elements with
| [r] -> load_result r
......@@ -1174,6 +1191,7 @@ and load_proof_or_transf ~env mg a =
with Not_found -> assert false
in
let obsolete = bool_attribute "obsolete" a true in
let obsolete = obsolete || prover_obsolete in
let timelimit = int_attribute "timelimit" a 10 in
let (_ : proof_attempt) =
raw_add_external_proof ~obsolete ~timelimit ~edit mg p res
......@@ -1200,16 +1218,17 @@ and load_proof_or_transf ~env mg a =
mtr.subgoals <-
List.rev
(List.fold_left
(load_goal ~env (Parent_transf mtr))
(load_goal ~env ~old_provers (Parent_transf mtr))
[] a.Xml.elements);
(* already done by raw_add_transformation
Hashtbl.add mg.transformations trname mtr *)
()
| s ->
eprintf "Session.load_proof_or_transf: unexpected element '%s'@." s;
assert false
eprintf
"[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
s
let load_theory ~env mf acc th =
let load_theory ~env ~old_provers mf acc th =
match th.Xml.name with
| "theory" ->
let thname =
......@@ -1221,14 +1240,14 @@ let load_theory ~env mf acc th =
mth.goals <-
List.rev
(List.fold_left
(load_goal ~env (Parent_theory mth))
(load_goal ~env ~old_provers (Parent_theory mth))
[] th.Xml.elements);
mth::acc
| s ->
eprintf "Session.load_theory: unexpected element '%s'@." s;
assert false
eprintf "[Warning] Session.load_theory: unexpected element '%s'@." s;
acc
let load_file ~env f =
let load_file ~env old_provers f =
match f.Xml.name with
| "file" ->
let fn =
......@@ -1239,19 +1258,38 @@ let load_file ~env f =
let mf = raw_add_file fn exp in
mf.theories <-
List.rev
(List.fold_left (load_theory ~env mf) [] f.Xml.elements)
(List.fold_left (load_theory ~env ~old_provers mf) [] f.Xml.elements);
old_provers
| "prover" ->
let id = string_attribute "id" f in
let name = string_attribute "name" f in
let version = string_attribute "version" f in
begin
try
let p = Util.Mstr.find id !current_provers in
if p.prover_name <> name || p.prover_version <> version then
eprintf
"[Warning] Database prover id '%s' = '%s %s' but on this computer '%s' = '%s %s'@."
id name version id p.prover_name p.prover_version
with Not_found ->
eprintf
"[Warning] Database has prover %s (%s %s) which is not available on this computer@."
id name version;
end;
Util.Mstr.add id (name,version) old_provers
| s ->
eprintf "Session.load_file: unexpected element '%s'@." s;
assert false
eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
old_provers
let load_session ~env xml =
let cont = xml.Xml.content in
match cont.Xml.name with
| "why3session" ->
List.iter (load_file ~env) cont.Xml.elements
let _old_provers =
List.fold_left (load_file ~env) Util.Mstr.empty cont.Xml.elements
in ()
| s ->
eprintf "Session.load_session: unexpected element '%s'@." s;
assert false
eprintf "[Warning] Session.load_session: unexpected element '%s'@." s
let db_filename = "why3session.xml"
......
......@@ -17,88 +17,11 @@
(* *)
(**************************************************************************)
(* distance of two terms *)
let dist_bool b = if b then 0.0 else 1.0
let average l =
let n,s = List.fold_left (fun (n,s) x -> (n+1,s+.x)) (0,0.0) l in
float n *. s
let rec pat_dist p1 p2 =
if ty_equal p1.pat_ty p2.pat_ty then
match p1.pat_node, p2.pat_node with
| Pwild, Pwild | Pvar _, Pvar _ -> 0.0
| Papp (f1, l1), Papp (f2, l2) ->
if ls_equal f1 f2 then
0.5 *. average (List.map2 pat_dist l1 l2)
else 1.0
| Pas (p1, _), Pas (p2, _) -> pat_dist p1 p2
| Por (p1, q1), Por (p2, q2) ->
0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ]
| _ -> 1.0
else 1.0
let rec t_dist c1 c2 m1 m2 e1 e2 =
let t_d = t_dist c1 c2 m1 m2 in
match e1.t_node, e2.t_node with
| Tvar v1, Tvar v2 ->
begin
try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2)
with Not_found -> 1.0
end
| Tconst c1, Tconst c2 -> 0.5 *. dist_bool (c1 = c2)
| Tapp(ls1,tl1), Tapp(ls2,tl2) ->
if ls_equal ls1 ls2 then
0.5 *. average (List.map2 t_d tl1 tl2)
else 1.0
| Tif(c1,t1,e1), Tif(c2,t2,e2) ->
0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2]
| Tlet(t1,b1), Tlet(t2,b2) ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. average [t_d t1 t2; t_dist c1 c2 m1 m2 e1 e2]
| Tcase (t1,bl1), Tcase (t2,bl2) ->
if List.length bl1 = List.length bl2 then
let br_dist ((pat1,_,_) as b1) ((pat2,_,_) as b2) =
let p1,e1 = t_open_branch b1 in
let p2,e2 = t_open_branch b2 in
let m1 = pat_rename_alpha c1 m1 p1 in
let m2 = pat_rename_alpha c2 m2 p2 in
average [pat_dist pat1 pat2 ; t_dist c1 c2 m1 m2 e1 e2]
in
0.5 *. average (t_d t1 t2 :: List.map2 br_dist bl1 bl2)
else
1.0
| Teps b1, Teps b2 ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
| Tquant (q1,((vl1,_,_,_) as b1)), Tquant (q2,((vl2,_,_,_) as b2)) ->
if q1 = q2 &&
list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2
then
let vl1,_,e1 = t_open_quant b1 in
let vl2,_,e2 = t_open_quant b2 in
let m1 = vl_rename_alpha c1 m1 vl1 in
let m2 = vl_rename_alpha c2 m2 vl2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
else
1.0
| Tbinop (a,f1,g1), Tbinop (b,f2,g2) ->
if a = b then 0.5 *. average [ t_d f1 f2 ; t_d g1 g2]
else 1.0
| Tnot f1, Tnot f2 -> 0.5 *. t_d f1 f2
| Ttrue, Ttrue | Tfalse, Tfalse -> 0.0
| _ -> 1.0
open Why3
open Ty
open Term
let t_dist t1 t2 = t_dist (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty t1 t2
(* similarity code of terms, or of "shapes"
example:
......@@ -107,6 +30,132 @@ example:
Forall(Int,App(infix_gteq,App(infix_st,Tvar 0,Tvar 0),Const(0)))
i.e: de bruijn indexes, first-order term
*)
let const_shape ~push acc c =
let b = Buffer.create 17 in
Format.bprintf b "%a" Pretty.print_const c;
push (Buffer.contents b) acc
let var_shape _v : string = assert false
let vs_rename_alpha c h vs = incr c; Mvs.add vs !c h
let vl_rename_alpha c h vl = List.fold_left (vs_rename_alpha c) h vl
let pat_shape _c _m _acc _p = assert false
let tag_and = "A"
let tag_if = "B"
let tag_const = "C"
let tag_eps = "E"
let tag_false = "F"
let tag_impl = "I"
let tag_let = "L"
let tag_not = "N"
let tag_or = "O"
let tag_iff = "Q"
let tag_case = "S"
let tag_true = "T"
let tag_var = "V"
let tag_forall = "W"
let tag_exists = "X"
let tag_app = "Y"
(*
[t_shape t] provides a traversal of the term structure, generally
in the order root-left-right, except for nodes Tquant and Tbin
which are traversed in the order right-root-left, so that in "A ->
B" we see B first, and if "Forall x,A" we see A first
*)
let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
let fn = t_shape ~push c m in
match t.t_node with
| Tconst c -> const_shape ~push (push tag_const acc) c
| Tvar v ->
let x =
try
string_of_int (Mvs.find v m)
with Not_found -> var_shape v
in
push x (push tag_var acc)
| Tapp (s,l) ->
List.fold_left fn
(push (s.ls_name.Ident.id_string) (push tag_app acc))
l
| Tif (f,t1,t2) -> fn (fn (fn (push tag_if acc) f) t1) t2
| Tlet (t1,b) ->
let u,t2 = t_open_bound b in
let m = vs_rename_alpha c m u in
t_shape ~push c m (fn (push tag_let acc) t1) t2
| Tcase (t1,bl) ->
let br_shape acc b =
let p,t2 = t_open_branch b in
let m = pat_shape c m acc p in
t_shape ~push c m acc t2
in
List.fold_left br_shape (fn (push tag_case acc) t1) bl
| Teps b ->
let u,f = t_open_bound b in
let m = vs_rename_alpha c m u in
t_shape ~push c m (push tag_eps acc) f
| Tquant (q,b) ->
let vl,_,f1 = t_open_quant b in
let m = vl_rename_alpha c m vl in
let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
push hq (t_shape ~push c m acc f1)
(* argument first, intentionally, to give more weight on A in
forall x,A *)
| Tbinop (o,f,g) ->
let tag = match o with
| Tand -> tag_and
| Tor -> tag_or
| Timplies -> tag_impl
| Tiff -> tag_iff
in
fn (push tag (fn acc g)) f
(* g first, intentionally, to give more weight on B in A->B *)
| Tnot f -> push tag_not (fn acc f)
| Ttrue -> push tag_true acc
| Tfalse -> push tag_false acc
let t_shape_buf t =
let b = Buffer.create 17 in
let push t () = Buffer.add_string b t in
let () = t_shape ~push (ref (-1)) Mvs.empty () t in
Buffer.contents b
let t_shape_list t =
let push t l = t::l in
List.rev (t_shape ~push (ref (-1)) Mvs.empty [] t)
let pr_shape_list fmt t =
List.iter (fun s -> Format.fprintf fmt "%s" s) (t_shape_list t)
(*
shape = list of string, ordered lexicographically
shape (forall x:t, P) = code(forall) :: shape (P)
shape (P -> Q) = code(->) :: shape(P) @ shape(Q)
shape (App(f,[t1,..,tn] ) =
code(app) :: code(f) @ code (t1) ... @ code (tn)
code(f) = user name (not unique but it is not a problem)
code(Var x) = code(Var) :: code(debruijn x)
code(Const n) = n (en tant que string ?)
*)
(*
code of a shape: maps shapes into real numbers in [0..1], such that
compare t1 t2 = code (shape t1) -. code (shape t2)
......@@ -135,6 +184,8 @@ example:
*)
(*
let const_code = function
| ConstInt n -> 1.0 /. (1.0 +. abs (float_of_string n)) /. 3.0
| ConstReal n -> (2.0 + 1.0 /. (1.0 +. abs (float_of_string x)) /. 3.0
......@@ -185,3 +236,91 @@ let rec t_code c m t =
let t_hash_alpha = t_hash_alpha (ref (-1)) Mvs.empty
*)
(* distance of two terms *)
(*
let dist_bool b = if b then 0.0 else 1.0
let average l =
let n,s = List.fold_left (fun (n,s) x -> (n+1,s+.x)) (0,0.0) l in
float n *. s
let rec pat_dist p1 p2 =
if ty_equal p1.pat_ty p2.pat_ty then
match p1.pat_node, p2.pat_node with
| Pwild, Pwild | Pvar _, Pvar _ -> 0.0
| Papp (f1, l1), Papp (f2, l2) ->
if ls_equal f1 f2 then
0.5 *. average (List.map2 pat_dist l1 l2)
else 1.0
| Pas (p1, _), Pas (p2, _) -> pat_dist p1 p2
| Por (p1, q1), Por (p2, q2) ->
0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ]
| _ -> 1.0
else 1.0
let rec t_dist c1 c2 m1 m2 e1 e2 =
let t_d = t_dist c1 c2 m1 m2 in
match e1.t_node, e2.t_node with
| Tvar v1, Tvar v2 ->
begin
try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2)
with Not_found -> 1.0
end
| Tconst c1, Tconst c2 -> 0.5 *. dist_bool (c1 = c2)
| Tapp(ls1,tl1), Tapp(ls2,tl2) ->
if ls_equal ls1 ls2 then
0.5 *. average (List.map2 t_d tl1 tl2)
else 1.0
| Tif(c1,t1,e1), Tif(c2,t2,e2) ->
0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2]
| Tlet(t1,b1), Tlet(t2,b2) ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. average [t_d t1 t2; t_dist c1 c2 m1 m2 e1 e2]
| Tcase (t1,bl1), Tcase (t2,bl2) ->
if List.length bl1 = List.length bl2 then
let br_dist ((pat1,_,_) as b1) ((pat2,_,_) as b2) =
let p1,e1 = t_open_branch b1 in
let p2,e2 = t_open_branch b2 in
let m1 = pat_rename_alpha c1 m1 p1 in
let m2 = pat_rename_alpha c2 m2 p2 in
average [pat_dist pat1 pat2 ; t_dist c1 c2 m1 m2 e1 e2]
in
0.5 *. average (t_d t1 t2 :: List.map2 br_dist bl1 bl2)
else
1.0
| Teps b1, Teps b2 ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
| Tquant (q1,b1), Tquant (q2,b2) ->
if q1 = q2 &&
list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2
then
let vl1,_,e1 = t_open_quant b1 in
let vl2,_,e2 = t_open_quant b2 in
let m1 = vl_rename_alpha c1 m1 vl1 in
let m2 = vl_rename_alpha c2 m2 vl2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
else
1.0