From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 31 Mar 2017 23:20:25 +0200
Subject: Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.
---
 engine/eConstr.mli | 26 +++++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e7287fc06..db10fbf42 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -28,9 +28,26 @@ 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
 
+(** {5 Universe variables} *)
+
+module ESorts :
+sig
+  type t
+  (** Type of sorts up-to universe unification. Essentially a wrapper around
+      Sorts.t so that normalization is ensured statically. *)
+
+  val make : Sorts.t -> t
+  (** Turn a sort into an up-to sort. *)
+
+  val kind : Evd.evar_map -> t -> Sorts.t
+  (** Returns the view into the current sort. Note that the kind of a variable
+      may change if the unification state of the evar map changes. *)
+
+end
+
 (** {5 Destructors} *)
 
-val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
 (** Same as {!Constr.kind} except that it expands evars and normalizes
     universes on the fly. *)
 
@@ -43,7 +60,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
 
-val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 (** Construct a term from a view. *)
 
 val of_constr : Constr.t -> t
@@ -123,7 +140,7 @@ val isRelN : Evd.evar_map -> int -> t -> bool
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
 val destVar : Evd.evar_map -> t -> Id.t
-val destSort : Evd.evar_map -> t -> Sorts.t
+val destSort : Evd.evar_map -> t -> ESorts.t
 val destCast : Evd.evar_map -> t -> t * cast_kind * t
 val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
@@ -242,6 +259,9 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_sorts : ESorts.t -> Sorts.t
+  (** Physical identity. Does not care for normalization. *)
+
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
 end
-- 
cgit v1.2.3