Adding a notion of monotonous evarmap.

3 files changed, 184 insertions, 0 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index befeaa147..7197a2583 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -3,4 +3,5 @@ Termops
 Namegen
 UState
 Evd
+Sigma
 Proofview_monad
diff --git a/engine/sigma.ml b/engine/sigma.ml
new file mode 100644
index 000000000..e6189e29c
--- /dev/null
+++ b/engine/sigma.ml
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+type 'a t = Evd.evar_map
+
+type ('a, 'b) le = unit
+
+let refl = ()
+let cons _ _  = ()
+let (+>) = fun _ _ -> ()
+
+type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
+
+type 'a evar = Evar.t
+
+let lift_evar evk () = evk
+
+let to_evar_map evd = evd
+let to_evar evk = evk
+
+(** API *)
+
+type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
+
+let new_evar sigma ?naming info =
+  let (sigma, evk) = Evd.new_evar sigma ?naming info in
+  Fresh (evk, sigma, ())
+
+let define evk c sigma =
+  Sigma ((), Evd.define evk c sigma, ())
+
+(** Run *)
+
+type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+
+let run sigma f : 'a * Evd.evar_map =
+  let Sigma (x, sigma, ()) = f.run sigma in
+  (x, sigma)
+
+(** Monotonic references *)
+
+type evdref = Evd.evar_map ref
+
+let apply evdref f =
+  let Sigma (x, sigma, ()) = f.run !evdref in
+  evdref := sigma;
+  x
+
+let purify f =
+  let f (sigma : Evd.evar_map) =
+    let evdref = ref sigma in
+    let ans = f evdref in
+    Sigma (ans, !evdref, ())
+  in
+  { run = f }
+
+(** Unsafe primitives *)
+
+module Unsafe =
+struct
+
+let le = ()
+let of_evar_map sigma = sigma
+let of_evar evk = evk
+let of_ref ref = ref
+let of_pair (x, sigma) = Sigma (x, sigma, ())
+
+end
+
+module Notations =
+struct
+  type ('a, 'r) sigma_ = ('a, 'r) sigma =
+    Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
+
+  let (+>) = fun _ _ -> ()
+
+  type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
+end
diff --git a/engine/sigma.mli b/engine/sigma.mli
new file mode 100644
index 000000000..f4c47e08c
--- /dev/null
+++ b/engine/sigma.mli
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** 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.
+*)
+
+(** {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.  *)
+
+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 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
+
+(** 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