1 files changed, 131 insertions, 0 deletions
diff --git a/engine/sigma.mli b/engine/sigma.mli
new file mode 100644
index 00000000..7473a251
--- /dev/null
+++ b/engine/sigma.mli
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Constr
+
+(** Monotonous state enforced by typing.
+
+    This module allows to constrain uses of evarmaps in a monotonous fashion,
+    and in particular statically suppress evar leaks and the like. To this
+    ends, it defines a type of indexed evarmaps whose phantom typing ensures
+    monotonous use.
+*)
+
+(** {5 Stages} *)
+
+type ('a, 'b) le
+(** Relationship stating that stage ['a] is anterior to stage ['b] *)
+
+val refl : ('a, 'a) le
+(** Reflexivity of anteriority *)
+
+val cons : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Transitivity of anteriority *)
+
+val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+(** Alias for {!cons} *)
+
+(** {5 Monotonous evarmaps} *)
+
+type 'r t
+(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *)
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+(** Return values at a later stage *)
+
+type 'r evar
+(** Stage-indexed evars *)
+
+(** {5 Constructors} *)
+
+val here : 'a -> 'r t -> ('a, 'r) sigma
+(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
+
+(** {5 Postponing} *)
+
+val lift_evar : 'r evar -> ('r, 's) le -> 's evar
+(** Any evar existing at stage ['r] is also valid at any later stage. *)
+
+(** {5 Downcasting} *)
+
+val to_evar_map : 'r t -> Evd.evar_map
+val to_evar : 'r evar -> Evar.t
+
+(** {5 Monotonous API} *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  Evd.evar_info -> 'r fresh
+
+val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
+
+(** Polymorphic universes *)
+
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string ->
+  Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?loc:Loc.t -> ?name:string ->
+  Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?loc:Loc.t -> ?name:string ->
+  Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
+
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
+  'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
+val fresh_constant_instance :
+  ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+val fresh_inductive_instance :
+  ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
+val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor ->
+  (pconstructor, 'r) sigma
+
+val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
+  'r t -> Globnames.global_reference -> (constr, 'r) sigma
+
+(** FILLME *)
+
+(** {5 Run} *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map
+
+(** {5 Imperative monotonic functions} *)
+
+type evdref
+(** Monotonic references over evarmaps *)
+
+val apply : evdref -> 'a run -> 'a
+(** Apply a monotonic function on a reference. *)
+
+val purify : (evdref -> 'a) -> 'a run
+(** Converse of {!apply}. *)
+
+(** {5 Unsafe primitives} *)
+
+module Unsafe :
+sig
+  val le : ('a, 'b) le
+  val of_evar_map : Evd.evar_map -> 'r t
+  val of_evar : Evd.evar -> 'r evar
+  val of_ref : Evd.evar_map ref -> evdref
+  val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma
+end
+
+(** {5 Notations} *)
+
+module Notations :
+sig
+  type ('a, 'r) sigma_ = ('a, 'r) sigma =
+    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+  val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
+  (** Alias for {!cons} *)
+end