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, 17 insertions, 3 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 4524b55bb1..f583bff64d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -37,10 +37,22 @@ let hcons_template_arity ar =
 
 (** {6 Constants } *)
 
+let instantiate cb c =
+  if cb.const_polymorphic then 
+    Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
+  else c
+
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some (force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof o)
+  | Def c -> Some (instantiate cb (force_constr c))
+  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o))
+
+let type_of_constant cb =
+  match cb.const_type with
+  | RegularArity t as x -> 
+    let t' = instantiate cb t in
+      if t' == t then x else RegularArity t'
+  | TemplateArity _ as x -> x
 
 let constraints_of_constant cb = Univ.Constraint.union 
   (Univ.UContext.constraints cb.const_universes)
@@ -57,7 +69,9 @@ let universes_of_constant cb =
       (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
 
 let universes_of_polymorphic_constant cb = 
-  if cb.const_polymorphic then universes_of_constant cb
+  if cb.const_polymorphic then 
+    let univs = universes_of_constant cb in
+      Univ.instantiate_univ_context univs
   else Univ.UContext.empty
 
 let constant_has_body cb = match cb.const_body with