Commit 9573328e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Termcode: memoize partial checksum computation

parent d93cc40f
......@@ -61,7 +61,9 @@ let debug = Debug.register_info_flag "session_pairing"
~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
session@ trees@ after@ modification@ of@ source@ files."
let current_shape_version = 3
let current_shape_version = 4
type shape_version = SV1 | SV2 | SV3
(* similarity code of terms, or of "shapes"
......@@ -138,32 +140,29 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
l
| Tif (f,t1,t2) ->
begin match version with
| 1 | 2 -> fn (fn (fn (push tag_if acc) f) t1) t2
| 3 -> fn (fn (fn (push tag_if acc) t2) t1) f
| _ -> assert false
| SV1 | SV2 -> fn (fn (fn (push tag_if acc) f) t1) t2
| SV3 -> fn (fn (fn (push tag_if acc) t2) t1) f
end
| Tcase (t1,bl) ->
let br_shape acc b =
let p,t2 = t_open_branch b in
match version with
| 1 | 2 ->
| SV1 | SV2 ->
let acc = pat_shape ~push c m acc p in
let m = pat_rename_alpha c m p in
t_shape ~version ~push c m acc t2
| 3 ->
| SV3 ->
let m1 = pat_rename_alpha c m p in
let acc = t_shape ~version ~push c m1 acc t2 in
pat_shape ~push c m acc p
| _ -> assert false
in
begin match version with
| 1 | 2 ->
| SV1 | SV2 ->
List.fold_left br_shape (fn (push tag_case acc) t1) bl
| 3 ->
| SV3 ->
let acc = push tag_case acc in
let acc = List.fold_left br_shape acc bl in
fn acc t1
| _ -> assert false
end
| Teps b ->
let u,f = t_open_bound b in
......@@ -197,42 +196,48 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
let m = vs_rename_alpha c m u in
begin
match version with
| 1 ->
| SV1 ->
t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
| 2 | 3 ->
| SV2 | SV3 ->
(* t2 first, intentionally *)
fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
| _ -> assert false
end
| Tnot f ->
begin match version with
| 1 | 2 -> push tag_not (fn acc f)
| 3 -> fn (push tag_not acc) f
| _ -> assert false
| SV1 | SV2 -> push tag_not (fn acc f)
| SV3 -> fn (push tag_not acc) f
end
| Ttrue -> push tag_true acc
| Tfalse -> push tag_false acc
(* (* dead code *)
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 ~version ~push (ref (-1)) Mvs.empty () t in
Buffer.contents b
*)
let t_shape_task ?(version=current_shape_version) t =
let t_shape_task ~version t =
let b = Buffer.create 17 in
let push t () = Buffer.add_string b t in
begin match version with
| 1 | 2 -> ()
| 3 ->
| SV1 | SV2 -> ()
| SV3 ->
let _, expl, _ = goal_expl_task ~root:false t in
Opt.iter (Buffer.add_string b) expl
| _ -> assert false
end;
let f = Task.task_goal_fmla t in
let () = t_shape ~version ~push (ref (-1)) Mvs.empty () f in
Buffer.contents b
let t_shape_task ?(version=current_shape_version) t =
let version = match version with
| 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3
| _ -> assert false
in
t_shape_task ~version t
(* Checksums *)
type checksum = string
......@@ -242,16 +247,19 @@ let checksum_of_string x = x
let equal_checksum x y = (x : checksum) = y
let dumb_checksum = ""
type checksum_version = CV1 | CV2
module Checksum = struct
let char = Buffer.add_char
let int b i = char b 'i'; Buffer.add_string b (string_of_int i)
let string b s =
char b '"'; Buffer.add_string b (String.escaped s); char b '"'
let char (_,_,_,buf) c = Buffer.add_char buf c
let int (_,_,_,buf as b) i =
char b 'i'; Buffer.add_string buf (string_of_int i)
let string (_,_,_,buf as b) s =
char b '"'; Buffer.add_string buf (String.escaped s); char b '"'
let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
let list e b l = char b '['; List.iter (e b) l; char b ']'
let ident, clear_ident =
let ident_v1, clear_ident_v1 =
let hident = Ident.Hid.create 17 in
let c = ref 0 in
(fun b id ->
......@@ -259,6 +267,17 @@ module Checksum = struct
with Not_found -> incr c; Ident.Hid.add hident id !c; !c)),
(fun () -> Ident.Hid.clear hident; c := 0)
let ident_v2 (_,c,m,_ as b) id =
let i = match Ident.Mid.find_opt id !m with
| Some i -> i
| None -> incr c; m := Ident.Mid.add id !c !m; !c
in
int b i
let ident (v,_,_,_ as b) id = match v with
| CV1 -> ident_v1 b id
| CV2 -> ident_v2 b id
let const b c =
let buf = Buffer.create 17 in
Format.bprintf buf "%a" Pretty.print_const c;
......@@ -393,17 +412,43 @@ module Checksum = struct
char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
| Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal
let task t =
let task_v1 t =
let c = ref 0 in
let m = ref Ident.Mid.empty in
let b = Buffer.create 8192 in
Task.task_iter (tdecl b) t;
clear_ident ();
Task.task_iter (tdecl (CV1,c,m,b)) t;
clear_ident_v1 ();
let s = Buffer.contents b in
Digest.to_hex (Digest.string s)
end
let task_v2 t (c,m,rest) =
let c = ref c in
let m = ref m in
let b = Buffer.create 8192 in
tdecl (CV2,c,m,b) t.Task.task_decl;
Buffer.add_string b (Digest.to_hex rest);
let s = Buffer.contents b in
Buffer.clear b;
(!c, !m, Digest.string s)
let task_checksum ?(version=0) t = ignore version; Checksum.task t
let task_v2 = Trans.fold task_v2 (0, Ident.Mid.empty, Digest.string "")
let task_v2 t =
let _,_,s = Trans.apply task_v2 t in
Digest.to_hex s
let task ~version t = match version with
| CV1 -> task_v1 t
| CV2 -> task_v2 t
end
let task_checksum ?(version=current_shape_version) t =
let version = match version with
| 1 | 2 | 3 -> CV1
| 4 -> CV2
| _ -> assert false
in
Checksum.task ~version t
(*************************************************************)
(* Pairing of new and old subgoals *)
......
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