Commit c33b1457 authored by MARCHE Claude's avatar MARCHE Claude

new shape version

parent bcbcd870
......@@ -154,7 +154,7 @@ New features:
o [Coq output] default tactic is now "intros ..." with a pattern
that matches the structure of the goal
o [why3replayer] option -obsolete-only
o co-inductive predicates (experimental ?)
o co-inductive predicates
o new option -e for "why3session latex" allows to specify when to
split tables in parts
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="examples/my_cosine/why3session.xml">
name="examples/my_cosine/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -63,10 +63,10 @@
name="TotalErrorExpanded"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="31" loccnumb="6" loccnume="24"
sum="e8eb30517031d5f9aa29e249a13fcaaf"
sum="23a30a50ceded9e62ee2bb8a8e3e3870"
proved="true"
expanded="true"
shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
shape="ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23LaroundaNearestTiesToEvenainfix -c1.0V2LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c0x1.p-5F">
<proof
prover="0"
timelimit="3"
......@@ -80,10 +80,10 @@
name="TotalError"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="51" loccnumb="6" loccnume="16"
sum="0457c10047c2e650ca89f0b4f6c924e4"
sum="616571c5bb8323133735b63f3fb2b63f"
proved="true"
expanded="true"
shape="Lacos_singleV0ainfix &lt;=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
shape="ainfix &lt;=aabsainfix -avalueV1acosavalueV0c0x1.p-23Lacos_singleV0Iainfix &lt;=aabsavalueV0c0x1.p-5F">
<proof
prover="0"
timelimit="10"
......
......@@ -785,8 +785,11 @@ let sched =
try
Debug.dprintf debug "@[<hov 2>[Info] Opening session...@\n";
let session =
if Sys.file_exists project_dir then S.read_session project_dir
else S.create_session project_dir in
if Sys.file_exists project_dir then
S.read_session project_dir
else
S.create_session project_dir
in
let env,(_:bool) =
M.update_session ~allow_obsolete:true session gconfig.env
gconfig.Gconfig.config
......
......@@ -53,8 +53,8 @@ type 'a goal =
goal_name : Ident.ident;
goal_expl : string option;
goal_parent : 'a goal_parent;
goal_checksum : string;
goal_shape : string;
mutable goal_checksum : string;
mutable goal_shape : string;
mutable goal_verified : bool;
goal_task: task_option;
mutable goal_expanded : bool;
......@@ -111,6 +111,7 @@ and 'a file =
and 'a session =
{ session_files : 'a file PHstr.t;
mutable session_shape_version : int;
session_dir : string; (** Absolute path *)
}
......@@ -254,7 +255,17 @@ let print_session fmt s = PTree.print fmt (PTreeT.Session s)
(** 2 Create a session *)
let create_session project_dir =
let empty_session ?shape_version dir =
let shape_version = match shape_version with
| Some v -> v
| None -> Termcode.current_shape_version
in
{ session_files = PHstr.create 3;
session_shape_version = shape_version;
session_dir = dir;
}
let create_session ?shape_version project_dir =
if not (Sys.file_exists project_dir) then
begin
dprintf debug
......@@ -262,9 +273,7 @@ let create_session project_dir =
for the project@." project_dir;
Unix.mkdir project_dir 0o777
end;
{ session_files = PHstr.create 3;
session_dir = project_dir;
}
empty_session ?shape_version project_dir
let load_env_session ?(includes=[]) session conf_path_opt =
......@@ -428,7 +437,8 @@ let save fname config session =
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
fprintf fmt "<!DOCTYPE why3session SYSTEM \"%a\">@\n"
save_string (Filename.concat (Whyconf.datadir (Whyconf.get_main config)) "why3session.dtd");
fprintf fmt "@[<v 1><why3session@ name=\"%a\">" save_string fname;
fprintf fmt "@[<v 1><why3session@ name=\"%a\" shape_version=\"%d\">"
save_string fname session.session_shape_version;
let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session)
(Mprover.empty,0) in
PHstr.iter (save_file provers fmt) session.session_files;
......@@ -629,14 +639,19 @@ let raw_add_no_task ~(keygen:'a keygen) parent name expl sum shape exp =
in
goal
(* a global variable indicating the shape version to use. It is set
when reading the attribute shape_version of an XML file
*)
let current_shape_version = ref 0
let raw_add_task ~(keygen:'a keygen) parent name expl t exp =
let parent_key = match parent with
| Parent_theory mth -> mth.theory_key
| Parent_transf mtr -> mtr.transf_key
in
let key = keygen ~parent:parent_key () in
let sum = Termcode.task_checksum t in
let shape = Termcode.t_shape_buf (Task.task_goal_fmla t) in
let sum = Termcode.task_checksum ~version:!current_shape_version t in
let shape = Termcode.t_shape_buf ~version:!current_shape_version (Task.task_goal_fmla t) in
let goal = { goal_name = name;
goal_expl = expl;
goal_parent = parent;
......@@ -916,12 +931,15 @@ let old_provers = ref Util.Mstr.empty
let get_old_provers () = !old_provers
let load_session session xml =
let cont = xml.Xml.content in
match cont.Xml.name with
match xml.Xml.name with
| "why3session" ->
let shape_version = int_attribute "shape_version" xml 1 in
session.session_shape_version <- shape_version;
dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
(** just to keep the old_provers somewhere *)
old_provers :=
List.fold_left (load_file session) Util.Mstr.empty cont.Xml.elements
old_provers :=
List.fold_left (load_file session) Util.Mstr.empty xml.Xml.elements;
dprintf debug "[Info] load_session: done@\n"
| s ->
eprintf "[Warning] Session.load_session: unexpected element '%s'@." s
......@@ -931,13 +949,13 @@ let read_session dir =
if not (Sys.file_exists dir && Sys.is_directory dir) then
raise (OpenError (Pp.sprintf "%s is not an existing directory" dir));
let xml_filename = Filename.concat dir db_filename in
let session = {session_files = PHstr.create 3; session_dir = dir} in
let session = empty_session dir in
(** If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists xml_filename then begin
try
let xml = Xml.from_file xml_filename in
try
load_session session xml;
load_session session xml.Xml.content;
with Sys_error msg ->
failwith ("Open session: sys error " ^ msg)
with
......@@ -1342,7 +1360,9 @@ let array_map_list f l =
| [] -> assert false
| x::rem -> r := rem; f i x)
let associate_subgoals gname (old_goals : 'a goal list) new_goals =
let associate_subgoals gname (old_goals : 'a goal list)
new_goals =
dprintf debug "[Info] associate_subgoals, shape_version = %d@\n" !current_shape_version;
(*
we make a map of old goals indexed by their checksums
*)
......@@ -1359,7 +1379,7 @@ let associate_subgoals gname (old_goals : 'a goal list) new_goals =
let id = (Task.task_goal g).Decl.pr_name in
let goal_name = gname.Ident.id_string ^ "." ^ (string_of_int (i+1)) in
let goal_name = Ident.id_register (Ident.id_derive goal_name id) in
let sum = Termcode.task_checksum g in
let sum = Termcode.task_checksum ~version:!current_shape_version g in
(i,id,goal_name,g,sum))
new_goals
in
......@@ -1419,7 +1439,8 @@ let associate_subgoals gname (old_goals : 'a goal list) new_goals =
| Some _ -> acc
| None ->
let shape =
Termcode.t_shape_buf (Task.task_goal_fmla g)
Termcode.t_shape_buf ~version:!current_shape_version
(Task.task_goal_fmla g)
in
shape_array.(i) <- shape;
(shape,New_goal i)::acc)
......@@ -1639,8 +1660,9 @@ and merge_trans ~keygen env to_goal _ from_transf =
from_transf_name to_goal_name.Ident.id_string;
let subgoals =
Trans.apply_transform from_transf.transf_name env (goal_task to_goal) in
let goals = associate_subgoals
to_goal_name from_transf.transf_goals subgoals in
let goals =
associate_subgoals to_goal_name from_transf.transf_goals subgoals
in
let goal (gid,name,t,_,_,_,_) = name, get_explanation gid t, t in
let transf = add_transformation ~keygen ~goal
from_transf_name to_goal goals in
......@@ -1681,12 +1703,14 @@ let merge_theory ~keygen env ~allow_obsolete from_th to_th =
) to_th.theory_goals
let merge_file ~keygen env ~allow_obsolete from_f to_f =
dprintf debug "[Info] merge_file, shape_version = %d@." !current_shape_version;
set_file_expanded to_f from_f.file_expanded;
let from_theories = List.fold_left
(fun acc t -> Util.Mstr.add t.theory_name.Ident.id_string t acc)
Util.Mstr.empty from_f.file_theories
in
Util.list_or
let b =
Util.list_or
(fun to_th ->
try
let from_th =
......@@ -1701,21 +1725,60 @@ let merge_file ~keygen env ~allow_obsolete from_f to_f =
| Not_found -> raise OutdatedSession
)
to_f.file_theories
in
dprintf debug "[Info] merge_file, done@\n";
b
let rec recompute_all_shapes_goal g =
let t = goal_task g in
g.goal_shape <- Termcode.t_shape_buf (Task.task_goal_fmla t);
g.goal_checksum <- Termcode.task_checksum t;
PHstr.iter recompute_all_shapes_transf g.goal_transformations
and recompute_all_shapes_transf _ tr =
List.iter recompute_all_shapes_goal tr.transf_goals
let recompute_all_shapes_theory t =
List. iter recompute_all_shapes_goal t.theory_goals
let recompute_all_shapes_file _ f =
List.iter recompute_all_shapes_theory f.file_theories
let recompute_all_shapes session =
PHstr.iter recompute_all_shapes_file session.session_files;
session.session_shape_version <- Termcode.current_shape_version
let update_session ~keygen ~allow_obsolete old_session env whyconf =
let new_session = create_session old_session.session_dir in
let new_env_session = { session = new_session;
env = env;
whyconf = whyconf;
loaded_provers = PHprover.create 5;
} in
current_shape_version := old_session.session_shape_version;
dprintf debug "[Info] update_session: shape_version = %d@\n" !current_shape_version;
let new_session =
create_session ~shape_version:!current_shape_version old_session.session_dir
in
let new_env_session =
{ session = new_session;
env = env;
whyconf = whyconf;
loaded_provers = PHprover.create 5;
}
in
let obsolete = PHstr.fold (fun _ old_file acc ->
dprintf debug "[Load] file '%s'@\n" old_file.file_name;
let new_file = add_file ~keygen new_env_session
?format:old_file.file_format old_file.file_name in
?format:old_file.file_format old_file.file_name
in
merge_file ~keygen env ~allow_obsolete old_file new_file
|| acc)
old_session.session_files false in
old_session.session_files false
in
dprintf debug "[Info] update_session: done@\n";
if !current_shape_version <> Termcode.current_shape_version then
begin
current_shape_version := Termcode.current_shape_version;
dprintf debug "[Info] update_session: recompute shapes@\n";
recompute_all_shapes new_session;
end;
new_env_session, obsolete
let get_project_dir fname =
......
......@@ -69,8 +69,8 @@ type 'a goal = private
goal_name : Ident.ident; (** The ident of the task *)
goal_expl : expl;
goal_parent : 'a goal_parent;
goal_checksum : string; (** checksum of the task *)
goal_shape : string; (** shape are produced by the module Termcode *)
mutable goal_checksum : string; (** checksum of the task *)
mutable goal_shape : string; (** shape are produced by the module Termcode *)
mutable goal_verified : bool;
goal_task: task_option;
mutable goal_expanded : bool;
......@@ -128,6 +128,7 @@ and 'a file = private
and 'a session = private
{ session_files : 'a file PHstr.t;
mutable session_shape_version : int;
session_dir : string;
}
......@@ -138,7 +139,7 @@ val print_attempt_status : Format.formatter -> proof_attempt_status -> unit
val print_external_proof : Format.formatter -> 'key proof_attempt -> unit
val create_session : string -> 'key session
val create_session : ?shape_version:int -> string -> 'key session
(** create a new_session in the given directory. The directory is
created if it doesn't exists yet. Don't change the current
directory of the program if you give a relative path *)
......
......@@ -22,6 +22,8 @@ open Ty
open Term
let current_shape_version = 2
(* similarity code of terms, or of "shapes"
example:
......@@ -93,8 +95,8 @@ let rec pat_shape ~(push:string->'a->'a) c m (acc:'a) p : 'a =
| Por (p, q) ->
pat_shape ~push c m (push tag_or (pat_shape ~push c m acc q)) p
let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
let fn = t_shape ~push c m in
let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
let fn = t_shape ~version ~push c m in
match t.t_node with
| Tconst c -> const_shape ~push (push tag_const acc) c
| Tvar v ->
......@@ -108,34 +110,30 @@ let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
(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 acc = pat_shape ~push c m acc p in
let m = pat_rename_alpha c m p in
t_shape ~push c m acc t2
t_shape ~version ~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
t_shape ~version ~push c m (push tag_eps acc) f
| Tquant (q,b) ->
let vl,triggers,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
(* argument first, intentionally, to give more weight on A in
forall x,A *)
let acc = push hq (t_shape ~push c m acc f1) in
let acc = push hq (t_shape ~version ~push c m acc f1) in
List.fold_right
(fun trigger acc ->
List.fold_right
(fun t acc ->
t_shape ~push c m acc t)
t_shape ~version ~push c m acc t)
trigger acc)
triggers acc
| Tbinop (o,f,g) ->
......@@ -147,16 +145,29 @@ let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
in
fn (push tag (fn acc g)) f
(* g first, intentionally, to give more weight on B in A->B *)
| Tlet (t1,b) ->
let u,t2 = t_open_bound b in
let m = vs_rename_alpha c m u in
begin
match version with
| 1 ->
t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
| 2 ->
(* t2 first, intentionally *)
fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
| _ -> assert false
end
| Tnot f -> push tag_not (fn acc f)
| Ttrue -> push tag_true acc
| Tfalse -> push tag_false acc
let t_shape_buf t =
let t_shape_buf ?(version=current_shape_version) 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
let () = t_shape ~version ~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)
......@@ -164,26 +175,27 @@ let t_shape_list t =
let pr_shape_list fmt t =
List.iter (fun s -> Format.fprintf fmt "%s" s) (t_shape_list t)
*)
(* shape of a task *)
let param_decl_shape ~(push:string->'a->'a) (acc:'a) ls : 'a =
push (ls.ls_name.Ident.id_string) acc
let logic_decl_shape ~(push:string->'a->'a) (acc:'a) (ls,def) : 'a =
let logic_decl_shape ~version ~(push:string->'a->'a) (acc:'a) (ls,def) : 'a =
let acc = push (ls.ls_name.Ident.id_string) acc in
let vl,t = Decl.open_ls_defn def in
let c = ref (-1) in
let m = vl_rename_alpha c Mvs.empty vl in
t_shape ~push c m acc t
t_shape ~version ~push c m acc t
let logic_ind_decl_shape ~(push:string->'a->'a) (acc:'a) (ls,cl) : 'a =
let logic_ind_decl_shape ~version ~(push:string->'a->'a) (acc:'a) (ls,cl) : 'a =
let acc = push (ls.ls_name.Ident.id_string) acc in
List.fold_right
(fun (_,t) acc -> t_shape ~push (ref (-1)) Mvs.empty acc t)
(fun (_,t) acc -> t_shape ~version ~push (ref (-1)) Mvs.empty acc t)
cl acc
let propdecl_shape ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
let propdecl_shape ~version ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
let tag = match k with
| Decl.Plemma -> tag_Plemma
| Decl.Paxiom -> tag_Paxiom
......@@ -192,9 +204,9 @@ let propdecl_shape ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
in
let acc = push tag acc in
let acc = push n.Decl.pr_name.Ident.id_string acc in
t_shape ~push (ref(-1)) Mvs.empty acc t
t_shape ~version ~push (ref(-1)) Mvs.empty acc t
let decl_shape ~(push:string->'a->'a) (acc:'a) d : 'a =
let decl_shape ~version ~(push:string->'a->'a) (acc:'a) d : 'a =
match d.Decl.d_node with
| Decl.Dtype _ts ->
push tag_Dtype acc
......@@ -206,37 +218,38 @@ let decl_shape ~(push:string->'a->'a) (acc:'a) d : 'a =
param_decl_shape ~push (push tag_Dparam acc) ls
| Decl.Dlogic ldl ->
List.fold_right
(fun d acc -> logic_decl_shape ~push acc d)
(fun d acc -> logic_decl_shape ~version ~push acc d)
ldl (push tag_Dlogic acc)
| Decl.Dind (_, idl) ->
List.fold_right
(fun d acc -> logic_ind_decl_shape ~push acc d)
(fun d acc -> logic_ind_decl_shape ~version ~push acc d)
idl (push tag_Dind acc)
| Decl.Dprop pdecl ->
propdecl_shape ~push (push tag_Dprop acc) pdecl
propdecl_shape ~version ~push (push tag_Dprop acc) pdecl
let tdecl_shape ~(push:string->'a->'a) (acc:'a) t : 'a =
let tdecl_shape ~version ~(push:string->'a->'a) (acc:'a) t : 'a =
match t.Theory.td_node with
| Theory.Decl d -> decl_shape ~push (push tag_tDecl acc) d
| Theory.Decl d -> decl_shape ~version ~push (push tag_tDecl acc) d
| Theory.Meta _ -> push tag_tMeta acc
| Theory.Clone _ -> push tag_tClone acc
| Theory.Use _ -> push tag_tUse acc
let rec task_shape ~(push:string->'a->'a) (acc:'a) t : 'a =
let rec task_shape ~version ~(push:string->'a->'a) (acc:'a) t : 'a =
match t with
| None -> acc
| Some t ->
task_shape ~push (tdecl_shape ~push acc t.Task.task_decl)
task_shape ~version ~push (tdecl_shape ~version ~push acc t.Task.task_decl)
t.Task.task_prev
(* checksum of a task
it is the MD5 digest of the shape
*)
let task_checksum t =
let task_checksum ?(version=current_shape_version) t =
let b = Buffer.create 257 in
let push t () = Buffer.add_string b t in
let () = task_shape ~push () t in
let () = task_shape ~version ~push () t in
let shape = Buffer.contents b in
Digest.to_hex (Digest.string shape)
......
......@@ -18,6 +18,8 @@
(* *)
(**************************************************************************)
val current_shape_version : int
(*
val t_dist : term -> term -> float
(** returns an heuristic distance between the two given terms. The
......@@ -36,7 +38,7 @@ val t_dist : term -> term -> float
*)
val t_shape_buf : Term.term -> string
val t_shape_buf : ?version:int -> Term.term -> string
(** returns a shape of the given term *)
(*
......@@ -46,4 +48,4 @@ val t_shape_list : Term.term -> string list
val pr_shape_list : Format.formatter -> Term.term -> unit
*)
val task_checksum : Task.task -> string
val task_checksum : ?version:int -> Task.task -> string
......@@ -55,6 +55,10 @@ theory TestSplit
goal G4 : forall x:int. ("stop_split" aa x && bb 1) && ("stop_split" aa 1 && bb 2)
use import int.Int
goal Glet : (let x = 1 in x+1 = 2) /\ (let y = 3 in y+2 = 4)
end
theory TestMinMax
......@@ -127,11 +131,11 @@ theory TestIntros
use import int.Int
goal G :
goal G :
forall x y : int. x > 0 /\ y > 0 ->
(exists z t:int. x + t = y + z) -> x > y
goal G2 :
goal G2 :
forall x y : int. (x > 0 /\ y > 0) /\ (x < 10 /\ y < 10) ->
(exists x' y':int. x + x' = y + y') -> x > y
......
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