Modulification and removing of structural equality in VCS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16704 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 134 insertions, 106 deletions

diff --git a/lib/dag.ml b/lib/dag.ml
index 90ff927c5f..5a695ce1bc 100644
--- a/lib/dag.ml
+++ b/lib/dag.ml
@@ -8,8 +8,13 @@
 
 module type S = sig
 
-  type cluster_id
-  val string_of_cluster_id : cluster_id -> string
+  module Cluster :
+  sig
+    type t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+  end
 
   type node
   type ('edge,'info) t
@@ -21,11 +26,11 @@ module type S = sig
   val mem : ('e,'i) t -> node -> bool
 
   val iter : ('e,'i) t -> 
-    (node -> cluster_id option -> 'i option ->
+    (node -> Cluster.t option -> 'i option ->
       (node * 'e) list -> unit) -> unit
 
   val create_cluster : ('e,'i) t -> node list -> ('e,'i) t
-  val cluster_of : ('e,'i) t -> node -> cluster_id option
+  val cluster_of : ('e,'i) t -> node -> Cluster.t option
 
   val get_info : ('e,'i) t -> node -> 'i option
   val set_info : ('e,'i) t -> node -> 'i -> ('e,'i) t
@@ -35,16 +40,22 @@ end
 
 module Make(OT : Map.OrderedType) = struct
 
+module Cluster =
+struct
+  type t = int
+  let equal = Int.equal
+  let compare = Int.compare
+  let to_string = string_of_int
+end
+
 type node = OT.t
-type cluster_id = int
-let string_of_cluster_id = string_of_int
 
 module NodeMap = Map.Make(OT)
 module NodeSet = Set.Make(OT)
 
 type ('edge,'info) t = {
   graph : (node * 'edge) list NodeMap.t;
-  clusters : cluster_id NodeMap.t;
+  clusters : Cluster.t NodeMap.t;
   infos : 'info NodeMap.t;
 }
 
diff --git a/lib/dag.mli b/lib/dag.mli
index 791d82db11..7332e20cf5 100644
--- a/lib/dag.mli
+++ b/lib/dag.mli
@@ -8,12 +8,17 @@
 
 module type S = sig
 
-  type cluster_id
-  val string_of_cluster_id : cluster_id -> string
+  module Cluster :
+  sig
+    type t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+  end
 
   type node
   type ('edge,'info) t
-  
+
   val empty : ('e,'i) t
 
   val add_edge : ('e,'i) t -> node -> 'e -> node -> ('e,'i) t
@@ -22,11 +27,11 @@ module type S = sig
   val mem : ('e,'i) t -> node -> bool
 
   val iter : ('e,'i) t -> 
-    (node -> cluster_id option -> 'i option ->
+    (node -> Cluster.t option -> 'i option ->
       (node * 'e) list -> unit) -> unit
 
   val create_cluster : ('e,'i) t -> node list -> ('e,'i) t
-  val cluster_of : ('e,'i) t -> node -> cluster_id option
+  val cluster_of : ('e,'i) t -> node -> Cluster.t option
 
   val get_info : ('e,'i) t -> node -> 'i option
   val set_info : ('e,'i) t -> node -> 'i -> ('e,'i) t
diff --git a/lib/vcs.ml b/lib/vcs.ml
index dda0384f06..040d46ea72 100644
--- a/lib/vcs.ml
+++ b/lib/vcs.ml
@@ -11,39 +11,43 @@ open Errors
 
 module type S = sig
 
-  type branch_name
-  val mk_branch_name : string -> branch_name
-  val string_of_branch_name : branch_name -> string
-  
-  val master : branch_name
-  
+  module Branch :
+  sig
+    type t
+    val make : string -> t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+    val master : t
+  end
+
   type id
-  
+
   (* Branches have [branch_info] attached to them. *)
   type ('kind) branch_info = {
     kind : [> `Master] as 'kind;
     root : id;
     pos  : id;
   }
-  
+
   type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
-  
+
   val empty : id -> ('kind,'diff,'info) t
-  
-  val current_branch : ('k,'e,'i) t -> branch_name
-  val branches : ('k,'e,'i) t -> branch_name list
-  
-  val get_branch : ('k,'e,'i) t -> branch_name -> 'k branch_info
-  val reset_branch : ('k,'e,'i) t -> branch_name -> id -> ('k,'e,'i) t
+
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
+
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
   val branch :
-    ('kind,'e,'i) t -> ?root:id -> branch_name -> 'kind -> ('kind,'e,'i) t
-  val delete_branch : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
+    ('kind,'e,'i) t -> ?root:id -> Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
   val merge : (* a 'diff is always Nop, fix that XXX *)
-    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:branch_name ->
-            branch_name -> ('k,'diff,'i) t
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
   val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
-  val checkout : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
-  
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
   val get_info : ('k,'e,'info) t -> id -> 'info option
 
@@ -60,13 +64,19 @@ module Dag = Dag.Make(OT)
 
 type id = OT.t
 
-type branch_name = string
-let mk_branch_name = 
-  let bid = ref 0 in
-  fun s -> incr bid; string_of_int !bid ^ "_" ^ s
-let string_of_branch_name s = s
-  
-let master = "master"
+module Branch =
+struct
+  type t = string
+  let make =
+    let bid = ref 0 in
+    fun s -> incr bid; string_of_int !bid ^ "_" ^ s
+  let equal = CString.equal
+  let compare = CString.compare
+  let to_string s = s
+  let master = "master"
+end
+
+module BranchMap = Map.Make(Branch)
 
 type 'kind branch_info = {
   kind : [> `Master] as 'kind;
@@ -75,42 +85,43 @@ type 'kind branch_info = {
 }
 
 type ('kind,'edge,'info) t = {
-  cur_branch   : branch_name;
-  heads        : (branch_name * 'kind branch_info) list;
+  cur_branch   : Branch.t;
+  heads        : 'kind branch_info BranchMap.t;
   dag          : ('edge,'info) Dag.t;
 }
 
 let empty root = {
-  cur_branch = master; 
-  heads = [ master, { root = root; pos = root; kind = `Master } ];
+  cur_branch = Branch.master;
+  heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master };
   dag = Dag.empty;
 }
 
 let add_node vcs id edges =
-  assert (edges <> []);
+  assert (not (CList.is_empty edges));
   { vcs with dag =
      List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges }
 
 let get_branch vcs head =
-  try List.assoc head vcs.heads
+  try BranchMap.find head vcs.heads
   with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
 
-let reset_branch vcs head id = { vcs with
-  heads =
-    List.map (fun (name, h as orig) -> 
-      if name = head then name, { h with pos = id } else orig)
-    vcs.heads }
+let reset_branch vcs head id =
+  let map name h =
+    if Branch.equal name head then { h with pos = id } else h
+  in
+  { vcs with heads = BranchMap.mapi map vcs.heads; }
 
 let branch vcs ?(root = (get_branch vcs vcs.cur_branch).pos) name kind =
   { vcs with
-      heads = (name, { root; pos = root; kind }) :: vcs.heads;
+      heads = BranchMap.add name { root; pos = root; kind } vcs.heads;
       cur_branch = name }
 
-let delete_branch vcs name = { vcs with
-  heads = List.filter (fun (n, _) -> n <> name) vcs.heads }
+let delete_branch vcs name =
+  let filter n _ = not (Branch.equal n name) in
+  { vcs with heads = BranchMap.filter filter vcs.heads }
 
 let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
-  assert (name <> into);
+  assert (not (Branch.equal name into));
   let br_id = (get_branch vcs name).pos in
   let cur_id = (get_branch vcs into).pos in
   let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
@@ -130,7 +141,7 @@ let get_info vcs id = Dag.get_info vcs.dag id
 let create_cluster vcs l = { vcs with dag = Dag.create_cluster vcs.dag l }
 
 let current_branch vcs = vcs.cur_branch
-let branches vcs = List.map fst vcs.heads
+let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
 let dag vcs = vcs.dag
 
 end
diff --git a/lib/vcs.mli b/lib/vcs.mli
index 7ac568c127..36005c2cba 100644
--- a/lib/vcs.mli
+++ b/lib/vcs.mli
@@ -27,12 +27,16 @@
 
 module type S = sig
 
-  type branch_name
-  val mk_branch_name : string -> branch_name
-  val string_of_branch_name : branch_name -> string
-  
-  val master : branch_name
-  
+  module Branch :
+  sig
+    type t
+    val make : string -> t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+    val master : t
+  end
+
   type id
   
   type ('kind) branch_info = {
@@ -45,19 +49,19 @@ module type S = sig
   
   val empty : id -> ('kind,'diff,'info) t
   
-  val current_branch : ('k,'e,'i) t -> branch_name
-  val branches : ('k,'e,'i) t -> branch_name list
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
   
-  val get_branch : ('k,'e,'i) t -> branch_name -> 'k branch_info
-  val reset_branch : ('k,'e,'i) t -> branch_name -> id -> ('k,'e,'i) t
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
   val branch :
-    ('kind,'e,'i) t -> ?root:id -> branch_name -> 'kind -> ('kind,'e,'i) t
-  val delete_branch : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
+    ('kind,'e,'i) t -> ?root:id -> Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
   val merge : (* a 'diff is always Nop, fix that XXX *)
-    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:branch_name ->
-            branch_name -> ('k,'diff,'i) t
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
   val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
-  val checkout : ('k,'e,'i) t -> branch_name -> ('k,'e,'i) t
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
   
   val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
   val get_info : ('k,'e,'info) t -> id -> 'info option
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index d72b1fd2fe..eb83c81f62 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -43,9 +43,9 @@ module Vcs_ = Vcs.Make(StateidOrderedType)
 
 type branch_type = [ `Master | `Proof of string * int ]
 type cmd_t = ast * Id.t list
-type fork_t = ast * Vcs_.branch_name * Id.t list
+type fork_t = ast * Vcs_.Branch.t * Id.t list
 type qed_t =
-  ast * vernac_qed_type * (Vcs_.branch_name * branch_type Vcs_.branch_info)
+  ast * vernac_qed_type * (Vcs_.Branch.t * branch_type Vcs_.branch_info)
 type seff_t = ast option
 type alias_t = state_id
 type transaction =
@@ -78,7 +78,7 @@ module Vcs_aux : sig
   val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int
   val find_proof_at_depth :
     (branch_type, 't, 'i) Vcs_.t -> int ->
-      Vcs_.branch_name * branch_type Vcs_.branch_info
+      Vcs_.Branch.t * branch_type Vcs_.branch_info
 
 end = struct (* {{{ *)
 
@@ -100,8 +100,8 @@ end (* }}} *)
 (* Imperative wrap around VCS to obtain _the_ VCS *)
 module VCS : sig
 
+  module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
   type id = state_id
-  type branch_name = Vcs_.branch_name
   type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
     kind : [> `Master] as 'branch_type;
     root : id;
@@ -113,20 +113,17 @@ module VCS : sig
 
   val init : id -> unit
 
-  val string_of_branch_name : branch_name -> string
-
-  val current_branch : unit -> branch_name
-  val checkout : branch_name -> unit
-  val master : branch_name
-  val branches : unit -> branch_name list
-  val get_branch : branch_name -> branch_type branch_info
-  val get_branch_pos : branch_name -> id
+  val current_branch : unit -> Branch.t
+  val checkout : Branch.t -> unit
+  val branches : unit -> Branch.t list
+  val get_branch : Branch.t -> branch_type branch_info
+  val get_branch_pos : Branch.t -> id
   val new_node : unit -> id
-  val merge : id -> ours:transaction -> ?into:branch_name -> branch_name -> unit
-  val delete_branch : branch_name -> unit
+  val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
+  val delete_branch : Branch.t -> unit
   val commit : id -> transaction -> unit
-  val mk_branch_name : ast -> branch_name
-  val branch : branch_name -> branch_type -> unit
+  val mk_branch_name : ast -> Branch.t
+  val branch : Branch.t -> branch_type -> unit
   
   val get_info : id -> state_info
   val reached : id -> bool -> unit
@@ -227,7 +224,7 @@ end = struct (* {{{ *)
     );
     StateidSet.iter (nodefmt oc) !ids;
     Hashtbl.iter (fun c nodes ->
-       fprintf oc "subgraph cluster_%s {\n" (Dag.string_of_cluster_id c);
+       fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c);
        List.iter (nodefmt oc) nodes;
        fprintf oc "color=blue; }\n"
     ) clus;
@@ -235,7 +232,7 @@ end = struct (* {{{ *)
       let shape = if head = b then "box3d" else "box" in
       fprintf oc "b%d -> %s;\n" i (node id);
       fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
-        (string_of_branch_name b);
+        (Branch.to_string b);
     ) heads;
     output_string oc "}\n";
     close_out oc;
@@ -254,7 +251,7 @@ end = struct (* {{{ *)
   let current_branch () = current_branch !vcs
 
   let checkout head = vcs := checkout !vcs head
-  let master = master
+  let master = Branch.master
   let branches () = branches !vcs
   let get_branch head = get_branch !vcs head
   let get_branch_pos head = (get_branch head).pos
@@ -266,7 +263,7 @@ end = struct (* {{{ *)
     vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
   let delete_branch branch = vcs := delete_branch !vcs branch
   let commit id t = vcs := commit !vcs id t
-  let mk_branch_name (_, _, x) = mk_branch_name
+  let mk_branch_name (_, _, x) = Branch.make
     (match x with
     | VernacDefinition (_,(_,i),_) -> string_of_id i
     | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
@@ -295,7 +292,7 @@ end = struct (* {{{ *)
       checkout branch;
       Proof_global.activate_proof_mode mode
     with Failure _ ->
-      checkout master;
+      checkout Branch.master;
       Proof_global.disactivate_proof_mode "Classic" (* XXX *)
 
   (* copies the transaction on every open branch *)
@@ -303,8 +300,8 @@ end = struct (* {{{ *)
     List.iter (fun b ->
       checkout b;
       let id = new_node () in
-      merge id ~ours:(Sideff t) ~into:b master)
-    (List.filter ((<>) master) (branches ()))
+      merge id ~ours:(Sideff t) ~into:b Branch.master)
+    (List.filter ((<>) Branch.master) (branches ()))
   
   let visit id =
     try
@@ -857,7 +854,7 @@ module Backtrack : sig
   val cur : unit -> state_id
 
   (* we could navigate the dag, but this ways easy *)
-  val branches_of : state_id -> VCS.branch_name list
+  val branches_of : state_id -> VCS.Branch.t list
 
   (* To be installed during initialization *)
   val undo_vernac_classifier : vernac_expr -> vernac_classification
@@ -989,7 +986,7 @@ let join_aborted_proofs () =
          Future.purify observe eop; aux view.next
     | `Sideff _ | `Alias _ | `Cmd _ | `Fork _ | `Qed _ -> aux view.next
   in
-    aux (VCS.get_branch_pos VCS.master)
+    aux (VCS.get_branch_pos VCS.Branch.master)
 
 let join () =
   finish ();
@@ -1002,10 +999,10 @@ let join () =
   VCS.print ()
 
 let merge_proof_branch x keep branch =
-  if branch = VCS.master then
+  if VCS.Branch.equal branch VCS.Branch.master then
     raise(State.exn_on dummy_state_id Proof_global.NoCurrentProof);
   let info = VCS.get_branch branch in
-  VCS.checkout VCS.master;
+  VCS.checkout VCS.Branch.master;
   let id = VCS.new_node () in
   VCS.merge id ~ours:(Qed (x,keep,(branch, info))) branch;
   VCS.delete_branch branch;
@@ -1068,7 +1065,7 @@ let process_transaction verbosely (loc, expr) =
       | VtStartProof (mode, names), w ->
           let id = VCS.new_node () in
           let bname = VCS.mk_branch_name x in
-          VCS.checkout VCS.master;
+          VCS.checkout VCS.Branch.master;
           VCS.commit id (Fork (x, bname, names));
           VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
           Proof_global.activate_proof_mode mode;
@@ -1085,7 +1082,7 @@ let process_transaction verbosely (loc, expr) =
       (* Side effect on all branches *)
       | VtSideff l, w ->
           let id = VCS.new_node () in
-          VCS.checkout VCS.master;
+          VCS.checkout VCS.Branch.master;
           VCS.commit id (Cmd (x,l));
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
@@ -1095,12 +1092,12 @@ let process_transaction verbosely (loc, expr) =
       | VtUnknown, VtNow ->
           let id = VCS.new_node () in
           let step () =
-            VCS.checkout VCS.master;
-            let mid = VCS.get_branch_pos VCS.master in
+            VCS.checkout VCS.Branch.master;
+            let mid = VCS.get_branch_pos VCS.Branch.master in
             Reach.known_state ~cache:(interactive ()) mid;
             interp id x;
             (* Vernac x may or may not start a proof *)
-            if head = VCS.master &&
+            if VCS.Branch.equal head VCS.Branch.master &&
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
@@ -1120,7 +1117,7 @@ let process_transaction verbosely (loc, expr) =
     (* Proof General *)
     begin match v with 
       | VernacStm (PGLast _) ->
-        if head <> VCS.master then
+        if head <> VCS.Branch.master then
           interp dummy_state_id
             (true,Loc.ghost,VernacShow (ShowGoal OpenSubgoals))
       | _ -> ()
@@ -1156,7 +1153,7 @@ let current_proof_depth () =
       distance cur
 
 let unmangle n =
-  let n = VCS.string_of_branch_name n in
+  let n = VCS.Branch.to_string n in
   let idx = String.index n '_' + 1 in
   Names.id_of_string (String.sub n idx (String.length n - idx))
 
@@ -1184,7 +1181,7 @@ let get_script prf =
     | `Alias id -> find acc id
     | `Fork _ -> find acc view.next
     in
-  find [] (VCS.get_branch_pos VCS.master)
+  find [] (VCS.get_branch_pos VCS.Branch.master)
 
 (* indentation code for Show Script, initially contributed
    by D. de Rauglaudre *)