Generic support for open terms in tactics

We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
  the general sigma of the goal so that tactics have no such low-level
  tclEVARS, Evd.merge, or check_evars to do:
  - what takes tclEVARS and check_evars in charge is now a new
    tactical of name tclWITHHOLES (this tactical has a flag to support
    tactics in either the "e"- mode and the non "e"- mode);
  - the merge of goal evars and holes is now done generically at
    interpretation time (in tacinterp) and as a side-effect it also
    anticipates the possibility to refer to evars of the goal in the
    arguments;
  - with this approach, we don't need such constr/open_constr or
    bindings/ebindings variants and we can get rid of all ugly
    inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
  this is the case e.g. of "rewrite !c" which morally reevaluates c at
  each new rewriting step; this kind of tactics still receive a
  specific sigma around their arguments and they have to merge evars
  and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 30 insertions, 22 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index a65cc24ff6..99e3c4e1d6 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -354,7 +354,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
 (***************************************************************)
 (* Bindings *)
 
-type arg_bindings = open_constr explicit_bindings
+type arg_bindings = constr explicit_bindings
 
 (* [clenv_independent clenv]
  * returns a list of metavariables which appear in the term cval,
@@ -411,12 +411,11 @@ let clenv_unify_binding_type clenv c t u =
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
 
-let clenv_assign_binding clenv k (sigma,c) =
+let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-  let clenv' = { clenv with evd = Evd.merge clenv.evd sigma} in
-  let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in
-  let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
-  { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
+  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+  { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
   if bl = [] then
@@ -425,13 +424,13 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,b,(sigma,c as sc)) ->
+      (fun clenv (loc,b,c) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding clenv k sc)
+	  clenv_assign_binding clenv k c)
       clenv bl
 
 let clenv_constrain_last_binding c clenv =
@@ -439,7 +438,7 @@ let clenv_constrain_last_binding c clenv =
   let k =
     try list_last all_mvs
     with Failure _ -> anomaly "clenv_constrain_with_bindings" in
-  clenv_assign_binding clenv k (Evd.empty,c)
+  clenv_assign_binding clenv k c
 
 let clenv_constrain_dep_args hyps_only bl clenv =
   if bl = [] then
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 5571efbc57..4f7ac40920 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -86,7 +86,7 @@ val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 (***************************************************************)
 (* Bindings *)
 
-type arg_bindings = open_constr explicit_bindings
+type arg_bindings = constr explicit_bindings
 
 (* bindings where the key is the position in the template of the
    clenv (dependent or not). Positions can be negative meaning to
@@ -107,10 +107,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 (* the optional int tells how many prods of the lemma have to be used *)
 (* use all of them if None *)
 val make_clenv_binding_apply :
-  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
+  evar_info sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
-  evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
+  evar_info sigma -> constr * constr -> constr bindings -> clausenv
 
 (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
    [lmetas] is a list of metas to be applied to a proof of [t] so that
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index dc1784f40c..a33c81b097 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1241,6 +1241,15 @@ let check_evars env initial_sigma evd c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
+(* This returns the evars of [sigma] that are not in [sigma0] and
+   [sigma] minus these evars *)
+
+let subtract_evars sigma0 sigma =
+  Evd.fold (fun evk ev (sigma,sigma' as acc) ->
+    if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else
+      (Evd.remove sigma evk,Evd.add sigma' evk ev))
+    sigma (sigma,Evd.empty)
+
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr
@@ -1376,4 +1385,3 @@ let pr_tycon_type env (abs, t) =
 let pr_tycon env = function
     None -> str "None"
   | Some t -> pr_tycon_type env t
-
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4bfef79983..205ca8bd64 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -90,6 +90,7 @@ val solve_simple_eqn :
    new unresolved evar remains in [c] *)
 val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
+val subtract_evars : evar_map -> evar_map -> evar_map * evar_map 
 val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d5bc868894..b741c9a413 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -703,9 +703,9 @@ let plain_instance s c =
      empty map).
  *)
 
-let instance s c =
+let instance sigma s c =
   (* if s = [] then c else *)
-  local_strong whd_betaiota Evd.empty (plain_instance s c)
+  local_strong whd_betaiota sigma (plain_instance s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -902,21 +902,21 @@ let meta_value evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
-      instance
+      instance evd
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
     | None -> mkMeta mv
   in
   valrec mv
 
-let meta_instance env b =
+let meta_instance sigma b =
   let c_sigma =
     List.map
-      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+      (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas)
   in
-  if c_sigma = [] then b.rebus else instance c_sigma b.rebus
+  if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus
 
-let nf_meta env c = meta_instance env (mk_freelisted c)
+let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
 
 (* Instantiate metas that create beta/iota redexes *)
 
@@ -924,7 +924,7 @@ let meta_value evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
-      instance
+      instance evd
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
     | None -> mkMeta mv
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9e5ced8a28..0b9e69d95b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -210,7 +210,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
 
 val whd_meta : (metavariable * constr) list -> constr -> constr
 val plain_instance : (metavariable * constr) list -> constr -> constr
-val instance : (metavariable * constr) list -> constr -> constr
+val instance :evar_map -> (metavariable * constr) list -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
 
 (*s Heuristic for Conversion with Evar *)