Here comes the commit, announced long ago, of the new tactic engine.

This is a fairly large commit (around 140 files and 7000 lines of code
impacted), it will cause some troubles for sure (I've listed the know
regressions below, there is bound to be more).
At this state of developpement it brings few features to the user, as
the old tactics were
ported with no change. Changes are on the side of the developer mostly.

Here comes a list of the major changes. I will stay brief, but the code
is hopefully well documented so that it is reasonably easy to infer the
details from it.

Feature developer-side:
* Primitives for a "real" refine tactic (generating a goal for each
evar).
* Abstract type of tactics, goals and proofs
* Tactics can act on several goals (formally all the focused goals). An
interesting consequence of this is that the tactical (. ; [ . | ... ])
can be separated in two
tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for
this particular syntax). We can also imagine a tactic to reorder the
goals.
* Possibility for a tactic to pass a value to following tactics (a
typical example is
an intro function which tells the following tactics which name it
introduced).
* backtracking primitives for tactics (it is now possible to implement a
tactical '+'
  with (a+b);c equivalent to (a;c+b;c) (itself equivalent to
(a;c||b;c)). This is a valuable
  tool to implement tactics like "auto" without nowing of the
implementation of tactics.
* A notion of proof modes, which allows to dynamically change the parser
for tactics. It is controlled at user level with the keywords Set
Default Proof Mode (this is the proof mode which is loaded at the start
of each proof) and Proof Mode (switches the proof mode of the current
proof) to control them.
* A new primitive Evd.fold_undefined which operates like an Evd.fold,
except it only goes through the evars whose body is Evar_empty. This is
a common operation throughout the code,
some of the fold-and-test-if-empty occurences have been replaced by
fold_undefined. For now,
it is only implemented as a fold-and-test, but we expect to have some
optimisations coming some day, as there can be a lot of evars in an
evar_map with this new implementation (I've observed a couple of
thousands), whereas there are rarely more than a dozen undefined ones.
Folding being a linear operation, this might result in a significant
speed-up.
* The declarative mode has been moved into the plugins. This is made
possible by the proof mode feature. I tried to document it so that it
can serve as a tutorial for a tactic mode plugin.

Features user-side:
* Unfocus does not go back to the root of the proof if several Focus-s
have been performed.
  It only goes back to the point where it was last focused.
* experimental (non-documented) support of keywords
BeginSubproof/EndSubproof:
  BeginSubproof focuses on first goal, one can unfocus only with
EndSubproof, and only
  if the proof is completed for that goal.
* experimental (non-documented) support for bullets ('+', '-' and '*')
  they act as hierarchical BeginSubproof/EndSubproof:
  First time one uses '+' (for instance) it focuses on first goal, when
the subproof is
  completed, one can use '+' again which unfocuses and focuses on next
first goal.
  Meanwhile, one cas use '*' (for instance) to focus more deeply.

Known regressions:
* The xml plugin had some functions related to proof trees. As the
structure of proof changed significantly, they do not work anymore.
* I do not know how to implement info or show script in this new engine.
Actually I don't even know what they were suppose to actually mean in
earlier versions either. I wager they would require some calm thinking
before going back to work.
* Declarative mode not entirely working (in particular proofs by
induction need to be restored).
* A bug in the inversion tactic (observed in some contributions)
* A bug in Program (observed in some contributions)
* Minor change in the 'old' type of tactics causing some contributions
to fail.
* Compilation time takes about 10-15% longer for unknown reasons (I
suspect it might be linked to the fact that I don't perform any
reduction at QED-s, and also to some linear operations on evar_map-s
(see Evd.fold_undefined above)).


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

9 files changed, 78 insertions, 659 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
deleted file mode 100644
index 7cbaf124a7..0000000000
--- a/pretyping/clenv.ml
+++ /dev/null
@@ -1,478 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Namegen
-open Sign
-open Environ
-open Evd
-open Reduction
-open Reductionops
-open Rawterm
-open Pattern
-open Tacred
-open Pretype_errors
-open Evarutil
-open Unification
-open Mod_subst
-open Coercion.Default
-
-(* Abbreviations *)
-
-let pf_env gls = Global.env_of_context gls.it.evar_hyps
-let pf_hyps gls = named_context_of_val gls.it.evar_hyps
-let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
-let pf_concl gl = gl.it.evar_concl
-
-(******************************************************************)
-(* Clausal environments *)
-
-type clausenv = {
-  env      : env;
-  evd      : evar_map;
-  templval : constr freelisted;
-  templtyp : constr freelisted }
-
-let cl_env ce = ce.env
-let cl_sigma ce =  ce.evd
-
-let subst_clenv sub clenv =
-  { templval = map_fl (subst_mps sub) clenv.templval;
-    templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    evd = subst_evar_defs_light sub clenv.evd;
-    env = clenv.env }
-
-let clenv_nf_meta clenv c = nf_meta clenv.evd c
-let clenv_term clenv c = meta_instance clenv.evd c
-let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
-let clenv_value clenv = meta_instance clenv.evd clenv.templval
-let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
-
-
-let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
-
-let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
-
-exception NotExtensibleClause
-
-let clenv_push_prod cl =
-  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
-  let rec clrec typ = match kind_of_term typ with
-    | Cast (t,_,_) -> clrec t
-    | Prod (na,t,u) ->
-	let mv = new_meta () in
-	let dep = dependent (mkRel 1) u in
-	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv t ~name:na' cl.evd in
-	let concl = if dep then subst1 (mkMeta mv) u else u in
-	let def = applist (cl.templval.rebus,[mkMeta mv]) in
-	{ templval = mk_freelisted def;
-	  templtyp = mk_freelisted concl;
-	  evd = e';
-	  env = cl.env }
-    | _ -> raise NotExtensibleClause
-  in clrec typ
-
-(* Instantiate the first [bound] products of [t] with metas (all products if
-   [bound] is [None]; unfold local defs *)
-
-let clenv_environments evd bound t =
-  let rec clrec (e,metas) n t =
-    match n, kind_of_term t with
-      | (Some 0, _) -> (e, List.rev metas, t)
-      | (n, Cast (t,_,_)) -> clrec (e,metas) n t
-      | (n, Prod (na,t1,t2)) ->
-	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) t2 in
-	  let na' = if dep then na else Anonymous in
-	  let e' = meta_declare mv t1 ~name:na' e in
-	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
-	    (if dep then (subst1 (mkMeta mv) t2) else t2)
-      | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
-      | (n, _) -> (e, List.rev metas, t)
-  in
-  clrec (evd,[]) bound t
-
-(* Instantiate the first [bound] products of [t] with evars (all products if
-   [bound] is [None]; unfold local defs *)
-
-let clenv_environments_evars env evd bound t =
-  let rec clrec (e,ts) n t =
-    match n, kind_of_term t with
-      | (Some 0, _) -> (e, List.rev ts, t)
-      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
-      | (n, Prod (na,t1,t2)) ->
-          let e',constr = Evarutil.new_evar e env t1 in
-	  let dep = dependent (mkRel 1) t2 in
-	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
-	    (if dep then (subst1 constr t2) else t2)
-      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
-      | (n, _) -> (e, List.rev ts, t)
-  in
-  clrec (evd,[]) bound t
-
-let clenv_conv_leq env sigma t c bound =
-  let ty = Retyping.get_type_of env sigma c in
-  let evd = Evd.create_goal_evar_defs sigma in
-  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
-  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
-  let evars = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar evars) args in
-  check_evars env sigma evars (applist (c,args));
-  args
-
-let mk_clenv_from_env environ sigma n (c,cty) =
-  let evd = create_goal_evar_defs sigma in
-  let (evd,args,concl) = clenv_environments evd n cty in
-  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
-    templtyp = mk_freelisted concl;
-    evd = evd;
-    env = environ }
-
-let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty)
-
-let mk_clenv_from gls = mk_clenv_from_n gls None
-
-let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
-
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
-
-(******************************************************************)
-
-(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
- * mv0, or if one of the free vars on mv1's freelist mentions
- * mv0 *)
-
-let mentions clenv mv0 =
-  let rec menrec mv1 =
-    mv0 = mv1 ||
-    let mlist =
-      try match meta_opt_fvalue clenv.evd mv1 with
-      | Some (b,_) -> b.freemetas
-      | None -> Metaset.empty
-      with Not_found -> Metaset.empty in
-    meta_exists menrec mlist
-  in menrec
-
-let error_incompatible_inst clenv mv  =
-  let na = meta_name clenv.evd mv in
-  match na with
-      Name id ->
-        errorlabstrm "clenv_assign"
-          (str "An incompatible instantiation has already been found for " ++
-           pr_id id)
-    | _ ->
-        anomaly "clenv_assign: non dependent metavar already assigned"
-
-(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
-let clenv_assign mv rhs clenv =
-  let rhs_fls = mk_freelisted rhs in
-  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
-    error "clenv_assign: circularity in unification";
-  try
-    if meta_defined clenv.evd mv then
-      if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
-        error_incompatible_inst clenv mv
-      else
-	clenv
-    else
-      let st = (ConvUpToEta 0,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
-  with Not_found ->
-    error "clenv_assign: undefined meta"
-
-
-
-(* [clenv_dependent hyps_only clenv]
- * returns a list of the metavars which appear in the template of clenv,
- * and which are dependent, This is computed by taking the metavars in cval,
- * in right-to-left order, and collecting the metavars which appear
- * in their types, and adding in all the metavars appearing in the
- * type of clenv.
- * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
-
-(* [clenv_metavars clenv mv]
- * returns a list of the metavars which appear in the type of
- * the metavar mv.  The list is unordered. *)
-
-let clenv_metavars evd mv =
-  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
-
-let dependent_metas clenv mvs conclmetas =
-  List.fold_right
-    (fun mv deps ->
-       Metaset.union deps (clenv_metavars clenv.evd mv))
-    mvs conclmetas
-
-let duplicated_metas c =
-  let rec collrec (one,more as acc) c =
-    match kind_of_term c with
-    | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
-    | _       -> fold_constr collrec acc c
-  in
-  snd (collrec ([],[]) c)
-
-let clenv_dependent hyps_only clenv =
-  let mvs = undefined_metas clenv.evd in
-  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
-  let deps = dependent_metas clenv mvs ctyp_mvs in
-  let nonlinear = duplicated_metas (clenv_value clenv) in
-  (* Make the assumption that duplicated metas have internal dependencies *)
-  List.filter
-    (fun mv -> if Metaset.mem mv deps
-               then not (hyps_only && Metaset.mem mv ctyp_mvs)
-               else List.mem mv nonlinear)
-    mvs
-
-let clenv_missing ce = clenv_dependent true ce
-
-(******************************************************************)
-
-let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
-  { clenv with
-      evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
-
-let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
-  { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
-
-let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
-    clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
-      (clenv_unify_meta_types ~flags:flags clenv)
-  else
-    clenv_unify allow_K CUMUL ~flags:flags
-      (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
-
-(* [clenv_pose_metas_as_evars clenv dep_mvs]
- * For each dependent evar in the clause-env which does not have a value,
- * pose a value for it by constructing a fresh evar.  We do this in
- * left-to-right order, so that every evar's type is always closed w.r.t.
- * metas.
-
- * Node added 14/4/08 [HH]: before this date, evars were collected in
-   clenv_dependent by collect_metas in the fold_constr order which is
-   (almost) the left-to-right order of dependencies in term. However,
-   due to K-redexes, collect_metas was sometimes missing some metas.
-   The call to collect_metas has been replaced by a call to
-   undefined_metas, but then the order was the one of definition of
-   the metas (numbers in increasing order) which is _not_ the
-   dependency order when a clenv_fchain occurs (because clenv_fchain
-   plugs a term with a list of consecutive metas in place of a - a priori -
-   arbitrary metavariable belonging to another sequence of consecutive metas:
-   e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of
-   (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2).
-   To ensure the dependency order, we check that the type of each meta
-   to pose is already meta-free, otherwise we postpone the transformation,
-   hoping that no cycle may happen.
-
-   Another approach could have been to use decimal numbers for metas so that
-   in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2)
-   then making the numeric order match the dependency order.
-*)
-
-let clenv_pose_metas_as_evars clenv dep_mvs =
-  let rec fold clenv = function
-  | [] -> clenv
-  | mv::mvs ->
-      let ty = clenv_meta_type clenv mv in
-      (* Postpone the evar-ization if dependent on another meta *)
-      (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
-      else
-	let (evd,evar) =
-	  new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
-	let clenv = clenv_assign mv evar {clenv with evd=evd} in
-	fold clenv mvs in
-  fold clenv dep_mvs
-
-let evar_clenv_unique_resolver = clenv_unique_resolver
-
-(******************************************************************)
-
-let connect_clenv gls clenv =
-  { clenv with
-    evd = evars_reset_evd gls.sigma clenv.evd;
-    env = Global.env_of_context gls.it.evar_hyps }
-
-(* [clenv_fchain mv clenv clenv']
- *
- * Resolves the value of "mv" (which must be undefined) in clenv to be
- * the template of clenv' be the value "c", applied to "n" fresh
- * metavars, whose types are chosen by destructing "clf", which should
- * be a clausale forme generated from the type of "c".  The process of
- * resolution can cause unification of already-existing metavars, and
- * of the fresh ones which get created.  This operation is a composite
- * of operations which pose new metavars, perform unification on
- * terms, and make bindings.
-
-   Otherwise said, from
-
-     [clenv] = [env;sigma;metas |- c:T]
-     [clenv'] = [env';sigma';metas' |- d:U]
-     [mv] = [mi] of type [Ti] in [metas]
-
-   then, if the unification of [Ti] and [U] produces map [rho], the
-   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
-   [rho'] being [rho;mi:=d].
-
-   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
-*)
-let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
-  (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
-  let clenv' =
-    { templval = clenv.templval;
-      templtyp = clenv.templtyp;
-      evd =
-        evar_merge (meta_merge clenv.evd nextclenv.evd) clenv.evd;
-      env = nextclenv.env } in
-  (* unify the type of the template of [nextclenv] with the type of [mv] *)
-  let clenv'' =
-    clenv_unify allow_K ~flags:flags CUMUL
-      (clenv_term clenv' nextclenv.templtyp)
-      (clenv_meta_type clenv' mv)
-      clenv' in
-  (* assign the metavar *)
-  let clenv''' =
-    clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv''
-  in
-  clenv'''
-
-(***************************************************************)
-(* Bindings *)
-
-type arg_bindings = constr explicit_bindings
-
-(* [clenv_independent clenv]
- * returns a list of metavariables which appear in the term cval,
- * and which are not dependent.  That is, they do not appear in
- * the types of other metavars which are in cval, nor in the type
- * of cval, ctyp. *)
-
-let clenv_independent clenv =
-  let mvs = collect_metas (clenv_value clenv) in
-  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
-  let deps = dependent_metas clenv mvs ctyp_mvs in
-  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
-
-let check_bindings bl =
-  match list_duplicates (List.map pi2 bl) with
-    | NamedHyp s :: _ ->
-	errorlabstrm ""
-	  (str "The variable " ++ pr_id s ++
-	   str " occurs more than once in binding list.");
-    | AnonHyp n :: _ ->
-	errorlabstrm ""
-	  (str "The position " ++ int n ++
-	   str " occurs more than once in binding list.")
-    | [] -> ()
-
-let meta_of_binder clause loc mvs = function
-  | NamedHyp s -> meta_with_name clause.evd s
-  | AnonHyp n ->
-      try List.nth mvs (n-1)
-      with (Failure _|Invalid_argument _) ->
-        errorlabstrm "" (str "No such binder.")
-
-let error_already_defined b =
-  match b with
-    | NamedHyp id ->
-        errorlabstrm ""
-          (str "Binder name \"" ++ pr_id id ++
-           str"\" already defined with incompatible value.")
-    | AnonHyp n ->
-        anomalylabstrm ""
-          (str "Position " ++ int n ++ str" already defined.")
-
-let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack clenv.evd u)) then
-    (* Not enough information to know if some subtyping is needed *)
-    CoerceToType, clenv, c
-  else
-    (* Enough information so as to try a coercion now *)
-    try
-      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
-      TypeProcessed, { clenv with evd = evd }, c
-    with 
-      | PretypeError (_,NotClean _) as e -> raise e
-      | e when precatchable_exception e ->
-	  TypeNotProcessed, clenv, c
-
-let clenv_assign_binding clenv k c =
-  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) 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 clenv_match_args bl clenv =
-  if bl = [] then
-    clenv
-  else
-    let mvs = clenv_independent clenv in
-    check_bindings bl;
-    List.fold_left
-      (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 c)
-      clenv bl
-
-let clenv_constrain_last_binding c clenv =
-  let all_mvs = collect_metas clenv.templval.rebus in
-  let k =
-    try list_last all_mvs
-    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
-  clenv_assign_binding clenv k c
-
-let clenv_constrain_dep_args hyps_only bl clenv =
-  if bl = [] then
-    clenv
-  else
-    let occlist = clenv_dependent hyps_only clenv in
-    if List.length occlist = List.length bl then
-      List.fold_left2 clenv_assign_binding clenv occlist bl
-    else
-      errorlabstrm ""
-	(strbrk "Not the right number of missing arguments (expected " ++
-	 int (List.length occlist) ++ str ").")
-
-(****************************************************************)
-(* Clausal environment for an application *)
-
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
-  | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args hyps_only largs clause
-  | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
-  | NoBindings ->
-      mk_clenv_from_n gls n (c,t)
-
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
-
-(****************************************************************)
-(* Pretty-print *)
-
-let pr_clenv clenv =
-  h 0
-    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
-     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
-     pr_evar_map clenv.evd)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
deleted file mode 100644
index 4f7ac40920..0000000000
--- a/pretyping/clenv.mli
+++ /dev/null
@@ -1,143 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Sign
-open Environ
-open Evd
-open Evarutil
-open Mod_subst
-open Rawterm
-open Unification
-(*i*)
-
-(***************************************************************)
-(* The Type of Constructions clausale environments. *)
-
-(* [env] is the typing context
- * [evd] is the mapping from metavar and evar numbers to their types
- *       and values.
- * [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- *)
-type clausenv = {
-  env      : env;
-  evd      : evar_map;
-  templval : constr freelisted;
-  templtyp : constr freelisted }
-
-(* Substitution is not applied on templenv (because [subst_clenv] is
-   applied only on hints which typing env is overwritten by the
-   goal env) *)
-val subst_clenv : substitution -> clausenv -> clausenv
-
-(* subject of clenv (instantiated) *)
-val clenv_value     : clausenv -> constr
-(* type of clenv (instantiated) *)
-val clenv_type      : clausenv -> types
-(* substitute resolved metas *)
-val clenv_nf_meta   : clausenv -> constr -> constr
-(* type of a meta in clenv context *)
-val clenv_meta_type : clausenv -> metavariable -> types
-
-val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
-val mk_clenv_from_n :
-  evar_info sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
-
-(***************************************************************)
-(* linking of clenvs *)
-
-val connect_clenv : evar_info sigma -> clausenv -> clausenv
-val clenv_fchain :
-  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
-
-(***************************************************************)
-(* Unification with clenvs *)
-
-(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
-val clenv_unify :
-  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
-
-(* unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
-
-(* same as above ([allow_K=false]) but replaces remaining metas
-   with fresh evars if [evars_flag] is [true] *)
-val evar_clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
-
-val clenv_dependent : bool -> clausenv -> metavariable list
-
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
-
-(***************************************************************)
-(* 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
-   start from the rightmost argument of the template. *)
-val clenv_independent : clausenv -> metavariable list
-val clenv_missing : clausenv -> metavariable list
-
-val clenv_constrain_last_binding : constr -> clausenv -> clausenv
-
-(* defines metas corresponding to the name of the bindings *)
-val clenv_match_args : arg_bindings -> clausenv -> clausenv
-
-val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
-
-(* start with a clenv to refine with a given term with bindings *)
-
-(* the arity of the lemma is fixed *)
-(* 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 -> constr bindings ->
-   clausenv
-val make_clenv_binding :
-  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
-   it produces the unification pattern [ccl]; [sigma'] is [sigma]
-   extended with [lmetas]; if [n] is defined, it limits the size of
-   the list even if [ccl] is still a product; otherwise, it stops when
-   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
-   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
-   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
-   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
-val clenv_environments :
- evar_map -> int option -> types -> evar_map * constr list * types
-
-(* [clenv_environments_evars env sigma n t] does the same but returns
-   a list of Evar's defined in [env] and extends [sigma] accordingly *)
-val clenv_environments_evars :
- env -> evar_map -> int option -> types -> evar_map * constr list * types
-
-(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
-val clenv_conv_leq :
- env -> evar_map -> types -> constr -> int -> constr list
-
-(* if the clause is a product, add an extra meta for this product *)
-exception NotExtensibleClause
-val clenv_push_prod : clausenv -> clausenv
-
-(***************************************************************)
-(* Pretty-print *)
-val pr_clenv : clausenv -> Pp.std_ppcmds
-
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 24850b4baf..6d37cf80f5 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -150,12 +150,11 @@ let evars_to_metas sigma (emap, c) =
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma =
-  let listev = to_list sigma in
-  List.fold_left
-    (fun l (ev,evi) ->
-       if evi.evar_body = Evar_empty then
-	 ((ev,nf_evar_info sigma evi)::l) else l)
-    [] listev
+  List.rev begin
+    Evd.fold_undefined begin fun ev evi l ->
+      (ev,nf_evar_info sigma evi)::l
+    end sigma []
+  end
 
 (**********************)
 (* Creating new evars *)
@@ -478,6 +477,10 @@ type clear_dependency_error =
 
 exception ClearDependencyError of identifier * clear_dependency_error
 
+open Store.Field
+
+let cleared = Store.field ()
+
 let rec check_and_clear_in_constr evdref err ids c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
@@ -539,6 +542,13 @@ let rec check_and_clear_in_constr evdref err ids c =
 	      let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
+	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
+	      let evi = Evd.find !evdref evk in
+	      let extra = evi.evar_extra in
+	      let extra' = cleared.set true extra in
+	      let evi' = { evi with evar_extra = extra' } in
+	      evdref := Evd.add !evdref evk evi' ;
+	    (* spiwack: /hacking session *)
 	      mkEvar(evk', Array.of_list nargs)
             end
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 205ca8bd64..39f8dd05ac 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -193,6 +193,10 @@ type clear_dependency_error =
 
 exception ClearDependencyError of identifier * clear_dependency_error
 
+(* spiwack: marks an evar that has been "defined" by clear. 
+    used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
+val cleared : bool Store.Field.t
+
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a9b42f052b..5b4a3f214d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -51,7 +51,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : bool list;
   evar_source : hole_kind located;
-  evar_extra : Dyn.t option}
+  evar_extra : Store.t }
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -59,7 +59,7 @@ let make_evar hyps ccl = {
   evar_body = Evar_empty;
   evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
   evar_source = (dummy_loc,InternalHole);
-  evar_extra = None
+  evar_extra = Store.empty
 }
 
 let evar_concl evi = evi.evar_concl
@@ -93,26 +93,31 @@ module ExistentialSet = Intset
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
 
+
 module EvarInfoMap = struct
-  type t = evar_info ExistentialMap.t
+  type t = evar_info ExistentialMap.t 
 
-  let empty = ExistentialMap.empty
+  let empty = ExistentialMap.empty 
+  let is_empty  = ExistentialMap.is_empty 
 
   let to_list evc = (* Workaround for change in Map.fold behavior *)
+    (* spiwack: seems to arrange the items in decreasing order.
+        Which would also be the behaviour of a naive [fold].
+        I don't understand above comment. *)
     let l = ref [] in
     ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc;
     !l
 
   let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
   let find evc k = ExistentialMap.find k evc
-  let remove evc k = ExistentialMap.remove k evc
+  let remove evc k = ExistentialMap.remove k evc 
   let mem evc k = ExistentialMap.mem k evc
   let fold = ExistentialMap.fold
   let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false
 
   let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
 
-  let equal = ExistentialMap.equal
+  let map = ExistentialMap.map
 
   let define evd evk body =
     let oldinfo =
@@ -182,6 +187,14 @@ module EvarInfoMap = struct
     try Some (existential_value sigma ev)
     with NotInstantiatedEvar -> None
 
+  (* Combinators on undefined evars. *)
+  let fold_undefined f  = ExistentialMap.fold begin fun ev evi acc -> 
+                                          match evar_body evi with
+					  | Evar_empty -> f ev evi acc
+					  | _ -> acc
+                                       end
+
+  let undefined evm = fold_undefined ExistentialMap.add evm empty
 end
 
 (*******************************************************************)
@@ -336,7 +349,23 @@ module EvarMap = struct
         (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty)
     || not (UniverseMap.equal (=) sm1 sm2))
 
-  let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
+  (* spiwack: used to workaround a bug in clenv: evar_merge
+        could merge an "old" version of an evar map into
+        a more up to date and erase evar definitions (in the case
+        of [constructor_tac] it actually erased a goal in some cases).
+       This is due to the fact that [open_constr] carry around their own
+       sigma which can be outdated by other operations. *)
+  let add_if_more_recent evd evk newinfo =
+    if newinfo.evar_body = Evar_empty && mem evd evk then
+	evd
+    else
+      add evd evk newinfo
+
+  let merge e e' = fold (fun n v sigma -> add_if_more_recent sigma n v) e' e
+
+  (* combinators on undefined values *)
+  let undefined (sigma,sm) = (EvarInfoMap.undefined sigma,sm)
+  let fold_undefined f (sigma,_) = EvarInfoMap.fold_undefined f sigma
 
 end
 
@@ -441,7 +470,6 @@ let progress_evar_map d1 d2 =
 (* spiwack: tentative. It might very well not be the semantics we want
      for merging evar_map *)
 let merge d1 d2 = {
-(* d1 with evars = EvarMap.merge d1.evars d2.evars*)
   evars = EvarMap.merge d1.evars d2.evars ;
   conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ;
   last_mods = ExistentialSet.union d1.last_mods d2.last_mods ;
@@ -488,7 +516,7 @@ let subst_evar_defs_light sub evd =
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+      evars = EvarInfoMap.map (subst_evar_info sub)  (fst evd.evars), (snd evd.evars)
   }
 
 let subst_evar_map = subst_evar_defs_light
@@ -536,7 +564,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
        evar_body = Evar_empty;
        evar_filter = filter;
        evar_source = src;
-       evar_extra = None} }
+       evar_extra = Store.empty } }
 
 let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk
 
@@ -546,12 +574,10 @@ let is_undefined_evar evd c = match kind_of_term c with
   | _ -> false
 
 let undefined_evars evd =
-  let evars =
-    EvarMap.fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then
-	    EvarMap.add sigma evk evi else sigma)
-      evd.evars EvarMap.empty
-  in
-    { evd with evars = evars }
+  let evars = EvarMap.undefined evd.evars in
+  { evd with evars = evars }
+
+let fold_undefined f evd = EvarMap.fold_undefined f evd.evars
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
@@ -694,7 +720,6 @@ let meta_with_name evd id =
            strbrk "\" occurs more than once in clause.")
 
 
-(* spiwack: we should try and replace this List.fold_left by a Metamap.fold.  *)
 let meta_merge evd1 evd2 =
   {evd2 with
     metas = List.fold_left (fun m (n,v) -> Metamap.add n v m)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b82e6d998d..f895ead42c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -123,7 +123,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : bool list;
   evar_source : hole_kind located;
-  evar_extra : Dyn.t option}
+  evar_extra : Store.t }
 
 val eq_evar_info : evar_info -> evar_info -> bool
 
@@ -185,6 +185,15 @@ val evars_reset_evd  : evar_map ->  evar_map -> evar_map
                    for moving to evarutils *)
 val is_undefined_evar :  evar_map -> constr -> bool
 val undefined_evars : evar_map -> evar_map
+(* [fold_undefined f m] iterates ("folds") function [f] over the undefined
+    evars (that is, whose value is [Evar_empty]) of map [m].
+    Making it effectively equivalent to {!Evd.fold} applies to
+    [f] and [undefined_evars m] *)
+(* spiwack: at the moment, [fold_undefined] is defined rather naively.
+    But we can hope to enable some optimisation in the future, as
+    an evar_map contains typically few undefined evars compared to all
+    its evars. *)
+val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val evar_declare :
   named_context_val -> evar -> types -> ?src:loc * hole_kind ->
       ?filter:bool list -> evar_map -> evar_map
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index cea33c1e98..6aa00c5f25 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -21,7 +21,6 @@ Typeclasses
 Classops
 Coercion
 Unification
-Clenv
 Detyping
 Indrec
 Cases
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4ec5cf1f17..88d4a4d6b3 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -355,18 +355,15 @@ let is_implicit_arg k =
    calls (e.g. when doing apply in an External hint in typeclass_instances).
    Would be solved by having real evars-as-goals. *)
 
-let ((bool_in : bool -> Dyn.t),
-    (bool_out : Dyn.t -> bool)) = Dyn.create "bool"
-
-let bool_false = bool_in false
+let resolvable = Store.field ()
+open Store.Field
 
 let is_resolvable evi =
-  match evi.evar_extra with
-      Some t -> if Dyn.tag t = "bool" then bool_out t else true
-    | None -> true
+  Option.default true (resolvable.get evi.evar_extra)
 
 let mark_unresolvable evi =
-  { evi with evar_extra = Some bool_false }
+  let t = resolvable.set false evi.evar_extra in
+  { evi with evar_extra = t }
 
 let mark_unresolvables sigma =
   Evd.fold (fun ev evi evs ->
@@ -374,7 +371,7 @@ let mark_unresolvables sigma =
     sigma Evd.empty
 
 let has_typeclasses evd =
-  Evd.fold (fun ev evi has -> has ||
+  Evd.fold_undefined (fun ev evi has -> has ||
     (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
     evd false
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 997b28c105..e53be5c0bf 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -77,10 +77,6 @@ val is_implicit_arg : hole_kind -> bool
 
 val instance_constructor : typeclass -> constr list -> constr * types
 
-(* Use evar_extra for marking resolvable evars. *)
-val bool_in : bool -> Dyn.t
-val bool_out : Dyn.t -> bool
-
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map