- Fix hashing of levels to get the "right" order in universe contexts etc...

- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.

9 files changed, 39 insertions, 29 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7a90f36752..f4420c489d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -229,7 +229,7 @@ let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
       let subst, csts = universes_and_subst_of cb u in
-	(map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
+	(map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
 let constant_context env kn =
@@ -248,7 +248,7 @@ let constant_value env (kn,u) =
       | Def l_body -> 
 	if cb.const_polymorphic then
 	  let subst, csts = universes_and_subst_of cb u in
-	    (subst_univs_constr subst (Mod_subst.force_constr l_body), csts)
+	    (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts)
 	else Mod_subst.force_constr l_body, Univ.Constraint.empty
       | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
       | Undef _ -> raise (NotEvaluableConst NoBody)
@@ -263,11 +263,11 @@ let constant_value_and_type env (kn, u) =
     if cb.const_polymorphic then
       let subst, cst = universes_and_subst_of cb u in
       let b' = match cb.const_body with
-	| Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body))
+	| Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body))
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_univs_constr subst) cb.const_type, cst
+	b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -284,7 +284,7 @@ let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
       let subst = Univ.make_universe_subst u cb.const_universes in
-	map_regular_arity (subst_univs_constr subst) cb.const_type
+	map_regular_arity (subst_univs_level_constr subst) cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -294,7 +294,7 @@ let constant_value_in env (kn,u) =
       let b = Mod_subst.force_constr l_body in
 	if cb.const_polymorphic then
 	  let subst = Univ.make_universe_subst u cb.const_universes in
-	    subst_univs_constr subst b
+	    subst_univs_level_constr subst b
 	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 6d48aaa4e3..94e4479d2d 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -149,7 +149,7 @@ let type_of_projection env (cst,u) =
     if cb.const_polymorphic then
       let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
       let subst = make_inductive_subst mib u in
-	Vars.subst_univs_constr subst pb.proj_type
+	Vars.subst_univs_level_constr subst pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
 
@@ -333,7 +333,7 @@ let judge_of_projection env p c ct =
   in
     assert(eq_mind pb.proj_ind (fst ind));
     let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in
+    let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
       substl (c :: List.rev args) ty
       
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3f1c4e75fd..f07217ac00 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -56,11 +56,11 @@ let inductive_params (mib,_) = mib.mind_nparams
 let make_inductive_subst mib u =
   if mib.mind_polymorphic then 
     make_universe_subst u mib.mind_universes
-  else Univ.empty_subst
+  else Univ.empty_level_subst
 
 let inductive_params_ctxt (mib,u) = 
   let subst = make_inductive_subst mib u in
-    Vars.subst_univs_context subst mib.mind_params_ctxt
+    Vars.subst_univs_level_context subst mib.mind_params_ctxt
 
 let inductive_instance mib =
   if mib.mind_polymorphic then 
@@ -89,7 +89,7 @@ let ind_subst mind mib u =
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind u subst mib c =
   let s = ind_subst mind mib u in
-    substl s (subst_univs_constr subst c)
+    substl s (subst_univs_level_constr subst c)
 
 let instantiate_params full t args sign =
   let fail () =
@@ -113,7 +113,7 @@ let full_inductive_instantiate mib u params sign =
   let t = mkArity (sign,dummy) in
   let subst = make_inductive_subst mib u in
   let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    Vars.subst_univs_context subst ar
+    Vars.subst_univs_level_context subst ar
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
   let subst = make_inductive_subst mib u in
@@ -217,7 +217,7 @@ let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
     if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
     else 
       let subst = make_inductive_subst mib u in
-	(subst_univs_constr subst a.mind_user_arity, subst)
+	(subst_univs_level_constr subst a.mind_user_arity, subst)
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -234,7 +234,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
     if not mib.mind_polymorphic then a.mind_user_arity
     else 
       let subst = make_inductive_subst mib u in
-	(subst_univs_constr subst a.mind_user_arity)
+	(subst_univs_level_constr subst a.mind_user_arity)
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a23d170f5b..497c064172 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,13 +35,14 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
 
-val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_subst
+val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst
 
 val inductive_instance : mutual_inductive_body -> universe_instance
 val inductive_context : mutual_inductive_body -> universe_context
 val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context
 
-val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints
+val instantiate_inductive_constraints : 
+  mutual_inductive_body -> universe_level_subst -> constraints
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters : 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 49f883628d..98c0dfc20f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -176,7 +176,7 @@ let type_of_projection env (cst,u) =
     if cb.const_polymorphic then
       let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
       let subst = make_inductive_subst mib u in
-	Vars.subst_univs_constr subst pb.proj_type
+	Vars.subst_univs_level_constr subst pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
 
@@ -374,7 +374,7 @@ let judge_of_projection env p cj =
   in
     assert(eq_mind pb.proj_ind (fst ind));
     let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in
+    let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
     let ty = substl (cj.uj_val :: List.rev args) ty in
       (* TODO: Universe polymorphism for projections *)
       {uj_val = mkProj (p,cj.uj_val);
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8984938d36..147efe86bc 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -454,7 +454,13 @@ module Level = struct
 
     let hcons = hashcons
     let equal = deep_equal (* Not shallow as serialization breaks sharing *)
-    let hash = Hashtbl.hash
+      
+    open Hashset.Combine
+
+    let hash = function
+      | Prop -> combinesmall 1 0
+      | Set -> combinesmall 1 1
+      | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d))
   end
   
   (* let hcons = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons *)
@@ -1898,7 +1904,7 @@ let check_context_subset (univs, cst) (univs', cst') =
 (** Substitutions. *)
 
 let make_universe_subst inst (ctx, csts) = 
-  try Array.fold_left2 (fun acc c i -> LMap.add c (Universe.make i) acc)
+  try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
         LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
   with Invalid_argument _ -> 
     anomaly (Pp.str "Mismatched instance and context when building universe substitution")
@@ -2115,7 +2121,7 @@ let subst_univs_universe_constraints subst csts =
 
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context subst (_, csts) = 
-  subst_univs_constraints (make_subst subst) csts
+  subst_univs_level_constraints subst csts
 
 let check_consistent_constraints (ctx,cstrs) cstrs' =
   (* TODO *) ()
diff --git a/kernel/univ.mli b/kernel/univ.mli
index cc5eedefb5..bf04c62e21 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -355,15 +355,13 @@ val constraints_of : 'a constrained -> constraints
 val check_context_subset : universe_context_set -> universe_context -> universe_context
 
 (** Make a universe level substitution: the list must match the context variables. *)
-val make_universe_subst : Instance.t -> universe_context -> universe_subst
-val empty_subst : universe_subst
-val is_empty_subst : universe_subst -> bool
+val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
 
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
 (** Get the instantiated graph. *)
-val instantiate_univ_context : universe_subst -> universe_context -> constraints
+val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
 
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
@@ -372,6 +370,9 @@ val subst_univs_level_constraints : universe_level_subst -> constraints -> const
 
 val normalize_univs_level_level : universe_level_subst -> universe_level -> universe_level
 
+
+val empty_subst : universe_subst
+val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
 (* val subst_univs_level_fail : universe_subst_fn -> universe_level -> universe_level *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 40a797a902..120c07d30d 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -299,5 +299,5 @@ let subst_univs_level_constr subst c =
     let c' = aux c in
       if !changed then c' else c
 
-let subst_univs_context s = 
-  map_rel_context (subst_univs_constr s)
+let subst_univs_level_context s = 
+  map_rel_context (subst_univs_level_constr s)
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 9d5d16d0c0..b4f616b139 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -78,7 +78,9 @@ val subst_univs_fn_puniverses : universe_level_subst_fn ->
   'a puniverses -> 'a puniverses
 
 val subst_univs_constr : universe_subst -> constr -> constr
+
+(** Level substitutions for polymorphism. *)
+
 val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
-
-val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context