Imported Upstream version 8.5~beta1+dfsg

1 files changed, 719 insertions, 338 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c20f75a9..b349ccb0 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,35 +23,106 @@ open Util
 
 (** {6 Identifiers } *)
 
-type identifier = string
+module Id =
+struct
+  type t = string
+
+  let equal = String.equal
+
+  let compare = String.compare
+
+  let hash = String.hash
+
+  let check_soft x =
+    let iter (fatal, x) =
+      if fatal then Errors.error x else Pp.msg_warning (str x)
+    in
+    Option.iter iter (Unicode.ident_refutation x)
 
-let id_of_string s = check_ident_soft s; String.copy s
-let string_of_id id = String.copy id
+  let is_valid s = match Unicode.ident_refutation s with
+  | None -> true
+  | Some _ -> false
 
-let id_ord = Pervasives.compare
+  let of_string s =
+    let () = check_soft s in
+    let s = String.copy s in
+    String.hcons s
 
-module IdOrdered =
+  let to_string id = String.copy id
+
+  let print id = str id
+
+  module Self =
   struct
-    type t = identifier
-    let compare = id_ord
+    type t = string
+    let compare = compare
   end
 
-module Idset = Set.Make(IdOrdered)
-module Idmap =
+  module Set = Set.Make(Self)
+  module Map = CMap.Make(Self)
+
+  module Pred = Predicate.Make(Self)
+
+  module List = String.List
+
+  let hcons = String.hcons
+
+end
+
+
+module Name =
 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
+  type t = Name of Id.t | Anonymous
+
+  let compare n1 n2 = match n1, n2 with
+    | Anonymous, Anonymous -> 0
+    | Name id1, Name id2 -> Id.compare id1 id2
+    | Anonymous, Name _ -> -1
+    | Name _, Anonymous -> 1
+
+  let equal n1 n2 = match n1, n2 with
+    | Anonymous, Anonymous -> true
+    | Name id1, Name id2 -> String.equal id1 id2
+    | _ -> false
+
+  let hash = function
+  | Anonymous -> 0
+  | Name id -> Id.hash id
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = Id.t -> Id.t
+      let hashcons hident = function
+        | Name id -> Name (hident id)
+        | n -> n
+      let equal n1 n2 =
+        n1 == n2 ||
+        match (n1,n2) with
+          | (Name id1, Name id2) -> id1 == id2
+          | (Anonymous,Anonymous) -> true
+          | _ -> false
+      let hash = hash
+    end
+
+  module Hname = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons Hname.generate Hname.hcons Id.hcons
+
 end
-module Idpred = Predicate.Make(IdOrdered)
+
+type name = Name.t = Name of Id.t | Anonymous
+(** Alias, to import constructors. *)
 
 (** {6 Various types based on identifiers } *)
 
-type name = Name of identifier | Anonymous
-type variable = identifier
+type variable = Id.t
+
+type module_ident = Id.t
+
+module ModIdset = Id.Set
+module ModIdmap = Id.Map
 
 (** {6 Directory paths = section names paths } *)
 
@@ -59,250 +130,491 @@ type variable = identifier
     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
+let default_module_name = "If you see this, it's a bug"
+
+module DirPath =
+struct
+  type t = module_ident list
+
+  let rec compare (p1 : t) (p2 : t) =
+    if p1 == p2 then 0
+    else begin match p1, p2 with
+    | [], [] -> 0
+    | [], _ -> -1
+    | _, [] -> 1
+    | id1 :: p1, id2 :: p2 ->
+      let c = Id.compare id1 id2 in
+      if Int.equal c 0 then compare p1 p2 else c
+    end
+
+  let rec equal p1 p2 = p1 == p2 || match p1, p2 with
+  | [], [] -> true
+  | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2
+  | _ -> false
+
+  let rec hash accu = function
+  | [] -> accu
+  | id :: dp ->
+    let accu = Hashset.Combine.combine (Id.hash id) accu in
+    hash accu dp
+
+  let hash dp = hash 0 dp
+
+  let make x = x
+  let repr x = x
+
+  let empty = []
 
-module ModIdmap = Idmap
+  let is_empty d = match d with [] -> true | _ -> false
 
-let make_dirpath x = x
-let repr_dirpath x = x
+  let to_string = function
+    | [] -> "<>"
+    | sl -> String.concat "." (List.rev_map Id.to_string sl)
 
-let empty_dirpath = []
+  let initial = [default_module_name]
 
-(** Printing of directory paths as ["coq_root.module.submodule"] *)
+  module Hdir = Hashcons.Hlist(Id)
 
-let string_of_dirpath = function
-  | [] -> "<>"
-  | sl -> String.concat "." (List.map string_of_id (List.rev sl))
+  let hcons = Hashcons.recursive_hcons Hdir.generate Hdir.hcons Id.hcons
+
+end
 
 (** {6 Unique names for bound modules } *)
 
-let u_number = ref 0
-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) =
-  string_of_dirpath p ^"."^s
-
-module Umap = Map.Make(struct
-			 type t = uniq_ident
-			 let compare = Pervasives.compare
-		       end)
-
-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
+module MBId =
+struct
+  type t = int * Id.t * DirPath.t
 
-(** {6 Names of structure elements } *)
+  let gen =
+    let seed = ref 0 in fun () ->
+      let ans = !seed in
+      let () = incr seed in
+      ans
 
-type label = identifier
+  let make dir s = (gen(), s, dir)
 
-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
+  let repr mbid = mbid
 
-module Labset = Idset
-module Labmap = Idmap
+  let to_string (i, s, p) =
+    DirPath.to_string p ^ "." ^ s
 
-(** {6 The module part of the kernel name } *)
+  let debug_to_string (i, s, p) =
+    "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
+
+  let compare (x : t) (y : t) =
+    if x == y then 0
+    else match (x, y) with
+    | (nl, idl, dpl), (nr, idr, dpr) ->
+      let ans = Int.compare nl nr in
+      if not (Int.equal ans 0) then ans
+      else
+        let ans = Id.compare idl idr in
+        if not (Int.equal ans 0) then ans
+        else
+          DirPath.compare dpl dpr
 
-type module_path =
-  | MPfile of dir_path
-  | MPbound of mod_bound_id
-  | MPdot of module_path * label
+  let equal x y = x == y ||
+    let (i1, id1, p1) = x in
+    let (i2, id2, p2) = y in
+    Int.equal i1 i2 && Id.equal id1 id2 && DirPath.equal p1 p2
 
-let rec check_bound_mp = function
-  | MPbound _ -> true
-  | MPdot(mp,_) ->check_bound_mp mp
-  | _ -> false
+  let to_id (_, s, _) = s
+
+  open Hashset.Combine
+
+  let hash (i, id, dp) =
+    combine3 (Int.hash i) (Id.hash id) (DirPath.hash dp)
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t)
+      let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+      let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+        (x == y) ||
+        (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
+      let hash = hash
+    end
+
+  module HashMBId = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons HashMBId.generate HashMBId.hcons (Id.hcons, DirPath.hcons)
 
-let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
-  | MPbound uid -> string_of_uid uid
-  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
-
-(** 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
-	if c<>0 then
-	  c
-	else
-	  mp_ord mp1 mp2
-  |  _,_ -> Pervasives.compare mp1 mp2
-
-module MPord = struct
-  type t = module_path
-  let compare = mp_ord
 end
 
-module MPset = Set.Make(MPord)
-module MPmap = Map.Make(MPord)
+module MBImap = CMap.Make(MBId)
+module MBIset = Set.Make(MBId)
 
-let default_module_name = "If you see this, it's a bug"
+(** {6 Names of structure elements } *)
+
+module Label =
+struct
+  include Id
+  let make = Id.of_string
+  let of_id id = id
+  let to_id id = id
+end
+
+(** {6 The module part of the kernel name } *)
+
+module ModPath = struct
+
+  type t =
+    | MPfile of DirPath.t
+    | MPbound of MBId.t
+    | MPdot of t * Label.t
+
+  type module_path = t
+
+  let rec is_bound = function
+    | MPbound _ -> true
+    | MPdot(mp,_) -> is_bound mp
+    | _ -> false
+
+  let rec to_string = function
+    | MPfile sl -> DirPath.to_string sl
+    | MPbound uid -> MBId.to_string uid
+    | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l
+
+  (** we compare labels first if both are MPdots *)
+  let rec compare mp1 mp2 =
+    if mp1 == mp2 then 0
+    else match mp1, mp2 with
+      | MPfile p1, MPfile p2 -> DirPath.compare p1 p2
+      | MPbound id1, MPbound id2 -> MBId.compare id1 id2
+      | MPdot (mp1, l1), MPdot (mp2, l2) ->
+        let c = String.compare l1 l2 in
+        if not (Int.equal c 0) then c
+        else compare mp1 mp2
+      | MPfile _, _ -> -1
+      | MPbound _, MPfile _ -> 1
+      | MPbound _, MPdot _ -> -1
+      | MPdot _, _ -> 1
+
+  let rec equal mp1 mp2 = mp1 == mp2 ||
+    match mp1, mp2 with
+    | MPfile p1, MPfile p2 -> DirPath.equal p1 p2
+    | MPbound id1, MPbound id2 -> MBId.equal id1 id2
+    | MPdot (mp1, l1), MPdot (mp2, l2) -> String.equal l1 l2 && equal mp1 mp2
+    | (MPfile _ | MPbound _ | MPdot _), _ -> false
+
+  open Hashset.Combine
+
+  let rec hash = function
+  | MPfile dp -> combinesmall 1 (DirPath.hash dp)
+  | MPbound id -> combinesmall 2 (MBId.hash id)
+  | MPdot (mp, lbl) ->
+    combinesmall 3 (combine (hash mp) (Label.hash lbl))
+
+  let initial = MPfile DirPath.initial
+
+  let rec dp = function
+  | MPfile sl -> sl
+  | MPbound (_,_,dp) -> dp
+  | MPdot (mp,l) -> dp mp
+
+  module Self_Hashcons = struct
+    type t = module_path
+    type u = (DirPath.t -> DirPath.t) * (MBId.t -> MBId.t) *
+	(string -> string)
+    let rec hashcons (hdir,huniqid,hstr as hfuns) = function
+      | MPfile dir -> MPfile (hdir dir)
+      | MPbound m -> MPbound (huniqid m)
+      | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
+    let rec equal d1 d2 =
+      d1 == d2 ||
+      match d1,d2 with
+      | MPfile dir1, MPfile dir2 -> dir1 == dir2
+      | MPbound m1, MPbound m2 -> m1 == m2
+      | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2
+      | _ -> false
+    let hash = hash
+  end
+
+  module HashMP = Hashcons.Make(Self_Hashcons)
+
+  let hcons =
+    Hashcons.simple_hcons HashMP.generate HashMP.hcons
+      (DirPath.hcons,MBId.hcons,String.hcons)
+
+end
 
-let initial_dir = make_dirpath [default_module_name]
-let initial_path = MPfile initial_dir
+module MPset = Set.Make(ModPath)
+module MPmap = CMap.Make(ModPath)
 
 (** {6 Kernel names } *)
 
-type kernel_name = module_path * dir_path * label
+module KerName = struct
 
-let make_kn mp dir l = (mp,dir,l)
-let repr_kn kn = kn
+  type t = {
+    canary : Canary.t;
+    modpath : ModPath.t;
+    dirpath : DirPath.t;
+    knlabel : Label.t;
+    mutable refhash : int;
+    (** Lazily computed hash. If unset, it is set to negative values. *)
+  }
 
-let modpath kn =
-  let mp,_,_ = repr_kn kn in mp
+  let canary = Canary.obj
 
-let label kn =
-  let _,_,l = repr_kn kn in l
+  type kernel_name = t
 
-let string_of_kn (mp,dir,l) =
-  let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#"
-  in
-  string_of_mp mp ^ str_dir ^ string_of_label l
+  let make modpath dirpath knlabel =
+    { modpath; dirpath; knlabel; refhash = -1; canary; }
+  let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
 
-let pr_kn kn = str (string_of_kn kn)
+  let make2 modpath knlabel =
+    { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; }
 
-let kn_ord kn1 kn2 =
-    let mp1,dir1,l1 = kn1 in
-    let mp2,dir2,l2 = kn2 in
-    let c = Pervasives.compare l1 l2 in
-      if c <> 0 then
-	c
+  let modpath kn = kn.modpath
+  let label kn = kn.knlabel
+
+  let to_string kn =
+    let dp =
+      if DirPath.is_empty kn.dirpath then "."
+      else "#" ^ DirPath.to_string kn.dirpath ^ "#"
+    in
+    ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+
+  let print kn = str (to_string kn)
+
+  let compare (kn1 : kernel_name) (kn2 : kernel_name) =
+    if kn1 == kn2 then 0
+    else
+      let c = String.compare kn1.knlabel kn2.knlabel in
+      if not (Int.equal c 0) then c
       else
-	let c = Pervasives.compare dir1 dir2 in
-	  if c<>0 then
-	    c
-	  else
-	    MPord.compare mp1 mp2
-
-module KNord = struct
-  type t = kernel_name
-  let compare = kn_ord
-end
+        let c = DirPath.compare kn1.dirpath kn2.dirpath in
+        if not (Int.equal c 0) then c
+        else ModPath.compare kn1.modpath kn2.modpath
+
+  let equal kn1 kn2 =
+    let h1 = kn1.refhash in
+    let h2 = kn2.refhash in
+    if 0 <= h1 && 0 <= h2 && not (Int.equal h1 h2) then false
+    else
+      Label.equal kn1.knlabel kn2.knlabel &&
+      DirPath.equal kn1.dirpath kn2.dirpath &&
+      ModPath.equal kn1.modpath kn2.modpath
+
+  open Hashset.Combine
+
+  let hash kn =
+    let h = kn.refhash in
+    if h < 0 then
+      let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in
+      let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in
+      (* Ensure positivity on all platforms. *)
+      let h = h land 0x3FFFFFFF in
+      let () = kn.refhash <- h in
+      h
+    else h
+
+  module Self_Hashcons = struct
+    type t = kernel_name
+    type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
+        * (string -> string)
+    let hashcons (hmod,hdir,hstr) kn =
+      let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
+      { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
+    let equal kn1 kn2 =
+      kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
+        kn1.knlabel == kn2.knlabel
+    let hash = hash
+  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
-   kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *)
-type constant = kernel_name*kernel_name
-
-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)
+  module HashKN = Hashcons.Make(Self_Hashcons)
+
+  let hcons =
+    Hashcons.simple_hcons HashKN.generate HashKN.hcons
+      (ModPath.hcons,DirPath.hcons,String.hcons)
 end
 
-(** 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)
+module KNmap = HMap.Make(KerName)
+module KNpred = Predicate.Make(KerName)
+module KNset = KNmap.Set
+
+(** {6 Kernel pairs } *)
+
+(** For constant and inductive names, we use 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 {% kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t %}
+
+   Invariants :
+    - the user and canonical kn may differ only on their [module_path],
+      the dirpaths and labels should be the same
+    - when user and canonical parts differ, we cannot be in a section
+      anymore, hence the dirpath must be empty
+    - two pairs with the same user part should have the same canonical part
+
+   Note: since most of the time the canonical and user parts are equal,
+   we handle this case with a particular constructor to spare some memory *)
+
+module KerPair = struct
+
+  type t =
+    | Same of KerName.t (** user = canonical *)
+    | Dual of KerName.t * KerName.t (** user then canonical *)
+
+  type kernel_pair = t
+
+  let canonical = function
+    | Same kn -> kn
+    | Dual (_,kn) -> kn
+
+  let user = function
+    | Same kn -> kn
+    | Dual (kn,_) -> kn
+
+  let same kn = Same kn
+  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
+
+  let make1 = same
+  let make2 mp l = same (KerName.make2 mp l)
+  let make3 mp dir l = same (KerName.make mp dir l)
+  let repr3 kp = KerName.repr (user kp)
+  let label kp = KerName.label (user kp)
+  let modpath kp = KerName.modpath (user kp)
+
+  let change_label kp lbl =
+    let (mp1,dp1,l1) = KerName.repr (user kp)
+    and (mp2,dp2,l2) = KerName.repr (canonical kp) in
+    assert (String.equal l1 l2 && DirPath.equal dp1 dp2);
+    if String.equal lbl l1 then kp
+    else
+      let kn = KerName.make mp1 dp1 lbl in
+      if mp1 == mp2 then same kn
+      else make kn (KerName.make mp2 dp2 lbl)
+
+  let to_string kp = KerName.to_string (user kp)
+  let print kp = str (to_string kp)
+
+  let debug_to_string = function
+    | Same kn -> "(" ^ KerName.to_string kn ^ ")"
+    | Dual (knu,knc) ->
+      "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")"
+
+  let debug_print kp = str (debug_to_string kp)
+
+  (** For ordering kernel pairs, both user or canonical parts may make
+      sense, according to your needs : user for the environments, canonical
+      for other uses (ex: non-logical things). *)
+
+  module UserOrd = struct
+    type t = kernel_pair
+    let compare x y = KerName.compare (user x) (user y)
+    let equal x y = x == y || KerName.equal (user x) (user y)
+    let hash x = KerName.hash (user x)
+  end
+
+  module CanOrd = struct
+    type t = kernel_pair
+    let compare x y = KerName.compare (canonical x) (canonical y)
+    let equal x y = x == y || KerName.equal (canonical x) (canonical y)
+    let hash x = KerName.hash (canonical x)
+  end
+
+  (** Default comparison is on the canonical part *)
+  let equal = CanOrd.equal
+
+  (** Hash-consing : we discriminate only on the user part, since having
+      the same user part implies having the same canonical part
+      (invariant of the system). *)
+
+  let hash = function
+  | Same kn -> KerName.hash kn
+  | Dual (kn, _) -> KerName.hash kn
+
+  module Self_Hashcons =
+    struct
+      type t = kernel_pair
+      type u = KerName.t -> KerName.t
+      let hashcons hkn = function
+        | Same kn -> Same (hkn kn)
+        | Dual (knu,knc) -> make (hkn knu) (hkn knc)
+      let equal x y = (user x) == (user y)
+      let hash = hash
+    end
+
+  module HashKP = Hashcons.Make(Self_Hashcons)
+
 end
 
-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)
+(** {6 Constant Names} *)
+
+module Constant = KerPair
 
+module Cmap = HMap.Make(Constant.CanOrd)
+module Cmap_env = HMap.Make(Constant.UserOrd)
+module Cpred = Predicate.Make(Constant.CanOrd)
+module Cset = Cmap.Set
+module Cset_env = Cmap_env.Set
 
 (** {6 Names of mutual inductive types } *)
 
-(** The same thing is done for mutual inductive names
-    it replaces also the old mind_equiv field of mutual
-    inductive types *)
+module MutInd = KerPair
+
+module Mindmap = HMap.Make(MutInd.CanOrd)
+module Mindset = Mindmap.Set
+module Mindmap_env = HMap.Make(MutInd.UserOrd)
+
 (** Beware: first inductive has index 0 *)
 (** Beware: first constructor has index 1 *)
 
-type mutual_inductive = kernel_name*kernel_name
-type inductive = mutual_inductive * int
+type inductive = MutInd.t * int
 type constructor = inductive * int
 
-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 = 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 mind_label mind= label (fst mind)
-
-let eq_mind (_,kn1) (_,kn2) = kn1=kn2
-
-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)
-let inductive_of_constructor (ind,i) = ind
-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)
+let ind_modpath (mind,_) = MutInd.modpath mind
+let constr_modpath (ind,_) = ind_modpath ind
+
+let ith_mutual_inductive (mind, _) i = (mind, i)
+let ith_constructor_of_inductive ind i = (ind, i)
+let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u)
+let inductive_of_constructor (ind, i) = ind
+let index_of_constructor (ind, i) = i
+
+let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
+let eq_user_ind (m1, i1) (m2, i2) =
+  Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
+
+let ind_ord (m1, i1) (m2, i2) =
+  let c = Int.compare i1 i2 in
+  if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c
+let ind_user_ord (m1, i1) (m2, i2) =
+  let c = Int.compare i1 i2 in
+  if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
+
+let ind_hash (m, i) =
+  Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
+let ind_user_hash (m, i) =
+  Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
+
+let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
+let eq_user_constructor (ind1, j1) (ind2, j2) =
+  Int.equal j1 j2 && eq_user_ind ind1 ind2
+
+let constructor_ord (ind1, j1) (ind2, j2) =
+  let c = Int.compare j1 j2 in
+  if Int.equal c 0 then ind_ord ind1 ind2 else c
+let constructor_user_ord (ind1, j1) (ind2, j2) =
+  let c = Int.compare j1 j2 in
+  if Int.equal c 0 then ind_user_ord ind1 ind2 else c
+
+let constructor_hash (ind, i) =
+  Hashset.Combine.combine (ind_hash ind) (Int.hash i)
+let constructor_user_hash (ind, i) =
+  Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
 
 module InductiveOrdered = struct
   type t = inductive
-  let compare (spx,ix) (spy,iy) =
-    let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c
+  let compare = ind_ord
 end
 
 module InductiveOrdered_env = struct
   type t = inductive
-  let compare (spx,ix) (spy,iy) =
-    let c = ix - iy in if c = 0 then User_ord.compare spx spy else c
+  let compare = ind_user_ord
 end
 
 module Indmap = Map.Make(InductiveOrdered)
@@ -310,14 +622,12 @@ module Indmap_env = Map.Make(InductiveOrdered_env)
 
 module ConstructorOrdered = struct
   type t = constructor
-  let compare (indx,ix) (indy,iy) =
-    let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c
+  let compare = constructor_ord
 end
 
 module ConstructorOrdered_env = struct
   type t = constructor
-  let compare (indx,ix) (indy,iy) =
-    let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c
+  let compare = constructor_user_ord
 end
 
 module Constrmap = Map.Make(ConstructorOrdered)
@@ -325,152 +635,223 @@ module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
 (* Better to have it here that in closure, since used in grammar.cma *)
 type evaluable_global_reference =
-  | EvalVarRef of identifier
-  | EvalConstRef of constant
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
 
-let eq_egr e1 e2 = match e1,e2 with
-    EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
-  | _,_ -> e1 = e2
+let eq_egr e1 e2 = match e1, e2 with
+    EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
+  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
+  | _, _ -> false
 
 (** {6 Hash-consing of name objects } *)
 
-module Hname = Hashcons.Make(
-  struct
-    type t = name
-    type u = identifier -> identifier
-    let hash_sub hident = function
-      | Name id -> Name (hident id)
-      | n -> n
-    let equal n1 n2 =
-      match (n1,n2) with
-	| (Name id1, Name id2) -> id1 == id2
-        | (Anonymous,Anonymous) -> true
-        | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
-module Hdir = Hashcons.Make(
-  struct
-    type t = dir_path
-    type u = identifier -> identifier
-    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
-      | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
-module Huniqid = Hashcons.Make(
-  struct
-    type t = uniq_ident
-    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)
-
-module Hmod = Hashcons.Make(
-  struct
-    type t = module_path
-    type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
-	(string -> string)
-    let rec hash_sub (hdir,huniqid,hstr as hfuns) = function
-      | MPfile dir -> MPfile (hdir dir)
-      | MPbound m -> MPbound (huniqid m)
-      | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l)
-    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) -> l1 == l2 && equal mod1 mod2
-      | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
-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) =
-      (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)
-
-(** 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
+    type u = MutInd.t -> MutInd.t
+    let hashcons hmind (mind, i) = (hmind mind, i)
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+    let hash = ind_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
+    let hashcons hind (ind, j) = (hind ind, j)
+    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+    let hash = constructor_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
-
+let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate Constant.HashKP.hcons KerName.hcons
+let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate MutInd.HashKP.hcons KerName.hcons
+let hcons_ind = Hashcons.simple_hcons Hind.generate Hind.hcons hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons hcons_ind
 
-(*******)
+(*****************)
 
-type transparent_state = Idpred.t * Cpred.t
+type transparent_state = Id.Pred.t * Cpred.t
 
-let empty_transparent_state = (Idpred.empty, Cpred.empty)
-let full_transparent_state = (Idpred.full, Cpred.full)
-let var_full_transparent_state = (Idpred.full, Cpred.empty)
-let cst_full_transparent_state = (Idpred.empty, Cpred.full)
+let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
+let full_transparent_state = (Id.Pred.full, Cpred.full)
+let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
+let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
 
 type 'a tableKey =
-  | ConstKey of constant
-  | VarKey of identifier
-  | RelKey of 'a
-
+  | ConstKey of 'a
+  | VarKey of Id.t
+  | RelKey of Int.t
 
 type inv_rel_key = int (* index in the [rel_context] part of environment
 			  starting by the end, {\em inverse}
 			  of de Bruijn indice *)
 
-type id_key = inv_rel_key tableKey
+let eq_table_key f ik1 ik2 =
+  if ik1 == ik2 then true
+  else match ik1,ik2 with
+  | ConstKey c1, ConstKey c2 -> f c1 c2
+  | VarKey id1, VarKey id2 -> Id.equal id1 id2
+  | RelKey k1, RelKey k2 -> Int.equal k1 k2
+  | _ -> false
+
+let eq_con_chk = Constant.UserOrd.equal
+let eq_mind_chk = MutInd.UserOrd.equal
+let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
+
+
+(*******************************************************************)
+(** Compatibility layers *)
+
+(** Backward compatibility for [Id] *)
+
+type identifier = Id.t
+
+let id_eq = Id.equal
+let id_ord = Id.compare
+let string_of_id = Id.to_string
+let id_of_string = Id.of_string
+
+module Idset = Id.Set
+module Idmap = Id.Map
+module Idpred = Id.Pred
+
+(** Compatibility layer for [Name] *)
+
+let name_eq = Name.equal
 
-let eq_id_key ik1 ik2 =
-  match ik1,ik2 with
-    ConstKey (_,kn1),
-      ConstKey (_,kn2) -> kn1=kn2
-    | a,b -> a=b
+(** Compatibility layer for [DirPath] *)
+
+type dir_path = DirPath.t
+let dir_path_ord = DirPath.compare
+let dir_path_eq = DirPath.equal
+let make_dirpath = DirPath.make
+let repr_dirpath = DirPath.repr
+let empty_dirpath = DirPath.empty
+let is_empty_dirpath = DirPath.is_empty
+let string_of_dirpath = DirPath.to_string
+let initial_dir = DirPath.initial
+
+(** Compatibility layer for [MBId] *)
+
+type mod_bound_id = MBId.t
+let mod_bound_id_ord = MBId.compare
+let mod_bound_id_eq = MBId.equal
+let make_mbid = MBId.make
+let repr_mbid = MBId.repr
+let debug_string_of_mbid = MBId.debug_to_string
+let string_of_mbid = MBId.to_string
+let id_of_mbid = MBId.to_id
+
+(** Compatibility layer for [Label] *)
+
+type label = Id.t
+let mk_label = Label.make
+let string_of_label = Label.to_string
+let pr_label = Label.print
+let id_of_label = Label.to_id
+let label_of_id = Label.of_id
+let eq_label = Label.equal
+
+(** Compatibility layer for [ModPath] *)
+
+type module_path = ModPath.t =
+  | MPfile of DirPath.t
+  | MPbound of MBId.t
+  | MPdot of module_path * Label.t
+let check_bound_mp = ModPath.is_bound
+let string_of_mp = ModPath.to_string
+let mp_ord = ModPath.compare
+let mp_eq = ModPath.equal
+let initial_path = ModPath.initial
+
+(** Compatibility layer for [KerName] *)
+
+type kernel_name = KerName.t
+let make_kn = KerName.make
+let repr_kn = KerName.repr
+let modpath = KerName.modpath
+let label = KerName.label
+let string_of_kn = KerName.to_string
+let pr_kn = KerName.print
+let kn_ord = KerName.compare
+
+(** Compatibility layer for [Constant] *)
+
+type constant = Constant.t
+
+
+module Projection = 
+struct 
+  type t = constant * bool
+    
+  let make c b = (c, b)
+
+  let constant = fst
+  let unfolded = snd
+  let unfold (c, b as p) = if b then p else (c, true)
+  let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+
+  let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = Constant.t -> Constant.t
+      let hashcons hc (c,b) = (hc c,b)
+      let equal ((c,b) as x) ((c',b') as y) =
+        x == y || (c == c' && b == b')
+      let hash = hash
+    end
+
+  module HashProjection = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con
+
+  let compare (c, b) (c', b') =
+    if b == b' then Constant.CanOrd.compare c c'
+    else if b then 1 else -1
+
+  let map f (c, b as x) =
+    let c' = f c in
+      if c' == c then x else (c', b)
+end
 
-let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
-let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
-let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2
+type projection = Projection.t
+
+let constant_of_kn = Constant.make1
+let constant_of_kn_equiv = Constant.make
+let make_con = Constant.make3
+let repr_con = Constant.repr3
+let canonical_con = Constant.canonical
+let user_con = Constant.user
+let con_label = Constant.label
+let con_modpath = Constant.modpath
+let eq_constant = Constant.equal
+let eq_constant_key = Constant.UserOrd.equal
+let con_ord = Constant.CanOrd.compare
+let con_user_ord = Constant.UserOrd.compare
+let string_of_con = Constant.to_string
+let pr_con = Constant.print
+let debug_string_of_con = Constant.debug_to_string
+let debug_pr_con = Constant.debug_print
+let con_with_label = Constant.change_label
+
+(** Compatibility layer for [MutInd] *)
+
+type mutual_inductive = MutInd.t
+let mind_of_kn = MutInd.make1
+let mind_of_kn_equiv = MutInd.make
+let make_mind = MutInd.make3
+let canonical_mind = MutInd.canonical
+let user_mind = MutInd.user
+let repr_mind = MutInd.repr3
+let mind_label = MutInd.label
+let mind_modpath = MutInd.modpath
+let eq_mind = MutInd.equal
+let mind_ord = MutInd.CanOrd.compare
+let mind_user_ord = MutInd.UserOrd.compare
+let string_of_mind = MutInd.to_string
+let pr_mind = MutInd.print
+let debug_string_of_mind = MutInd.debug_to_string
+let debug_pr_mind = MutInd.debug_print