Monotonizing the Evarutil module.

Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.

7 files changed, 79 insertions, 46 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2cbf3a265..91bf11eb5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -28,6 +28,7 @@ open Evarutil
 open Evarsolve
 open Evarconv
 open Evd
+open Sigma.Notations
 
 (* Pattern-matching errors *)
 
@@ -1947,8 +1948,10 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
         let sigma,t = match tycon with
 	| Some t -> sigma,t
 	| None -> 
-	  let sigma, (t, _) = 
+          let sigma = Sigma.Unsafe.of_evar_map sigma in
+          let Sigma ((t, _), sigma, _) =
 	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
+          let sigma = Sigma.to_evar_map sigma in
 	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 99e51330e..f3ff26876 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1007,7 +1007,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | None ->
         let evty = set_holes evdref cty subst in
         let instance = Filter.filter_list filter instance in
-        let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
+        let evd = Sigma.Unsafe.of_evar_map !evdref in
+        let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
+        let evd = Sigma.to_evar_map evd in
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
         ev in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0dd0ad2e0..518f4df40 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -19,6 +19,7 @@ open Retyping
 open Reductionops
 open Evarutil
 open Pretype_errors
+open Sigma.Notations
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -180,7 +181,9 @@ let restrict_evar_key evd evk filter candidates =
       let candidates = match candidates with
       | NoUpdate -> evi.evar_candidates
       | UpdateWith c -> Some c in
-      restrict_evar evd evk filter candidates
+      let sigma = Sigma.Unsafe.of_evar_map evd in
+      let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
+      (Sigma.to_evar_map sigma, evk)
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
@@ -570,7 +573,9 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let evd = Sigma.to_evar_map evd in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -631,8 +636,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
      ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
-  let evd,ev2_in_sign =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (ev2_in_sign, evd, _) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
+  let evd = Sigma.to_evar_map evd in
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cd5188cd7..2ed557683 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -19,6 +19,7 @@ open Environ
 open Evd
 open Reductionops
 open Pretype_errors
+open Sigma.Notations
 
 (** Combinators *)
 
@@ -41,7 +42,7 @@ let e_new_global evdref x =
   evd_comb1 (Evd.fresh_global (Global.env())) evdref x
 
 let new_global evd x = 
-  Evd.fresh_global (Global.env()) evd x
+  Sigma.fresh_global (Global.env()) evd x
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -342,15 +343,18 @@ let push_rel_context_to_named_context env typ =
 let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let restrict_evar evd evk filter candidates =
+  let evd = Sigma.to_evar_map evd in
   let evd, evk' = Evd.restrict evk filter ?candidates evd in
-  Evd.declare_future_goal evk' evd, evk'
+  Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
 let new_pure_evar_full evd evi =
+  let evd = Sigma.to_evar_map evd in
   let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
-  (evd, evk)
+  Sigma.Unsafe.of_pair (evk, evd)
 
 let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+  let evd = Sigma.to_evar_map evd in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let evi = {
@@ -367,17 +371,17 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
   in
-  (evd,newevk)
+  Sigma.Unsafe.of_pair (newevk, evd)
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  (evd,mkEvar (newevk,Array.of_list instance))
+  let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
@@ -386,24 +390,26 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let evd = Sigma.to_evar_map evd in
-  let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  Sigma.Unsafe.of_pair (c, sigma)
+let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  (Sigma.to_evar_map evd, evk)
 
 let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
-  let evd', s = new_sort_variable rigid evd in
-  let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in
-    evd', (e, s)
+  let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
+  let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+  Sigma ((e, s), evd', p +> q)
 
 let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
-  let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
-    evdref := evd';
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
+  let sigma = Sigma.to_evar_map sigma in
+    evdref := sigma;
     c
 
 let new_Type ?(rigid=Evd.univ_flexible) env evd = 
-  let evd', s = new_sort_variable rigid evd in
-    evd', mkSort s
+  let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
+  Sigma (mkSort s, sigma, p)
 
 let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
   let evd', s = new_sort_variable rigid !evdref in
@@ -501,7 +507,9 @@ let rec check_and_clear_in_constr env evdref err ids c =
             else
               let origfilter = Evd.evar_filter evi in
               let filter = Evd.Filter.apply_subfilter origfilter filter in
-              let evd,_ = restrict_evar !evdref evk filter None in
+              let evd = Sigma.Unsafe.of_evar_map !evdref in
+              let Sigma (_, evd, _) = restrict_evar evd evk filter None in
+              let evd = Sigma.to_evar_map evd in
               evdref := evd;
 	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
 	      let evi = Evd.find !evdref evk in
@@ -708,7 +716,10 @@ let define_pure_evar_as_product evd evk =
   let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
   let evd1,(dom,u1) =
-    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+    let evd = Sigma.Unsafe.of_evar_map evd in
+    let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+    (Sigma.to_evar_map evd1, e)
+  in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
@@ -719,7 +730,10 @@ let define_pure_evar_as_product evd evk =
       else
 	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-	  new_type_evar newenv evd1 status ~src ~filter in
+          let evd1 = Sigma.Unsafe.of_evar_map evd1 in
+          let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
+          (Sigma.to_evar_map evd3, e)
+        in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
@@ -798,8 +812,8 @@ let define_evar_as_sort env evd (ev,args) =
    any type has type Type. May cause some trouble, but not so far... *)
 
 let judge_of_new_Type evd =
-  let evd', s = new_univ_variable univ_rigid evd in
-    evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+  let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
+  Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
 
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d87c7ef8d..bc4c37a91 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -27,12 +27,12 @@ val new_evar :
   ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
-  named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * evar
+  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
 
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
+val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
 
 (** the same with side-effects *)
 val e_new_evar :
@@ -44,23 +44,23 @@ val e_new_evar :
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  evar_map * (constr * sorts)
+  (constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
-val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
-val restrict_evar : evar_map -> existential_key -> Filter.t ->
-  constr list option -> evar_map * existential_key
+val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
+  constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
-val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
 val e_new_global : evar_map ref -> Globnames.global_reference -> constr
 
 (** Create a fresh evar in a context different from its definition context:
@@ -70,11 +70,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> 
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> 
+ named_context_val -> 'r Sigma.t -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  constr list -> evar_map * constr
+  constr list -> (constr, 'r) Sigma.sigma
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
@@ -138,7 +138,7 @@ val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
 
 (** {6 Value/Type constraints} *)
 
-val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
+val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 
 type type_constraint = types option
 type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11fba7b94..835dc2f80 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,6 +42,7 @@ open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
+open Sigma.Notations
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
@@ -444,10 +445,13 @@ let pretype_sort evdref = function
   | GType s -> evd_comb1 judge_of_Type evdref s
 
 let new_type_evar env evdref loc =
-  let e, s = 
-    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
-      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
-  in e
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma ((e, _), sigma, _) =
+    Evarutil.new_type_evar env sigma
+      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
+  in
+  evdref := Sigma.to_evar_map sigma;
+  e
 
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bd46911c9..085aaf78a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,7 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
+open Sigma.Notations
 
 (* Errors *)
 
@@ -385,7 +386,9 @@ let substl_with_function subst sigma constr =
     if i <= k + Array.length v then
       match v.(i-k-1) with
       | (fx, Some (min, ref)) ->
-        let (sigma, evk) = Evarutil.new_pure_evar venv !evd dummy in
+        let sigma = Sigma.Unsafe.of_evar_map !evd in
+        let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in
+        let sigma = Sigma.to_evar_map sigma in
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
         lift k (mkEvar (evk, [|fx;ref|]))