Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.

4 files changed, 58 insertions, 28 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 166340b412..28e9ffdb27 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -23,12 +23,21 @@ val make : Sorts.t -> t
 val kind : Evd.evar_map -> t -> Sorts.t
 val unsafe_to_sorts : t -> Sorts.t
 end
+module EInstance :
+sig
+type t
+val make : Univ.Instance.t -> t
+val kind : Evd.evar_map -> t -> Univ.Instance.t
+val empty : t
+val is_empty : t -> bool
+val unsafe_to_instance : t -> Univ.Instance.t
+end
 type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
@@ -50,6 +59,16 @@ struct
   let unsafe_to_sorts s = s
 end
 
+module EInstance =
+struct
+  type t = Univ.Instance.t
+  let make i = i
+  let kind sigma i = Evd.normalize_universe_instance sigma i
+  let empty = Univ.Instance.empty
+  let is_empty = Univ.Instance.is_empty
+  let unsafe_to_instance t = t
+end
+
 type t = Constr.t
 
 let safe_evar_value sigma ev =
@@ -63,15 +82,6 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | Const (c', u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstU (c', u')
-  | Ind (i, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkIndU (i, u')
-  | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstructU (co, u')
   | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
     let ev = destEvar f in
@@ -137,7 +147,7 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
-let in_punivs a = (a, Univ.Instance.empty)
+let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
@@ -762,6 +772,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
+let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index db10fbf424..3a9469e55a 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -45,9 +45,21 @@ sig
 
 end
 
+module EInstance :
+sig
+  type t
+  (** Type of universe instances up-to universe unification. Similar to
+      {ESorts.t} for {Univ.Instance.t}. *)
+
+  val make : Univ.Instance.t -> t
+  val kind : Evd.evar_map -> t -> Univ.Instance.t
+  val empty : t
+  val is_empty : t -> bool
+end
+
 (** {5 Destructors} *)
 
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
 (** Same as {!Constr.kind} except that it expands evars and normalizes
     universes on the fly. *)
 
@@ -60,7 +72,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
 
-val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 (** Construct a term from a view. *)
 
 val of_constr : Constr.t -> t
@@ -89,13 +101,13 @@ val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
 val mkConst : constant -> t
-val mkConstU : pconstant -> t
+val mkConstU : constant * EInstance.t -> t
 val mkProj : (projection * t) -> t
 val mkInd : inductive -> t
-val mkIndU : pinductive -> t
+val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
-val mkConstructU : pconstructor -> t
-val mkConstructUi : pinductive * int -> t
+val mkConstructU : constructor * EInstance.t -> t
+val mkConstructUi : (inductive * EInstance.t) * int -> t
 val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
@@ -146,10 +158,10 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
 val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
 val destApp : Evd.evar_map -> t -> t * t array
-val destConst : Evd.evar_map -> t -> constant puniverses
+val destConst : Evd.evar_map -> t -> constant * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
-val destInd : Evd.evar_map -> t -> inductive puniverses
-val destConstruct : Evd.evar_map -> t -> constructor puniverses
+val destInd : Evd.evar_map -> t -> inductive * EInstance.t
+val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
 val destCase : Evd.evar_map -> t -> case_info * t * t * t array
 val destProj : Evd.evar_map -> t -> projection * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
@@ -262,6 +274,9 @@ sig
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
 
+  val to_instance : EInstance.t -> Univ.Instance.t
+  (** Physical identity. Does not care for normalization. *)
+
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
 end
diff --git a/engine/termops.ml b/engine/termops.ml
index a679163456..64f4c6dc5e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1150,7 +1150,7 @@ let global_of_constr sigma c =
   | Const (c, u) -> ConstRef c, u
   | Ind (i, u) -> IndRef i, u
   | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Univ.Instance.empty
+  | Var id -> VarRef id, EConstr.EInstance.empty
   | _ -> raise Not_found
 
 let is_global sigma c t =
@@ -1169,8 +1169,12 @@ let isGlobalRef sigma c =
 
 let is_template_polymorphic env sigma f =
   match EConstr.kind sigma f with
-  | Ind ind -> Environ.template_polymorphic_pind ind env
-  | Const c -> Environ.template_polymorphic_pconstant c env
+  | Ind (ind, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_ind ind env
+  | Const (cst, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_constant cst env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
@@ -1453,8 +1457,8 @@ let global_app_of_constr sigma c =
   | Const (c, u) -> (ConstRef c, u), None
   | Ind (i, u) -> (IndRef i, u), None
   | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | Var id -> (VarRef id, EConstr.EInstance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c
   | _ -> raise Not_found
 
 let prod_applist sigma c l =
diff --git a/engine/termops.mli b/engine/termops.mli
index 0dd5d96fbd..fe6dfb0ce1 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -250,7 +250,7 @@ val clear_named_body : Id.t -> env -> env
 val global_vars : env -> Evd.evar_map -> constr -> Id.t list
 val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option
+val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -259,7 +259,7 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses
+val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
 
 val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool