cleaning up checksum code (will change checksums)

src/session/session.ml

@@ -1781,7 +1781,7 @@ let print_external_proof fmt p =
 
 module AssoGoals : sig
   val associate : 'a goal list -> 'b goal list ->
-    ('b goal * ('a goal option) * bool) list
+    ('b goal * ('a goal * bool) option) list
 end = struct
 (** When Why3 will require 3.12 put all of that in a function using
     explicit type argument "(type t)" and remove all the Obj.magic *)
@@ -1805,19 +1805,19 @@ end = struct
     let name g     = g.goal_name
   end
 
-  module AssoGoals = Tc.AssoMake2(FromGoal)(ToGoal)
+  module AssoGoals = Tc.Pairing(FromGoal)(ToGoal)
   open ToGoal
   open FromGoal
 
   let associate (from_goals: 'ffrom goal list) (to_goals: 'tto goal list) :
-      ('tto goal * ('ffrom goal option) * bool) list =
+      ('tto goal * ('ffrom goal * bool) option) list =
     let from_goals : ffrom goal list =
       Obj.magic (from_goals : 'ffrom goal list) in
     let to_goals   : tto goal list =
       Obj.magic (to_goals : 'tto goal list) in
-    let associated : (tto goal * (ffrom goal option) * bool) list =
+    let associated : (tto goal * (ffrom goal * bool) option) list =
       AssoGoals.associate from_goals to_goals in
-    (Obj.magic associated : ('tto goal * ('ffrom goal option) * bool) list)
+    (Obj.magic associated : ('tto goal * ('ffrom goal * bool) option) list)
 
 end
 
@@ -1881,9 +1881,9 @@ and merge_trans ~keygen ~theories env to_goal _ from_transf =
         env.session.session_shape_version;
       AssoGoals.associate from_transf.transf_goals to_transf.transf_goals in
     List.iter (function
-    | (to_goal, Some from_goal, obsolete) ->
+    | (to_goal, Some (from_goal, obsolete)) ->
       merge_any_goal ~keygen ~theories env obsolete  from_goal to_goal
-    | (_, None, _) -> ()
+    | (_, None) -> ()
     ) associated
   with Exit -> ()
 
@@ -2270,9 +2270,9 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
       env.session.session_shape_version;
     AssoGoals.associate from_transf.transf_goals to_transf.transf_goals in
   List.iter (function
-  | (to_goal, Some from_goal, _obsolete) ->
+  | (to_goal, Some (from_goal, _obsolete)) ->
     add_goal_to_parent ~keygen env from_goal to_goal
-  | (_, None, _) -> ()
+  | (_, None) -> ()
   ) associated;
   to_transf
 

src/session/termcode.ml

@@ -11,12 +11,7 @@
 
 open Term
 
-type checksum = string
-let print_checksum = Format.pp_print_string
-let string_of_checksum x = x
-let checksum_of_string x = x
-let equal_checksum x y = (x : checksum) = y
-let dumb_checksum = ""
+(* Shapes *)
 
 type shape = string
 let print_shape = Format.pp_print_string
@@ -161,6 +156,15 @@ let t_shape_buf ?(version=current_shape_version) t =
   Buffer.contents b
 
 
+(* Checksums *)
+
+type checksum = string
+let print_checksum = Format.pp_print_string
+let string_of_checksum x = x
+let checksum_of_string x = x
+let equal_checksum x y = (x : checksum) = y
+let dumb_checksum = ""
+
 module Checksum = struct
 
   let char = Buffer.add_char
@@ -170,8 +174,14 @@ module Checksum = struct
   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_printer = Ident.create_ident_printer []
-  let ident b id = string b (Ident.id_unique ident_printer id)
+  (* let ident_printer = Ident.create_ident_printer [] *)
+  (* let ident b id = string b (Ident.id_unique ident_printer id) *)
+  let hident = Ident.Hid.create 17
+  let ident =
+    let c = ref 0 in
+    fun b id ->
+      int b (try Ident.Hid.find hident id
+        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)
 
   let const b c =
     let buf = Buffer.create 17 in
@@ -196,32 +206,26 @@ module Checksum = struct
     | Por (p, q) -> char b 'o'; pat b p; pat b q
 
   (* start: c V v i m e F E A O I q l n t f *)
-  let rec term c m b t = match t.t_node with
+  let rec term b t = match t.t_node with
     | Tconst c -> const b c
-    | Tvar v ->
-        begin try let x = Mvs.find v m in char b 'V'; int b x
-        with Not_found -> char b 'v'; ident b v.vs_name end
-    | Tapp (s, l) -> char b 'a'; ident b s.ls_name; list (term c m) b l
-    | Tif (f, t1, t2) -> char b 'i'; term c m b f; term c m b t1; term c m b t2
+    | Tvar v -> char b 'v'; ident b v.vs_name
+    | Tapp (s, l) -> char b 'a'; ident b s.ls_name; list term b l
+    | Tif (f, t1, t2) -> char b 'i'; term b f; term b t1; term b t2
     | Tcase (t1, bl) ->
         let branch b br =
           let p, t2 = t_open_branch br in
-          pat b p;
-          let m = pat_rename_alpha c m p in
-          term c m b t2
+          pat b p; term b t2
         in
-        char b 'm'; term c m b t1; list branch b bl
+        char b 'm'; term b t1; list branch b bl
     | Teps bf ->
         let vs, f = t_open_bound bf in
-        let m = vs_rename_alpha c m vs in
-        char b 'e'; vsymbol b vs; term c m b f
+        char b 'e'; vsymbol b vs; term b f
     | Tquant (q, bf) ->
         let vl, triggers, f1 = t_open_quant bf in
-        let m = vl_rename_alpha c m vl in
         char b (match q with Tforall -> 'F' | Texists -> 'E');
         list vsymbol b vl;
-        list (list (term c m)) b triggers;
-        term c m b f1
+        list (list term) b triggers;
+        term b f1
     | Tbinop (o, f, g) ->
         let tag = match o with
           | Tand -> 'A'
@@ -229,13 +233,12 @@ module Checksum = struct
           | Timplies -> 'I'
           | Tiff -> 'q'
         in
-        char b tag; term c m b f; term c m b g
+        char b tag; term b f; term b g
     | Tlet (t1, bt) ->
         let vs, t2 = t_open_bound bt in
-        char b 'l'; vsymbol b vs; term c m b t1;
-        let m = vs_rename_alpha c m vs in
-        term c m b t2
-    | Tnot f -> char b 'n'; term c m b f
+        char b 'l'; vsymbol b vs; term b t1;
+        term b t2
+    | Tnot f -> char b 'n'; term b f
     | Ttrue -> char b 't'
     | Tfalse -> char b 'f'
 
@@ -251,10 +254,9 @@ module Checksum = struct
     list tvsymbol b (Ty.Stv.elements ls.ls_opaque);
     int b ls.ls_constr
 
-  (* start: T D R L I P *)
+  (* start: T D R L I P (C M) *)
   let decl b d = match d.Decl.d_node with
     | Decl.Dtype ts ->
-        (* FIXME: alpha-equivalence for type variables as well *)
         char b 'T'; tysymbol b ts
     | Decl.Ddata ddl ->
         let constructor b (ls, l) = lsymbol b ls; list (option lsymbol) b l in
@@ -266,15 +268,13 @@ module Checksum = struct
         let logic_decl b (ls, defn) =
           lsymbol b ls;
           let vl, t = Decl.open_ls_defn defn in
-          let c = ref (-1) in
-          let m = vl_rename_alpha c Mvs.empty vl in
-          list vsymbol b vl; (* FIXME: really needed? (we did lsymbol above) *)
-          term c m b t
+          list vsymbol b vl;
+          term b t
         in
         char b 'L'; list logic_decl b ldl
     | Decl.Dind (s, idl) ->
         let clause b (pr, f) =
-          ident b pr.Decl.pr_name; term (ref (-1)) Mvs.empty b f in
+          ident b pr.Decl.pr_name; term b f in
         let ind_decl b (ls, cl) = lsymbol b ls; list clause b cl in
         char b 'I'; char b (match s with Decl.Ind -> 'i' | Decl.Coind -> 'c');
         list ind_decl b idl
@@ -287,7 +287,7 @@ module Checksum = struct
         in
         string b tag;
         ident b n.Decl.pr_name;
-        term (ref (-1)) Mvs.empty b t
+        term b t
 
   let meta_arg_type b = function
     | Theory.MTty       -> char b 'y'
@@ -300,8 +300,7 @@ module Checksum = struct
   let meta b m =
     string b m.Theory.meta_name;
     list meta_arg_type b m.Theory.meta_type;
-    char b (if m.Theory.meta_excl then 't' else 'f');
-    string b (string_of_format m.Theory.meta_desc) (* FIXME: necessary? *)
+    char b (if m.Theory.meta_excl then 't' else 'f')
 
   let meta_arg b = function
     | Theory.MAty t  -> char b 'y'; ty b t
@@ -313,13 +312,16 @@ module Checksum = struct
 
   let tdecl b d = match d.Theory.td_node with
     | Theory.Decl d -> decl b d
-    | Theory.Use _ | Theory.Clone _ -> () (* FIXME: OK? *)
+    | Theory.Use _ -> assert false
+    | Theory.Clone (th, _) ->
+        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 b = Buffer.create 8192 in
-    Ident.forget_all ident_printer;
+    (* Ident.forget_all ident_printer; *)
     Task.task_iter (tdecl b) t;
+    Ident.Hid.clear hident;
     let s = Buffer.contents b in
     Digest.to_hex (Digest.string s)
 
@@ -327,357 +329,37 @@ end
 
 let task_checksum ?(version=0) t = ignore version; Checksum.task t
 
-(*************************)
-(**       Pairing       **)
-
-(** needed accessor *)
-module type S = sig
-  type t
-  val checksum : t -> string
-  val shape    : t -> string
-  val name       : t -> Ident.ident
-end
-
-(*
-module type Sold = sig
-  type t
-  val checksum : t -> string
-  val shape    : t -> string
-  val id       : t -> Ident.ident
-(* .goal_name *)
-end
-*)
-
-(*
-module type Snew = sig
-  type t
-  val checksum : t -> string
-  val shape    : t -> string
-  (* Termcode.t_shape_buf ~version:!current_shape_version *)
-  (*   (Task.task_goal_fmla g) *)
-
-  val name     : t -> string (** for debugging *)
-(* 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 *)
-
-  val id      : t -> Ident.ident
-(* let id = (Task.task_goal g).Decl.pr_name in *)
-
-(* 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 *)
-
-
-end
-*)
-
 
 (*************************************************************)
-(* pairing of new and old subgoals of a given transformation *)
+(* Pairing of new and old subgoals                           *)
 (*************************************************************)
 
 (* we have an ordered list of new subgoals
 
-           subgoals = [g1; g2; g3; ...]
+     newgoals = [g1; g2; g3; ...]
 
    and a list of old subgoals
 
-          old_subgoals = [h1 ; h2 ; ... ]
-
-   we build a map from each new subgoal g to tuples
-       (id,subgoal_name,subtask,sum,old_subgoal,obsolete)
+     oldgoals = [h1 ; h2 ; ... ]
 
-   where
-     id = name of the goal of g
-     subgoal_name = name of parent goal with "dot n" added
-     subtask = the corresponding task
-     sum = the checksum of that task
-     old_subgoal = ref to an optional old subgoal which is paired with g
-     obsolete = true when paired to an old goal with different checksum
+   we build a list
 
-*)
+     [g1, None; g2, Some (h3, false); g3, Some (h2, true); ...]
 
-module AssoMake (Old : S) (New : S) = struct
-
-type 'a any_goal =
-  | New_goal of int
-  | Old_goal of Old.t
-
-let array_map_list f l =
-  let r = ref l in
-  Array.init (List.length l)
-    (fun i ->
-       match !r with
-         | [] -> assert false
-         | x::rem -> r := rem; f i x)
-
-let associate (old_goals : Old.t list) new_goals =
-  (*
-     we make a map of old goals indexed by their checksums
-  *)
-  let old_goals_map = Hashtbl.create 7 in
-  List.iter
-    (fun g -> Hashtbl.add old_goals_map (Old.checksum g) g)
-    old_goals;
-  (*
-     we make an array of new goals with their numbers and checksums
-  *)
-  let new_goals_array =
-    array_map_list
-      (fun i g -> i,g)
-      new_goals
-  in
-  let pairing_array =
-    Array.make (Array.length new_goals_array) None
-  in
-  let obsolete_array =
-    Array.make (Array.length new_goals_array) false
-  in
-  (*
-     Phase 1: we first associate each new goal for which there is an
-     old goal with the same checksum.
-  *)
-  let associate_goals ~obsolete i g =
-    pairing_array.(i) <- Some g;
-    obsolete_array.(i) <- obsolete;
-    Hashtbl.remove old_goals_map (Old.checksum g)
-  in
-  Array.iter
-    (fun (i,g) ->
-       try
-         let h = Hashtbl.find old_goals_map (New.checksum g) in
-         (* an old goal has the same checksum *)
-         Debug.dprintf debug
-           "Merge phase 1: old goal '%s' -> new goal '%s'@."
-           (Old.name h).Ident.id_string (New.name g).Ident.id_string;
-         associate_goals ~obsolete:false i h
-       with Not_found ->
-         Debug.dprintf debug
-           "Merge phase 1: no old goal -> new goal '%s'@."
-           (New.name g).Ident.id_string;
-         ())
-    new_goals_array;
-  (* Phase 2: we now build a list of all remaining new and old goals,
-     ordered by shapes, then by name *)
-  let old_goals_without_pairing =
-    Hashtbl.fold
-      (fun _ g acc ->
-         let s = (Old.shape g) in
-         if s = "" then
-           (* We don't try to associate old goals without shapes:
-              they will be paired in order in next phase *)
-           acc
-         else
-           (s,Old_goal g)::acc)
-      old_goals_map
-      []
-  in
-  let all_goals_without_pairing =
-    Array.fold_left
-      (fun acc (i,g) ->
-         match pairing_array.(i) with
-           | Some _ -> acc
-           | None ->
-               let shape = New.shape g
-                 (* Termcode.t_shape_buf ~version:!current_shape_version *)
-                 (*   (Task.task_goal_fmla g) *)
-               in
-               (* shape_array.(i) <- shape; *)
-               (shape,New_goal i)::acc)
-      old_goals_without_pairing
-      new_goals_array
-  in
-  let sort_by_shape =
-    List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2)
-      all_goals_without_pairing
-  in
-  if Debug.test_flag debug then begin
-    Debug.dprintf debug "[Merge] pairing the following shapes:@.";
-    List.iter
-      (fun (s,g) ->
-         match g with
-           | New_goal _ ->
-               Debug.dprintf debug "new: %s@." s
-           | Old_goal _ ->
-               Debug.dprintf debug "old: %s@." s)
-      sort_by_shape;
-  end;
-  let rec similarity_shape n s1 s2 =
-    if String.length s1 <= n || String.length s2 <= n then n else
-      if s1.[n] = s2.[n] then similarity_shape (n+1) s1 s2
-      else n
-  in
-(*  let rec match_shape (opt:int option) goals : bool =
-    (* when [opt] is [Some n] then it means [goals] starts with a goal g
-       which is already claimed to be associated by the former goal h.
-       We return a boolean which is true when that first goal g was also
-       claimed by the next goal, with a proximity measure larger than n,
-       meaning that the former goal h cannot associate with g
-    *)
-    match goals with
-      | [] -> false
-      | (si,New_goal i)::rem ->
-          begin match rem with
-            | [] -> false
-            | (_,New_goal _)::_ ->
-                let (_:bool) = match_shape None rem in false
-            | (sh,Old_goal h)::_ ->
-                try_associate si i sh h opt rem
-          end
-      | (sh,Old_goal h)::rem ->
-          begin match rem with
-            | [] -> false
-            | (_,Old_goal _)::_ ->
-                let (_:bool) = match_shape None rem in false
-            | (si,New_goal i)::_ ->
-                try_associate si i sh h opt rem
-          end
-  and try_associate si i sh h opt rem =
-    let n = similarity_shape 0 si sh in
-    Debug.dprintf debug "[Merge] try_associate: claiming \
-      similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
-    if (match opt with
-      | None ->
-          Debug.dprintf debug "[Merge] try_associate: \
-            no previous claim@.";
-          true
-      | Some m ->
-          Debug.dprintf debug "[Merge] try_associate: \
-            previous claim was %d@." m;
-          m < n)
-    then
-      (* try to associate i with h *)
-      let b = match_shape (Some n) rem in
-      if b then
-        begin
-          (* h or i was already paired in rem *)
-          Debug.dprintf debug "[Merge] try_associate: \
-            failed because claimed further@.";
-          false
-        end
-      else
-        begin
-          Debug.dprintf debug "[Merge] try_associate: \
-            succeeded to associate new goal@\n%s@\nwith \
-            old goal@\n%s@." si sh;
-          associate_goals ~obsolete:true i h;
-          true
-        end
-    else
-      (* no need to try to associate i with h *)
-      begin
-        Debug.dprintf debug "[Merge] try_associate: \
-          no claim further attempted@.";
-        let (_:bool) = match_shape None rem in
-        false
-      end
-  in
-  let (_:bool) = match_shape None sort_by_shape in
+   where each new goal is mapped either to
+   - None: no pairing at all
+   - Some (h, false): exact matching (equal checksums)
+   - Some (h, true): inexact matching (goal obsolete)
 *)
-  let rec match_shape (min:int) goals : bool * (string * 'a any_goal) list =
-    (* try to associate in [goals] each pair of old and new goal whose
-       similarity is at least [min]. Returns a pair [(b,rem)] where
-       [rem] is the sublist of [goals] made of goals which have not
-       been paired, and [b] is a boolean telling that the head of
-       [rem] is the same has the head of [goals] *)
-    match goals with
-      | [] -> (true, goals)
-      | ((si,New_goal i) as hd)::rem ->
-          begin match rem with
-            | [] -> (true, goals)
-            | (_,New_goal _)::_ ->
-                let (b,rem2) = match_shape min rem in
-                if b then
-                  (true, hd::rem2)
-                else
-                  match_shape min (hd::rem2)
-            | (sh,Old_goal h)::_ ->
-                try_associate min si i sh h hd rem
-          end
-      | ((sh,Old_goal h) as hd)::rem ->
-          begin match rem with
-            | [] -> (true, goals)
-            | (_,Old_goal _)::_ ->
-                let (b,rem2) = match_shape min rem in
-                if b then
-                  (true, hd::rem2)
-                else
-                  match_shape min (hd::rem2)
-            | (si,New_goal i)::_ ->
-                try_associate min si i sh h hd rem
-          end
-            (** si : shape of i
-                i  : id of the new goal
-                sh : shape of h
-                h  : an old goal
-                hd : the head
-                rem : the tail of the list *)
-  and try_associate min si i sh h hd rem =
-    let n = similarity_shape 0 si sh in
-    Debug.dprintf debug "[Merge] try_associate: claiming \
-      similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
-    if n < min then
-      begin
-        Debug.dprintf debug "[Merge] try_associate: claiming \
-          dropped because similarity lower than min = %d@." min;
-        let (b,rem2) = match_shape min rem in
-        if b then
-          (true, hd::rem2)
-        else
-          match_shape min (hd::rem2)
-      end
-    else
-      match match_shape n rem with
-        | false, rem2 ->
-            Debug.dprintf debug "[Merge] try_associate: claiming \
-              dropped because head was consumed by larger similarity@.";
-            match_shape min (hd::rem2)
-        | true, [] -> assert false
-        | true, _::rem2 ->
-            Debug.dprintf debug "[Merge] try_associate: claiming \
-              succeeded (similarity %d) for new shape@\n%s@\nand \
-              old shape@\n%s@." n si sh;
-            associate_goals ~obsolete:true i h;
-            let (_,rem3) = match_shape min rem2 in
-            (false, rem3)
-  in
-  let (_b,_rem) = match_shape 0 sort_by_shape in
-  (*
-     Phase 3: we now associate remaining new goals to the remaining
-     old goals in the same order as original
-  *)
-  Debug.dprintf debug "[Merge] phase 3: associate remaining goals@.";
-  let remaining_old_goals =
-    Hashtbl.fold
-      (fun _ g acc -> (Old.name g,g)::acc)
-      old_goals_map
-      []
-  in
-  let remaining_old_goals =
-    ref (List.sort (fun (s1,_) (s2,_) ->
-      String.compare s1.Ident.id_string s2.Ident.id_string)
-           remaining_old_goals)
-  in
-  Array.iteri
-    (fun i opt ->
-       match opt with
-         | Some _ -> ()
-         | None ->
-             match !remaining_old_goals with
-               | [] -> ()
-               | (_,h) :: rem ->
-                   remaining_old_goals := rem;
-                   associate_goals ~obsolete:true i h)
-    pairing_array;
-
-  Array.fold_right
-    (fun (i,g) res -> (g, pairing_array.(i), obsolete_array.(i))::res)
-    new_goals_array []
 
+module type S = sig
+  type t
+  val checksum : t -> string
+  val shape    : t -> string
+  val name     : t -> Ident.ident
 end
 
-module AssoMake2 (Old : S) (New : S) = struct
+module Pairing(Old: S)(New: S) = struct
 
   let rec lcp n s1 s2 =
     if String.length s1 <= n || String.length s2 <= n then n
@@ -724,7 +406,7 @@ module AssoMake2 (Old : S) (New : S) = struct
     let new_goal_index = Hid.create 17 in
     let result =
       let make i newg =
-        Hid.add new_goal_index (New.name newg) i; (newg, None, false) in
+        Hid.add new_goal_index (New.name newg) i; (newg, None) in
       Array.mapi make (Array.of_list newgoals) in
     let new_goal_index newg =
       try Hid.find new_goal_index (New.name newg)
@@ -738,7 +420,7 @@ module AssoMake2 (Old : S) (New : S) = struct
       try
         let oldg = Hashtbl.find old_checksums c in