Move the handling of the principal evar from refine to evd.

See previous commit for more discussion.

Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.

4 files changed, 66 insertions, 22 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ca6d26f61..dd74ecf38 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -360,36 +360,48 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ =
+let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
+  let default_naming =
+    if principal then
+        (* waiting for a more principled approach
+           (unnamed evars, private names?) *)
+        Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
+      else
+        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 evd = Evd.declare_future_goal newevk evd in
+  let evd =
+    if principal then Evd.declare_principal_goal newevk evd
+    else Evd.declare_future_goal newevk evd
+  in
   (evd,newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance =
+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 typ in
+  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
 (* [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 env evd ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) 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 =
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ~naming instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_type_evar env evd ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid =
+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 env evd' ?src ?filter ~naming (mkSort s) in
+  let evd', e = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
     evd', (e, s)
 
-let e_new_type_evar env evdref ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid =
-  let evd', c = new_type_evar env !evdref ?src ?filter ~naming rigid in
+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';
     c
 
@@ -402,8 +414,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
     evdref := evd'; mkSort s
 
   (* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) ty =
-  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ~naming ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
+  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
   evdref := evd';
   ev
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f38c1ea0f..ea00f8067 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -24,12 +24,14 @@ val mk_new_meta : unit -> constr
 val new_evar :
   env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * constr
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * constr
 
 val new_pure_evar :
   named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * evar
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * evar
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
@@ -37,18 +39,19 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 val e_new_evar :
   env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> types -> constr
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> constr
 
 (** 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 ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> rigid ->
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
   evar_map * (constr * sorts)
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> constr * sorts
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
@@ -71,6 +74,7 @@ val new_evar_instance :
  named_context_val -> evar_map -> 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
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c592ab9a5..35ca18e4f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -585,8 +585,16 @@ type evar_map = {
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
   effects    : Declareops.side_effects;
-  future_goals : Evar.t list; (** list of newly created evars,
-                                  to be eventually turned into goals if not solved.*)
+  future_goals : Evar.t list; (** list of newly created evars, to be
+                                  eventually turned into goals if not solved.*)
+  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
+                                             contained
+                                             [future_goals]. The evar
+                                             [e] will inherit
+                                             properties (now: the
+                                             name) of the evar which
+                                             will be instantiated with
+                                             a term containing [e]. *)
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -796,6 +804,7 @@ let empty = {
   effects    = Declareops.no_seff;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
+  principal_future_goal = None;
 }
 
 let from_env ?ctx e = 
@@ -984,10 +993,19 @@ let eval_side_effects evd = evd.effects
 let declare_future_goal evk evd =
   { evd with future_goals = evk::evd.future_goals }
 
+let declare_principal_goal evk evd =
+  match evd.principal_future_goal with
+  | None -> { evd with
+    future_goals = evk::evd.future_goals;
+    principal_future_goal=Some evk; }
+  | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
 let future_goals evd = evd.future_goals
 
+let principal_future_goal evd = evd.principal_future_goal
+
 let reset_future_goals evd =
-  { evd with future_goals = [] }
+  { evd with future_goals = [] ; principal_future_goal=None }
 
 let meta_diff ext orig = 
   Metamap.fold (fun m v acc ->
@@ -1445,6 +1463,7 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
+  principal_future_goal = evd.principal_future_goal;
 }
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 45432de36..c15975b0e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -284,13 +284,22 @@ val declare_future_goal : Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
+val declare_principal_goal : Evar.t -> evar_map -> evar_map
+(** Adds an existential variable to the list of future goals and make
+    it principal. Only one existential variable can be made principal, an
+    error is raised otherwise. For internal uses only. *)
+
 val future_goals : evar_map -> Evar.t list
 (** Retrieves the list of future goals. Used by the [refine] primitive
     of the tactic engine. *)
 
+val principal_future_goal : evar_map -> Evar.t option
+(** Retrieves the name of the principal existential variable if there
+    is one. Used by the [refine] primitive of the tactic engine. *)
+
 val reset_future_goals : evar_map -> evar_map
-(** Clears the list of future goals. Used by the [refine] primitive of
-    the tactic engine. *)
+(** Clears the list of future goals (as well as the principal future
+    goal). Used by the [refine] primitive of the tactic engine. *)
 
 (** {5 Sort variables}