Merge branch 'experimental/upstream' into upstream

1 files changed, 172 insertions, 113 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 642f5562..8c228404 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1,35 +1,34 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting
+   parts of file initial.ml from CoC V4.8, Dec 1988, by Gérard Huet,
+   Thierry Coquand and Christine Paulin *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Extra functions for splitting/generation of identifiers by Hugo Herbelin *)
+(* Restructuration by Jacek Chrzaszcz as part of the implementation of
+   the module system, Aug 2002 *)
+(* Abstraction over the type of constant for module inlining by Claudio
+   Sacerdoti, Nov 2004 *)
+(* Miscellaneous features or improvements by Hugo Herbelin, 
+   Élie Soubiran, ... *)
 
 open Pp
 open Util
 
-(*s Identifiers *)
+(** {6 Identifiers } *)
 
 type identifier = string
 
-let id_ord = Pervasives.compare
-
 let id_of_string s = check_ident_soft s; String.copy s
-
 let string_of_id id = String.copy id
 
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
-  struct
-    type t = string
-    type u = string -> string
-    let hash_sub hstr id = hstr id
-    let equal id1 id2 = id1 == id2
-    let hash = Hashtbl.hash
-  end)
+let id_ord = Pervasives.compare
 
 module IdOrdered =
   struct
@@ -38,15 +37,27 @@ module IdOrdered =
   end
 
 module Idset = Set.Make(IdOrdered)
-module Idmap = Map.Make(IdOrdered)
+module Idmap =
+struct
+  include Map.Make(IdOrdered)
+  exception Finded
+  let exists f m =
+    try iter (fun a b -> if f a b then raise Finded) m ; false
+    with |Finded -> true
+  let singleton k v = add k v empty
+end
 module Idpred = Predicate.Make(IdOrdered)
 
-(* Names *)
+(** {6 Various types based on identifiers } *)
 
 type name = Name of identifier | Anonymous
+type variable = identifier
 
-(* Dirpaths are lists of module identifiers. The actual representation
-   is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *)
+(** {6 Directory paths = section names paths } *)
+
+(** Dirpaths are lists of module identifiers.
+    The actual representation is reversed to optimise sharing:
+    Coq.A.B is ["B";"A";"Coq"] *)
 
 type module_ident = identifier
 type dir_path = module_ident list
@@ -58,14 +69,17 @@ let repr_dirpath x = x
 
 let empty_dirpath = []
 
+(** Printing of directory paths as ["coq_root.module.submodule"] *)
+
 let string_of_dirpath = function
   | [] -> "<>"
   | sl -> String.concat "." (List.map string_of_id (List.rev sl))
 
+(** {6 Unique names for bound modules } *)
 
 let u_number = ref 0
-type uniq_ident = int * string * dir_path
-let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
+type uniq_ident = int * identifier * dir_path
+let make_uid dir s = incr u_number;(!u_number,s,dir)
  let debug_string_of_uid (i,s,p) =
  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
 let string_of_uid (i,s,p) =
@@ -76,30 +90,31 @@ module Umap = Map.Make(struct
 			 let compare = Pervasives.compare
 		       end)
 
-type label = string
-
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
 let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
 let string_of_mbid = string_of_uid
 let id_of_mbid (_,s,_) = s
-let label_of_mbid (_,s,_) = s
 
+(** {6 Names of structure elements } *)
 
-let mk_label l = l
-let string_of_label = string_of_id
+type label = identifier
 
+let mk_label = id_of_string
+let string_of_label = string_of_id
+let pr_label l = str (string_of_label l)
 let id_of_label l = l
 let label_of_id id = id
 
 module Labset = Idset
 module Labmap = Idmap
 
+(** {6 The module part of the kernel name } *)
+
 type module_path =
   | MPfile of dir_path
   | MPbound of mod_bound_id
- (* | MPapp of module_path * module_path *)
   | MPdot of module_path * label
 
 let rec check_bound_mp = function
@@ -110,12 +125,9 @@ let rec check_bound_mp = function
 let rec string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
   | MPbound uid -> string_of_uid uid
- (* | MPapp (mp1,mp2) -> 
-      "("^string_of_mp mp ^ " " ^ 
-	string_of_mp mp^")"*)
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
-(* we compare labels first if both are MPdots *)
+(** we compare labels first if both are MPdots *)
 let rec mp_ord mp1 mp2 = match (mp1,mp2) with
     MPdot(mp1,l1), MPdot(mp2,l2) ->
       let c = Pervasives.compare l1 l2 in
@@ -133,7 +145,12 @@ end
 module MPset = Set.Make(MPord)
 module MPmap = Map.Make(MPord)
 
-(* Kernel names *)
+let default_module_name = "If you see this, it's a bug"
+
+let initial_dir = make_dirpath [default_module_name]
+let initial_path = MPfile initial_dir
+
+(** {6 Kernel names } *)
 
 type kernel_name = module_path * dir_path * label
 
@@ -147,11 +164,12 @@ let label kn =
   let _,_,l = repr_kn kn in l
 
 let string_of_kn (mp,dir,l) =
-  string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l
+  let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#"
+  in
+  string_of_mp mp ^ str_dir ^ string_of_label l
 
 let pr_kn kn = str (string_of_kn kn)
 
-
 let kn_ord kn1 kn2 =
     let mp1,dir1,l1 = kn1 in
     let mp2,dir2,l2 = kn2 in
@@ -165,100 +183,104 @@ let kn_ord kn1 kn2 =
 	  else
 	    MPord.compare mp1 mp2
 
-(* a constant name is a kernel name couple (kn1,kn2) 
+module KNord = struct
+  type t = kernel_name
+  let compare = kn_ord
+end
+
+module KNmap = Map.Make(KNord)
+module KNpred = Predicate.Make(KNord)
+module KNset = Set.Make(KNord)
+
+(** {6 Constant names } *)
+
+(** a constant name is a kernel name couple (kn1,kn2)
    where kn1 corresponds to the name used at toplevel
-   (i.e. what the user see) 
-   and kn2 corresponds to the canonical kernel name 
-   i.e. in the environment we have 
+   (i.e. what the user see)
+   and kn2 corresponds to the canonical kernel name
+   i.e. in the environment we have
    kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *)
 type constant = kernel_name*kernel_name
 
-(* For the environment we distinguish constants by their 
-   user part*)
+let constant_of_kn kn = (kn,kn)
+let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
+let make_con mp dir l = constant_of_kn (mp,dir,l)
+let make_con_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_con mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
+let canonical_con con = snd con
+let user_con con = fst con
+let repr_con con = fst con
+
+let eq_constant (_,kn1) (_,kn2) = kn1=kn2
+
+let con_label con = label (fst con)
+let con_modpath con = modpath (fst con)
+
+let string_of_con con = string_of_kn (fst con)
+let pr_con con = str (string_of_con con)
+let debug_string_of_con con =
+  "(" ^ string_of_kn (fst con) ^ "," ^ string_of_kn (snd con) ^ ")"
+let debug_pr_con con = str (debug_string_of_con con)
+
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+  if lbl = l1 && lbl = l2 then con
+  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
+(** For the environment we distinguish constants by their user part*)
 module User_ord = struct
   type t = kernel_name*kernel_name
   let compare x y= kn_ord (fst x) (fst y)
 end
 
-(* For other uses (ex: non-logical things) it is enough
-   to deal with the canonical part *)
+(** For other uses (ex: non-logical things) it is enough
+    to deal with the canonical part *)
 module Canonical_ord = struct
   type t = kernel_name*kernel_name
   let compare x y= kn_ord (snd x) (snd y)
 end
 
-
-module KNord = struct
-  type t = kernel_name
-  let compare =kn_ord
-end
-
-module KNmap = Map.Make(KNord)
-module KNpred = Predicate.Make(KNord)
-module KNset = Set.Make(KNord)
-
 module Cmap = Map.Make(Canonical_ord)
 module Cmap_env = Map.Make(User_ord)
 module Cpred = Predicate.Make(Canonical_ord)
 module Cset = Set.Make(Canonical_ord)
 module Cset_env = Set.Make(User_ord)
 
-module Mindmap = Map.Make(Canonical_ord)
-module Mindset = Set.Make(Canonical_ord)
-module Mindmap_env = Map.Make(User_ord)
-
-let default_module_name = "If you see this, it's a bug"
 
-let initial_dir = make_dirpath [default_module_name]
-let initial_path = MPfile initial_dir
+(** {6 Names of mutual inductive types } *)
 
-type variable = identifier
+(** The same thing is done for mutual inductive names
+    it replaces also the old mind_equiv field of mutual
+    inductive types *)
+(** Beware: first inductive has index 0 *)
+(** Beware: first constructor has index 1 *)
 
-(* The same thing is done for mutual inductive names 
-   it replaces also the old mind_equiv field of mutual 
-   inductive types*)
 type mutual_inductive = kernel_name*kernel_name
 type inductive = mutual_inductive * int
 type constructor = inductive * int
 
-let constant_of_kn kn = (kn,kn)
-let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = constant_of_kn (mp,dir,l)
-let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
-let canonical_con con = snd con
-let user_con con = fst con
-let repr_con con = fst con
-let string_of_con con = string_of_kn (fst con)
-let con_label con = label (fst con)
-let pr_con con = pr_kn (fst con)
-let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ str ")"
-let eq_constant (_,kn1) (_,kn2) = kn1=kn2
-let debug_string_of_con con =  string_of_kn (fst con)^"'"^string_of_kn (snd con)
-
-let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
-  if lbl = l1 && lbl = l2 then con
-  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
-
-let con_modpath con = modpath (fst con)
-
 let mind_modpath mind = modpath (fst mind)
 let ind_modpath ind = mind_modpath (fst ind)
 let constr_modpath c = ind_modpath (fst c)
 
-
 let mind_of_kn kn = (kn,kn)
 let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
-let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_mind mp dir l = mind_of_kn (mp,dir,l)
+let make_mind_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_mind mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
 let canonical_mind mind = snd mind
 let user_mind mind = fst mind
 let repr_mind mind = fst mind
-let string_of_mind mind = string_of_kn (fst mind)
 let mind_label mind= label (fst mind)
-let pr_mind mind = pr_kn (fst mind)
-let debug_pr_mind mind = str "("++ pr_kn (fst mind) ++ str ","++ pr_kn (snd mind)++ str ")"
+
 let eq_mind (_,kn1) (_,kn2) = kn1=kn2
-let debug_string_of_mind mind =  string_of_kn (fst mind)^"'"^string_of_kn (snd mind)
+
+let string_of_mind mind = string_of_kn (fst mind)
+let pr_mind mind = str (string_of_mind mind)
+let debug_string_of_mind mind =
+  "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")"
+let debug_pr_mind con = str (debug_string_of_mind con)
 
 let ith_mutual_inductive (kn,_) i = (kn,i)
 let ith_constructor_of_inductive ind i = (ind,i)
@@ -267,6 +289,10 @@ let index_of_constructor (ind,i) = i
 let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2
 let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2
 
+module Mindmap = Map.Make(Canonical_ord)
+module Mindset = Set.Make(Canonical_ord)
+module Mindmap_env = Map.Make(User_ord)
+
 module InductiveOrdered = struct
   type t = inductive
   let compare (spx,ix) (spy,iy) =
@@ -306,7 +332,8 @@ let eq_egr e1 e2 = match e1,e2 with
     EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
   | _,_ -> e1 = e2
 
-(* Hash-consing of name objects *)
+(** {6 Hash-consing of name objects } *)
+
 module Hname = Hashcons.Make(
   struct
     type t = name
@@ -326,7 +353,7 @@ module Hdir = Hashcons.Make(
   struct
     type t = dir_path
     type u = identifier -> identifier
-    let hash_sub hident d = List.map hident d
+    let hash_sub hident d = list_smartmap hident d
     let rec equal d1 d2 = match (d1,d2) with
       | [],[] -> true
       | id1::d1,id2::d2 -> id1 == id2 & equal d1 d2
@@ -337,9 +364,9 @@ module Hdir = Hashcons.Make(
 module Huniqid = Hashcons.Make(
   struct
     type t = uniq_ident
-    type u = (string -> string) * (dir_path -> dir_path)
-    let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir)
-    let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 & s1 = s2 & dir1 == dir2
+    type u = (identifier -> identifier) * (dir_path -> dir_path)
+    let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+    let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2
     let hash = Hashtbl.hash
   end)
 
@@ -355,34 +382,66 @@ module Hmod = Hashcons.Make(
     let rec equal d1 d2 = match (d1,d2) with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
       | MPbound m1, MPbound m2 -> m1 == m2
-      | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2
+      | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2
       | _ -> false
     let hash = Hashtbl.hash
   end)
 
-
-module Hcn = Hashcons.Make(
-  struct 
-    type t = kernel_name*kernel_name
+module Hkn = Hashcons.Make(
+  struct
+    type t = kernel_name
     type u = (module_path -> module_path)
 	* (dir_path -> dir_path) * (string -> string)
-    let hash_sub (hmod,hdir,hstr) ((md,dir,l),(mde,dire,le)) = 
-      ((hmod md, hdir dir, hstr l),(hmod mde, hdir dire, hstr le))
-    let equal ((mod1,dir1,l1),_) ((mod2,dir2,l2),_) =
+    let hash_sub (hmod,hdir,hstr) (md,dir,l) =
+      (hmod md, hdir dir, hstr l)
+    let equal (mod1,dir1,l1) (mod2,dir2,l2) =
       mod1 == mod2 && dir1 == dir2 && l1 == l2
     let hash = Hashtbl.hash
   end)
 
-let hcons_names () =
-  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
-  let hident = Hashcons.simple_hcons Hident.f hstring in
-  let hname = Hashcons.simple_hcons Hname.f hident in
-  let hdir = Hashcons.simple_hcons Hdir.f hident in
-  let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
-  let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
-  let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
-  let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
-  (hcn,hmind,hdir,hname,hident,hstring)
+(** For [constant] and [mutual_inductive], we discriminate only on
+    the user part : having the same user part implies having the
+    same canonical part (invariant of the system). *)
+
+module Hcn = Hashcons.Make(
+  struct
+    type t = kernel_name*kernel_name
+    type u = kernel_name -> kernel_name
+    let hash_sub hkn (user,can) = (hkn user, hkn can)
+    let equal (user1,_) (user2,_) = user1 == user2
+    let hash (user,_) = Hashtbl.hash user
+  end)
+
+module Hind = Hashcons.Make(
+  struct
+    type t = inductive
+    type u = mutual_inductive -> mutual_inductive
+    let hash_sub hmind (mind, i) = (hmind mind, i)
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
+    let hash = Hashtbl.hash
+  end)
+
+module Hconstruct = Hashcons.Make(
+  struct
+    type t = constructor
+    type u = inductive -> inductive
+    let hash_sub hind (ind, j) = (hind ind, j)
+    let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
+    let hash = Hashtbl.hash
+  end)
+
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f ()
+let hcons_ident = hcons_string
+let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident
+let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident
+let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath)
+let hcons_mp =
+  Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string)
+let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string)
+let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind
 
 
 (*******)