Move to a representation of universe polymorphic constants using indices for variables.

Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.

1 files changed, 12 insertions, 20 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 48a7964c3..2a4f3a948 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -212,13 +212,9 @@ let add_constant_key kn cb linkinfo env =
 let add_constant kn cb env =
   add_constant_key kn cb (no_link_info ()) env
 
-let universes_of cb = 
-  cb.const_universes
-
-let universes_and_subst_of cb u =
-  let univs = universes_of cb in
-  let subst = Univ.make_universe_subst u univs in
-    subst, Univ.instantiate_univ_context subst univs
+let constraints_of cb u =
+  let univs = cb.const_universes in
+    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -230,8 +226,8 @@ let map_regular_arity f = function
 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_level_constr subst) cb.const_type, csts)
+      let csts = constraints_of cb u in
+	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
 let constant_context env kn =
@@ -249,8 +245,8 @@ let constant_value env (kn,u) =
       match cb.const_body with
       | Def l_body -> 
 	if cb.const_polymorphic then
-	  let subst, csts = universes_and_subst_of cb u in
-	    (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts)
+	  let csts = constraints_of cb u in
+	    (subst_instance_constr u (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,13 +259,13 @@ let constant_opt_value env cst =
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst, cst = universes_and_subst_of cb u in
+      let cst = constraints_of cb u in
       let b' = match cb.const_body with
-	| Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body))
+	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst
+	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -285,8 +281,7 @@ let constant_value_and_type env (kn, u) =
 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_level_constr subst) cb.const_type
+      map_regular_arity (subst_instance_constr u) cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -294,10 +289,7 @@ let constant_value_in env (kn,u) =
   match cb.const_body with
     | Def l_body -> 
       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_level_constr subst b
-	else b
+	subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)