Ajout hashconsing univers

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

4 files changed, 44 insertions, 3 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 1f68c1a359..075b3dbad5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1733,11 +1733,27 @@ module Htype =
       let hash = Hashtbl.hash
     end)
 
-let hsort _ _ s = s
+module Hsorts =
+  Hashcons.Make(
+    struct
+      type t = sorts
+      type u = universe -> universe
+      let hash_sub huniv = function
+          Prop c -> Prop c
+        | Type u -> Type (huniv u)
+      let equal s1 s2 =
+        match (s1,s2) with
+            (Prop c1, Prop c2) -> c1=c2
+          | (Type u1, Type u2) -> u1 == u2
+          |_ -> false
+      let hash = Hashtbl.hash
+    end)
+
+let hsort = Hsorts.f
 
 let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
-  let hsortscci = Hashcons.simple_hcons hsort hspcci in
-  let hsortsfw = Hashcons.simple_hcons hsort hspfw in
+  let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
+  let hsortsfw = Hashcons.simple_hcons hsort hcons1_univ in
   let hcci = hcons_term (hsortscci,hspcci,hname,hident) in
   let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
@@ -1748,6 +1764,11 @@ let hcons1_constr =
   let (hc,_,_) = hcons_constr hnames in
   hc
 
+let hcons1_types =
+  let hnames = hcons_names () in
+  let (_,_,ht) = hcons_constr hnames in
+  ht
+
 (* Abstract decomposition of constr to deal with generic functions *)
 
 type fix_kind = RFix of (int array * int) | RCoFix of int
diff --git a/kernel/term.mli b/kernel/term.mli
index fd2eba41ae..2d65491c44 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -680,3 +680,4 @@ val hcons_constr:
     (types -> types)
 
 val hcons1_constr : constr -> constr
+val hcons1_types : types -> types
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 49b2f60728..7c3060820a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -426,3 +426,20 @@ let dump_universes output g =
   in
     UniverseMap.iter dump_arc g 
 
+module Huniv =
+  Hashcons.Make(
+    struct
+      type t = universe
+      type u = string -> string
+      let hash_sub hstr {u_mod=sp; u_num=n} = 
+	{u_mod=List.map hstr sp; u_num=n}
+      let equal {u_mod=sp1; u_num=n1} {u_mod=sp2; u_num=n2} =
+          (List.length sp1 = List.length sp2)
+              & List.for_all2 (==) sp1 sp2 & n1=n2
+      let hash = Hashtbl.hash
+    end)
+
+
+let hcons1_univ u =
+  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
+  Hashcons.simple_hcons Huniv.f hstring u
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 9c717ec31e..0c405084de 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -71,3 +71,5 @@ val string_of_univ : universe -> string
 (*s Dumping to a file *)
 
 val dump_universes : out_channel -> universes -> unit
+
+val hcons1_univ : universe -> universe