Hardening the API of evarmaps.

The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.

6 files changed, 46 insertions, 53 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index fc4f5e040e..1af8565bdb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -632,14 +632,30 @@ let reassign_name_defined evk evk' (evtoid,idtoev) =
   (EvMap.add evk' id (EvMap.remove evk evtoid),
    Idmap.add id evk' (Idmap.remove id idtoev))
 
-let add d e i = match i.evar_body with
+let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
+  let evar_names = add_name_undefined naming e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
   let evar_names = remove_name_possibly_already_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
+let add d e i = add_with_name d e i
+
+(** New evars *)
+
+let evar_counter_summary_name = "evar counter"
+
+(* Generator of existential names *)
+let new_untyped_evar =
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
+  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+
+let new_evar evd ?naming evi =
+  let evk = new_untyped_evar () in
+  let evd = add_with_name evd ?naming evk evi in
+  (evd, evk)
+
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
@@ -831,27 +847,8 @@ let define evk body evd =
   let evar_names = remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
-    ?(filter=Filter.identity) ?candidates ?(store=Store.empty)
-    ?(naming=Misctypes.IntroAnonymous) evd =
-  let () = match Filter.repr filter with
-  | None -> ()
-  | Some filter ->
-    assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)))
-  in
-  let evar_info = {
-    evar_hyps = hyps;
-    evar_concl = ty;
-    evar_body = Evar_empty;
-    evar_filter = filter;
-    evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
-  in
-  let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in
-  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
-
-let restrict evk evk' filter ?candidates evd =
+let restrict evk filter ?candidates evd =
+  let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
@@ -863,7 +860,7 @@ let restrict evk evk' filter ?candidates evd =
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }
+    defn_evars; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
diff --git a/engine/evd.mli b/engine/evd.mli
index 94d9d5f662..e240ebc310 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -143,6 +143,10 @@ val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
 
+val new_evar : evar_map ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar
+(** Creates a fresh evar mapping to the given information. *)
+
 val add : evar_map -> evar -> evar_info -> evar_map
 (** [add sigma ev info] adds [ev] with evar info [info] in sigma.
     Precondition: ev must not preexist in [sigma]. *)
@@ -230,14 +234,8 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 (** {6 Misc} *)
 
-val evar_declare :
-  named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
-      ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t ->
-      ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map
-(** Convenience function. Just a wrapper around {!add}. *)
-
-val restrict : evar -> evar -> Filter.t -> ?candidates:constr list ->
-  evar_map -> evar_map
+val restrict : evar -> Filter.t -> ?candidates:constr list ->
+  evar_map -> evar_map * evar
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
@@ -614,3 +612,7 @@ val create_evar_defs      : evar_map -> evar_map
 (** Create an [evar_map] with empty meta map: *)
 
 val create_goal_evar_defs : evar_map -> evar_map
+
+(** {5 Summary names} *)
+
+val evar_counter_summary_name : string
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bb07bf0563..d5bb564f66 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -830,7 +830,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
-            let (i',ev) = new_evar env i ~src:dloc (substl ks b) in
+            let (i',ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
 	    (i', ev :: ks, m - 1,test))
 	(evd,[],List.length bs,fun i -> Success i) bs
     in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ee6bbe7fbe..6684b06048 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -239,17 +239,6 @@ let make_pure_subst evi args =
         | _ -> anomaly (Pp.str "Instance does not match its signature"))
     (evar_filtered_context evi) (Array.rev_to_list args,[]))
 
-(**********************)
-(* Creating new evars *)
-(**********************)
-
-let evar_counter_summary_name = "evar counter"
-
-(* Generator of existential names *)
-let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
-  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
-
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -354,17 +343,15 @@ 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 evk' = new_untyped_evar () in
-  let evd = Evd.restrict evk evk' filter ?candidates evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates evd in
   Evd.declare_future_goal evk' evd, evk'
 
 let new_pure_evar_full evd evi =
-  let evk = new_untyped_evar () in
-  let evd = Evd.add evd evk evi in
+  let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
+let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
   let default_naming =
     if principal then
         (* waiting for a more principled approach
@@ -374,8 +361,16 @@ let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?nam
         Misctypes.IntroAnonymous
   in
   let naming = Option.default default_naming naming in
-  let newevk = new_untyped_evar() in
-  let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
+  let evi = {
+    evar_hyps = sign;
+    evar_concl = typ;
+    evar_body = Evar_empty;
+    evar_filter = filter;
+    evar_source = src;
+    evar_candidates = candidates;
+    evar_extra = store; }
+  in
+  let (evd, newevk) = Evd.new_evar evd ~naming evi in
   let evd =
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f1d94b0a4f..76d67c748d 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -252,4 +252,3 @@ val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
 val meta_counter_summary_name : string
-val evar_counter_summary_name : string
diff --git a/stm/stm.ml b/stm/stm.ml
index 4a303f036e..f178c3ae4a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -166,7 +166,7 @@ type visit = { step : step; next : Stateid.t }
 
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = [ Evarutil.meta_counter_summary_name;
-                       Evarutil.evar_counter_summary_name;
+                       Evd.evar_counter_summary_name;
                        "program-tcc-table" ]
 type state = {
   system : States.state;