Specializing hash functions for widely used types.

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

11 files changed, 174 insertions, 46 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index a32be4f69..98fb467c8 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -213,7 +213,11 @@ module IdKeyHash =
 struct
   type t = id_key
   let equal = Names.eq_id_key
-  let hash = Hashtbl.hash
+  open Hashset.Combine
+  let hash = function
+  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | VarKey id -> combinesmall 2 (Id.hash id)
+  | RelKey i -> combinesmall 3 (Int.hash i)
 end
 
 module KeyTable = Hashtbl.Make(IdKeyHash)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index bd6326cf4..6a71b0cfc 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -542,6 +542,12 @@ let term_array_table = HashsetTermArray.create 4999
 
 open Hashset.Combine
 
+let hash_cast_kind = function
+| VMcast -> 0
+| NATIVEcast -> 1
+| DEFAULTcast -> 2
+| REVERTcast -> 3
+
 (* [hashcons hash_consing_functions constr] computes an hash-consed
    representation for [constr] using [hash_consing_functions] on
    leaves. *)
@@ -549,39 +555,39 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
   let rec hash_term t =
     match t with
       | Var i ->
-	(Var (sh_id i), combinesmall 1 (Hashtbl.hash i))
+	(Var (sh_id i), combinesmall 1 (Id.hash i))
       | Sort s ->
-	(Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s))
+	(Sort (sh_sort s), combinesmall 2 (Sorts.hash s))
       | Cast (c, k, t) ->
 	let c, hc = sh_rec c in
 	let t, ht = sh_rec t in
-	(Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht))
+	(Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht))
       | Prod (na,t,c) ->
 	let t, ht = sh_rec t
 	and c, hc = sh_rec c in
-	(Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc))
+	(Prod (sh_na na, t, c), combinesmall 4 (combine3 (Name.hash na) ht hc))
       | Lambda (na,t,c) ->
 	let t, ht = sh_rec t
 	and c, hc = sh_rec c in
-	(Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc))
+	(Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Name.hash na) ht hc))
       | LetIn (na,b,t,c) ->
 	let b, hb = sh_rec b in
 	let t, ht = sh_rec t in
 	let c, hc = sh_rec c in
-	(LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc))
+	(LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Name.hash na) hb ht hc))
       | App (c,l) ->
 	let c, hc = sh_rec c in
 	let l, hl = hash_term_array l in
 	(App (c,l), combinesmall 7 (combine hl hc))
       | Evar (e,l) ->
 	let l, hl = hash_term_array l in
-	(Evar (e,l), combinesmall 8 (combine (Hashtbl.hash e) hl))
+	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Const c ->
-	(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
-      | Ind ((kn,i) as ind) ->
-	(Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i))
-      | Construct (((kn,i),j) as c)->
-	(Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j))
+	(Const (sh_con c), combinesmall 9 (Constant.hash c))
+      | Ind ind ->
+	(Ind (sh_ind ind), combinesmall 10 (ind_hash ind))
+      | Construct c ->
+	(Construct (sh_construct c), combinesmall 11 (constructor_hash c))
       | Case (ci,p,c,bl) ->
 	let p, hp = sh_rec p
 	and c, hc = sh_rec c in
@@ -591,14 +597,18 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Fix (ln,(lna,tl,bl)) ->
 	let bl,hbl = hash_term_array bl in
 	let tl,htl = hash_term_array tl in
-	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
-        let h = combine3 (Hashtbl.hash lna) hbl htl in
+        let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
+        let fold accu na = combine (Name.hash na) accu in
+        let hna = Array.fold_left fold 0 lna in
+        let h = combine3 hna hbl htl in
 	(Fix (ln,(lna,tl,bl)), combinesmall 13 h)
       | CoFix(ln,(lna,tl,bl)) ->
 	let bl,hbl = hash_term_array bl in
 	let tl,htl = hash_term_array tl in
-	Array.iteri (fun i x -> lna.(i) <- sh_na x) lna;
-        let h = combine3 (Hashtbl.hash lna) hbl htl in
+        let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
+        let fold accu na = combine (Name.hash na) accu in
+        let hna = Array.fold_left fold 0 lna in
+        let h = combine3 hna hbl htl in
 	(CoFix (ln,(lna,tl,bl)), combinesmall 14 h)
       | Meta n ->
 	(t, combinesmall 15 n)
@@ -616,9 +626,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
   and hash_term_array t =
     let accu = ref 0 in
     for i = 0 to Array.length t - 1 do
-      let x, h = sh_rec t.(i) in
+      let x, h = sh_rec (Array.unsafe_get t i) in
       accu := combine !accu h;
-      t.(i) <- x
+      Array.unsafe_set t i x
     done;
     (* [h] must be positive. *)
     let h = !accu land 0x3FFFFFFF in
@@ -636,9 +646,12 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 
 let rec hash t =
   match kind t with
-    | Var i -> combinesmall 1 (Hashtbl.hash i)
-    | Sort s -> combinesmall 2 (Hashtbl.hash s)
-    | Cast (c, _, _) -> hash c
+    | Var i -> combinesmall 1 (Id.hash i)
+    | Sort s -> combinesmall 2 (Sorts.hash s)
+    | Cast (c, k, t) ->
+      let hc = hash c in
+      let ht = hash t in
+      combinesmall 3 (combine3 hc (hash_cast_kind k) ht)
     | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c))
     | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c))
     | LetIn (_, b, t, c) ->
@@ -647,13 +660,13 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Evar (e,l) ->
-      combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l))
+      combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
     | Const c ->
-      combinesmall 9 (Hashtbl.hash c)	(* TODO: proper hash function for constants *)
-    | Ind (kn,i) ->
-      combinesmall 10 (combine (Hashtbl.hash kn) i)
-    | Construct ((kn,i),j) ->
-      combinesmall 11 (combine3 (Hashtbl.hash kn) i j)
+      combinesmall 9 (Constant.hash c)
+    | Ind ind ->
+      combinesmall 10 (ind_hash ind)
+    | Construct c ->
+      combinesmall 11 (constructor_hash c)
     | Case (_ , p, c, bl) ->
       combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
     | Fix (ln ,(_, tl, bl)) ->
diff --git a/kernel/evar.ml b/kernel/evar.ml
index d7e32626f..62d54027c 100644
--- a/kernel/evar.ml
+++ b/kernel/evar.ml
@@ -12,6 +12,7 @@ let repr x = x
 let unsafe_of_int x = x
 let compare = Int.compare
 let equal = Int.equal
+let hash = Int.hash
 
 module Self =
 struct
diff --git a/kernel/evar.mli b/kernel/evar.mli
index 8e8b88d94..9f1017351 100644
--- a/kernel/evar.mli
+++ b/kernel/evar.mli
@@ -27,5 +27,8 @@ val equal : t -> t -> bool
 val compare : t -> t -> int
 (** Comparison over existential variables. *)
 
+val hash : t -> int
+(** Hash over existential variables. *)
+
 module Set : Set.S with type elt = t
 module Map : CMap.ExtS with type key = t and module Set := Set
diff --git a/kernel/names.ml b/kernel/names.ml
index 00b8df486..c505017f6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -32,6 +32,8 @@ struct
 
   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)
@@ -82,6 +84,10 @@ struct
     | 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
@@ -96,7 +102,7 @@ struct
           | (Name id1, Name id2) -> id1 == id2
           | (Anonymous,Anonymous) -> true
           | _ -> false
-      let hash = Hashtbl.hash
+      let hash = hash
     end
 
   module Hname = Hashcons.Make(Self_Hashcons)
@@ -141,6 +147,14 @@ struct
 
   let equal p1 p2 = Int.equal (compare p1 p2) 0
 
+  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
 
@@ -198,6 +212,11 @@ struct
 
   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
@@ -207,7 +226,7 @@ struct
       let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
         (x == y) ||
         (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
-      let hash = Hashtbl.hash
+      let hash = hash
     end
 
   module HashMBId = Hashcons.Make(Self_Hashcons)
@@ -267,6 +286,14 @@ module ModPath = struct
 
   let equal mp1 mp2 = Int.equal (compare mp1 mp2) 0
 
+  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
 
   module Self_Hashcons = struct
@@ -284,7 +311,7 @@ module ModPath = struct
       | MPbound m1, MPbound m2 -> m1 == m2
       | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2
       | _ -> false
-    let hash = Hashtbl.hash
+    let hash = hash
   end
 
   module HashMP = Hashcons.Make(Self_Hashcons)
@@ -336,6 +363,11 @@ module KerName = struct
 
   let equal kn1 kn2 = Int.equal (compare kn1 kn2) 0
 
+  open Hashset.Combine
+
+  let hash (mp, dp, lbl) =
+    combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl)
+
   module Self_Hashcons = struct
     type t = kernel_name
     type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
@@ -344,7 +376,7 @@ module KerName = struct
       (hmod mp,hdir dir,hstr l)
     let equal (mp1,dir1,l1) (mp2,dir2,l2) =
       mp1 == mp2 && dir1 == dir2 && l1 == l2
-    let hash = Hashtbl.hash
+    let hash = hash
   end
 
   module HashKN = Hashcons.Make(Self_Hashcons)
@@ -446,6 +478,14 @@ module KerPair = struct
       the same user part implies having the same canonical part
       (invariant of the system). *)
 
+  open Hashset.Combine
+
+  let hash = function
+  | Same kn -> combinesmall 1 (KerName.hash kn)
+  | Dual (kn1, kn2) ->
+    let hk = combine (KerName.hash kn1) (KerName.hash kn2) in
+    combinesmall 2 hk
+
   module Self_Hashcons =
     struct
       type t = kernel_pair
@@ -454,7 +494,7 @@ module KerPair = struct
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
       let equal x y = (user x) == (user y)
-      let hash = Hashtbl.hash
+      let hash = hash
     end
 
   module HashKP = Hashcons.Make(Self_Hashcons)
@@ -500,6 +540,8 @@ let ind_ord (m1, i1) (m2, i2) =
 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 eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let constructor_ord (ind1, j1) (ind2, j2) =
@@ -508,6 +550,8 @@ let constructor_ord (ind1, j1) (ind2, j2) =
 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)
 
 module InductiveOrdered = struct
   type t = inductive
@@ -553,7 +597,7 @@ module Hind = Hashcons.Make(
     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 = Hashtbl.hash
+    let hash = ind_hash
   end)
 
 module Hconstruct = Hashcons.Make(
@@ -562,7 +606,7 @@ module Hconstruct = Hashcons.Make(
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
     let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
-    let hash = Hashtbl.hash
+    let hash = constructor_hash
   end)
 
 let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate KerName.hcons
diff --git a/kernel/names.mli b/kernel/names.mli
index 6f4ac9a53..417e35aaa 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -21,6 +21,9 @@ sig
   val compare : t -> t -> int
   (** Comparison over identifiers *)
 
+  val hash : t -> int
+  (** Hash over identifiers *)
+
   val is_valid : string -> bool
   (** Check that a string may be converted to an identifier. *)
 
@@ -59,6 +62,9 @@ sig
   val equal : t -> t -> bool
   (** Equality over names. *)
 
+  val hash : t -> int
+  (** Hash over names. *)
+
   val hcons : t -> t
   (** Hashconsing over names. *)
 
@@ -86,6 +92,9 @@ sig
   val compare : t -> t -> int
   (** Comparison over directory paths. *)
 
+  val hash : t -> int
+  (** Hash over directory paths. *)
+
   val make : module_ident list -> t
   (** Create a directory path. (The list must be reversed). *)
 
@@ -122,6 +131,9 @@ sig
   val compare : t -> t -> int
   (** Comparison over labels. *)
 
+  val hash : t -> int
+  (** Hash over labels. *)
+
   val make : string -> t
   (** Create a label out of a string. *)
 
@@ -156,6 +168,9 @@ sig
   val compare : t -> t -> int
   (** Comparison over unique bound names. *)
 
+  val hash : t -> int
+  (** Hash over unique bound names. *)
+
   val make : DirPath.t -> Id.t -> t
   (** The first argument is a file name, to prevent conflict between different
       files. *)
@@ -188,6 +203,7 @@ sig
 
   val compare : t -> t -> int
   val equal : t -> t -> bool
+  val hash : t -> int
 
   val is_bound : t -> bool
 
@@ -279,6 +295,9 @@ sig
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
+  val hash : t -> int
+  (** Hashing function *)
+
   val change_label : t -> Label.t -> t
   (** Builds a new constant name with a different label *)
 
@@ -381,10 +400,12 @@ val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val eq_ind : inductive -> inductive -> bool
 val ind_ord : inductive -> inductive -> int
+val ind_hash : inductive -> int
 val ind_user_ord : inductive -> inductive -> int
 val eq_constructor : constructor -> constructor -> bool
 val constructor_ord : constructor -> constructor -> int
 val constructor_user_ord : constructor -> constructor -> int
+val constructor_hash : constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 874e4a573..d656eceb6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -148,11 +148,11 @@ open Hashset.Combine
 let hash_symbol symb =
   match symb with
   | SymbValue v -> combinesmall 1 (Hashtbl.hash v)
-  | SymbSort s -> combinesmall 2 (Hashtbl.hash s)
-  | SymbName name -> combinesmall 3 (Hashtbl.hash name)
-  | SymbConst c -> combinesmall 4 (Hashtbl.hash c)
+  | SymbSort s -> combinesmall 2 (Sorts.hash s)
+  | SymbName name -> combinesmall 3 (Name.hash name)
+  | SymbConst c -> combinesmall 4 (Constant.hash c)
   | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
-  | SymbInd ind -> combinesmall 6 (Hashtbl.hash ind)
+  | SymbInd ind -> combinesmall 6 (ind_hash ind)
 
 module HashedTypeSymbol = struct
   type t = symbol
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index d2469c4fd..04deade92 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -46,6 +46,19 @@ let family = function
 
 let family_equal = (==)
 
+open Hashset.Combine
+
+let hash = function
+| Prop p ->
+  let h = match p with
+  | Pos -> 0
+  | Null -> 1
+  in
+  combinesmall 1 h
+| Type u ->
+  let h = Universe.hash u in
+  combinesmall 2 h
+
 module Hsorts =
   Hashcons.Make(
     struct
@@ -59,7 +72,7 @@ module Hsorts =
         | (Prop c1, Prop c2) -> c1 == c2
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
-      let hash = Hashtbl.hash
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 51e8a6f6c..b64e92fba 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -22,6 +22,7 @@ val type1  : t
 
 val equal : t -> t -> bool
 val compare : t -> t -> int
+val hash : t -> int
 
 val is_prop : t -> bool
 val family : t -> family
diff --git a/kernel/univ.ml b/kernel/univ.ml
index aa6c9c4c8..9b5c42f56 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -31,9 +31,11 @@ open Util
 
 module UniverseLevel = struct
 
+  open Names
+
   type t =
     | Set
-    | Level of int * Names.DirPath.t
+    | Level of int * DirPath.t
 
   (* A specialized comparison function: we compare the [int] part first.
      This way, most of the time, the [DirPath.t] part is not considered.
@@ -53,19 +55,24 @@ module UniverseLevel = struct
     | Level (i1, dp1), Level (i2, dp2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
-      else Names.DirPath.compare dp1 dp2)
+      else DirPath.compare dp1 dp2)
 
   let equal u v = match u,v with
     | Set, Set -> true
     | Level (i1, dp1), Level (i2, dp2) ->
-      Int.equal i1 i2 && Names.DirPath.equal dp1 dp2
+      Int.equal i1 i2 && DirPath.equal dp1 dp2
     | _ -> false
 
+  let hash = function
+  | Set -> 0
+  | Level (i, dp) ->
+    Hashset.Combine.combine (Int.hash i) (DirPath.hash dp)
+
   let make m n = Level (n, m)
 
   let to_string = function
     | Set -> "Set"
-    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (n,d) -> DirPath.to_string d^"."^string_of_int n
 end
 
 module UniverseLMap = Map.Make (UniverseLevel)
@@ -109,6 +116,21 @@ struct
 
   let make l = Atom l
 
+  open Hashset.Combine
+
+  let rec hash_list accu = function
+  | [] -> 0
+  | u :: us ->
+    let accu = combine (UniverseLevel.hash u) accu in
+    hash_list accu us
+
+  let hash = function
+  | Atom u -> combinesmall 1 (UniverseLevel.hash u)
+  | Max (lt, le) ->
+    let hlt = hash_list 0 lt in
+    let hle = hash_list 0 le in
+    combinesmall 2 (combine hlt hle)
+
 end
 
 open Universe
@@ -996,7 +1018,7 @@ module Hunivlevel =
 	| UniverseLevel.Level (n,d), UniverseLevel.Level (n',d') ->
 	  n == n' && d == d'
 	| _ -> false
-      let hash = Hashtbl.hash
+      let hash = UniverseLevel.hash
     end)
 
 module Huniv =
@@ -1015,7 +1037,7 @@ module Huniv =
 	      (List.for_all2eq (==) gel gel') &&
               (List.for_all2eq (==) gtl gtl')
 	  | _ -> false
-      let hash = Hashtbl.hash
+      let hash = Universe.hash
     end)
 
 let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7511769c4..64555fbb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,6 +20,9 @@ sig
   val equal : t -> t -> bool
   (** Equality function *)
 
+  val hash : t -> int
+  (** Hash function *)
+
   val make : Names.DirPath.t -> int -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
@@ -41,6 +44,9 @@ sig
   val equal : t -> t -> bool
   (** Equality function *)
 
+  val hash : t -> int
+  (** Hash function *)
+
   val make : UniverseLevel.t -> t
   (** Create a constraint-free universe out of a given level. *)