Monomorphization (library)

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

1 files changed, 110 insertions, 69 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 871381530..7c1100165 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -46,10 +46,16 @@ type visibility = Until of int | Exactly of int
 (* The [repr] function is assumed to return the reversed list of idents. *)
 module type UserName = sig
   type t
+  val equal : t -> t -> bool
   val to_string : t -> string
   val repr : t -> identifier * module_ident list
 end
 
+module type EqualityType =
+sig
+  type t
+  val equal : t -> t -> bool
+end
 
 (* A ['a t] is a map from [user_name] to ['a], with possible lookup by
    partially qualified names of type [qualid]. The mapping of
@@ -61,39 +67,41 @@ end
    the same object.
 *)
 module type NAMETREE = sig
-  type 'a t
+  type elt
+  type t
   type user_name
 
-  val empty : 'a t
-  val push : visibility -> user_name -> 'a -> 'a t -> 'a t
-  val locate : qualid -> 'a t -> 'a
-  val find : user_name -> 'a t -> 'a
-  val exists : user_name -> 'a t -> bool
-  val user_name : qualid -> 'a t -> user_name
-  val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
-  val find_prefixes : qualid -> 'a t -> 'a list
+  val empty : t
+  val push : visibility -> user_name -> elt -> t -> t
+  val locate : qualid -> t -> elt
+  val find : user_name -> t -> elt
+  val exists : user_name -> t -> bool
+  val user_name : qualid -> t -> user_name
+  val shortest_qualid : Idset.t -> user_name -> t -> qualid
+  val find_prefixes : qualid -> t -> elt list
 end
 
-module Make(U:UserName) : NAMETREE with type user_name = U.t
-				     =
+module Make (U : UserName) (E : EqualityType) : NAMETREE
+  with type user_name = U.t and type elt = E.t =
 struct
+  type elt = E.t
 
   type user_name = U.t
 
-  type 'a path_status =
+  type path_status =
       Nothing
-    | Relative of user_name * 'a
-    | Absolute of user_name * 'a
+    | Relative of user_name * elt
+    | Absolute of user_name * elt
 
   (* Dictionaries of short names *)
-  type 'a nametree =
-      { path : 'a path_status;
-	map : 'a nametree ModIdmap.t }
+  type nametree =
+      { path : path_status;
+	map : nametree ModIdmap.t }
 
   let mktree p m = { path=p; map=m }
   let empty_tree = mktree Nothing ModIdmap.empty
 
-  type 'a t = 'a nametree Idmap.t
+  type t = nametree Idmap.t
 
   let empty = Idmap.empty
 
@@ -125,8 +133,8 @@ struct
     | [] ->
 	match tree.path with
 	  | Absolute (uname',o') ->
-	      if o'=o then begin
-		assert (uname=uname');
+	      if E.equal o' o then begin
+		assert (U.equal uname uname');
 		tree
 		  (* we are putting the same thing for the second time :) *)
 	      end
@@ -146,7 +154,7 @@ let rec push_exactly uname o level tree = function
 	try ModIdmap.find modid tree.map
 	with Not_found -> empty_tree
       in
-        if level = 0 then
+        if Int.equal level 0 then
 	  let this =
 	    match tree.path with
 	      | Absolute (n,_) ->
@@ -219,9 +227,10 @@ let shortest_qualid ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Idset.mem id ctx in
   let rec find_uname pos dir tree =
+    let is_empty = match pos with [] -> true | _ -> false in
     match tree.path with
     | Absolute (u,_) | Relative (u,_)
-          when u=uname && not(pos=[] && hidden) -> List.rev pos
+          when U.equal u uname && not (is_empty && hidden) -> List.rev pos
     | _ ->
 	match dir with
 	    [] -> raise Not_found
@@ -256,36 +265,68 @@ end
 
 (* Global name tables *************************************************)
 
-module SpTab = Make (struct
-		       type t = full_path
-		       let to_string = string_of_path
-		       let repr sp =
-			 let dir,id = repr_path sp in
-			   id, (repr_dirpath dir)
-		     end)
+module FullPath =
+struct
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+      id, (repr_dirpath dir)
+end
 
+module ExtRefEqual =
+struct
+  type t = extended_global_reference
+  let equal e1 e2 = Int.equal (ExtRefOrdered.compare e1 e2) 0
+end
 
-type ccitab = extended_global_reference SpTab.t
-let the_ccitab = ref (SpTab.empty : ccitab)
+module KnEqual =
+struct
+  type t = kernel_name
+  let equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0
+end
 
-type kntab = kernel_name SpTab.t
-let the_tactictab = ref (SpTab.empty : kntab)
+module MPEqual =
+struct
+  type t = module_path
+  let equal = mp_eq
+end
+
+module ExtRefTab = Make(FullPath)(ExtRefEqual)
+module KnTab = Make(FullPath)(KnEqual)
+module MPTab = Make(FullPath)(MPEqual)
+
+type ccitab = ExtRefTab.t
+let the_ccitab = ref (ExtRefTab.empty : ccitab)
 
-type mptab = module_path SpTab.t
-let the_modtypetab = ref (SpTab.empty : mptab)
+type kntab = KnTab.t
+let the_tactictab = ref (KnTab.empty : kntab)
 
+type mptab = MPTab.t
+let the_modtypetab = ref (MPTab.empty : mptab)
+
+module DirPath =
+struct
+  type t = dir_path
+  let equal d1 d2 = Int.equal (dir_path_ord d1 d2) 0
+  let to_string = string_of_dirpath
+  let repr dir = match repr_dirpath dir with
+    | [] -> anomaly "Empty dirpath"
+    | id :: l -> (id, l)
+end
+
+module GlobDir =
+struct
+  type t = global_dir_reference
+  let equal = eq_global_dir_reference
+end
 
-module DirTab = Make(struct
-		       type t = dir_path
-		       let to_string = string_of_dirpath
-		       let repr dir = match repr_dirpath dir with
-			 | [] -> anomaly "Empty dirpath"
-			 | id::l -> (id,l)
-		     end)
+module DirTab = Make(DirPath)(GlobDir)
 
 (* If we have a (closed) module M having a submodule N, than N does not
    have the entry in [the_dirtab]. *)
-type dirtab = global_dir_reference DirTab.t
+type dirtab = DirTab.t
 let the_dirtab = ref (DirTab.empty : dirtab)
 
 
@@ -317,19 +358,19 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 let push_xref visibility sp xref =
   match visibility with
     | Until _ ->
-	the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
     | _ ->
 	begin
-	  if SpTab.exists sp !the_ccitab then
-	    match SpTab.find sp !the_ccitab with
+	  if ExtRefTab.exists sp !the_ccitab then
+	    match ExtRefTab.find sp !the_ccitab with
 	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
 		    TrueGlobal( ConstructRef _) as xref ->
-		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	      | _ -> 
-		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	    else
-	      the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	      the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	end
 
 let push_cci visibility sp ref =
@@ -342,13 +383,13 @@ let push_syndef visibility sp kn =
 let push = push_cci
 
 let push_modtype vis sp kn =
-  the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
+  the_modtypetab := MPTab.push vis sp kn !the_modtypetab;
   the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
 (* This is for tactic definition names *)
 
 let push_tactic vis sp kn =
-  the_tactictab := SpTab.push vis sp kn !the_tactictab;
+  the_tactictab := KnTab.push vis sp kn !the_tactictab;
   the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
 
 
@@ -364,22 +405,22 @@ let push_dir vis dir dir_ref =
 
 
 (* This should be used when syntactic definitions are allowed *)
-let locate_extended qid = SpTab.locate qid !the_ccitab
+let locate_extended qid = ExtRefTab.locate qid !the_ccitab
 
 (* This should be used when no syntactic definitions is expected *)
 let locate qid = match locate_extended qid with
   | TrueGlobal ref -> ref
   | SynDef _ -> raise Not_found
-let full_name_cci qid = SpTab.user_name qid !the_ccitab
+let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab
 
 let locate_syndef qid = match locate_extended qid with
   | TrueGlobal _ -> raise Not_found
   | SynDef kn -> kn
 
-let locate_modtype qid = SpTab.locate qid !the_modtypetab
-let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
+let locate_modtype qid = MPTab.locate qid !the_modtypetab
+let full_name_modtype qid = MPTab.user_name qid !the_modtypetab
 
-let locate_tactic qid = SpTab.locate qid !the_tactictab
+let locate_tactic qid = KnTab.locate qid !the_tactictab
 
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
@@ -401,9 +442,9 @@ let locate_section qid =
 
 let locate_all qid =
   List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
-    (SpTab.find_prefixes qid !the_ccitab) []
+    (ExtRefTab.find_prefixes qid !the_ccitab) []
 
-let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab
+let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
 (* Derived functions *)
 
@@ -413,11 +454,11 @@ let locate_constant qid =
     | _ -> raise Not_found
 
 let global_of_path sp =
-  match SpTab.find sp !the_ccitab with
+  match ExtRefTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
-let extended_global_of_path sp = SpTab.find sp !the_ccitab
+let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
 let global r =
   let (loc,qid) = qualid_of_reference r in
@@ -432,7 +473,7 @@ let global r =
 
 (* Exists functions ********************************************************)
 
-let exists_cci sp = SpTab.exists sp !the_ccitab
+let exists_cci sp = ExtRefTab.exists sp !the_ccitab
 
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
@@ -440,7 +481,7 @@ let exists_section = exists_dir
 
 let exists_module = exists_dir
 
-let exists_modtype sp = SpTab.exists sp !the_modtypetab
+let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 (* Reverse locate functions ***********************************************)
 
@@ -471,11 +512,11 @@ let shortest_qualid_of_global ctx ref =
     | VarRef id -> make_qualid empty_dirpath id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        SpTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef ctx kn =
   let sp = path_of_syndef kn in
-    SpTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_module mp =
   let dir = MPmap.find mp !the_modrevtab in
@@ -483,11 +524,11 @@ let shortest_qualid_of_module mp =
 
 let shortest_qualid_of_modtype kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    SpTab.shortest_qualid Idset.empty sp !the_modtypetab
+    MPTab.shortest_qualid Idset.empty sp !the_modtypetab
 
 let shortest_qualid_of_tactic kn =
   let sp = KNmap.find kn !the_tacticrevtab in
-    SpTab.shortest_qualid Idset.empty sp !the_tactictab
+    KnTab.shortest_qualid Idset.empty sp !the_tactictab
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
@@ -513,10 +554,10 @@ type frozen = ccitab * dirtab * mptab * kntab
     * globrevtab * mprevtab * mptrevtab * knrevtab
 
 let init () =
-  the_ccitab := SpTab.empty;
+  the_ccitab := ExtRefTab.empty;
   the_dirtab := DirTab.empty;
-  the_modtypetab := SpTab.empty;
-  the_tactictab := SpTab.empty;
+  the_modtypetab := MPTab.empty;
+  the_tactictab := KnTab.empty;
   the_globrevtab := Globrevtab.empty;
   the_modrevtab := MPmap.empty;
   the_modtyperevtab := MPmap.empty;