aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml488
-rw-r--r--proofs/clenv.mli143
-rw-r--r--proofs/clenvtac.ml1
-rw-r--r--proofs/decl_expr.mli105
-rw-r--r--proofs/decl_mode.ml127
-rw-r--r--proofs/decl_mode.mli74
-rw-r--r--proofs/evar_refiner.ml18
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/goal.ml572
-rw-r--r--proofs/goal.mli228
-rw-r--r--proofs/logic.ml287
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/pfedit.ml369
-rw-r--r--proofs/pfedit.mli57
-rw-r--r--proofs/proof.ml294
-rw-r--r--proofs/proof.mli133
-rw-r--r--proofs/proof_global.ml295
-rw-r--r--proofs/proof_global.mli89
-rw-r--r--proofs/proof_trees.ml107
-rw-r--r--proofs/proof_trees.mli48
-rw-r--r--proofs/proof_type.ml13
-rw-r--r--proofs/proof_type.mli12
-rw-r--r--proofs/proofs.mllib9
-rw-r--r--proofs/proofview.ml491
-rw-r--r--proofs/proofview.mli203
-rw-r--r--proofs/refiner.ml619
-rw-r--r--proofs/refiner.mli83
-rw-r--r--proofs/tacmach.ml51
-rw-r--r--proofs/tacmach.mli38
-rw-r--r--proofs/tactic_debug.ml12
30 files changed, 3262 insertions, 1709 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
new file mode 100644
index 0000000000..35db5e6ed1
--- /dev/null
+++ b/proofs/clenv.ml
@@ -0,0 +1,488 @@
+(************************************************************************)
+(* 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 = Refiner.pf_env
+let pf_hyps = Refiner.pf_hyps
+let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c
+let pf_concl = Tacmach.pf_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 (pf_env gls) 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 =
+ let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+ if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
+ clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) concl
+ (clenv_unify_meta_types ~flags:flags clenv)
+ else
+ clenv_unify allow_K CUMUL ~flags:flags
+ (meta_reducible_instance clenv.evd clenv.templtyp) concl 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 =
+ let evd = Evd.fold begin fun ev evi acc ->
+ if evi.evar_body = Evar_empty then
+ acc
+ else
+ Evd.add acc ev evi
+ end
+ clenv.evd gls.sigma
+ in
+ let evd = evars_reset_evd evd clenv.evd in
+ { clenv with
+ evd = evd ;
+ env = Goal.V82.env evd (sig_it gls) }
+
+(* [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/proofs/clenv.mli b/proofs/clenv.mli
new file mode 100644
index 0000000000..2533fc5379
--- /dev/null
+++ b/proofs/clenv.mli
@@ -0,0 +1,143 @@
+(************************************************************************)
+(* 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 : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from_n :
+ Goal.goal sigma -> int option -> constr * types -> clausenv
+val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+
+(***************************************************************)
+(* linking of clenvs *)
+
+val connect_clenv : Goal.goal 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 -> Goal.goal 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 -> Goal.goal 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 :
+ Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+ clausenv
+val make_clenv_binding :
+ Goal.goal 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/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 9bc818e861..f977768bd6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -20,7 +20,6 @@ open Evd
open Evarutil
open Proof_type
open Refiner
-open Proof_trees
open Logic
open Reduction
open Reductionops
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
deleted file mode 100644
index 20a95dabff..0000000000
--- a/proofs/decl_expr.mli
+++ /dev/null
@@ -1,105 +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 Names
-open Util
-open Tacexpr
-
-type 'it statement =
- {st_label:name;
- st_it:'it}
-
-type thesis_kind =
- Plain
- | For of identifier
-
-type 'this or_thesis =
- This of 'this
- | Thesis of thesis_kind
-
-type side = Lhs | Rhs
-
-type elim_type =
- ET_Case_analysis
- | ET_Induction
-
-type block_type =
- B_proof
- | B_claim
- | B_focus
- | B_elim of elim_type
-
-type ('it,'constr,'tac) cut =
- {cut_stat: 'it;
- cut_by: 'constr list option;
- cut_using: 'tac option}
-
-type ('var,'constr) hyp =
- Hvar of 'var
- | Hprop of 'constr statement
-
-type ('constr,'tac) casee =
- Real of 'constr
- | Virtual of ('constr statement,'constr,'tac) cut
-
-type ('hyp,'constr,'pat,'tac) bare_proof_instr =
- | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
- | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
- | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
- | Pcut of ('constr or_thesis statement,'constr,'tac) cut
- | Prew of side * ('constr statement,'constr,'tac) cut
- | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
- | Passume of ('hyp,'constr) hyp list
- | Plet of ('hyp,'constr) hyp list
- | Pgiven of ('hyp,'constr) hyp list
- | Pconsider of 'constr*('hyp,'constr) hyp list
- | Pclaim of 'constr statement
- | Pfocus of 'constr statement
- | Pdefine of identifier * 'hyp list * 'constr
- | Pcast of identifier or_thesis * 'constr
- | Psuppose of ('hyp,'constr) hyp list
- | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
- | Ptake of 'constr list
- | Pper of elim_type * ('constr,'tac) casee
- | Pend of block_type
- | Pescape
-
-type emphasis = int
-
-type ('hyp,'constr,'pat,'tac) gen_proof_instr=
- {emph: emphasis;
- instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
-
-
-type raw_proof_instr =
- ((identifier*(Topconstr.constr_expr option)) located,
- Topconstr.constr_expr,
- Topconstr.cases_pattern_expr,
- raw_tactic_expr) gen_proof_instr
-
-type glob_proof_instr =
- ((identifier*(Genarg.rawconstr_and_expr option)) located,
- Genarg.rawconstr_and_expr,
- Topconstr.cases_pattern_expr,
- Tacexpr.glob_tactic_expr) gen_proof_instr
-
-type proof_pattern =
- {pat_vars: Term.types statement list;
- pat_aliases: (Term.constr*Term.types) statement list;
- pat_constr: Term.constr;
- pat_typ: Term.types;
- pat_pat: Rawterm.cases_pattern;
- pat_expr: Topconstr.cases_pattern_expr}
-
-type proof_instr =
- (Term.constr statement,
- Term.constr,
- proof_pattern,
- Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
deleted file mode 100644
index ba675327c6..0000000000
--- a/proofs/decl_mode.ml
+++ /dev/null
@@ -1,127 +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*)
-
-open Names
-open Term
-open Evd
-open Util
-
-let daimon_flag = ref false
-
-let set_daimon_flag () = daimon_flag:=true
-let clear_daimon_flag () = daimon_flag:=false
-let get_daimon_flag () = !daimon_flag
-
-type command_mode =
- Mode_tactic
- | Mode_proof
- | Mode_none
-
-let mode_of_pftreestate pts =
- let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
- if goal.evar_extra = None then
- Mode_tactic
- else
- Mode_proof
-
-let get_current_mode () =
- try
- mode_of_pftreestate (Pfedit.get_pftreestate ())
- with _ -> Mode_none
-
-let check_not_proof_mode str =
- if get_current_mode () = Mode_proof then
- error str
-
-type split_tree=
- Skip_patt of Idset.t * split_tree
- | Split_patt of Idset.t * inductive *
- (bool array * (Idset.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (identifier * (int * int))
-
-type elim_kind =
- EK_dep of split_tree
- | EK_nodep
- | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
- {per_casee:constr;
- per_ctype:types;
- per_ind:inductive;
- per_pred:constr;
- per_args:constr list;
- per_params:constr list;
- per_nparams:int;
- per_wf:recpath}
-
-type stack_info =
- Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
- | Suppose_case
- | Claim
- | Focus_claim
-
-type pm_info =
- { pm_stack : stack_info list}
-
-let pm_in,pm_out = Dyn.create "pm_info"
-
-let get_info gl=
- match gl.evar_extra with
- None -> invalid_arg "get_info"
- | Some extra ->
- try pm_out extra with _ -> invalid_arg "get_info"
-
-let get_stack pts =
- let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
- info.pm_stack
-
-let get_top_stack pts =
- let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
- info.pm_stack
-
-let get_end_command pts =
- match mode_of_pftreestate pts with
- Mode_proof ->
- Some
- begin
- match get_top_stack pts with
- [] -> "\"end proof\""
- | Claim::_ -> "\"end claim\""
- | Focus_claim::_-> "\"end focus\""
- | (Suppose_case :: Per (et,_,_,_) :: _
- | Per (et,_,_,_) :: _ ) ->
- begin
- match et with
- Decl_expr.ET_Case_analysis ->
- "\"end cases\" or start a new case"
- | Decl_expr.ET_Induction ->
- "\"end induction\" or start a new case"
- end
- | _ -> anomaly "lonely suppose"
- end
- | Mode_tactic ->
- begin
- try
- ignore
- (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
- Some "\"return\""
- with Not_found -> None
- end
- | Mode_none ->
- error "no proof in progress"
-
-let get_last env =
- try
- let (id,_,_) = List.hd (Environ.named_context env) in id
- with Invalid_argument _ -> error "no previous statement to use"
-
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
deleted file mode 100644
index 734dc04421..0000000000
--- a/proofs/decl_mode.mli
+++ /dev/null
@@ -1,74 +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 Names
-open Term
-open Evd
-open Tacmach
-
-val set_daimon_flag : unit -> unit
-val clear_daimon_flag : unit -> unit
-val get_daimon_flag : unit -> bool
-
-type command_mode =
- Mode_tactic
- | Mode_proof
- | Mode_none
-
-val mode_of_pftreestate : pftreestate -> command_mode
-
-val get_current_mode : unit -> command_mode
-
-val check_not_proof_mode : string -> unit
-
-type split_tree=
- Skip_patt of Idset.t * split_tree
- | Split_patt of Idset.t * inductive *
- (bool array * (Idset.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (identifier * (int * int))
-
-type elim_kind =
- EK_dep of split_tree
- | EK_nodep
- | EK_unknown
-
-type recpath = int option*Declarations.wf_paths
-
-type per_info =
- {per_casee:constr;
- per_ctype:types;
- per_ind:inductive;
- per_pred:constr;
- per_args:constr list;
- per_params:constr list;
- per_nparams:int;
- per_wf:recpath}
-
-type stack_info =
- Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
- | Suppose_case
- | Claim
- | Focus_claim
-
-type pm_info =
- {pm_stack : stack_info list }
-
-val pm_in : pm_info -> Dyn.t
-
-val get_info : Proof_type.goal -> pm_info
-
-val get_end_command : pftreestate -> string option
-
-val get_stack : pftreestate -> stack_info list
-
-val get_top_stack : pftreestate -> stack_info list
-
-val get_last: Environ.env -> identifier
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e4fab3f2f8..6dfbbdc121 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -14,7 +14,6 @@ open Term
open Evd
open Evarutil
open Sign
-open Proof_trees
open Refiner
(******************************************)
@@ -55,19 +54,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
(* vernac command Existential *)
-let instantiate_pf_com n com pfts =
- let gls = top_goal_of_pftreestate pfts in
- let sigma = gls.sigma in
- let (evk,evi) =
- let evl = Evarutil.non_instantiated sigma in
- if (n <= 0) then
- error "incorrect existential variable index"
- else if List.length evl < n then
- error "not so many uninstantiated existential variables"
- else
- List.nth evl (n-1)
- in
+(* Main component of vernac command Existential *)
+let instantiate_pf_com evk com sigma =
+ let evi = Evd.find sigma evk in
let env = Evd.evar_env evi in
let rawc = Constrintern.intern_constr sigma env com in
let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
- change_constraints_pftreestate sigma' pfts
+ sigma'
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 0bd6168095..28c79d11e9 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -24,6 +24,6 @@ val w_refine : evar * evar_info ->
(var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map
val instantiate_pf_com :
- int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+ Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
new file mode 100644
index 0000000000..a9202318df
--- /dev/null
+++ b/proofs/goal.ml
@@ -0,0 +1,572 @@
+(************************************************************************)
+(* 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 Lesscer General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+
+(* This module implements the abstract interface to goals *)
+(* A general invariant of the module, is that a goal whose associated
+ evar is defined in the current evar_map, should not be accessed. *)
+
+(* type of the goals *)
+type goal = {
+ content : Evd.evar; (* Corresponding evar. Allows to retrieve
+ logical information once put together
+ with an evar_map. *)
+ tags : string list (* Heriditary? tags to be displayed *)
+}
+(* spiwack: I don't deal with the tags, yet. It is a worthy discussion
+ whether we do want some tags displayed besides the goal or not. *)
+
+(* access primitive *)
+(* invariant : [e] must exist in [em] *)
+let content evars { content = e } = Evd.find evars e
+
+
+(* Builds a new (empty) goal with evar [e] *)
+let build e =
+ { content = e ;
+ tags = []
+ }
+
+(* Builds a new goal with content evar [e] and
+ inheriting from goal [gl]*)
+let descendent gl e =
+ { gl with content = e}
+
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and
+ is the current avatar of [g] (for instance [g] was changed by [clear]
+ into [g']). It returns [None] if [g] has been (partially) solved. *)
+open Store.Field
+let rec advance sigma g =
+ let evi = Evd.find sigma g.content in
+ if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
+ let v =
+ match evi.Evd.evar_body with
+ | Evd.Evar_defined c -> c
+ | _ -> Util.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
+ in
+ let (e,_) = Term.destEvar v in
+ let g' = { g with content = e } in
+ advance sigma g'
+ else
+ match evi.Evd.evar_body with
+ | Evd.Evar_defined _ -> None
+ | _ -> Some g
+
+(*** Goal tactics ***)
+
+
+(* Goal tactics are [subgoal sensitive]-s *)
+type subgoals = { subgoals: goal list }
+
+(* type of the base elements of the goal API.*)
+(* it has an extra evar_info with respect to what would be expected,
+ it is supposed to be the evar_info of the goal in the evar_map.
+ The idea is that it is computed by the [run] function as an
+ optimisation, since it will generaly not change during the
+ evaluation. *)
+type 'a sensitive =
+ Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
+
+(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
+(* the evar_info corresponding to the goal is computed at once
+ as an optimisation (it shouldn't change during the evaluation). *)
+let eval t env defs gl =
+ let info = content defs gl in
+ let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
+ let rdefs = ref defs in
+ let r = t env rdefs gl info in
+ ( r , !rdefs )
+
+(* monadic bind on sensitive expressions *)
+let bind e f env rdefs goal info =
+ f (e env rdefs goal info) env rdefs goal info
+
+(* monadic return on sensitive expressions *)
+let return v _ _ _ _ = v
+
+(* interpretation of "open" constr *)
+(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
+ In an ideal world, this could/should be the other way round.
+ As of now, though, it seems at least quite useful to build tactics. *)
+let interp_constr cexpr env rdefs _ _ =
+ let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in
+ rdefs := defs ;
+ c
+
+(* Type of constr with holes used by refine. *)
+(* The list of evars doesn't necessarily contain all the evars in the constr,
+ only those the constr has introduced. *)
+(* The variables in [myevars] are supposed to be stored
+ in decreasing order. Breaking this invariant might cause
+ many things to go wrong. *)
+type refinable = {
+ me: constr;
+ my_evars: Evd.evar list
+}
+
+module Refinable = struct
+ type t = refinable
+
+ type handle = Evd.evar list ref
+
+ let make t env rdefs gl info =
+ let r = ref [] in
+ let me = t r env rdefs gl info in
+ { me = me;
+ my_evars = !r }
+ let make_with t env rdefs gl info =
+ let r = ref [] in
+ let (me,side) = t r env rdefs gl info in
+ { me = me ; my_evars = !r } , side
+
+ let mkEvar handle env typ _ rdefs _ _ =
+ let ev = Evarutil.e_new_evar rdefs env typ in
+ let (e,_) = Term.destEvar ev in
+ handle := e::!handle;
+ ev
+
+ (* [with_type c typ] constrains term [c] to have type [typ]. *)
+ let with_type t typ env rdefs _ _ =
+ (* spiwack: this function assumes that no evars can be created during
+ this sort of coercion.
+ If it is not the case it could produce bugs. We would need to add a handle
+ and add the new evars to it. *)
+ let my_type = Retyping.get_type_of env !rdefs t in
+ let j = Environ.make_judge t my_type in
+ let tycon = Evarutil.mk_tycon_type typ in
+ let (new_defs,j') =
+ Coercion.Default.inh_conv_coerce_to (Util.dummy_loc) env !rdefs j tycon
+ in
+ rdefs := new_defs;
+ j'.Environ.uj_val
+
+ (* spiwack: it is not very fine grain since it solves all typeclasses holes,
+ not only those containing the current goal, or a given term. But it
+ seems to fit our needs so far. *)
+ let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
+ rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs;
+ ()
+
+
+
+ (* a pessimistic (i.e : there won't be many positive answers) filter
+ over evar_maps *)
+ let evar_map_filter f evm =
+ Evd.fold (fun ev evi r ->
+ if f ev evi then
+ Evd.add r ev evi
+ else
+ r
+ )
+ evm
+ Evd.empty
+
+ (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
+ let rec fusion l1 l2 = match l1 , l2 with
+ | [] , _ -> l2
+ | _ , [] -> l1
+ | a::l1 , b::_ when a>b -> a::(fusion l1 l2)
+ | a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
+ | _ , b::l2 -> b::(fusion l1 l2)
+
+ (* [constr_of_raw] is a pretyping function. The [check_type] argument
+ asks whether the term should have the same type as the conclusion.
+ [resolve_classes] is a flag on pretyping functions which, if set to true,
+ calls the typeclass resolver.
+ The principal argument is a [rawconstr] which is then pretyped in the
+ context of a term, the remaining evars are registered to the handle.
+ It is the main component of the toplevel refine tactic.*)
+ (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
+ a bit hackish. However it does not seem possible to move it out until
+ pretyping is defined as some proof procedure. *)
+ let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info =
+ (* We need to keep trace of what [rdefs] was originally*)
+ let init_defs = !rdefs in
+ (* if [check_type] is true, then creates a type constraint for the
+ proof-to-be *)
+ let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
+ (* call to [understand_tcc_evars] returns a constr with undefined evars
+ these evars will be our new goals *)
+ let open_constr =
+ Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
+ in
+ (* [!rdefs] contains the evar_map outputed by [understand_...] *)
+ let post_defs = !rdefs in
+ (* [delta_evars] holds the evars that have been introduced by this
+ refinement (but not immediatly solved) *)
+ (* spiwack: this is the hackish part, don't know how to do any better though. *)
+ let delta_evars = evar_map_filter (fun ev evi ->
+ evi.Evd.evar_body = Evd.Evar_empty &&
+ not (Evd.mem init_defs ev)
+ )
+ post_defs
+ in
+ (* [delta_evars] in the shape of a list of [evar]-s*)
+ let delta_list = List.map fst (Evd.to_list delta_evars) in
+ (* The variables in [myevars] are supposed to be stored
+ in decreasing order. Breaking this invariant might cause
+ many things to go wrong. *)
+ handle := fusion delta_list !handle ;
+ open_constr
+
+end
+
+(* [refine t] takes a refinable term and use it as a partial proof for current
+ goal. *)
+let refine step env rdefs gl info =
+ (* subgoals to return *)
+ (* The evars in [my_evars] are stored in reverse order.
+ It is expectingly better however to display the goal
+ in increasing order. *)
+ rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ;
+ let subgoals = List.map (descendent gl) (List.rev step.my_evars) in
+ (* creates the new [evar_map] by defining the evar of the current goal
+ as being [refine_step]. *)
+ let new_defs = Evd.define gl.content (step.me) !rdefs in
+ rdefs := new_defs;
+ (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
+ let subgoals =
+ Option.List.flatten (List.map (advance !rdefs) subgoals)
+ in
+ { subgoals = subgoals }
+
+
+(*** Cleaning goals ***)
+
+let clear ids env rdefs gl info =
+ let hyps = Evd.evar_hyps info in
+ let concl = Evd.evar_concl info in
+ let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
+ let cleared_env = Environ.reset_with_named_context hyps env in
+ let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
+ let (cleared_evar,_) = Term.destEvar cleared_concl in
+ let cleared_goal = descendent gl cleared_evar in
+ rdefs := Evd.define gl.content cleared_concl !rdefs;
+ { subgoals = [cleared_goal] }
+
+let wrap_apply_to_hyp_and_dependent_on sign id f g =
+ try Environ.apply_to_hyp_and_dependent_on sign id f g
+ with Environ.Hyp_not_found ->
+ Util.error "No such assumption"
+
+let check_typability env sigma c =
+ let _ = Typing.type_of env sigma c in ()
+
+let recheck_typability (what,id) env sigma t =
+ try check_typability env sigma t
+ with _ ->
+ let s = match what with
+ | None -> "the conclusion"
+ | Some id -> "hypothesis "^(Names.string_of_id id) in
+ Util.error
+ ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))
+
+let remove_hyp_body env sigma id =
+ let sign =
+ wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
+ (fun (_,c,t) _ ->
+ match c with
+ | None -> Util.error ((Names.string_of_id id)^" is not a local definition")
+ | Some c ->(id,None,t))
+ (fun (id',c,t as d) sign ->
+ (
+ begin
+ let env = Environ.reset_with_named_context sign env in
+ match c with
+ | None -> recheck_typability (Some id',id) env sigma t
+ | Some b ->
+ let b' = mkCast (b,DEFAULTcast, t) in
+ recheck_typability (Some id',id) env sigma b'
+ end;d))
+ in
+ Environ.reset_with_named_context sign env
+
+
+let clear_body idents env rdefs gl info =
+ let info = content !rdefs gl in
+ let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
+ let aux env id =
+ let env' = remove_hyp_body env !rdefs id in
+ recheck_typability (None,id) env' !rdefs (Evd.evar_concl info);
+ env'
+ in
+ let new_env =
+ List.fold_left aux full_env idents
+ in
+ let concl = Evd.evar_concl info in
+ let (defs',new_constr) = Evarutil.new_evar !rdefs new_env concl in
+ let (new_evar,_) = destEvar new_constr in
+ let new_goal = descendent gl new_evar in
+ rdefs := Evd.define gl.content new_constr defs';
+ { subgoals = [new_goal] }
+
+
+(*** Sensitive primitives ***)
+
+(* [concl] is the conclusion of the current goal *)
+let concl _ _ _ info =
+ Evd.evar_concl info
+
+(* [hyps] is the [named_context_val] representing the hypotheses
+ of the current goal *)
+let hyps _ _ _ info =
+ Evd.evar_hyps info
+
+(* [env] is the current [Environ.env] containing both the
+ environment in which the proof is ran, and the goal hypotheses *)
+let env env _ _ _ = env
+
+(* [defs] is the [Evd.evar_map] at the current evaluation point *)
+let defs _ rdefs _ _ =
+ !rdefs
+
+(* Cf mli for more detailed comment.
+ [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
+ to communicate whether or not the value is defined in the particular context. *)
+exception UndefinedHere
+let null _ _ _ _ = raise UndefinedHere
+
+let plus s1 s2 env rdefs goal info =
+ try s1 env rdefs goal info
+ with UndefinedHere -> s2 env rdefs goal info
+
+(* Equality of two goals *)
+let equal { content = e1 } { content = e2 } = e1 = e2
+
+let here goal value _ _ goal' _ =
+ if equal goal goal' then
+ value
+ else
+ raise UndefinedHere
+
+(* arnaud: voir Ă  la passer dans Util ? *)
+let rec list_mem_with eq x = function
+ | y::_ when eq x y -> true
+ | _::l -> list_mem_with eq x l
+ | [] -> false
+
+let here_list goals value _ _ goal' _ =
+ if list_mem_with equal goal' goals then
+ value
+ else
+ raise UndefinedHere
+
+
+(*** Conversion in goals ***)
+
+let convert_hyp check (id,b,bt as d) env rdefs gl info =
+ let sigma = !rdefs in
+ (* This function substitutes the new type and body definitions
+ in the appropriate variable when used with {!Environ.apply_hyps}. *)
+ let replace_function =
+ (fun _ (_,c,ct) _ ->
+ if check && not (Reductionops.is_conv env sigma bt ct) then
+ Util.error ("Incorrect change of the type of "^(Names.string_of_id id));
+ if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
+ Util.error ("Incorrect change of the body of "^(Names.string_of_id id));
+ d)
+ in
+ (* Modified named context. *)
+ let new_hyps =
+ Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
+ in
+ let new_env = Environ.reset_with_named_context new_hyps env in
+ let new_constr =
+ Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
+ in
+ let (new_evar,_) = Term.destEvar new_constr in
+ let new_goal = descendent gl new_evar in
+ rdefs := Evd.define gl.content new_constr !rdefs;
+ { subgoals = [new_goal] }
+
+let convert_concl check cl' env rdefs gl info =
+ let sigma = !rdefs in
+ let cl = concl env rdefs gl info in
+ check_typability env sigma cl';
+ if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
+ let new_constr =
+ Evarutil.e_new_evar rdefs env cl'
+ in
+ let (new_evar,_) = Term.destEvar new_constr in
+ let new_goal = descendent gl new_evar in
+ rdefs := Evd.define gl.content new_constr !rdefs;
+ { subgoals = [new_goal] }
+ else
+ Util.error "convert-concl rule passed non-converting term"
+
+
+(*** Bureaucracy in hypotheses ***)
+
+(* Renames a hypothesis. *)
+let rename_hyp_sign id1 id2 sign =
+ Environ.apply_to_hyp_and_dependent_on sign id1
+ (fun (_,b,t) _ -> (id2,b,t))
+ (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
+let rename_hyp id1 id2 env rdefs gl info =
+ let hyps = hyps env rdefs gl info in
+ if id1 <> id2 &&
+ List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
+ Util.error ((Names.string_of_id id2)^" is already used.");
+ let new_hyps = rename_hyp_sign id1 id2 hyps in
+ let new_env = Environ.reset_with_named_context new_hyps env in
+ let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
+ let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
+ let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
+ let (new_evar,_) = Term.destEvar new_subproof in
+ let new_goal = descendent gl new_evar in
+ rdefs := Evd.define gl.content new_subproof !rdefs;
+ { subgoals = [new_goal] }
+
+(*** Additional functions ***)
+
+(* emulates List.map for functions of type
+ [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
+ new evar_map to next definition. *)
+(*This sort of construction actually works with any monad (here the State monade
+ in Haskell). There is a generic construction in Haskell called mapM.
+*)
+let rec list_map f l s =
+ match l with
+ | [] -> ([],s)
+ | a::l -> let (a,s) = f s a in
+ let (l,s) = list_map f l s in
+ (a::l,s)
+
+
+(* Layer to implement v8.2 tactic engine ontop of the new architecture.
+ Types are different from what they used to be due to a change of the
+ internal types. *)
+module V82 = struct
+
+ (* Old style env primitive *)
+ let env evars gl =
+ let evi = content evars gl in
+ Evd.evar_env evi
+
+ (* For printing *)
+ let unfiltered_env evars gl =
+ let evi = content evars gl in
+ Evd.evar_unfiltered_env evi
+
+ (* Old style hyps primitive *)
+ let hyps evars gl =
+ let evi = content evars gl in
+ evi.Evd.evar_hyps
+
+ (* Access to ".evar_concl" *)
+ let concl evars gl =
+ let evi = content evars gl in
+ evi.Evd.evar_concl
+
+ (* Access to ".evar_extra" *)
+ let extra evars gl =
+ let evi = content evars gl in
+ evi.Evd.evar_extra
+
+ (* Old style filtered_context primitive *)
+ let filtered_context evars gl =
+ let evi = content evars gl in
+ Evd.evar_filtered_context evi
+
+ (* Old style mk_goal primitive *)
+ let mk_goal evars hyps concl extra =
+ let evk = Evarutil.new_untyped_evar () in
+ let evi = { Evd.evar_hyps = hyps;
+ Evd.evar_concl = concl;
+ Evd.evar_filter = List.map (fun _ -> true)
+ (Environ.named_context_of_val hyps);
+ Evd.evar_body = Evd.Evar_empty;
+ Evd.evar_source = (Util.dummy_loc,Evd.GoalEvar);
+ Evd.evar_extra = extra }
+ in
+ let evi = Typeclasses.mark_unresolvable evi in
+ let evars = Evd.add evars evk evi in
+ let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in
+ let inst = Array.of_list (List.map mkVar ids) in
+ let ev = Term.mkEvar (evk,inst) in
+ (build evk, ev, evars)
+
+ (* Equality function on goals *)
+ let equal evars gl1 gl2 =
+ let evi1 = content evars gl1 in
+ let evi2 = content evars gl2 in
+ Evd.eq_evar_info evi1 evi2
+
+ (* Creates a dummy [goal sigma] for use in auto *)
+ let dummy_goal =
+ (* This goal seems to be marshalled somewhere. Therefore it cannot be
+ marked unresolvable for typeclasses, as non-empty Store.t-s happen
+ to have functional content. *)
+ let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
+ let evk = Evarutil.new_untyped_evar () in
+ let sigma = Evd.add Evd.empty evk evi in
+ { Evd.it = build evk ; Evd.sigma = sigma }
+
+ (* Makes a goal out of an evar *)
+ let build = build
+
+ (* Instantiates a goal with an open term *)
+ let partial_solution sigma { content=evk } c =
+ Evd.define evk c sigma
+
+ (* Parts of the progress tactical *)
+ let same_goal evars1 gl1 evars2 gl2 =
+ let evi1 = content evars1 gl1 in
+ let evi2 = content evars2 gl2 in
+ Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+ Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
+
+ let weak_progress glss gls =
+ match glss.Evd.it with
+ | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
+ | _ -> true
+
+ let progress glss gls =
+ weak_progress glss gls
+ (* spiwack: progress normally goes like this:
+ (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
+ This is immensly slow in the current implementation. Maybe we could
+ reimplement progress_evar_map with restricted folds like "fold_undefined",
+ with a good implementation of them.
+ *)
+
+ (* Used for congruence closure *)
+ let new_goal_with sigma gl new_hyps =
+ let evi = content sigma gl in
+ let new_evi = { evi with Evd.evar_hyps = new_hyps } in
+ let new_evi = Typeclasses.mark_unresolvable new_evi in
+ let evk = Evarutil.new_untyped_evar () in
+ let new_sigma = Evd.add Evd.empty evk new_evi in
+ { Evd.it = build evk ; sigma = new_sigma }
+
+ (* Used by the typeclasses *)
+ let nf_evar sigma gl =
+ let evi = content sigma gl in
+ let evi = Evarutil.nf_evar_info sigma evi in
+ let sigma = Evd.add sigma gl.content evi in
+ (gl,sigma)
+
+ (* Goal represented as a type, doesn't take into account section variables *)
+ let abstract_type sigma gl =
+ let (gl,sigma) = nf_evar sigma gl in
+ let env = env sigma gl in
+ let genv = Global.env () in
+ let is_proof_var decl =
+ try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
+ with Not_found -> true in
+ Environ.fold_named_context_reverse (fun t decl ->
+ if is_proof_var decl then
+ mkNamedProd_or_LetIn decl t
+ else
+ t
+ ) ~init:(concl sigma gl) env
+
+end
diff --git a/proofs/goal.mli b/proofs/goal.mli
new file mode 100644
index 0000000000..49e3c9b1ae
--- /dev/null
+++ b/proofs/goal.mli
@@ -0,0 +1,228 @@
+(************************************************************************)
+(* 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: goal.mli aspiwack $ *)
+
+(* This module implements the abstract interface to goals *)
+
+type goal
+
+(* spiwack: this primitive is not extremely brilliant. It may be a good
+ idea to define goals and proof views in the same file to avoid this
+ sort of communication pipes. But I find it heavy. *)
+val build : Evd.evar -> goal
+
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and
+ is the current avatar of [g] (for instance [g] was changed by [clear]
+ into [g']). It returns [None] if [g] has been (partially) solved. *)
+open Store.Field
+val advance : Evd.evar_map -> goal -> goal option
+
+
+(*** Goal tactics ***)
+
+
+(* Goal tactics are [subgoal sensitive]-s *)
+type subgoals = private { subgoals: goal list }
+
+(* Goal sensitive values *)
+type +'a sensitive
+
+(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
+val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map
+
+(* monadic bind on sensitive expressions *)
+val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive
+
+(* monadic return on sensitive expressions *)
+val return : 'a -> 'a sensitive
+
+
+(* interpretation of "open" constr *)
+(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
+ In an ideal world, this could/should be the other way round.
+ As of now, though, it seems at least quite useful to build tactics. *)
+val interp_constr : Topconstr.constr_expr -> Term.constr sensitive
+
+(* Type of constr with holes used by refine. *)
+type refinable
+
+module Refinable : sig
+ type t = refinable
+ type handle
+
+ val make : (handle -> Term.constr sensitive) -> refinable sensitive
+ val make_with : (handle -> (Term.constr*'a) sensitive) -> (refinable*'a) sensitive
+
+ val mkEvar : handle -> Environ.env -> Term.types -> Term.constr sensitive
+
+ (* [with_type c typ] constrains term [c] to have type [typ]. *)
+ val with_type : Term.constr -> Term.types -> Term.constr sensitive
+
+ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+
+
+ (* [constr_of_raw h check_type resolve_classes] is a pretyping function.
+ The [check_type] argument asks whether the term should have the same
+ type as the conclusion. [resolve_classes] is a flag on pretyping functions
+ which, if set to true, calls the typeclass resolver.
+ The principal argument is a [rawconstr] which is then pretyped in the
+ context of a term, the remaining evars are registered to the handle.
+ It is the main component of the toplevel refine tactic.*)
+ val constr_of_raw :
+ handle -> bool -> bool -> Rawterm.rawconstr -> Term.constr sensitive
+
+end
+
+(* [refine t] takes a refinable term and use it as a partial proof for current
+ goal. *)
+val refine : refinable -> subgoals sensitive
+
+
+(*** Cleaning goals ***)
+
+(* Implements the [clear] tactic *)
+val clear : Names.identifier list -> subgoals sensitive
+
+(* Implements the [clearbody] tactic *)
+val clear_body : Names.identifier list -> subgoals sensitive
+
+
+(*** Conversion in goals ***)
+
+(* Changes an hypothesis of the goal with a convertible type and body.
+ Checks convertibility if the boolean argument is true. *)
+val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive
+
+(* Changes the conclusion of the goal with a convertible type and body.
+ Checks convertibility if the boolean argument is true. *)
+val convert_concl : bool -> Term.constr -> subgoals sensitive
+
+(*** Bureaucracy in hypotheses ***)
+
+(* Renames a hypothesis. *)
+val rename_hyp : Names.identifier -> Names.identifier -> subgoals sensitive
+
+(*** Sensitive primitives ***)
+
+(* [concl] is the conclusion of the current goal *)
+val concl : Term.constr sensitive
+
+(* [hyps] is the [named_context_val] representing the hypotheses
+ of the current goal *)
+val hyps : Environ.named_context_val sensitive
+
+(* [env] is the current [Environ.env] containing both the
+ environment in which the proof is ran, and the goal hypotheses *)
+val env : Environ.env sensitive
+
+(* [defs] is the [Evd.evar_map] at the current evaluation point *)
+val defs : Evd.evar_map sensitive
+
+(* These four functions serve as foundation for the goal sensitive part
+ of the tactic monad (see Proofview).
+ [here] is a special sort of [return]: [here g a] is the value [a], but
+ does not have any value (it raises an exception) if evaluated in
+ any other goal than [g].
+ [here_list] is the same, except with a list of goals rather than a single one.
+ [plus a b] is the same as [a] if [a] is defined in the current goal, otherwise
+ it is [b]. Effectively it's defined in the goals where [a] and [b] are defined.
+ [null] is defined in no goal. (it is a neutral element for [plus]). *)
+(* spiwack: these primitives are a bit hackish, but I couldn't find another way
+ to pass information between goals, like for an intro tactic which gives to
+ each goal the name of the variable it introduce.
+ In pratice, in my experience, the primitives given in Proofview (in terms of
+ [here] and [plus]) are sufficient to define any tactics, hence these might
+ be another example of communication primitives between Goal and Proofview.
+ Still, I can't see a way to prevent using the Proofview primitive to read
+ a goal sensitive value out of its valid context. *)
+val null : 'a sensitive
+
+val plus : 'a sensitive -> 'a sensitive -> 'a sensitive
+
+val here : goal -> 'a -> 'a sensitive
+
+val here_list : goal list -> 'a -> 'a sensitive
+
+(*** Additional functions ***)
+
+(* emulates List.map for functions of type
+ [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
+ new evar_map to next definition *)
+val list_map : (Evd.evar_map -> 'a -> 'b * Evd.evar_map) ->
+ 'a list ->
+ Evd.evar_map ->
+ 'b list *Evd.evar_map
+
+(* Layer to implement v8.2 tactic engine ontop of the new architecture.
+ Types are different from what they used to be due to a change of the
+ internal types. *)
+module V82 : sig
+
+ (* Old style env primitive *)
+ val env : Evd.evar_map -> goal -> Environ.env
+
+ (* For printing *)
+ val unfiltered_env : Evd.evar_map -> goal -> Environ.env
+
+ (* Old style hyps primitive *)
+ val hyps : Evd.evar_map -> goal -> Environ.named_context_val
+
+ (* Access to ".evar_concl" *)
+ val concl : Evd.evar_map -> goal -> Term.constr
+
+ (* Access to ".evar_extra" *)
+ val extra : Evd.evar_map -> goal -> Store.t
+
+ (* Old style filtered_context primitive *)
+ val filtered_context : Evd.evar_map -> goal -> Sign.named_context
+
+ (* Old style mk_goal primitive, returns a new goal with corresponding
+ hypotheses and conclusion, together with a term which is precisely
+ the evar corresponding to the goal, and an updated evar_map. *)
+ val mk_goal : Evd.evar_map ->
+ Environ.named_context_val ->
+ Term.constr ->
+ Store.t ->
+ goal * Term.constr * Evd.evar_map
+
+ (* Equality function on goals *)
+ val equal : Evd.evar_map -> goal -> goal -> bool
+
+ (* Creates a dummy [goal sigma] for use in auto *)
+ val dummy_goal : goal Evd.sigma
+
+ (* Makes a goal out of an evar *)
+ (* spiwack: used by [Proofview.init], not entirely clean probably, but it is
+ the only way I could think of to preserve compatibility with previous Coq
+ stuff. *)
+ val build : Evd.evar -> goal
+
+
+ (* Instantiates a goal with an open term *)
+ val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+
+ (* Principal part of the weak-progress tactical *)
+ val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
+
+ (* Principal part of the progress tactical *)
+ val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
+
+ (* Principal part of tclNOTSAMEGOAL *)
+ val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
+
+ (* Used for congruence closure *)
+ val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma
+
+ (* Used by the typeclasses *)
+ val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
+
+ (* Goal represented as a type, doesn't take into account section variables *)
+ val abstract_type : Evd.evar_map -> goal -> Term.types
+
+end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 11155d3698..7c092bb66e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,7 +21,6 @@ open Reductionops
open Inductive
open Inductiveops
open Typing
-open Proof_trees
open Proof_type
open Typeops
open Type_errors
@@ -326,22 +325,18 @@ let goal_type_of env sigma c =
(if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c
let rec mk_refgoals sigma goal goalacc conclty trm =
- let env = evar_env goal in
- let hyps = goal.evar_hyps in
- let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
-(*
- if not (occur_meta trm) then
- let t'ty = (unsafe_machine env sigma trm).uj_type in
- let _ = conv_leq_goal env sigma trm t'ty conclty in
- (goalacc,t'ty)
- else
-*)
+ let env = Goal.V82.env sigma goal in
+ let hyps = Goal.V82.hyps sigma goal in
+ let mk_goal hyps concl =
+ Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
+ in
match kind_of_term trm with
| Meta _ ->
let conclty = nf_betaiota sigma conclty in
if !check && occur_meta conclty then
raise (RefinerError (MetaInType conclty));
- (mk_goal hyps conclty)::goalacc, conclty
+ let (gl,ev,sigma) = mk_goal hyps conclty in
+ gl::goalacc, conclty, sigma, ev
| Cast (t,_, ty) ->
check_typability env sigma ty;
@@ -349,30 +344,32 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
mk_refgoals sigma goal goalacc ty t
| App (f,l) ->
- let (acc',hdty) =
+ let (acc',hdty,sigma,applicand) =
match kind_of_term f with
| Ind _ | Const _
when (isInd f or has_polymorphic_type (destConst f)) ->
(* Sort-polymorphism of definition and inductive types *)
goalacc,
- type_of_global_reference_knowing_conclusion env sigma f conclty
+ type_of_global_reference_knowing_conclusion env sigma f conclty,
+ sigma, f
| _ ->
mk_hdgoals sigma goal goalacc f
in
- let (acc'',conclty') =
+ let (acc'',conclty',sigma, args) =
mk_arggoals sigma goal acc' hdty (Array.to_list l) in
check_conv_leq_goal env sigma trm conclty' conclty;
- (acc'',conclty')
+ (acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args))
- | Case (_,p,c,lf) ->
- let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+ | Case (ci,p,c,lf) ->
+ let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
check_conv_leq_goal env sigma trm conclty' conclty;
- let acc'' =
+ let (acc'',sigma, rbranches) =
array_fold_left2
- (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
- acc' lbrty lf
+ (fun (lacc,sigma,bacc) ty fi ->
+ let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
+ (acc',sigma,[]) lbrty lf
in
- (acc'',conclty')
+ (acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches)))
| _ ->
if occur_meta trm then
@@ -380,70 +377,77 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let t'ty = goal_type_of env sigma trm in
check_conv_leq_goal env sigma trm t'ty conclty;
- (goalacc,t'ty)
+ (goalacc,t'ty,sigma, trm)
-(* Same as mkREFGOALS but without knowing te type of the term. Therefore,
+(* Same as mkREFGOALS but without knowing the type of the term. Therefore,
* Metas should be casted. *)
and mk_hdgoals sigma goal goalacc trm =
- let env = evar_env goal in
- let hyps = goal.evar_hyps in
- let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
+ let env = Goal.V82.env sigma goal in
+ let hyps = Goal.V82.hyps sigma goal in
+ let mk_goal hyps concl =
+ Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
- (mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
+ let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in
+ gl::goalacc,ty,sigma,ev
| Cast (t,_, ty) ->
check_typability env sigma ty;
mk_refgoals sigma goal goalacc ty t
| App (f,l) ->
- let (acc',hdty) =
+ let (acc',hdty,sigma,applicand) =
if isInd f or isConst f
& not (array_exists occur_meta l) (* we could be finer *)
then
- (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
+ (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f)
else mk_hdgoals sigma goal goalacc f
in
- mk_arggoals sigma goal acc' hdty (Array.to_list l)
+ let (acc'',conclty',sigma, args) =
+ mk_arggoals sigma goal acc' hdty (Array.to_list l) in
+ (acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args))
- | Case (_,p,c,lf) ->
- let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
- let acc'' =
+ | Case (ci,p,c,lf) ->
+ let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
+ let (acc'',sigma,rbranches) =
array_fold_left2
- (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
- acc' lbrty lf
+ (fun (lacc,sigma,bacc) ty fi ->
+ let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
+ (acc',sigma,[]) lbrty lf
in
- (acc'',conclty')
+ (acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches)))
| _ ->
if !check && occur_meta trm then
anomaly "refine called with a dependent meta";
- goalacc, goal_type_of env sigma trm
+ goalacc, goal_type_of env sigma trm, sigma, trm
and mk_arggoals sigma goal goalacc funty = function
- | [] -> goalacc,funty
+ | [] -> goalacc,funty,sigma, []
| harg::tlargs as allargs ->
- let t = whd_betadeltaiota (evar_env goal) sigma funty in
+ let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
match kind_of_term t with
| Prod (_,c1,b) ->
- let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
- mk_arggoals sigma goal acc' (subst1 harg b) tlargs
+ let (acc',hargty,sigma,arg') = mk_refgoals sigma goal goalacc c1 harg in
+ let (acc'',fty, sigma', args) =
+ mk_arggoals sigma goal acc' (subst1 harg b) tlargs in
+ (acc'',fty,sigma',arg'::args)
| LetIn (_,c1,_,b) ->
mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
| _ -> raise (RefinerError (CannotApply (t,harg)))
and mk_casegoals sigma goal goalacc p c =
- let env = evar_env goal in
- let (acc',ct) = mk_hdgoals sigma goal goalacc c in
- let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+ let env = Goal.V82.env sigma goal in
+ let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
let indspec =
try find_mrectype env sigma ct
with Not_found -> anomaly "mk_casegoals" in
let (lbrty,conclty) =
type_case_branches_with_names env indspec p c in
- (acc'',lbrty,conclty)
+ (acc'',lbrty,conclty,sigma,p',c')
let convert_hyp sign sigma (id,b,bt as d) =
@@ -461,18 +465,6 @@ let convert_hyp sign sigma (id,b,bt as d) =
d) in
reorder_val_context env sign' !reorder
-(* Normalizing evars in a goal. Called by tactic Local_constraints
- (i.e. when the sigma of the proof tree changes). Detect if the
- goal is unchanged *)
-let norm_goal sigma gl =
- let red_fun = Evarutil.nf_evar sigma in
- let ncl = red_fun gl.evar_concl in
- let ngl =
- { gl with
- evar_concl = ncl;
- evar_hyps = map_named_val red_fun gl.evar_hyps } in
- if Evd.eq_evar_info ngl gl then None else Some ngl
-
(************************************************************************)
@@ -480,10 +472,12 @@ let norm_goal sigma gl =
(* Primitive tactics are handled here *)
let prim_refiner r sigma goal =
- let env = evar_env goal in
- let sign = goal.evar_hyps in
- let cl = goal.evar_concl in
- let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
+ let env = Goal.V82.env sigma goal in
+ let sign = Goal.V82.hyps sigma goal in
+ let cl = Goal.V82.concl sigma goal in
+ let mk_goal hyps concl =
+ Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
+ in
match r with
(* Logical rules *)
| Intro id ->
@@ -491,19 +485,23 @@ let prim_refiner r sigma goal =
error "New variable is already declared";
(match kind_of_term (strip_outer_cast cl) with
| Prod (_,c1,b) ->
- let sg = mk_goal (push_named_context_val (id,None,c1) sign)
+ let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
(subst1 (mkVar id) b) in
+ let sigma =
+ Goal.V82.partial_solution sigma goal (mkNamedLambda id c1 ev) in
([sg], sigma)
| LetIn (_,c1,t1,b) ->
- let sg =
+ let (sg,ev,sigma) =
mk_goal (push_named_context_val (id,Some c1,t1) sign)
(subst1 (mkVar id) b) in
+ let sigma =
+ Goal.V82.partial_solution sigma goal (mkNamedLetIn id c1 t1 ev) in
([sg], sigma)
| _ ->
raise (RefinerError IntroNeedsProduct))
| Cut (b,replace,id,t) ->
- let sg1 = mk_goal sign (nf_betaiota sigma t) in
+ let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
let sign,cl,sigma =
if replace then
let nexthyp = get_hyp_after id (named_context_of_val sign) in
@@ -515,7 +513,10 @@ let prim_refiner r sigma goal =
(if !check && mem_named_context id (named_context_of_val sign) then
error "New variable is already declared";
push_named_context_val (id,None,t) sign,cl,sigma) in
- let sg2 = mk_goal sign cl in
+ let (sg2,ev2,sigma) =
+ Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
+ let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in
+ let sigma = Goal.V82.partial_solution sigma goal oterm in
if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
| FixRule (f,n,rest,j) ->
@@ -545,9 +546,24 @@ let prim_refiner r sigma goal =
("Name "^string_of_id f^" already used in the environment");
mk_sign (push_named_context_val (f,None,ar) sign) oth
| [] ->
- List.map (fun (_,_,c) -> mk_goal sign c) all
+ Goal.list_map (fun sigma (_,_,c) ->
+ let (gl,ev,sig')=
+ Goal.V82.mk_goal sigma sign c
+ (Goal.V82.extra sigma goal)
+ in ((gl,ev),sig'))
+ all sigma
in
- (mk_sign sign all, sigma)
+ let (gls_evs,sigma) = mk_sign sign all in
+ let (gls,evs) = List.split gls_evs in
+ let ids = List.map pi1 all in
+ let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+ let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
+ let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+ let typarray = Array.of_list (List.map pi3 all) in
+ let bodies = Array.of_list evs in
+ let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
+ let sigma = Goal.V82.partial_solution sigma goal oterm in
+ (gls,sigma)
| Cofix (f,others,j) ->
let rec check_is_coind env cl =
@@ -572,32 +588,55 @@ let prim_refiner r sigma goal =
with
| Not_found ->
mk_sign (push_named_context_val (f,None,ar) sign) oth)
- | [] -> List.map (fun (_,c) -> mk_goal sign c) all
+ | [] -> Goal.list_map (fun sigma(_,c) ->
+ let (gl,ev,sigma) =
+ Goal.V82.mk_goal sigma sign c
+ (Goal.V82.extra sigma goal)
+ in
+ ((gl,ev),sigma))
+ all sigma
in
- (mk_sign sign all, sigma)
+ let (gls_evs,sigma) = mk_sign sign all in
+ let (gls,evs) = List.split gls_evs in
+ let (ids,types) = List.split all in
+ let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+ let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+ let typarray = Array.of_list types in
+ let bodies = Array.of_list evs in
+ let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in
+ let sigma = Goal.V82.partial_solution sigma goal oterm in
+ (gls,sigma)
| Refine c ->
check_meta_variables c;
- let (sgl,cl') = mk_refgoals sigma goal [] cl c in
+ let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
let sgl = List.rev sgl in
+ let sigma = Goal.V82.partial_solution sigma goal oterm in
(sgl, sigma)
(* Conversion rules *)
| Convert_concl (cl',_) ->
check_typability env sigma cl';
if (not !check) || is_conv_leq env sigma cl' cl then
- let sg = mk_goal sign cl' in
+ let (sg,ev,sigma) = mk_goal sign cl' in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
([sg], sigma)
else
error "convert-concl rule passed non-converting term"
| Convert_hyp (id,copt,ty) ->
- ([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
+ let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([gl], sigma)
(* And now the structural rules *)
| Thin ids ->
let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
- ([mk_goal hyps concl], nsigma)
+ let (gl,ev,sigma) =
+ Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
+ in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([gl], sigma)
| ThinBody ids ->
let clear_aux env id =
@@ -606,7 +645,8 @@ let prim_refiner r sigma goal =
env'
in
let sign' = named_context_val (List.fold_left clear_aux env ids) in
- let sg = mk_goal sign' cl in
+ let (sg,ev,sigma) = mk_goal sign' cl in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
([sg], sigma)
| Move (withdep, hfrom, hto) ->
@@ -614,11 +654,15 @@ let prim_refiner r sigma goal =
split_sign hfrom hto (named_context_of_val sign) in
let hyps' =
move_hyp withdep toleft (left,declfrom,right) hto in
- ([mk_goal hyps' cl], sigma)
+ let (gl,ev,sigma) = mk_goal hyps' cl in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([gl], sigma)
| Order ord ->
let hyps' = reorder_val_context env sign ord in
- ([mk_goal hyps' cl], sigma)
+ let (gl,ev,sigma) = mk_goal hyps' cl in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([gl], sigma)
| Rename (id1,id2) ->
if !check & id1 <> id2 &&
@@ -626,12 +670,19 @@ let prim_refiner r sigma goal =
error ((string_of_id id2)^" is already used.");
let sign' = rename_hyp id1 id2 sign in
let cl' = replace_vars [id1,mkVar id2] cl in
- ([mk_goal sign' cl'], sigma)
+ let (gl,ev,sigma) = mk_goal sign' cl' in
+ let ev = Term.replace_vars [(id2,mkVar id1)] ev in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([gl], sigma)
| Change_evars ->
- match norm_goal sigma goal with
- Some ngl -> ([ngl],sigma)
- | None -> ([goal], sigma)
+ (* spiwack: a priori [Change_evars] is now devoid of operational content.
+ The new proof engine keeping the evar_map up to date at all time.
+ As a compatibility mesure I leave the rule.
+ It is possible that my assumption is wrong and some uses of
+ [Change_evars] are not subsumed by the new engine. In which
+ case something has to be done here. (Feb. 2010) *)
+ ([goal],sigma)
(************************************************************************)
(************************************************************************)
@@ -671,77 +722,3 @@ let proof_variable_index x =
| [] -> raise Not_found
in
aux 1
-
-let prim_extractor subfun vl pft =
- let cl = pft.goal.evar_concl in
- match pft.ref with
- | Some (Prim (Intro id), [spf]) ->
- (match kind_of_term (strip_outer_cast cl) with
- | Prod (_,ty,_) ->
- let cty = subst_proof_vars vl ty in
- mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
- | LetIn (_,b,ty,_) ->
- let cb = subst_proof_vars vl b in
- let cty = subst_proof_vars vl ty in
- mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
- | _ -> error "Incomplete proof!")
-
- | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) ->
- let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
- mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
- subfun (add_proof_var id vl) spf2)
-
- | Some (Prim (FixRule (f,n,others,j)),spfl) ->
- let firsts,lasts = list_chop j others in
- let all = Array.of_list (firsts@(f,n,cl)::lasts) in
- let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
- let names = Array.map (fun (f,_,_) -> Name f) all in
- let vn = Array.map (fun (_,n,_) -> n-1) all in
- let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
- (add_proof_var f vl) others in
- let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkFix ((vn,j),(names,lcty,lfix))
-
- | Some (Prim (Cofix (f,others,j)),spfl) ->
- let firsts,lasts = list_chop j others in
- let all = Array.of_list (firsts@(f,cl)::lasts) in
- let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
- let names = Array.map (fun (f,_) -> Name f) all in
- let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
- (add_proof_var f vl) others in
- let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkCoFix (j,(names,lcty,lfix))
-
- | Some (Prim (Refine c),spfl) ->
- let mvl = collect_meta_variables c in
- let metamap = List.combine mvl (List.map (subfun vl) spfl) in
- let cc = subst_proof_vars vl c in
- plain_instance metamap cc
-
- (* Structural and conversion rules do not produce any proof *)
- | Some (Prim (Convert_concl (t,k)),[pf]) ->
- if k = DEFAULTcast then subfun vl pf
- else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
- | Some (Prim (Convert_hyp _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Thin _),[pf]) ->
- (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
- subfun vl pf
-
- | Some (Prim (ThinBody _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Move _|Order _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Rename (id1,id2)),[pf]) ->
- subfun (rebind id1 id2 vl) pf
-
- | Some (Prim Change_evars, [pf]) ->
- subfun vl pf
-
- | Some _ -> anomaly "prim_extractor"
-
- | None-> error "prim_extractor handed incomplete proof"
-
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0d56da382a..560e577366 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -38,9 +38,6 @@ val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
type proof_variable
-val prim_extractor :
- (proof_variable list -> proof_tree -> constr)
- -> proof_variable list -> proof_tree -> constr
val proof_variable_index : identifier -> proof_variable list -> int
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f3658ad4b6..6da73c2f67 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -20,322 +20,115 @@ open Environ
open Evd
open Typing
open Refiner
-open Proof_trees
open Tacexpr
open Proof_type
open Lib
open Safe_typing
-(*********************************************************************)
-(* Managing the proofs state *)
-(* Mainly contributed by C. Murthy *)
-(*********************************************************************)
+let refining = Proof_global.there_are_pending_proofs
+let check_no_pending_proofs = Proof_global.check_no_pending_proof
-type lemma_possible_guards = int list list
+let get_current_proof_name = Proof_global.get_current_proof_name
+let get_all_proof_names = Proof_global.get_all_proof_names
-type proof_topstate = {
- mutable top_end_tac : tactic option;
- top_init_tac : tactic option;
- top_compute_guard : lemma_possible_guards;
- top_goal : goal;
- top_strength : Decl_kinds.goal_kind;
- top_hook : declaration_hook }
+type lemma_possible_guards = Proof_global.lemma_possible_guards
-let proof_edits =
- (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
+let delete_proof = Proof_global.discard
+let delete_current_proof = Proof_global.discard_current
+let delete_all_proofs = Proof_global.discard_all
-let get_all_proof_names () = Edit.dom proof_edits
+let undo n =
+ let p = Proof_global.give_me_the_proof () in
+ for i = 1 to n do
+ Proof.undo p
+ done
-let msg_proofs use_resume =
- match Edit.dom proof_edits with
- | [] -> (spc () ++ str"(No proof-editing in progress).")
- | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
- (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
- str"." ++
- (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
- else (mt ()))
-)
-
-let undo_default = 50
-let undo_limit = ref undo_default
-
-(*********************************************************************)
-(* Functions for decomposing and modifying the proof state *)
-(*********************************************************************)
-
-let get_state () =
- match Edit.read proof_edits with
- | None -> errorlabstrm "Pfedit.get_state"
- (str"No focused proof" ++ msg_proofs true)
- | Some(_,pfs,ts) -> (pfs,ts)
-
-let get_topstate () = snd(get_state())
-let get_pftreestate () = fst(get_state())
-
-let get_end_tac () = let ts = get_topstate () in ts.top_end_tac
-
-let get_goal_context n =
- let pftree = get_pftreestate () in
- let goal = nth_goal_of_pftreestate n pftree in
- (project goal, pf_env goal)
-
-let get_current_goal_context () = get_goal_context 1
-
-let set_current_proof = Edit.focus proof_edits
-
-let resume_proof (loc,id) =
+let current_proof_depth () =
try
- Edit.focus proof_edits id
- with Invalid_argument "Edit.focus" ->
- user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
+ let p = Proof_global.give_me_the_proof () in
+ Proof.V82.depth p
+ with Proof_global.NoCurrentProof -> -1
-let suspend_proof () =
+(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+ is the depth of the focus stack). *)
+let undo_todepth n =
try
- Edit.unfocus proof_edits
- with Invalid_argument "Edit.unfocus" ->
- errorlabstrm "Pfedit.suspend_current_proof"
- (str"No active proof" ++ (msg_proofs true))
-
-let resume_last_proof () =
- match (Edit.last_focused proof_edits) with
- | None ->
- errorlabstrm "resume_last" (str"No proof-editing in progress.")
- | Some p ->
- Edit.focus proof_edits p
+ undo ((current_proof_depth ()) - n )
+ with Proof_global.NoCurrentProof when n=0 -> ()
-let get_current_proof_name () =
- match Edit.read proof_edits with
- | None ->
- errorlabstrm "Pfedit.get_proof"
- (str"No focused proof" ++ msg_proofs true)
- | Some(na,_,_) -> na
+let set_undo _ = ()
+let get_undo _ = None
-let add_proof (na,pfs,ts) =
- Edit.create proof_edits (na,pfs,ts,!undo_limit+1)
-let delete_proof_gen = Edit.delete proof_edits
-
-let delete_proof (loc,id) =
- try
- delete_proof_gen id
- with (UserError ("Edit.delete",_)) ->
- user_err_loc
- (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
-
-let mutate f =
- try
- Edit.mutate proof_edits (fun _ pfs -> f pfs)
- with Invalid_argument "Edit.mutate" ->
- errorlabstrm "Pfedit.mutate"
- (str"No focused proof" ++ msg_proofs true)
-
-let start (na,ts) =
- let pfs = mk_pftreestate ts.top_goal in
- let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
- add_proof(na,pfs,ts)
+let start_proof id str hyps c ?init_tac ?compute_guard hook =
+ let goals = [ (Global.env_of_context hyps , c) ] in
+ let init_tac = Option.map Proofview.V82.tactic init_tac in
+ Proof_global.start_proof id str goals ?compute_guard hook;
+ Option.iter Proof_global.run_tactic init_tac
let restart_proof () =
- match Edit.read proof_edits with
- | None ->
- errorlabstrm "Pfedit.restart"
- (str"No focused proof to restart" ++ msg_proofs true)
- | Some(na,_,ts) ->
- delete_proof_gen na;
- start (na,ts);
- set_current_proof na
-
-let proof_term () =
- extract_pftreestate (get_pftreestate())
-
-(* Detect is one has completed a subtree of the initial goal *)
-let subtree_solved () =
- let pts = get_pftreestate () in
- is_complete_proof (proof_of_pftreestate pts) &
- not (is_top_pftreestate pts)
-
-let tree_solved () =
- let pts = get_pftreestate () in
- is_complete_proof (proof_of_pftreestate pts)
-
-let top_tree_solved () =
- let pts = get_pftreestate () in
- is_complete_proof (proof_of_pftreestate (top_of_tree pts))
-
-(*********************************************************************)
-(* Undo functions *)
-(*********************************************************************)
-
-let set_undo = function
- | None -> undo_limit := undo_default
- | Some n ->
- if n>=0 then
- undo_limit := n
- else
- error "Cannot set a negative undo limit"
-
-let get_undo () = Some !undo_limit
-
-let undo n =
- try
- Edit.undo proof_edits n;
- (* needed because the resolution of a subtree is done in 2 steps
- then a sequence of undo can lead to a focus on a completely solved
- subtree - this solution only works properly if undoing one step *)
- if subtree_solved() then Edit.undo proof_edits 1
- with (Invalid_argument "Edit.undo") ->
- errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
-
-(* Undo current focused proof to reach depth [n]. This is used in
- [vernac_backtrack]. *)
-let undo_todepth n =
- try
- Edit.undo_todepth proof_edits n
- with (Invalid_argument "Edit.undo") ->
- errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
-
-(* Return the depth of the current focused proof stack, this is used
- to put informations in coq prompt (in emacs mode). *)
-let current_proof_depth() =
- try
- Edit.depth proof_edits
- with (Invalid_argument "Edit.depth") -> -1
-
-(*********************************************************************)
-(* Proof cooking *)
-(*********************************************************************)
+ let p = Proof_global.give_me_the_proof () in
+ try while true do
+ Proof.undo p
+ done with Proof.EmptyUndoStack -> ()
+
+let resume_last_proof () = Proof_global.resume_last ()
+let resume_proof (_,id) = Proof_global.resume id
+let suspend_proof () = Proof_global.suspend ()
+
+let cook_proof hook =
+ let prf = Proof_global.give_me_the_proof () in
+ hook prf;
+ match Proof_global.close_proof () with
+ | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
+ | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."
let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f
-let cook_proof k =
- let (pfs,ts) = get_state()
- and ident = get_current_proof_name () in
- let {evar_concl=concl} = ts.top_goal
- and strength = ts.top_strength in
- let pfterm = extract_pftreestate pfs in
- !xml_cook_proof (strength,pfs);
- k pfs;
- (ident,
- ({ const_entry_body = pfterm;
- const_entry_type = Some concl;
- const_entry_opaque = true;
- const_entry_boxed = false},
- ts.top_compute_guard, strength, ts.top_hook))
-
-let current_proof_statement () =
- let ts = get_topstate() in
- (get_current_proof_name (), ts.top_strength,
- ts.top_goal.evar_concl, ts.top_hook)
-
-(*********************************************************************)
-(* Abort functions *)
-(*********************************************************************)
-
-let refining () = [] <> (Edit.dom proof_edits)
-
-let check_no_pending_proofs () =
- if refining () then
- errorlabstrm "check_no_pending_proofs"
- (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
- str"Use \"Abort All\" first or complete proof(s).")
+let get_pftreestate () =
+ Proof_global.give_me_the_proof ()
-let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
-
-let delete_all_proofs () = Edit.clear proof_edits
-
-(*********************************************************************)
-(* Modifying the end tactic of the current profftree *)
-(*********************************************************************)
let set_end_tac tac =
- let top = get_topstate () in
- top.top_end_tac <- Some tac
-
-(*********************************************************************)
-(* Modifying the current prooftree *)
-(*********************************************************************)
-
-let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook =
- let top_goal = mk_goal sign concl None in
- let ts = {
- top_end_tac = None;
- top_init_tac = init_tac;
- top_compute_guard = compute_guard;
- top_goal = top_goal;
- top_strength = str;
- top_hook = hook}
- in
- start(na,ts);
- set_current_proof na
-
-let solve_nth k tac =
- let pft = get_pftreestate () in
- if not (List.mem (-1) (cursor_of_pftreestate pft)) then
- mutate (solve_nth_pftreestate k tac)
- else
- error "cannot apply a tactic when we are descended behind a tactic-node"
-
-let by tac = mutate (solve_pftreestate tac)
-
-let instantiate_nth_evar_com n c =
- mutate (Evar_refiner.instantiate_pf_com n c)
+ let tac = Proofview.V82.tactic tac in
+ Proof_global.set_endline_tactic tac
-let traverse n = mutate (traverse n)
-
-(* [traverse_to path]
-
- Traverses the current proof to get to the location specified by
- [path].
-
- ALGORITHM: The algorithm works on reversed paths. One just has to remove
- the common part on the reversed paths.
-
-*)
-
-let common_ancestor l1 l2 =
- let rec common_aux l1 l2 =
- match l1, l2 with
- | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2'
- | _, _ -> List.rev l1, List.length l2
- in
- common_aux (List.rev l1) (List.rev l2)
-
-let rec traverse_up = function
- | 0 -> (function pf -> pf)
- | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf))
-
-let rec traverse_down = function
- | [] -> (function pf -> pf)
- | n::l -> (function pf -> Refiner.traverse n (traverse_down l pf))
-
-let traverse_to path =
- let up_and_down path pfs =
- let cursor = cursor_of_pftreestate pfs in
- let down_list, up_count = common_ancestor path cursor in
- traverse_down down_list (traverse_up up_count pfs)
- in
- mutate (up_and_down path)
-
-(* traverse the proof tree until it reach the nth subgoal *)
-let traverse_nth_goal n = mutate (nth_unproven n)
-
-let traverse_prev_unproven () = mutate prev_unproven
-
-let traverse_next_unproven () = mutate next_unproven
+let get_goal_context i =
+ try
+ let p = Proof_global.give_me_the_proof () in
+ let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in
+ let goal = List.nth goals (i-1) in
+ (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
+ with Proof_global.NoCurrentProof -> Util.error "No focused proof."
-(* The goal focused on *)
-let focus_n = ref 0
-let make_focus n = focus_n := n
-let focus () = !focus_n
-let focused_goal () = let n = !focus_n in if n=0 then 1 else n
+let get_current_goal_context () = get_goal_context 1
-let reset_top_of_tree () =
- mutate top_of_tree
+let current_proof_statement () =
+ match Proof_global.V82.get_current_initial_conclusions () with
+ | (id,([concl],strength,hook)) -> id,strength,concl,hook
+ | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"
+
+let solve_nth ?(with_end_tac=false) gi tac =
+ try
+ let tac = Proofview.V82.tactic tac in
+ let tac = if with_end_tac then
+ Proof_global.with_end_tac tac
+ else
+ tac
+ in
+ Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac)
+ with
+ | Proof_global.NoCurrentProof -> Util.error "No focused proof"
+ | Proofview.IndexOutOfRange | Failure "list_chop" ->
+ let msg = str "No such goal: " ++ int gi ++ str "." in
+ Util.errorlabstrm "" msg
+
+let by = solve_nth 1
+
+let instantiate_nth_evar_com n com =
+ let pf = Proof_global.give_me_the_proof () in
+ Proof.V82.instantiate_evar n com pf
-let reset_top_of_script () =
- mutate (fun pts ->
- try
- up_until_matching_rule is_proof_instr pts
- with Not_found -> top_of_tree pts)
(**********************************************************************)
(* Shortcut to build a term using tactics *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index acb852471d..9e24061d32 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -20,6 +20,7 @@ open Tacmach
open Tacexpr
(*i*)
+
(*s Several proofs can be opened simultaneously but at most one is
focused at some time. The following functions work by side-effect
on current set of open proofs. In this module, ``proofs'' means an
@@ -57,17 +58,16 @@ val delete_all_proofs : unit -> unit
val undo : int -> unit
-(* Same as undo, but undoes the current proof stack to reach depth
- [n]. This is used in [vernac_backtrack]. *)
-val undo_todepth : int -> unit
+(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+ is the depth of the undo stack). *)
+val undo_todepth : int -> unit
(* Returns the depth of the current focused proof stack, this is used
to put informations in coq prompt (in emacs mode). *)
val current_proof_depth: unit -> int
-(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
- sets the size to the default value (12) *)
-
+(* [set_undo (Some n)] used to set the size of the ``undo'' stack.
+ These function now do nothing and will disapear. *)
val set_undo : int option -> unit
val get_undo : unit -> int option
@@ -78,7 +78,7 @@ val get_undo : unit -> int option
systematically apply at initialization time (e.g. to start the
proof of mutually dependent theorems) *)
-type lemma_possible_guards = int list list
+type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
@@ -110,22 +110,18 @@ val suspend_proof : unit -> unit
it fails if there is no current proof of if it is not completed;
it also tells if the guardness condition has to be inferred. *)
-val cook_proof : (Refiner.pftreestate -> unit) ->
+val cook_proof : (Proof.proof -> unit) ->
identifier *
- (Entries.definition_entry * lemma_possible_guards * goal_kind *
- declaration_hook)
+ (Entries.definition_entry * lemma_possible_guards * goal_kind *
+ declaration_hook)
(* To export completed proofs to xml *)
-val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
+val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
-(*s [get_pftreestate ()] returns the current focused pending proof or
+(*s [get_Proof.proof ()] returns the current focused pending proof or
raises [UserError "no focused proof"] *)
-val get_pftreestate : unit -> pftreestate
-
-(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
-
-val get_end_tac : unit -> tactic option
+val get_pftreestate : unit -> Proof.proof
(* [get_goal_context n] returns the context of the [n]th subgoal of
the current focused proof or raises a [UserError] if there is no
@@ -160,7 +156,7 @@ val set_end_tac : tactic -> unit
current focused proof or raises a UserError if no proof is focused or
if there is no [n]th subgoal *)
-val solve_nth : int -> tactic -> unit
+val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
(* [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof or raises a UserError if there is no focused proof or
@@ -175,31 +171,6 @@ val by : tactic -> unit
val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
-(*s To deal with subgoal focus *)
-
-val make_focus : int -> unit
-val focus : unit -> int
-val focused_goal : unit -> int
-val subtree_solved : unit -> bool
-val tree_solved : unit -> bool
-val top_tree_solved : unit -> bool
-
-val reset_top_of_tree : unit -> unit
-val reset_top_of_script : unit -> unit
-
-val traverse : int -> unit
-val traverse_nth_goal : int -> unit
-val traverse_next_unproven : unit -> unit
-val traverse_prev_unproven : unit -> unit
-
-
-(* These two functions make it possible to implement more elaborate
- proof and goal management, as it is done, for instance in pcoq *)
-
-val traverse_to : int list -> unit
-val mutate : (pftreestate -> pftreestate) -> unit
-
-
(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
val build_constant_by_tactic : named_context_val -> types -> tactic ->
diff --git a/proofs/proof.ml b/proofs/proof.ml
new file mode 100644
index 0000000000..0c298cc630
--- /dev/null
+++ b/proofs/proof.ml
@@ -0,0 +1,294 @@
+(************************************************************************)
+(* 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$ *)
+
+(* Module defining the last essential tiles of interactive proofs.
+ The features of the Proof module are undoing and focusing.
+ A proof is a mutable object, it contains a proofview, and some information
+ to be able to undo actions, and to unfocus the current view. All three
+ of these being meant to evolve.
+ - Proofview: a proof is primarily the data of the current view.
+ That which is shown to the user (as a remainder, a proofview
+ is mainly the logical state of the proof, together with the
+ currently focused goals).
+ - Focus: a proof has a focus stack: the top of the stack contains
+ the context in which to unfocus the current view to a view focused
+ with the rest of the stack.
+ In addition, this contains, for each of the focus context, a
+ "focus kind" and a "focus condition" (in practice, and for modularity,
+ the focus kind is actually stored inside the condition). To unfocus, one
+ needs to know the focus kind, and the condition (for instance "no condition" or
+ the proof under focused must be complete) must be met.
+ - Undo: since proofviews and focus stacks are immutable objects,
+ it could suffice to hold the previous states, to allow to return to the past.
+ However, we also allow other modules to do actions that can be undone.
+ Therefore the undo stack stores action to be ran to undo.
+*)
+
+open Term
+
+type focus_kind = int
+type focus_condition = focus_kind -> Proofview.proofview -> bool
+
+let next_kind = ref 0
+let new_focus_kind () =
+ let r = !next_kind in
+ incr next_kind;
+ r
+
+(* To be authorized to unfocus one must meet the condition prescribed by
+ the action which focused.*)
+(* spiwack: we could consider having a list of authorized focus_kind instead
+ of just one, if anyone needs it *)
+(* [no_cond] only checks that the unfocusing command uses the right
+ [focus_kind]. *)
+let no_cond k0 k _ = k0 = k
+(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
+ and that the focused proofview is complete. *)
+let done_cond k0 k p = k0 = k && Proofview.finished p
+
+
+(* Subpart of the type of proofs. It contains the parts of the proof which
+ are under control of the undo mechanism *)
+type proof_state = {
+ (* Current focused proofview *)
+ proofview: Proofview.proofview;
+ (* History of the focusings, provides information on how
+ to unfocus the proof.
+ The list is empty when the proof is fully unfocused. *)
+ focus_stack: (focus_condition*Proofview.focus_context) list;
+ (* Extra information which can be freely used to create new behaviours. *)
+ intel: Store.t
+}
+
+type proof_info = {
+ mutable endline_tactic : unit Proofview.tactic ;
+ initial_conclusions : Term.types list
+}
+
+type undo_action =
+ | State of proof_state
+ | Effect of (unit -> unit)
+
+type proof = { (* current proof_state *)
+ mutable state : proof_state;
+ (* The undo stack *)
+ mutable undo_stack : undo_action list;
+ info : proof_info
+ }
+
+
+(*** General proof functions ***)
+
+let start goals =
+ { state = { proofview = Proofview.init goals ;
+ focus_stack = [] ;
+ intel = Store.empty} ;
+ undo_stack = [] ;
+ info = { endline_tactic = Proofview.tclUNIT ();
+ initial_conclusions = List.map snd goals }
+ }
+
+let rec unroll_focus pv = function
+ | (_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
+ | [] -> pv
+
+(* spiwack: a proof is considered completed even if its still focused, if the focus
+ doesn't hide any goal. *)
+let is_done p =
+ Proofview.finished p.state.proofview &&
+ Proofview.finished (unroll_focus p.state.proofview p.state.focus_stack)
+
+(* spiwack: for compatibility with <= 8.2 proof engine *)
+let has_unresolved_evar p =
+ Proofview.V82.has_unresolved_evar p.state.proofview
+
+(* Returns the list of partial proofs to initial goals *)
+let partial_proof p =
+ List.map fst (Proofview.return p.state.proofview)
+
+exception UnfinishedProof
+exception HasUnresolvedEvar
+let return p =
+ if not (is_done p) then
+ raise UnfinishedProof
+ else if has_unresolved_evar p then
+ (* spiwack: for compatibility with <= 8.2 proof engine *)
+ raise HasUnresolvedEvar
+ else
+ Proofview.return p.state.proofview
+
+(*** The following functions implement the basic internal mechanisms
+ of proofs, they are not meant to be exported in the .mli ***)
+
+(* An auxiliary function to push a {!focus_context} on the focus stack. *)
+let push_focus kind context pr =
+ pr.state <- { pr.state with focus_stack = (kind,context)::pr.state.focus_stack }
+
+exception FullyUnfocused
+
+(* An auxiliary function to read the kind of the next focusing step *)
+let cond_of_focus pr =
+ match pr.state.focus_stack with
+ | (cond,_)::_ -> cond
+ | _ -> raise FullyUnfocused
+
+(* An auxiliary function to pop and read the last {!Proofview.focus_context}
+ on the focus stack. *)
+let pop_focus pr =
+ match pr.state.focus_stack with
+ | focus::other_focuses ->
+ pr.state <- { pr.state with focus_stack = other_focuses }; focus
+ | _ ->
+ raise FullyUnfocused
+
+(* Auxiliary function to push a [proof_state] onto the undo stack. *)
+let push_undo save ({ undo_stack = stack } as pr) =
+ pr.undo_stack <- save::stack
+
+(* Auxiliary function to pop and read a [save_state] from the undo stack. *)
+exception EmptyUndoStack
+let pop_undo pr =
+ match pr.undo_stack with
+ | state::stack -> pr.undo_stack <- stack; state
+ | _ -> raise EmptyUndoStack
+
+
+(* This function focuses the proof [pr] between indices [i] and [j] *)
+let _focus cond i j pr =
+ let (focused,context) = Proofview.focus i j pr.state.proofview in
+ push_focus cond context pr;
+ pr.state <- { pr.state with proofview = focused }
+
+(* This function unfocuses the proof [pr], it raises [CannotUnfocus],
+ if the proof is already fully unfocused.
+ This function does not care about the condition of the current focus. *)
+let _unfocus pr =
+ let (_,fc) = pop_focus pr in
+ pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
+
+
+(*** Endline tactic ***)
+
+(* spiwack this is an information about the UI, it might be a good idea to move
+ it to the Proof_global module *)
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac p =
+ p.info.endline_tactic <- tac
+
+let with_end_tac pr tac =
+ Proofview.tclTHEN tac pr.info.endline_tactic
+
+(*** The following functions define the safety mechanism of the
+ proof system, they may be unsafe if not used carefully. There is
+ currently no reason to export them in the .mli ***)
+
+(* This functions saves the current state into a [proof_state]. *)
+let save_state { state = ps } = State ps
+
+(* This function stores the current proof state in the undo stack. *)
+let save pr =
+ push_undo (save_state pr) pr
+
+(* This function restores a state, presumably from the top of the undo stack. *)
+let restore_state save pr =
+ match save with
+ | State save -> pr.state <- save
+ | Effect undo -> undo ()
+
+(* Interpretes the Undo command. *)
+let undo pr =
+ (* On a single line, since the effects commute *)
+ restore_state (pop_undo pr) pr
+
+(* Adds an undo effect to the undo stack. Use it with care, errors here might result
+ in inconsistent states. *)
+let add_undo effect pr =
+ push_undo (Effect effect) pr
+
+(* Focus command (focuses on the [i]th subgoal) *)
+(* spiwack: there could also, easily be a focus-on-a-range tactic, is there
+ a need for it? *)
+let focus cond i pr =
+ save pr;
+ _focus cond i i pr
+
+(* Unfocus command.
+ Fails if the proof is not focused. *)
+let unfocus kind pr =
+ let starting_point = save_state pr in
+ try
+ let cond = cond_of_focus pr in
+ if cond kind pr.state.proofview then
+ (_unfocus pr;
+ push_undo starting_point pr)
+ else
+ Util.error "This proof is focused, but cannot be unfocused this way"
+ with FullyUnfocused ->
+ Util.error "This proof is not focused"
+
+let no_focused_goal p =
+ Proofview.finished p.state.proofview
+
+(*** Function manipulation proof extra informations ***)
+
+let get_proof_info pr =
+ pr.state.intel
+
+let set_proof_info info pr =
+ save pr;
+ pr.state <- { pr.state with intel=info }
+
+
+(*** Tactics ***)
+
+let run_tactic env tac pr =
+ let starting_point = save_state pr in
+ let sp = pr.state.proofview in
+ try
+ let tacticced_proofview = Proofview.apply env tac sp in
+ pr.state <- { pr.state with proofview = tacticced_proofview };
+ push_undo starting_point pr
+ with e ->
+ restore_state starting_point pr;
+ raise e
+
+
+
+(*** Compatibility layer with <=v8.2 ***)
+module V82 = struct
+ let subgoals p =
+ Proofview.V82.goals p.state.proofview
+
+ let background_subgoals p =
+ Proofview.V82.goals (unroll_focus p.state.proofview p.state.focus_stack)
+
+ let get_initial_conclusions p =
+ p.info.initial_conclusions
+
+ let depth p = List.length p.undo_stack
+
+ let top_goal p =
+ let { Evd.it=gls ; sigma=sigma } =
+ Proofview.V82.top_goals p.state.proofview
+ in
+ { Evd.it=List.hd gls ; sigma=sigma }
+
+ let instantiate_evar n com pr =
+ let starting_point = save_state pr in
+ let sp = pr.state.proofview in
+ try
+ let new_proofview = Proofview.V82.instantiate_evar n com sp in
+ pr.state <- { pr.state with proofview = new_proofview };
+ push_undo starting_point pr
+ with e ->
+ restore_state starting_point pr;
+ raise e
+end
diff --git a/proofs/proof.mli b/proofs/proof.mli
new file mode 100644
index 0000000000..2b1c3f5c20
--- /dev/null
+++ b/proofs/proof.mli
@@ -0,0 +1,133 @@
+(************************************************************************)
+(* 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: proof.mli aspiwack $ *)
+
+(* Module defining the last essential tiles of interactive proofs.
+ The features of the Proof module are undoing and focusing.
+ A proof is a mutable object, it contains a proofview, and some information
+ to be able to undo actions, and to unfocus the current view. All three
+ of these being meant to evolve.
+ - Proofview: a proof is primarily the data of the current view.
+ That which is shown to the user (as a remainder, a proofview
+ is mainly the logical state of the proof, together with the
+ currently focused goals).
+ - Focus: a proof has a focus stack: the top of the stack contains
+ the context in which to unfocus the current view to a view focused
+ with the rest of the stack.
+ In addition, this contains, for each of the focus context, a
+ "focus kind" and a "focus condition" (in practice, and for modularity,
+ the focus kind is actually stored inside the condition). To unfocus, one
+ needs to know the focus kind, and the condition (for instance "no condition" or
+ the proof under focused must be complete) must be met.
+ - Undo: since proofviews and focus stacks are immutable objects,
+ it could suffice to hold the previous states, to allow to return to the past.
+ However, we also allow other modules to do actions that can be undone.
+ Therefore the undo stack stores action to be ran to undo.
+*)
+
+open Term
+
+(* Type of a proof. *)
+type proof
+
+
+(*** General proof functions ***)
+
+val start : (Environ.env * Term.types) list -> proof
+
+(* Returns [true] is the considered proof is completed, that is if no goal remain
+ to be considered (this does not require that all evars have been solved). *)
+val is_done : proof -> bool
+
+(* Returns the list of partial proofs to initial goals. *)
+val partial_proof : proof -> Term.constr list
+
+(* Returns the proofs (with their type) of the initial goals.
+ Raises [UnfinishedProof] is some goals remain to be considered.
+ Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
+exception UnfinishedProof
+exception HasUnresolvedEvar
+val return : proof -> (Term.constr * Term.types) list
+
+(* Interpretes the Undo command. Raises [EmptyUndoStack] if
+ the undo stack is empty. *)
+exception EmptyUndoStack
+val undo : proof -> unit
+
+(* Adds an undo effect to the undo stack. Use it with care, errors here might result
+ in inconsistent states. *)
+val add_undo : (unit -> unit) -> proof -> unit
+
+(*** Focusing actions ***)
+
+(* [focus_kind] is the type used by focusing and unfocusing
+ commands to synchronise. Focusing and unfocusing commands use
+ a particular focus_kind, and if they don't match, the unfocusing command
+ will fail. *)
+type focus_kind
+val new_focus_kind : unit -> focus_kind
+
+(* To be authorized to unfocus one must meet the condition prescribed by
+ the action which focused.*)
+type focus_condition
+(* [no_cond] only checks that the unfocusing command uses the right
+ [focus_kind]. *)
+val no_cond : focus_kind -> focus_condition
+(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
+ and that the focused proofview is complete. *)
+val done_cond : focus_kind -> focus_condition
+
+(* focus command (focuses on the [i]th subgoal) *)
+(* there could also, easily be a focus-on-a-range tactic, is there
+ a need for it? *)
+val focus : focus_condition -> int -> proof -> unit
+
+exception FullyUnfocused
+(* Unfocusing command.
+ Raises [FullyUnfocused] if the proof is not focused. *)
+val unfocus : focus_kind -> proof -> unit
+
+(* returns [true] if there is no goal under focus. *)
+val no_focused_goal : proof -> bool
+
+(*** Function manipulation proof extra informations ***)
+
+val get_proof_info : proof -> Store.t
+
+val set_proof_info : Store.t -> proof -> unit
+
+
+(*** Endline tactic ***)
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+val set_endline_tactic : unit Proofview.tactic -> proof -> unit
+
+val with_end_tac : proof -> unit Proofview.tactic -> unit Proofview.tactic
+
+(*** Tactics ***)
+
+val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
+
+
+(*** Compatibility layer with <=v8.2 ***)
+module V82 : sig
+ val subgoals : proof -> Goal.goal list Evd.sigma
+
+ (* All the subgoals of the proof, including those which are not focused. *)
+ val background_subgoals : proof -> Goal.goal list Evd.sigma
+
+ val get_initial_conclusions : proof -> Term.types list
+
+ val depth : proof -> int
+
+ val top_goal : proof -> Goal.goal Evd.sigma
+
+ (* Implements the Existential command *)
+ val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
+end
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
new file mode 100644
index 0000000000..420ff84325
--- /dev/null
+++ b/proofs/proof_global.ml
@@ -0,0 +1,295 @@
+(************************************************************************)
+(* 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$ *)
+
+(***********************************************************************)
+(* *)
+(* This module defines the global proof environment *)
+(* In particular it keeps tracks of whether or not there is *)
+(* a proof which is currently being edited. *)
+(* *)
+(***********************************************************************)
+
+open Pp
+open Names
+
+(*** Proof Modes ***)
+
+(* Type of proof modes :
+ - A function [set] to set it *from standard mode*
+ - A function [reset] to reset the *standard mode* from it *)
+type proof_mode = {
+ name : string ;
+ set : unit -> unit ;
+ reset : unit -> unit
+}
+
+let proof_modes = Hashtbl.create 6
+let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m
+(* initial mode: standard mode *)
+let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
+let _ = register_proof_mode standard
+
+(* Default proof mode, to be set at the beginning of proofs. *)
+let default_proof_mode = ref standard
+
+let set_default_proof_mode =
+ Goptions.declare_string_option {Goptions.
+ optsync = true ;
+ optname = "default proof mode" ;
+ optkey = ["Default";"Proof";"Mode"] ;
+ optread = begin fun () ->
+ let { name = name } = !default_proof_mode in name
+ end;
+ optwrite = begin fun n ->
+ default_proof_mode := Hashtbl.find proof_modes n
+ end
+ }
+
+(*** Proof Global Environment ***)
+
+(* local shorthand *)
+type nproof = identifier*Proof.proof
+
+(* Extra info on proofs. *)
+type lemma_possible_guards = int list list
+type proof_info = {
+ strength : Decl_kinds.goal_kind ;
+ compute_guard : lemma_possible_guards;
+ hook :Tacexpr.declaration_hook ;
+ mode : proof_mode
+}
+
+(* Invariant: a proof is at most in one of current_proof and suspended. And the
+ domain of proof_info is the union of that of current_proof and suspended.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are to
+ be resumed when the current proof is closed, aborted or suspended. *)
+let current_proof = ref ([]:nproof list)
+let suspended = ref ([] : nproof list)
+let proof_info = ref (Idmap.empty : proof_info Idmap.t)
+
+(* Current proof_mode, for bookkeeping *)
+let current_proof_mode = ref !default_proof_mode
+
+(* combinators for proof modes *)
+let update_proof_mode () =
+ match !current_proof with
+ | (id,_)::_ ->
+ let { mode = m } = Idmap.find id !proof_info in
+ !current_proof_mode.reset ();
+ current_proof_mode := m;
+ !current_proof_mode.set ()
+ | _ ->
+ !current_proof_mode.reset ();
+ current_proof_mode := standard
+
+(* combinators for the current_proof and suspended lists *)
+let push a l = l := a::!l;
+ update_proof_mode ()
+
+exception NoSuchProof
+let rec extract id l =
+ let rec aux = function
+ | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
+ | np::l -> let (np', l) = aux l in (np' , np::l)
+ | [] -> raise NoSuchProof
+ in
+ let (np,l') = aux !l in
+ l := l';
+ update_proof_mode ();
+ np
+
+exception NoCurrentProof
+let extract_top l =
+ match !l with
+ | np::l' -> l := l' ; update_proof_mode (); np
+ | [] -> raise NoCurrentProof
+let find_top l =
+ match !l with
+ | np::_ -> np
+ | [] -> raise NoCurrentProof
+
+let rotate_top l1 l2 =
+ let np = extract_top l1 in
+ push np l2
+
+let rotate_find id l1 l2 =
+ let np = extract id l1 in
+ push np l2
+
+
+(* combinators for the proof_info map *)
+let add id info m =
+ m := Idmap.add id info !m
+let remove id m =
+ m := Idmap.remove id !m
+
+(*** Proof Global manipulation ***)
+
+let get_all_proof_names () =
+ List.map fst !current_proof @
+ List.map fst !suspended
+
+let give_me_the_proof () =
+ snd (find_top current_proof)
+
+let get_current_proof_name () =
+ fst (find_top current_proof)
+
+(* spiwack: it might be considered to move error messages away.
+ Or else to remove special exceptions from Proof_global.
+ Arguments for the former: there is no reason Proof_global is only
+ accessed directly through vernacular commands. Error message should be
+ pushed to external layers, and so we should be able to have a finer
+ control on error message on complex actions. *)
+let msg_proofs use_resume =
+ match get_all_proof_names () with
+ | [] -> (spc () ++ str"(No proof-editing in progress).")
+ | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
+ (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
+ str"." ++
+ (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
+ else (mt ()))
+ )
+
+
+let there_is_a_proof () = !current_proof <> []
+let there_are_suspended_proofs () = !suspended <> []
+let there_are_pending_proofs () =
+ there_is_a_proof () ||
+ there_are_suspended_proofs ()
+let check_no_pending_proof () =
+ if not (there_are_pending_proofs ()) then
+ ()
+ else begin
+ pp_with Format.str_formatter
+ (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+ str"Use \"Abort All\" first or complete proof(s).") ;
+ Util.error (Format.flush_str_formatter ())
+ end
+
+
+let suspend () =
+ rotate_top current_proof suspended
+
+let resume_last () =
+ rotate_top suspended current_proof
+
+let resume id =
+ rotate_find id suspended current_proof
+
+let discard_gen id =
+ try
+ ignore (extract id current_proof);
+ remove id proof_info
+ with NoSuchProof -> ignore (extract id suspended)
+
+let discard (loc,id) =
+ try
+ discard_gen id
+ with NoSuchProof ->
+ Util.user_err_loc
+ (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+
+let discard_current () =
+ let (id,_) = extract_top current_proof in
+ remove id proof_info
+
+let discard_all () =
+ current_proof := [];
+ suspended := [];
+ proof_info := Idmap.empty
+
+(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+ typically called by the Proof Mode command. *)
+(* Core component.
+ No undo handling.
+ Applies to proof [id], and proof mode [m]. *)
+let set_proof_mode m id =
+ let info = Idmap.find id !proof_info in
+ let info = { info with mode = m } in
+ proof_info := Idmap.add id info !proof_info;
+ update_proof_mode ()
+(* Complete function.
+ Handles undo.
+ Applies to current proof, and proof mode name [mn]. *)
+let set_proof_mode mn =
+ let m = Hashtbl.find proof_modes mn in
+ let id = get_current_proof_name () in
+ let pr = give_me_the_proof () in
+ Proof.add_undo begin let curr = !current_proof_mode in fun () ->
+ set_proof_mode curr id ; update_proof_mode ()
+ end pr ;
+ set_proof_mode m id
+
+(* [start_proof s str env t hook tac] starts a proof of name [s] and
+ conclusion [t]; [hook] is optionally a function to be applied at
+ proof end (e.g. to declare the built constructions as a coercion
+ or a setoid morphism); init_tac is possibly a tactic to
+ systematically apply at initialization time (e.g. to start the
+ proof of mutually dependent theorems).
+ It raises exception [ProofInProgress] if there is a proof being
+ currently edited. *)
+let start_proof id str goals ?(compute_guard=[]) hook =
+ (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+ let p = Proof.start goals in
+ add id { strength=str ;
+ compute_guard=compute_guard ;
+ hook=hook ;
+ mode = ! default_proof_mode } proof_info ;
+ push (id,p) current_proof
+
+(* arnaud: Ă  enlever *)
+let run_tactic tac =
+ let p = give_me_the_proof () in
+ let env = Global.env () in
+ Proof.run_tactic env tac p
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+ let p = give_me_the_proof () in
+ Proof.set_endline_tactic tac p
+
+let with_end_tac tac =
+ let p = give_me_the_proof () in
+ Proof.with_end_tac p tac
+
+let close_proof () =
+ (* spiwack: for now close_proof doesn't actually discard the proof, it is done
+ by [Command.save]. *)
+ try
+ let id = get_current_proof_name () in
+ let p = give_me_the_proof () in
+ let proofs_and_types = Proof.return p in
+ let entries = List.map (fun (c,t) -> { Entries.const_entry_body = c ;
+ const_entry_type = Some t;
+ const_entry_opaque = true ;
+ const_entry_boxed = false } )
+ proofs_and_types
+ in
+ let { compute_guard=cg ; strength=str ; hook=hook } =
+ Idmap.find id !proof_info
+ in
+ (id, (entries,cg,str,hook))
+ with
+ | Proof.UnfinishedProof ->
+ Util.error "Attempt to save an incomplete proof"
+ | Proof.HasUnresolvedEvar ->
+ Util.error "Attempt to save a proof with existential variables still non-instantiated"
+
+module V82 = struct
+ let get_current_initial_conclusions () =
+ let p = give_me_the_proof () in
+ let id = get_current_proof_name () in
+ let { strength=str ; hook=hook } =
+ Idmap.find id !proof_info
+ in
+ (id,(Proof.V82.get_initial_conclusions p, str, hook))
+end
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
new file mode 100644
index 0000000000..84a61c755a
--- /dev/null
+++ b/proofs/proof_global.mli
@@ -0,0 +1,89 @@
+(************************************************************************)
+(* 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$ *)
+
+(***********************************************************************)
+(* *)
+(* This module defines the global proof environment *)
+(* Especially it keeps tracks of whether or not there is *)
+(* a proof which is currently being edited. *)
+(* *)
+(***********************************************************************)
+
+(* Type of proof modes :
+ - A name
+ - A function [set] to set it *from standard mode*
+ - A function [reset] to reset the *standard mode* from it *)
+type proof_mode = {
+ name : string ;
+ set : unit -> unit ;
+ reset : unit -> unit
+}
+(* Registers a new proof mode which can then be adressed by name
+ in [set_default_proof_mode].
+ One mode is already registered - the standard mode - named "No",
+ It corresponds to Coq default setting are they are set when coqtop starts. *)
+val register_proof_mode : proof_mode -> unit
+
+val there_is_a_proof : unit -> bool
+val there_are_pending_proofs : unit -> bool
+val check_no_pending_proof : unit -> unit
+
+val get_current_proof_name : unit -> Names.identifier
+val get_all_proof_names : unit -> Names.identifier list
+
+val discard : Names.identifier Util.located -> unit
+val discard_current : unit -> unit
+val discard_all : unit -> unit
+
+(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+ typically called by the Proof Mode command. *)
+val set_proof_mode : string -> unit
+
+exception NoCurrentProof
+val give_me_the_proof : unit -> Proof.proof
+
+
+(* [start_proof s str goals ~init_tac ~compute_guard hook] starts
+ a proof of name [s] and
+ conclusion [t]; [hook] is optionally a function to be applied at
+ proof end (e.g. to declare the built constructions as a coercion
+ or a setoid morphism). *)
+type lemma_possible_guards = int list list
+val start_proof : Names.identifier ->
+ Decl_kinds.goal_kind ->
+ (Environ.env * Term.types) list ->
+ ?compute_guard:lemma_possible_guards ->
+ Tacexpr.declaration_hook ->
+ unit
+
+val close_proof : unit ->
+ Names.identifier *
+ (Entries.definition_entry list *
+ lemma_possible_guards *
+ Decl_kinds.goal_kind *
+ Tacexpr.declaration_hook)
+
+val suspend : unit -> unit
+val resume_last : unit -> unit
+val resume : Names.identifier -> unit
+
+(* Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
+ no current proof. *)
+val run_tactic : unit Proofview.tactic -> unit
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+val set_endline_tactic : unit Proofview.tactic -> unit
+
+(* Appends the endline tactic of the current proof to a tactic. *)
+val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
+
+module V82 : sig
+ val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
+end
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
deleted file mode 100644
index a5bd073a30..0000000000
--- a/proofs/proof_trees.ml
+++ /dev/null
@@ -1,107 +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 Closure
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Sign
-open Evd
-open Environ
-open Evarutil
-open Decl_expr
-open Proof_type
-open Tacred
-open Typing
-open Libnames
-open Nametab
-
-(*
-let is_bind = function
- | Tacexpr.Cbindings _ -> true
- | _ -> false
-*)
-
-(* Functions on goals *)
-
-let mk_goal hyps cl extra =
- { evar_hyps = hyps; evar_concl = cl;
- evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
- evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar);
- evar_extra = extra }
-
-(* Functions on proof trees *)
-
-let ref_of_proof pf =
- match pf.ref with
- | None -> failwith "rule_of_proof"
- | Some r -> r
-
-let rule_of_proof pf =
- let (r,_) = ref_of_proof pf in r
-
-let children_of_proof pf =
- let (_,cl) = ref_of_proof pf in cl
-
-let goal_of_proof pf = pf.goal
-
-let subproof_of_proof pf = match pf.ref with
- | Some (Nested (_,pf), _) -> pf
- | _ -> failwith "subproof_of_proof"
-
-let status_of_proof pf = pf.open_subgoals
-
-let is_complete_proof pf = pf.open_subgoals = 0
-
-let is_leaf_proof pf = (pf.ref = None)
-
-let is_tactic_proof pf = match pf.ref with
- | Some (Nested (Tactic _,_),_) -> true
- | _ -> false
-
-
-let pf_lookup_name_as_displayed env ccl s =
- Detyping.lookup_name_as_displayed env ccl s
-
-let pf_lookup_index_as_renamed env ccl n =
- Detyping.lookup_index_as_renamed env ccl n
-
-(* Functions on rules (Proof mode) *)
-
-let is_dem_rule = function
- Decl_proof _ -> true
- | _ -> false
-
-let is_proof_instr = function
- Nested(Proof_instr (_,_),_) -> true
- | _ -> false
-
-let is_focussing_command = function
- Decl_proof b -> b
- | Nested (Proof_instr (b,_),_) -> b
- | _ -> false
-
-
-(*********************************************************************)
-(* Pretty printing functions *)
-(*********************************************************************)
-
-open Pp
-
-let db_pr_goal g =
- let env = evar_env g in
- let penv = print_named_context env in
- let pc = print_constr_env env g.evar_concl in
- str" " ++ hv 0 (penv ++ fnl () ++
- str "============================" ++ fnl () ++
- str" " ++ pc) ++ fnl ()
-
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
deleted file mode 100644
index 6d1fc143d3..0000000000
--- a/proofs/proof_trees.mli
+++ /dev/null
@@ -1,48 +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 Evd
-open Environ
-open Proof_type
-(*i*)
-
-(* This module declares readable constraints, and a few utilities on
- constraints and proof trees *)
-
-val mk_goal : named_context_val -> constr -> Dyn.t option -> goal
-
-val rule_of_proof : proof_tree -> rule
-val ref_of_proof : proof_tree -> (rule * proof_tree list)
-val children_of_proof : proof_tree -> proof_tree list
-val goal_of_proof : proof_tree -> goal
-val subproof_of_proof : proof_tree -> proof_tree
-val status_of_proof : proof_tree -> int
-val is_complete_proof : proof_tree -> bool
-val is_leaf_proof : proof_tree -> bool
-val is_tactic_proof : proof_tree -> bool
-
-val pf_lookup_name_as_displayed : env -> constr -> identifier -> int option
-val pf_lookup_index_as_renamed : env -> constr -> int -> int option
-
-val is_proof_instr : rule -> bool
-val is_focussing_command : rule -> bool
-
-(*s Pretty printing functions. *)
-
-(*i*)
-open Pp
-(*i*)
-
-val db_pr_goal : goal -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index bc29534081..2fffa39527 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -16,7 +16,7 @@ open Libnames
open Term
open Util
open Tacexpr
-open Decl_expr
+(* open Decl_expr *)
open Rawterm
open Genarg
open Nametab
@@ -26,6 +26,10 @@ open Pattern
(* This module defines the structure of proof tree and the tactic type. So, it
is used by Proof_tree and Refiner *)
+type goal = Goal.goal
+
+type tactic = goal sigma -> goal list sigma
+
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
@@ -54,13 +58,6 @@ and rule =
and compound_rule=
| Tactic of tactic_expr * bool
- | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
-
-and goal = evar_info
-
-and tactic = goal sigma -> (goal list sigma * validation)
-
-and validation = (proof_tree list -> proof_tree)
and tactic_expr =
(constr,
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b5c4a234d1..9692f19bc9 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -16,7 +16,6 @@ open Libnames
open Term
open Util
open Tacexpr
-open Decl_expr
open Rawterm
open Genarg
open Nametab
@@ -26,6 +25,10 @@ open Pattern
(* This module defines the structure of proof tree and the tactic type. So, it
is used by [Proof_tree] and [Refiner] *)
+type goal = Goal.goal
+
+type tactic = goal sigma -> goal list sigma
+
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
@@ -89,13 +92,6 @@ and rule =
and compound_rule=
(* the boolean of Tactic tells if the default tactic is used *)
| Tactic of tactic_expr * bool
- | Proof_instr of bool * proof_instr
-
-and goal = evar_info
-
-and tactic = goal sigma -> (goal list sigma * validation)
-
-and validation = (proof_tree list -> proof_tree)
and tactic_expr =
(constr,
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 05b86b1a04..66001e77a5 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,12 +1,15 @@
+Goal
+Evar_refiner
+Proofview
+Proof
+Proof_global
Tacexpr
Proof_type
Redexpr
-Proof_trees
Logic
Refiner
-Evar_refiner
Tacmach
Pfedit
Tactic_debug
+Clenv
Clenvtac
-Decl_mode
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
new file mode 100644
index 0000000000..a08941df03
--- /dev/null
+++ b/proofs/proofview.ml
@@ -0,0 +1,491 @@
+(************************************************************************)
+(* 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$ *)
+
+(* The proofview datastructure is a pure datastructure underlying the notion
+ of proof (namely, a proof is a proofview which can evolve and has safety
+ mechanisms attached).
+ The general idea of the structure is that it is composed of a chemical
+ solution: an unstructured bag of stuff which has some relations with
+ one another, which represents the various subnodes of the proof, together
+ with a comb: a datastructure that gives order to some of these nodes,
+ namely the open goals.
+ The natural candidate for the solution is an {!Evd.evar_map}, that is
+ a calculus of evars. The comb is then a list of goals (evars wrapped
+ with some extra information, like possible name anotations).
+ There is also need of a list of the evars which initialised the proofview
+ to be able to return information about the proofview. *)
+
+(* Type of proofviews. *)
+type proofview = {
+ initial : (Term.constr * Term.types) list;
+ solution : Evd.evar_map;
+ comb : Goal.goal list
+ }
+
+(* Initialises a proofview, the argument is a list of environement,
+ conclusion types, and optional names, creating that many initial goals. *)
+let init =
+ let rec aux = function
+ | [] -> { initial = [] ;
+ solution = Evd.empty ;
+ comb = []
+ }
+ | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
+ aux l
+ in
+ let ( new_defs , econstr ) =
+ Evarutil.new_evar sol env typ
+ in
+ let (e,_) = Term.destEvar econstr in
+ let gl = Goal.build e in
+ { initial = (econstr,typ)::ret;
+ solution = new_defs ;
+ comb = gl::comb }
+ in
+ fun l -> let v = aux l in
+ (* Marks all the goal unresolvable for typeclasses. *)
+ { v with solution = Typeclasses.mark_unresolvables v.solution }
+
+(* Returns whether this proofview is finished or not. That is,
+ if it has empty subgoals in the comb. There could still be unsolved
+ subgoaled, but they would then be out of the view, focused out. *)
+let finished = function
+ | {comb = []} -> true
+ | _ -> false
+
+(* Returns the current value of the proofview partial proofs. *)
+let return { initial=init; solution=defs } =
+ List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init
+
+(* spiwack: this function should probably go in the Util section,
+ but I'd rather have Util (or a separate module for lists)
+ raise proper exceptions before *)
+(* [IndexOutOfRange] occurs in case of malformed indices
+ with respect to list lengths. *)
+exception IndexOutOfRange
+
+(* [list_goto i l] returns a pair of lists [c,t] where
+ [c] has length [i] and is the reversed of the [i] first
+ elements of [l], and [t] is the rest of the list.
+ The idea is to navigate through the list, [c] is then
+ seen as the context of the current position.
+ Raises [IndexOutOfRange] if [i > length l]*)
+let list_goto =
+ let rec aux acc index = function
+ | l when index = 0-> (acc,l)
+ | [] -> raise IndexOutOfRange
+ | a::q -> aux (a::acc) (index-1) q
+ in
+ fun i l ->
+ if i < 0 then
+ raise IndexOutOfRange
+ else
+ aux [] i l
+
+(* Type of the object which allow to unfocus a view.*)
+(* First component is a reverse list of what comes before
+ and second component is what goes after (in the expected
+ order) *)
+type focus_context = Goal.goal list * Goal.goal list
+
+(* This (internal) function extracts a sublist between two indices, and
+ returns this sublist together with its context:
+ if it returns [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
+ original list.
+ The focused list has lenght [j-i-1] and contains the goals from
+ number [i] to number [j] (both included) the first goal of the list
+ being numbered [1].
+ [focus_sublist i j l] raises [IndexOutOfRange] if
+ [i > length l], or [j > length l] or [ j < i ]. *)
+let focus_sublist i j l =
+ let (left,sub_right) = list_goto (i-1) l in
+ let (sub, right) =
+ try
+ Util.list_chop (j-i+1) sub_right
+ with Failure "list_chop" ->
+ Util.errorlabstrm "nth_unproven" (Pp.str"Not such unproven subgoal")
+ in
+ (sub, (left,right))
+
+(* Inverse operation to the previous one. *)
+let unfocus_sublist (left,right) s =
+ List.rev_append left (s@right)
+
+
+(* [focus i j] focuses a proofview on the goals from index [i] to index [j]
+ (inclusive). (i.e. goals number [i] to [j] become the only goals of the
+ returned proofview).
+ It returns the focus proof, and a context for the focus trace. *)
+let focus i j sp =
+ let (new_comb, context) = focus_sublist i j sp.comb in
+ ( { sp with comb = new_comb } , context )
+
+(* Unfocuses a proofview with respect to a context. *)
+let undefined defs l =
+ Option.List.flatten (List.map (Goal.advance defs) l)
+let unfocus c sp =
+ { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
+
+
+(* The tactic monad:
+ - Tactics are objects which apply a transformation to all
+ the subgoals of the current view at the same time. By opposed
+ to the old vision of applying it to a single goal. It mostly
+ allows to consider tactic like [reorder] to reorder the goals
+ in the current view (which might be useful for the tactic designer)
+ (* spiwack: the ordering of goals, though, is perhaps a bit
+ brittle. It would be much more interesting to find a more
+ robust way to adress goals, I have no idea at this time
+ though*)
+ or global automation tactic for dependent subgoals (instantiating
+ an evar has influences on the other goals of the proof in progress,
+ not being able to take that into account causes the current eauto
+ tactic to fail on some instances where it could succeed).
+ - Tactics are a monad ['a tactic], in a sense a tactic can be
+ seens as a function (without argument) which returns a value
+ of type 'a and modifies the environement (in our case: the view).
+ Tactics of course have arguments, but these are given at the
+ meta-level as OCaml functions.
+ Most tactics, in the sense we are used to, return [ () ], that is
+ no really interesting values. But some might pass information
+ around; the [(>>--)] and [(>>==)] bind-like construction are the
+ main ingredients of this information passing.
+ (* spiwack: I don't know how much all this relates to F. Kirchner and
+ C. Muñoz. I wasn't able to understand how they used the monad
+ structure in there developpement.
+ *)
+ The tactics seen in Coq's Ltac are (for now at least) only
+ [unit tactic], the return values are kept for the OCaml toolkit.
+ The operation or the monad are [Proofview.tclUNIT] (which is the
+ "return" of the tactic monad) [Proofview.tclBIND] (which is
+ the "bind", also noted [(>=)]) and [Proofview.tclTHEN] (which is a
+ specialized bind on unit-returning tactics).
+*)
+
+(* type of tactics *)
+(* spiwack: double-continuation backtracking monads are reasonable
+ folklore for "search" implementations (including Tac interactive prover's
+ tactics). Yet it's quite hard to wrap your head around these.
+ I recommand reading a few times the "Backtracking, Interleaving, and Terminating
+ Monad Transformers" paper by O. Kiselyov, C. Chen, D. Fridman.
+ The peculiar shape of the monadic type is reminiscent of that of the continuation
+ monad transformer.
+ A good way to get a feel of what's happening is to look at what happens when
+ executing [apply (tclUNIT ())].
+ The disjunction function is unlike that of the LogicT paper, because we want and
+ need to backtrack over state as well as values. Therefore we cannot be
+ polymorphic over the inner monad. *)
+type proof_step = { goals : Goal.goal list ; defs : Evd.evar_map }
+type +'a result = { proof_step : proof_step ;
+ content : 'a }
+
+(* nb=non-backtracking *)
+type +'a nb_tactic = proof_step -> 'a result
+
+(* double-continutation backtracking *)
+(* "sk" stands for "success continuation", "fk" for "failure continuation" *)
+type 'r fk = exn -> 'r
+type (-'a,'r) sk = 'a -> 'r fk -> 'r
+type +'a tactic0 = { go : 'r. ('a, 'r nb_tactic) sk -> 'r nb_tactic fk -> 'r nb_tactic }
+
+(* We obtain a tactic by parametrizing with an environment *)
+(* spiwack: alternatively the environment could be part of the "nb_tactic" state
+ monad. As long as we do not intend to change the environment during a tactic,
+ it's probably better here. *)
+type +'a tactic = Environ.env -> 'a tactic0
+
+(* unit of [nb_tactic] *)
+let nb_tac_unit a step = { proof_step = step ; content = a }
+
+(* Applies a tactic to the current proofview. *)
+let apply env t sp =
+ let start = { goals = sp.comb ; defs = sp.solution } in
+ let res = (t env).go (fun a _ step -> nb_tac_unit a step) (fun e _ -> raise e) start in
+ let next = res.proof_step in
+ {sp with
+ solution = next.defs ;
+ comb = next.goals
+ }
+
+(*** tacticals ***)
+
+
+(* Unit of the tactic monad *)
+let tclUNIT a _ = { go = fun sk fk step -> sk a fk step }
+
+(* Bind operation of the tactic monad *)
+let tclBIND t k env = { go = fun sk fk step ->
+ (t env).go (fun a fk -> (k a env).go sk fk) fk step
+}
+
+(* Interpretes the ";" (semicolon) of Ltac.
+ As a monadic operation, it's a specialized "bind"
+ on unit-returning tactic (meaning "there is no value to bind") *)
+let tclTHEN t1 t2 env = { go = fun sk fk step ->
+ (t1 env).go (fun () fk -> (t2 env).go sk fk) fk step
+}
+
+(* [tclIGNORE t] has the same operational content as [t],
+ but drops the value at the end. *)
+let tclIGNORE tac env = { go = fun sk fk step ->
+ (tac env).go (fun _ fk -> sk () fk) fk step
+}
+
+(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t1 fails.
+ No interleaving for the moment. *)
+(* spiwack: compared to the LogicT paper, we backtrack at the same state
+ where [t1] has been called, not the state where [t1] failed. *)
+let tclOR t1 t2 env = { go = fun sk fk step ->
+ (t1 env).go sk (fun _ _ -> (t2 env).go sk fk step) step
+}
+
+(* [tclZERO e] always fails with error message [e]*)
+let tclZERO e env = { go = fun _ fk step -> fk e step }
+
+
+(* Focusing operation on proof_steps. *)
+let focus_proof_step i j ps =
+ let (new_subgoals, context) = focus_sublist i j ps.goals in
+ ( { ps with goals = new_subgoals } , context )
+
+(* Unfocusing operation of proof_steps. *)
+let unfocus_proof_step c ps =
+ { ps with
+ goals = undefined ps.defs (unfocus_sublist c ps.goals)
+ }
+
+(* Focuses a tactic at a range of subgoals, found by their indices. *)
+(* arnaud: bug if 0 goals ! *)
+let tclFOCUS i j t env = { go = fun sk fk step ->
+ let (focused,context) = focus_proof_step i j step in
+ (t env).go (fun a fk step -> sk a fk (unfocus_proof_step context step)) fk focused
+}
+
+(* Dispatch tacticals are used to apply a different tactic to each goal under
+ consideration. They come in two flavours:
+ [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
+ [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
+ and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
+ corresponds to that of the tactic which created [g].
+ It is to be noted that the return value of [tclDISPATCHS ts] makes only
+ sense in the goals immediatly built by it, and would cause an anomaly
+ is used otherwise. *)
+exception SizeMismatch
+(* spiwack: we use an parametrised function to generate the dispatch tacticals.
+ [tclDISPATCHGEN] takes a [null] argument to generate the return value
+ if there are no goal under focus, and a [join] argument to explain how
+ the return value at two given lists of subgoals are combined when
+ both lists are being concatenated.
+ [join] and [null] need be some sort of comutative monoid. *)
+let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
+ match tacs,step.goals with
+ | [] , [] -> (tclUNIT null env).go sk fk step
+ | t::tacs , first::goals ->
+ (tclDISPATCHGEN null join tacs env).go
+ begin fun x fk step ->
+ match Goal.advance step.defs first with
+ | None -> sk x fk step
+ | Some first ->
+ (t env).go
+ begin fun y fk step' ->
+ sk (join x y) fk { step' with
+ goals = step'.goals@step.goals
+ }
+ end
+ fk
+ { step with goals = [first] }
+ end
+ fk
+ { step with goals = goals }
+ | _ -> raise SizeMismatch
+}
+
+(* takes a tactic which can raise exception and makes it pure by *failing*
+ on with these exceptions. Does not catch anomalies. *)
+let purify t =
+ let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
+ with Util.Anomaly _ as e -> raise e
+ | e -> sk (Util.Inr e) fk step
+ }
+ in
+ tclBIND t' begin function
+ | Util.Inl x -> tclUNIT x
+ | Util.Inr e -> tclZERO e
+ end
+let tclDISPATCHGEN null join tacs = purify (tclDISPATCHGEN null join tacs)
+
+let unitK () () = ()
+let tclDISPATCH = tclDISPATCHGEN () unitK
+
+let extend_to_list =
+ let rec copy n x l =
+ if n < 0 then raise SizeMismatch
+ else if n = 0 then l
+ else copy (n-1) x (x::l)
+ in
+ fun startxs rx endxs l ->
+ let ns = List.length startxs in
+ let ne = List.length endxs in
+ let n = List.length l in
+ startxs@(copy (n-ne-ns) rx endxs)
+let tclEXTEND tacs1 rtac tacs2 env = { go = fun sk fk step ->
+ let tacs = extend_to_list tacs1 rtac tacs2 step.goals in
+ (tclDISPATCH tacs env).go sk fk step
+}
+
+(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
+ [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
+ Allows backtracking between goals. *)
+let list_of_sensitive s k env step =
+ Goal.list_map begin fun defs g ->
+ let (a,defs) = Goal.eval s env defs g in
+ (k a) , defs
+ end step.goals step.defs
+(* In form of a tactic *)
+let list_of_sensitive s k env = { go = fun sk fk step ->
+ let (tacs,defs) = list_of_sensitive s k env step in
+ sk tacs fk { step with defs = defs }
+}
+
+(* This is a helper function for the dispatching tactics (like [tclGOALBIND] and
+ [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic
+ whose return value is, again, ['a sensitive] but only has value in the
+ (unmodified) goals under focus. *)
+let here_s b env = { go = fun sk fk step ->
+ sk (Goal.bind (Goal.here_list step.goals b) (fun b -> b)) fk step
+}
+
+let rec tclGOALBIND s k =
+ (* spiwack: the first line ensures that the value returned by the tactic [k] will
+ not "escape its scope". *)
+ let k a = tclBIND (k a) here_s in
+ purify begin
+ tclBIND (list_of_sensitive s k) begin fun tacs ->
+ tclDISPATCHGEN Goal.null Goal.plus tacs
+ end
+ end
+
+(* spiwack: this should probably be moved closer to the [tclDISPATCH] tactical. *)
+let tclDISPATCHS tacs =
+ let tacs =
+ List.map begin fun tac ->
+ tclBIND tac here_s
+ end tacs
+ in
+ purify begin
+ tclDISPATCHGEN Goal.null Goal.plus tacs
+ end
+
+let rec tclGOALBINDU s k =
+ purify begin
+ tclBIND (list_of_sensitive s k) begin fun tacs ->
+ tclDISPATCHGEN () unitK tacs
+ end
+ end
+
+(* spiwack: up to a few details, same errors are in the Logic module.
+ this should be maintained synchronized, probably. *)
+open Pretype_errors
+let rec catchable_exception = function
+ | Stdpp.Exc_located(_,e) -> catchable_exception e
+ | Util.UserError _ | Type_errors.TypeError _
+ | Indrec.RecursionSchemeError _
+ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+ (* unification errors *)
+ | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+ |CannotFindWellTypedAbstraction _
+ |UnsolvableImplicit _)) -> true
+ | Typeclasses_errors.TypeClassError
+ (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+ | _ -> false
+
+(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
+ everything is done in one step. *)
+let sensitive_on_step s env step =
+ let wrap g ((defs, partial_list) as partial_res) =
+ match Goal.advance defs g with
+ | None ->partial_res
+ | Some g ->
+ let {Goal.subgoals = sg } , d' = Goal.eval s env defs g in
+ (d',sg::partial_list)
+ in
+ let ( new_defs , combed_subgoals ) =
+ List.fold_right wrap step.goals (step.defs,[])
+ in
+ { defs = new_defs;
+ goals = List.flatten combed_subgoals }
+let tclSENSITIVE s =
+ purify begin
+ fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
+ end
+
+module Notations = struct
+ let (>-) = Goal.bind
+ let (>>-) = tclGOALBINDU
+ let (>>--) = tclGOALBIND
+ let (>=) = tclBIND
+ let (>>=) t k = t >= fun s -> s >>- k
+ let (>>==) t k = t >= fun s -> s >>-- k
+ let (<*>) = tclTHEN
+ let (<+>) = tclOR
+end
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 = struct
+ type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+
+ let tactic tac _ = { go = fun sk fk ps ->
+ (* spiwack: we ignore the dependencies between goals here, expectingly
+ preserving the semantics of <= 8.2 tactics *)
+ let tac evd gl =
+ let glsigma = tac { Evd.it = gl ; Evd.sigma = evd } in
+ let sigma = glsigma.Evd.sigma in
+ let g = glsigma.Evd.it in
+ ( g , sigma )
+ in
+ (* Old style tactics expect the goals normalized with respect to evars. *)
+ let (initgoals,initevd) =
+ Goal.list_map Goal.V82.nf_evar ps.goals ps.defs
+ in
+ let (goalss,evd) = Goal.list_map tac initgoals initevd in
+ let sgs = List.flatten goalss in
+ sk () fk { defs = evd ; goals = sgs }
+}
+
+ let has_unresolved_evar pv =
+ let evd = pv.solution in
+ (* arnaud: essayer une procédure moins coûteuse *)
+ not ((Evarutil.non_instantiated evd) = [])
+
+ (* Returns the open goals of the proofview together with the evar_map to
+ interprete them. *)
+ let goals { comb = comb ; solution = solution } =
+ { Evd.it = comb ; sigma = solution}
+
+ let top_goals { initial=initial ; solution=solution } =
+ let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
+ { Evd.it = goals ; sigma=solution }
+
+ let instantiate_evar n com pv =
+ let (evk,_) =
+ let evl = Evarutil.non_instantiated pv.solution in
+ if (n <= 0) then
+ Util.error "incorrect existential variable index"
+ else if List.length evl < n then
+ Util.error "not so many uninstantiated existential variables"
+ else
+ List.nth evl (n-1)
+ in
+ { pv with
+ solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
+
+ let purify = purify
+end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
new file mode 100644
index 0000000000..cd5520d4e5
--- /dev/null
+++ b/proofs/proofview.mli
@@ -0,0 +1,203 @@
+(************************************************************************)
+(* 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: proofview.mli aspiwack $ *)
+
+(* The proofview datastructure is a pure datastructure underlying the notion
+ of proof (namely, a proof is a proofview which can evolve and has safety
+ mechanisms attached).
+ The general idea of the structure is that it is composed of a chemical
+ solution: an unstructured bag of stuff which has some relations with
+ one another, which represents the various subnodes of the proof, together
+ with a comb: a datastructure that gives order to some of these nodes,
+ namely the open goals.
+ The natural candidate for the solution is an {!Evd.evar_map}, that is
+ a calculus of evars. The comb is then a list of goals (evars wrapped
+ with some extra information, like possible name anotations).
+ There is also need of a list of the evars which initialised the proofview
+ to be able to return information about the proofview. *)
+
+open Term
+
+type proofview
+
+(* Initialises a proofview, the argument is a list of environement,
+ conclusion types, creating that many initial goals. *)
+val init : (Environ.env * Term.types) list -> proofview
+
+(* Returns whether this proofview is finished or not.That is,
+ if it has empty subgoals in the comb. There could still be unsolved
+ subgoaled, but they would then be out of the view, focused out. *)
+val finished : proofview -> bool
+
+(* Returns the current value of the proofview partial proofs. *)
+val return : proofview -> (constr*types) list
+
+
+(*** Focusing operations ***)
+
+(* [IndexOutOfRange] occurs in case of malformed indices
+ with respect to list lengths. *)
+exception IndexOutOfRange
+
+(* Type of the object which allow to unfocus a view.*)
+type focus_context
+
+(* [focus i j] focuses a proofview on the goals from index [i] to index [j]
+ (inclusive). (i.e. goals number [i] to [j] become the only goals of the
+ returned proofview).
+ It returns the focus proof, and a context for the focus trace. *)
+val focus : int -> int -> proofview -> proofview * focus_context
+
+(* Unfocuses a proofview with respect to a context. *)
+val unfocus : focus_context -> proofview -> proofview
+
+(* The tactic monad:
+ - Tactics are objects which apply a transformation to all
+ the subgoals of the current view at the same time. By opposed
+ to the old vision of applying it to a single goal. It mostly
+ allows to consider tactic like [reorder] to reorder the goals
+ in the current view (which might be useful for the tactic designer)
+ (* spiwack: the ordering of goals, though, is actually rather
+ brittle. It would be much more interesting to find a more
+ robust way to adress goals, I have no idea at this time
+ though*)
+ or global automation tactic for dependent subgoals (instantiating
+ an evar has influences on the other goals of the proof in progress,
+ not being able to take that into account causes the current eauto
+ tactic to fail on some instances where it could succeed).
+ - Tactics are a monad ['a tactic], in a sense a tactic can be
+ seens as a function (without argument) which returns a value
+ of type 'a and modifies the environement (in our case: the view).
+ Tactics of course have arguments, but these are given at the
+ meta-level as OCaml functions.
+ Most tactics in the sense we are used to return [ () ], that is
+ no really interesting values. But some might, to pass information
+ around; for instance [Proofview.freeze] allows to store a certain
+ goal sensitive value "at the present time" (which means, considering the
+ structure of the dynamics of proofs, [Proofview.freeze s] will have,
+ for every current goal [gl], and for any of its descendent [g'] in
+ the future the same value in [g'] that in [gl]).
+ (* spiwack: I don't know how much all this relates to F. Kirchner and
+ C. Muñoz. I wasn't able to understand how they used the monad
+ structure in there developpement.
+ *)
+ The tactics seen in Coq's Ltac are (for now at least) only
+ [unit tactic], the return values are kept for the OCaml toolkit.
+ The operation or the monad are [Proofview.tclIDTAC] (which is the
+ "return" of the tactic monad) [Proofview.tclBIND] (which is
+ the "bind") and [Proofview.tclTHEN] (which is a specialized
+ bind on unit-returning tactics).
+*)
+
+
+type +'a tactic
+
+(* Applies a tactic to the current proofview. *)
+val apply : Environ.env -> 'a tactic -> proofview -> proofview
+
+(*** tacticals ***)
+
+(* Unit of the tactic monad *)
+val tclUNIT : 'a -> 'a tactic
+
+(* Bind operation of the tactic monad *)
+val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
+(* Interpetes the ";" (semicolon) of Ltac.
+ As a monadic operation, it's a specialized "bind"
+ on unit-returning tactic (meaning "there is no value to bind") *)
+val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
+
+(* [tclIGNORE t] has the same operational content as [t],
+ but drops the value at the end. *)
+val tclIGNORE : 'a tactic -> unit tactic
+
+(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t2 fails.
+ No interleaving at this point. *)
+val tclOR : 'a tactic -> 'a tactic -> 'a tactic
+
+(* [tclZERO] always fails *)
+val tclZERO : exn -> 'a tactic
+
+(* Focuses a tactic at a range of subgoals, found by their indices. *)
+val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
+
+(* Dispatch tacticals are used to apply a different tactic to each goal under
+ consideration. They come in two flavours:
+ [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
+ [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
+ and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
+ corresponds to that of the tactic which created [g].
+ It is to be noted that the return value of [tclDISPATCHS ts] makes only
+ sense in the goals immediatly built by it, and would cause an anomaly
+ is used otherwise. *)
+val tclDISPATCH : unit tactic list -> unit tactic
+val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
+
+(* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
+ is "repeated" enough time such that every goal has a tactic assigned to it
+ ([b] is the list of tactics applied to the first goals, [e] to the last goals, and [r]
+ is applied to every goal in between. *)
+val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
+
+(* A sort of bind which takes a [Goal.sensitive] as a first argument,
+ the tactic then acts on each goal separately.
+ Allows backtracking between goals. *)
+val tclGOALBIND : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
+
+(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
+val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
+
+(* Notations for building tactics. *)
+module Notations : sig
+ (* Goal.bind *)
+ val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
+ (* tclGOALBINDU *)
+ val (>>-) : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
+ (* tclGOALBIND *)
+ val (>>--) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+
+ (* tclBIND *)
+ val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
+ (* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
+ tactic monad and the goal-sensitive monad.
+ It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
+ needs a bind, since it usually avoids to delay the interpretation of the
+ goal sensitive value to a location where it does not make sense anymore. *)
+ val (>>=) : 'a Goal.sensitive tactic -> ('a -> unit tactic) -> unit tactic
+ val (>>==) : 'a Goal.sensitive tactic -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+
+ (* tclTHEN *)
+ val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+ (* tclOR *)
+ val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
+end
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 : sig
+ type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+ val tactic : tac -> unit tactic
+
+ val has_unresolved_evar : proofview -> bool
+
+ (* Returns the open goals of the proofview together with the evar_map to
+ interprete them. *)
+ val goals : proofview -> Goal.goal list Evd.sigma
+
+ val top_goals : proofview -> Goal.goal list Evd.sigma
+
+ (* Implements the Existential command *)
+ val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview
+
+ (* spiwack: [purify] might be useful while writing tactics manipulating exception
+ explicitely or from the [V82] submodule (neither being advised, though *)
+ val purify : 'a tactic -> 'a tactic
+end
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a320b67cda..ffb18f2655 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -18,53 +18,20 @@ open Sign
open Environ
open Reductionops
open Type_errors
-open Proof_trees
open Proof_type
open Logic
-type transformation_tactic = proof_tree -> (goal list * validation)
-
-let hypotheses gl = gl.evar_hyps
-let conclusion gl = gl.evar_concl
let sig_it x = x.it
let project x = x.sigma
-let pf_status pf = pf.open_subgoals
-
-let is_complete pf = (0 = (pf_status pf))
-
-let on_open_proofs f pf = if is_complete pf then pf else f pf
let and_status = List.fold_left (+) 0
(* Getting env *)
-let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
-let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
-
-
-let descend n p =
- match p.ref with
- | None -> error "It is a leaf."
- | Some(r,pfl) ->
- if List.length pfl >= n then
- (match list_chop (n-1) pfl with
- | left,(wanted::right) ->
- (wanted,
- (fun pfl' ->
- if false (* debug *) then assert
- (List.length pfl'=1 & (List.hd pfl').goal = wanted.goal);
- let pf' = List.hd pfl' in
- let spfl = left@(pf'::right) in
- let newstatus = and_status (List.map pf_status spfl) in
- { p with
- open_subgoals = newstatus;
- ref = Some(r,spfl) }))
- | _ -> assert false)
- else
- error "Too few subproofs"
-
+let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
+let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
gives
@@ -80,121 +47,9 @@ let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
let m,l = list_chop h l in
(List.hd fl m) :: (mapshape t (List.tl fl) l)
-(* [frontier : proof_tree -> goal list * validation]
- given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
- to be solved to complete the proof, and [v] is the corresponding
- validation *)
-
-let rec frontier p =
- match p.ref with
- | None ->
- ([p.goal],
- (fun lp' ->
- let p' = List.hd lp' in
- if Evd.eq_evar_info p'.goal p.goal then
- p'
- else
- errorlabstrm "Refiner.frontier"
- (str"frontier was handed back a ill-formed proof.")))
- | Some(r,pfl) ->
- let gll,vl = List.split(List.map frontier pfl) in
- (List.flatten gll,
- (fun retpfl ->
- let pfl' = mapshape (List.map List.length gll) vl retpfl in
- { p with
- open_subgoals = and_status (List.map pf_status pfl');
- ref = Some(r,pfl')}))
-
-(* TODO LEM: I might have to make sure that these hooks are called
- only when called from solve_nth_pftreestate; I can build the hook
- call into the "f", then.
- *)
-let solve_hook = ref ignore
-let set_solve_hook = (:=) solve_hook
-
-let rec frontier_map_rec f n p =
- if n < 1 || n > p.open_subgoals then p else
- match p.ref with
- | None ->
- let p' = f p in
- if Evd.eq_evar_info p'.goal p.goal then
- begin
- !solve_hook p';
- p'
- end
- else
- errorlabstrm "Refiner.frontier_map"
- (str"frontier_map was handed back a ill-formed proof.")
- | Some(r,pfl) ->
- let (_,rpfl') =
- List.fold_left
- (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
- (n,[]) pfl in
- let pfl' = List.rev rpfl' in
- { p with
- open_subgoals = and_status (List.map pf_status pfl');
- ref = Some(r,pfl')}
-
-let frontier_map f n p =
- let nmax = p.open_subgoals in
- let n = if n < 0 then nmax + n + 1 else n in
- if n < 1 || n > nmax then
- errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
- frontier_map_rec f n p
-
-let rec frontier_mapi_rec f i p =
- if p.open_subgoals = 0 then p else
- match p.ref with
- | None ->
- let p' = f i p in
- if Evd.eq_evar_info p'.goal p.goal then
- begin
- !solve_hook p';
- p'
- end
- else
- errorlabstrm "Refiner.frontier_mapi"
- (str"frontier_mapi was handed back a ill-formed proof.")
- | Some(r,pfl) ->
- let (_,rpfl') =
- List.fold_left
- (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
- (i,[]) pfl in
- let pfl' = List.rev rpfl' in
- { p with
- open_subgoals = and_status (List.map pf_status pfl');
- ref = Some(r,pfl')}
-
-let frontier_mapi f p = frontier_mapi_rec f 1 p
-
-(* [list_pf p] is the lists of goals to be solved in order to complete the
- proof [p] *)
-
-let list_pf p = fst (frontier p)
-
-let rec nb_unsolved_goals pf = pf.open_subgoals
-
-(* leaf g is the canonical incomplete proof of a goal g *)
-
-let leaf g =
- { open_subgoals = 1;
- goal = g;
- ref = None }
-
-(* refiner r is a tactic applying the rule r *)
-
-let check_subproof_connection gl spfl =
- list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
-
-let abstract_operation syntax semantics gls =
- let (sgl_sigma,validation) = semantics gls in
- let hidden_proof = validation (List.map leaf sgl_sigma.it) in
- (sgl_sigma,
- fun spfl ->
- assert (check_subproof_connection sgl_sigma.it spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = gls.it;
- ref = Some(Nested(syntax,hidden_proof),spfl)})
+
+let abstract_operation syntax semantics =
+ semantics
let abstract_tactic_expr ?(dflt=false) te tacfun gls =
abstract_operation (Tactic(te,dflt)) tacfun gls
@@ -207,16 +62,11 @@ let abstract_extended_tactic ?(dflt=false) s args =
abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
let refiner = function
- | Prim pr as r ->
+ | Prim pr ->
let prim_fun = prim_refiner pr in
(fun goal_sigma ->
let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
- ({it=sgl; sigma = sigma'},
- (fun spfl ->
- assert (check_subproof_connection sgl spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = goal_sigma.it;
- ref = Some(r,spfl) })))
+ {it=sgl; sigma = sigma'})
| Nested (_,_) | Decl_proof _ ->
@@ -226,83 +76,15 @@ let refiner = function
| Daimon ->
fun gls ->
- ({it=[];sigma=gls.sigma},
- fun spfl ->
- assert (spfl=[]);
- { open_subgoals = 0;
- goal = gls.it;
- ref = Some(Daimon,[])})
+ {it=[];sigma=gls.sigma}
let norm_evar_tac gl = refiner (Prim Change_evars) gl
-let norm_evar_proof sigma pf =
- let nf_subgoal i sgl =
- let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
- v (List.map leaf gll.it) in
- frontier_mapi nf_subgoal pf
-
-(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
- takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
- where pfterm is the constr corresponding to the proof
- and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
- where the mi are metavariables numbers, and ci are their types.
- Their proof should be completed in order to complete the initial proof *)
-
-let extract_open_proof sigma pf =
- let next_meta =
- let meta_cnt = ref 0 in
- let rec f () =
- incr meta_cnt;
- if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
- else !meta_cnt
- in f
- in
- let open_obligations = ref [] in
- let rec proof_extractor vl = function
- | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
-
- | {ref=Some(Nested(_,hidden_proof),spfl)} ->
- let sgl,v = frontier hidden_proof in
- let flat_proof = v spfl in
- proof_extractor vl flat_proof
-
- | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
-
- | {ref=(None|Some(Daimon,[]));goal=goal} ->
- let visible_rels =
- map_succeed
- (fun id ->
- try let n = proof_variable_index id vl in (n,id)
- with Not_found -> failwith "caught")
- (ids_of_named_context (named_context_of_val goal.evar_hyps)) in
- let sorted_rels =
- Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
- let sorted_env =
- List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
- sorted_rels in
- let abs_concl =
- List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
- sorted_env goal.evar_concl in
- let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
- let meta = next_meta () in
- open_obligations := (meta,abs_concl):: !open_obligations;
- applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
-
- | _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
- in
- let pfterm = proof_extractor [] pf in
- (pfterm, List.rev !open_obligations)
-
(*********************)
(* Tacticals *)
(*********************)
-(* unTAC : tactic -> goal sigma -> proof sigma *)
-
-let unTAC tac g =
- let (gl_sigma,v) = tac g in
- { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
let unpackage glsig = (ref (glsig.sigma)),glsig.it
@@ -310,13 +92,9 @@ let repackage r v = {it=v;sigma = !r}
let apply_sig_tac r tac g =
check_for_interrupt (); (* Breakpoint *)
- let glsigma,v = tac (repackage r g) in
+ let glsigma = tac (repackage r g) in
r := glsigma.sigma;
- (glsigma.it,v)
-
-let idtac_valid = function
- [pf] -> pf
- | _ -> anomaly "Refiner.idtac_valid"
+ glsigma.it
(* [goal_goal_list : goal sigma -> goal list sigma] *)
let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
@@ -325,7 +103,7 @@ let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
let tclNORMEVAR = norm_evar_tac
(* identity tactic without any message *)
-let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
+let tclIDTAC gls = goal_goal_list gls
(* the message printing identity tactic *)
let tclIDTAC_MESSAGE s gls =
@@ -344,23 +122,21 @@ let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
let start_tac gls =
let (sigr,g) = unpackage gls in
- (sigr,[g],idtac_valid)
+ (sigr,[g])
-let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
+let finish_tac (sigr,gl) = repackage sigr gl
(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
+let thens3parts_tac tacfi tac tacli (sigr,gs) =
let nf = Array.length tacfi in
let nl = Array.length tacli in
let ng = List.length gs in
if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
- let gll,pl =
- List.split
+ let gll =
(list_map_i (fun i ->
apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
0 gs) in
- (sigr, List.flatten gll,
- compose p (mapshape (List.map List.length gll) pl))
+ (sigr,List.flatten gll)
(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
let thensf_tac taci tac = thens3parts_tac taci tac [||]
@@ -369,10 +145,10 @@ let thensf_tac taci tac = thens3parts_tac taci tac [||]
let thensl_tac tac taci = thens3parts_tac [||] tac taci
(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs,p) =
- let gll,pl =
- List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in
- (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl))
+let thensi_tac tac (sigr,gs) =
+ let gll =
+ list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+ (sigr, List.flatten gll)
let then_tac tac = thensf_tac [||] tac
@@ -382,7 +158,7 @@ let non_existent_goal n =
(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
the last goal (i=-1). *)
-let theni_tac i tac ((_,gl,_) as subgoals) =
+let theni_tac i tac ((_,gl) as subgoals) =
let nsg = List.length gl in
let k = if i < 0 then nsg + i + 1 else i in
if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
@@ -451,42 +227,29 @@ let rec tclTHENLIST = function
let tclMAP tacfun l =
List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
-(* various progress criterions *)
-let same_goal gl subgoal =
- eq_constr (conclusion subgoal) (conclusion gl) &&
- eq_named_context_val (hypotheses subgoal) (hypotheses gl)
-
-
-let weak_progress gls ptree =
- (List.length gls.it <> 1) ||
- (not (same_goal (List.hd gls.it) ptree.it))
-
-let progress gls ptree =
- (progress_evar_map ptree.sigma gls.sigma) ||
- (weak_progress gls ptree)
-
+(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
+the goal unchanged *)
+let tclWEAK_PROGRESS tac ptree =
+ let rslt = tac ptree in
+ if Goal.V82.weak_progress rslt ptree then rslt
+ else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
the goal unchanged *)
let tclPROGRESS tac ptree =
let rslt = tac ptree in
- if progress (fst rslt) ptree then rslt
+ if Goal.V82.progress rslt ptree then rslt
else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
-(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
- if tac leaves the goal unchanged, possibly modifying sigma *)
-let tclWEAK_PROGRESS tac ptree =
- let rslt = tac ptree in
- if weak_progress (fst rslt) ptree then rslt
- else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.")
-
-
(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
one of them being identical to the original goal *)
let tclNOTSAMEGOAL (tac : tactic) goal =
+ let same_goal gls1 evd2 gl2 =
+ Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
+ in
let rslt = tac goal in
- let gls = (fst rslt).it in
- if List.exists (same_goal goal.it) gls
+ let {it=gls;sigma=sigma} = rslt in
+ if List.exists (same_goal goal sigma) gls
then errorlabstrm "Refiner.tclNOTSAMEGOAL"
(str"Tactic generated a subgoal identical to the original goal.")
else rslt
@@ -525,9 +288,9 @@ let tclORELSE_THEN t1 t2then t2else gls =
with e -> catch_failerror e; None
with
| None -> t2else gls
- | Some (sgl,v) ->
+ | Some sgl ->
let (sigr,gl) = unpackage sgl in
- finish_tac (then_tac t2then (sigr,gl,v))
+ finish_tac (then_tac t2then (sigr,gl))
(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -601,14 +364,12 @@ let rec tclREPEAT_MAIN t g =
(*s Tactics handling a list of goals. *)
-type validation_list = proof_tree list -> proof_tree list
-
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = (goal list sigma) -> (goal list sigma)
(* Functions working on goal list for correct backtracking in Prolog *)
let tclFIRSTLIST = tclFIRST
-let tclIDTAC_list gls = (gls, fun x -> x)
+let tclIDTAC_list gls = gls
(* first_goal : goal list sigma -> goal sigma *)
@@ -628,286 +389,20 @@ let apply_tac_list tac glls =
let (sigr,lg) = unpackage glls in
match lg with
| (g1::rest) ->
- let (gl,p) = apply_sig_tac sigr tac g1 in
- let n = List.length gl in
- (repackage sigr (gl@rest),
- fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
+ let gl = apply_sig_tac sigr tac g1 in
+ repackage sigr (gl@rest)
| _ -> error "apply_tac_list"
let then_tactic_list tacl1 tacl2 glls =
- let (glls1,pl1) = tacl1 glls in
- let (glls2,pl2) = tacl2 glls1 in
- (glls2, compose pl1 pl2)
+ let glls1 = tacl1 glls in
+ let glls2 = tacl2 glls1 in
+ glls2
(* Transform a tactic_list into a tactic *)
let tactic_list_tactic tac gls =
- let (glres,vl) = tac (goal_goal_list gls) in
- (glres, compose idtac_valid vl)
-
-
-
-(* The type of proof-trees state and a few utilities
- A proof-tree state is built from a proof-tree, a set of global
- constraints, and a stack which allows to navigate inside the
- proof-tree remembering how to rebuild the global proof-tree
- possibly after modification of one of the focused children proof-tree.
- The number in the stack corresponds to
- either the selected subtree and the validation is a function from a
- proof-tree list consisting only of one proof-tree to the global
- proof-tree
- or -1 when the move is done behind a registered tactic in which
- case the validation corresponds to a constant function giving back
- the original proof-tree. *)
-
-type pftreestate = {
- tpf : proof_tree ;
- tpfsigma : evar_map;
- tstack : (int * validation) list }
-
-let proof_of_pftreestate pts = pts.tpf
-let is_top_pftreestate pts = pts.tstack = []
-let cursor_of_pftreestate pts = List.map fst pts.tstack
-let evc_of_pftreestate pts = pts.tpfsigma
-
-let top_goal_of_pftreestate pts =
- { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
-
-let nth_goal_of_pftreestate n pts =
- let goals = fst (frontier pts.tpf) in
- try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
- with Invalid_argument _ | Failure _ -> non_existent_goal n
-
-let traverse n pts = match n with
- | 0 -> (* go to the parent *)
- (match pts.tstack with
- | [] -> error "traverse: no ancestors"
- | (_,v)::tl ->
- let pf = v [pts.tpf] in
- let pf = norm_evar_proof pts.tpfsigma pf in
- { tpf = pf;
- tstack = tl;
- tpfsigma = pts.tpfsigma })
- | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
- (match pts.tpf.ref with
- | Some (Nested (_,spf),_) ->
- let v = (fun pfl -> pts.tpf) in
- { tpf = spf;
- tstack = (-1,v)::pts.tstack;
- tpfsigma = pts.tpfsigma }
- | _ -> error "traverse: not a tactic-node")
- | n -> (* when n>0, go to the nth child *)
- let (npf,v) = descend n pts.tpf in
- { tpf = npf;
- tpfsigma = pts.tpfsigma;
- tstack = (n,v):: pts.tstack }
-
-let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc }
-
-let app_tac sigr tac p =
- let (gll,v) = tac {it=p.goal;sigma= !sigr} in
- sigr := gll.sigma;
- v (List.map leaf gll.it)
-
-(* modify proof state at current position *)
-
-let map_pftreestate f pts =
- let sigr = ref pts.tpfsigma in
- let tpf' = f sigr pts.tpf in
- let tpf'' =
- if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
- { tpf = tpf'';
- tpfsigma = !sigr;
- tstack = pts.tstack }
-
-(* solve the nth subgoal with tactic tac *)
-
-let solve_nth_pftreestate n tac =
- map_pftreestate
- (fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
-
-let solve_pftreestate = solve_nth_pftreestate 1
-
-(* This function implements a poor man's undo at the current goal.
- This is a gross approximation as it does not attempt to clean correctly
- the global constraints given in tpfsigma. *)
-
-let weak_undo_pftreestate pts =
- let pf = leaf pts.tpf.goal in
- { tpf = pf;
- tpfsigma = pts.tpfsigma;
- tstack = pts.tstack }
-
-(* Gives a new proof (a leaf) of a goal gl *)
-let mk_pftreestate g =
- { tpf = leaf g;
- tstack = [];
- tpfsigma = Evd.empty }
-
-(* Extracts a constr from a proof-tree state ; raises an error if the
- proof is not complete or the state does not correspond to the head
- of the proof-tree *)
-
-let extract_open_pftreestate pts =
- extract_open_proof pts.tpfsigma pts.tpf
-
-let extract_pftreestate pts =
- if pts.tstack <> [] then
- errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed");
- let pfterm,subgoals = extract_open_pftreestate pts in
- let exl = Evarutil.non_instantiated pts.tpfsigma in
- if subgoals <> [] or exl <> [] then
- errorlabstrm "extract_proof"
- (if subgoals <> [] then
- str "Attempt to save an incomplete proof"
- else
- str "Attempt to save a proof with existential variables still non-instantiated");
- let env = Global.env_of_context pts.tpf.goal.evar_hyps in
- nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
- (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
- (***
- local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
- ***)
-(* Focus on the first leaf proof in a proof-tree state *)
-
-let rec first_unproven pts =
- let pf = (proof_of_pftreestate pts) in
- if is_complete_proof pf then
- errorlabstrm "first_unproven" (str"No unproven subgoals");
- if is_leaf_proof pf then
- pts
- else
- let childnum =
- list_try_find_i
- (fun n pf ->
- if not(is_complete_proof pf) then n else failwith "caught")
- 1 (children_of_proof pf)
- in
- first_unproven (traverse childnum pts)
-
-(* Focus on the last leaf proof in a proof-tree state *)
-
-let rec last_unproven pts =
- let pf = proof_of_pftreestate pts in
- if is_complete_proof pf then
- errorlabstrm "last_unproven" (str"No unproven subgoals");
- if is_leaf_proof pf then
- pts
- else
- let children = (children_of_proof pf) in
- let nchilds = List.length children in
- let childnum =
- list_try_find_i
- (fun n pf ->
- if not(is_complete_proof pf) then n else failwith "caught")
- 1 (List.rev children)
- in
- last_unproven (traverse (nchilds-childnum+1) pts)
-
-let rec nth_unproven n pts =
- let pf = proof_of_pftreestate pts in
- if is_complete_proof pf then
- errorlabstrm "nth_unproven" (str"No unproven subgoals");
- if is_leaf_proof pf then
- if n = 1 then
- pts
- else
- errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
- else
- let children = children_of_proof pf in
- let rec process i k = function
- | [] ->
- errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
- | pf1::rest ->
- let k1 = nb_unsolved_goals pf1 in
- if k1 < k then
- process (i+1) (k-k1) rest
- else
- nth_unproven k (traverse i pts)
- in
- process 1 n children
-
-let rec node_prev_unproven loc pts =
- let pf = proof_of_pftreestate pts in
- match cursor_of_pftreestate pts with
- | [] -> last_unproven pts
- | n::l ->
- if is_complete_proof pf or loc = 1 then
- node_prev_unproven n (traverse 0 pts)
- else
- let child = List.nth (children_of_proof pf) (loc - 2) in
- if is_complete_proof child then
- node_prev_unproven (loc - 1) pts
- else
- first_unproven (traverse (loc - 1) pts)
-
-let rec node_next_unproven loc pts =
- let pf = proof_of_pftreestate pts in
- match cursor_of_pftreestate pts with
- | [] -> first_unproven pts
- | n::l ->
- if is_complete_proof pf ||
- loc = (List.length (children_of_proof pf)) then
- node_next_unproven n (traverse 0 pts)
- else if is_complete_proof (List.nth (children_of_proof pf) loc) then
- node_next_unproven (loc + 1) pts
- else
- last_unproven(traverse (loc + 1) pts)
-
-let next_unproven pts =
- let pf = proof_of_pftreestate pts in
- if is_leaf_proof pf then
- match cursor_of_pftreestate pts with
- | [] -> error "next_unproven"
- | n::_ -> node_next_unproven n (traverse 0 pts)
- else
- node_next_unproven (List.length (children_of_proof pf)) pts
-
-let prev_unproven pts =
- let pf = proof_of_pftreestate pts in
- if is_leaf_proof pf then
- match cursor_of_pftreestate pts with
- | [] -> error "prev_unproven"
- | n::_ -> node_prev_unproven n (traverse 0 pts)
- else
- node_prev_unproven 1 pts
-
-let rec top_of_tree pts =
- if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
-
-(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
-let change_rule f pts =
- let mark_top _ pt =
- match pt.ref with
- Some (oldrule,l) ->
- {pt with ref=Some (f oldrule,l)}
- | _ -> invalid_arg "change_rule" in
- map_pftreestate mark_top pts
-
-let match_rule p pts =
- match (proof_of_pftreestate pts).ref with
- Some (r,_) -> p r
- | None -> false
-
-let rec up_until_matching_rule p pts =
- if is_top_pftreestate pts then
- raise Not_found
- else
- let one_up = traverse 0 pts in
- if match_rule p one_up then
- pts
- else
- up_until_matching_rule p one_up
-
-let rec up_to_matching_rule p pts =
- if match_rule p pts then
- pts
- else
- if is_top_pftreestate pts then
- raise Not_found
- else
- let one_up = traverse 0 pts in
- up_to_matching_rule p one_up
+ let glres = tac (goal_goal_list gls) in
+ glres
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
@@ -918,28 +413,8 @@ let pp_info = ref (fun _ _ _ -> assert false)
let set_info_printer f = pp_info := f
let tclINFO (tac : tactic) gls =
- let (sgl,v) as res = tac gls in
- begin try
- let pf = v (List.map leaf (sig_it sgl)) in
- let sign = named_context_of_val (sig_it gls).evar_hyps in
- msgnl (hov 0 (str" == " ++
- !pp_info (project gls) sign pf))
- with e when catchable_exception e ->
- msgnl (hov 0 (str "Info failed to apply validation"))
- end;
- res
-
-let pp_proof = ref (fun _ _ _ -> assert false)
-let set_proof_printer f = pp_proof := f
-
-let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
- (if stack = []
- then str "Rooted proof tree is:"
- else (str "Proof tree at occurrence [" ++
- prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n)
- (List.rev stack) ++ str "] is:")) ++ fnl() ++
- !pp_proof sigma (Global.named_context()) pf ++
- Evd.pr_evar_map sigma
+ msgnl (hov 0 (str "Warning: info is currently not working"));
+ tac gls
(* Check that holes in arguments have been resolved *)
@@ -962,5 +437,5 @@ let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
else
let res = tclTHEN (tclEVARS sigma) (tac c) gl in
if not accept_unresolved_holes then
- check_evars (pf_env gl) (fst res).sigma sigma gl;
+ check_evars (pf_env gl) (res).sigma sigma gl;
res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index e853c12b7c..77f2e48a7d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -12,9 +12,9 @@
open Term
open Sign
open Evd
-open Proof_trees
open Proof_type
open Tacexpr
+open Logic
(*i*)
(* The refiner (handles primitive rules and high-level tactics). *)
@@ -28,14 +28,14 @@ val pf_hyps : goal sigma -> named_context
val unpackage : 'a sigma -> evar_map ref * 'a
val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
- evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
-
-type transformation_tactic = proof_tree -> (goal list * validation)
+ evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
(*s Hiding the implementation of tactics. *)
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
a single proof node. The boolean tells if the default tactic is used. *)
+(* spiwack: currently here for compatibility, abstract_operation
+ is a second projection *)
val abstract_operation : compound_rule -> tactic -> tactic
val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
@@ -43,22 +43,6 @@ val abstract_extended_tactic :
?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
val refiner : rule -> tactic
-val frontier : transformation_tactic
-val list_pf : proof_tree -> goal list
-val unTAC : tactic -> goal sigma -> proof_tree sigma
-
-
-(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
-val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
-(* [frontier_map f n p] applies f on the n-th open subgoal of p and
- rebuilds proof-tree.
- n=1 for first goal, n negative counts from the right *)
-val frontier_map :
- (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree
-
-(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *)
-val frontier_mapi :
- (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree
(*s Tacticals. *)
@@ -153,8 +137,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.std_ppcmds -> tactic
val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
-val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
+val tclPROGRESS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
val tclINFO : tactic -> tactic
@@ -173,9 +157,7 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
(*s Tactics handling a list of goals. *)
-type validation_list = proof_tree list -> proof_tree list
-
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = goal list sigma -> goal list sigma
val tclFIRSTLIST : tactic_list list -> tactic_list
val tclIDTAC_list : tactic_list
@@ -191,57 +173,4 @@ val goal_goal_list : 'a sigma -> 'a list sigma
extension of the sigma of the goal *)
val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
-(*s Functions for handling the state of the proof editor. *)
-
-type pftreestate
-
-val proof_of_pftreestate : pftreestate -> proof_tree
-val cursor_of_pftreestate : pftreestate -> int list
-val is_top_pftreestate : pftreestate -> bool
-val match_rule : (rule -> bool) -> pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> evar_map
-val top_goal_of_pftreestate : pftreestate -> goal sigma
-val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
-
-val traverse : int -> pftreestate -> pftreestate
-val map_pftreestate :
- (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
-val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
-val solve_pftreestate : tactic -> pftreestate -> pftreestate
-
-(* a weak version of logical undoing, that is really correct only *)
-(* if there are no existential variables. *)
-val weak_undo_pftreestate : pftreestate -> pftreestate
-
-val mk_pftreestate : goal -> pftreestate
-val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
-val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
-val extract_pftreestate : pftreestate -> constr
-val first_unproven : pftreestate -> pftreestate
-val last_unproven : pftreestate -> pftreestate
-val nth_unproven : int -> pftreestate -> pftreestate
-val node_prev_unproven : int -> pftreestate -> pftreestate
-val node_next_unproven : int -> pftreestate -> pftreestate
-val next_unproven : pftreestate -> pftreestate
-val prev_unproven : pftreestate -> pftreestate
-val top_of_tree : pftreestate -> pftreestate
-val match_rule : (rule -> bool) -> pftreestate -> bool
-val up_until_matching_rule : (rule -> bool) ->
- pftreestate -> pftreestate
-val up_to_matching_rule : (rule -> bool) ->
- pftreestate -> pftreestate
-val change_rule : (rule -> rule) -> pftreestate -> pftreestate
-val change_constraints_pftreestate
- : evar_map -> pftreestate -> pftreestate
-
-
(*s Pretty-printers. *)
-
-(*i*)
-open Pp
-(*i*)
-val set_info_printer :
- (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
-val set_proof_printer :
- (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
-val print_pftreestate : pftreestate -> Pp.std_ppcmds
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9e35abfc89..6dbdf17cb8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -21,7 +21,6 @@ open Evd
open Typing
open Redexpr
open Tacred
-open Proof_trees
open Proof_type
open Logic
open Refiner
@@ -34,7 +33,6 @@ let re_sig it gc = { it = it; sigma = gc }
(**************************************************************)
type 'a sigma = 'a Evd.sigma;;
-type validation = Proof_type.validation;;
type tactic = Proof_type.tactic;;
let unpackage = Refiner.unpackage
@@ -46,7 +44,7 @@ let project = Refiner.project
let pf_env = Refiner.pf_env
let pf_hyps = Refiner.pf_hyps
-let pf_concl gls = (sig_it gls).evar_concl
+let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
let pf_hyps_types gls =
let sign = Environ.named_context (pf_env gls) in
List.map (fun (id,_,x) -> (id, x)) sign
@@ -123,11 +121,11 @@ let pf_matches = pf_apply Matching.matches_conv
(* Tactics handling a list of goals *)
(************************************)
-type transformation_tactic = proof_tree -> (goal list * validation)
+type transformation_tactic = proof_tree -> goal list
type validation_list = proof_tree list -> proof_tree list
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = Refiner.tactic_list
let first_goal = first_goal
let goal_goal_list = goal_goal_list
@@ -138,37 +136,6 @@ let tclFIRSTLIST = tclFIRSTLIST
let tclIDTAC_list = tclIDTAC_list
-(********************************************************)
-(* Functions for handling the state of the proof editor *)
-(********************************************************)
-
-type pftreestate = Refiner.pftreestate
-
-let proof_of_pftreestate = proof_of_pftreestate
-let cursor_of_pftreestate = cursor_of_pftreestate
-let is_top_pftreestate = is_top_pftreestate
-let evc_of_pftreestate = evc_of_pftreestate
-let top_goal_of_pftreestate = top_goal_of_pftreestate
-let nth_goal_of_pftreestate = nth_goal_of_pftreestate
-let traverse = traverse
-let solve_nth_pftreestate = solve_nth_pftreestate
-let solve_pftreestate = solve_pftreestate
-let weak_undo_pftreestate = weak_undo_pftreestate
-let mk_pftreestate = mk_pftreestate
-let extract_pftreestate = extract_pftreestate
-let extract_open_pftreestate = extract_open_pftreestate
-let first_unproven = first_unproven
-let last_unproven = last_unproven
-let nth_unproven = nth_unproven
-let node_prev_unproven = node_prev_unproven
-let node_next_unproven = node_next_unproven
-let next_unproven = next_unproven
-let prev_unproven = prev_unproven
-let top_of_tree = top_of_tree
-let frontier = frontier
-let change_constraints_pftreestate = change_constraints_pftreestate
-
-
(********************************************)
(* Definition of the most primitive tactics *)
(********************************************)
@@ -243,10 +210,18 @@ let rec pr_list f = function
| [] -> mt ()
| a::l1 -> (f a) ++ pr_list f l1
+let db_pr_goal sigma g =
+ let env = Goal.V82.env sigma g in
+ let penv = print_named_context env in
+ let pc = print_constr_env env (Goal.V82.concl sigma g) in
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
+
let pr_gls gls =
- hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+ hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
let pr_glls glls =
hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
- prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+ prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls))
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a808ca4190..f4bb1d9220 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Sign
open Environ
open Evd
open Reduction
-open Proof_trees
open Proof_type
open Refiner
open Redexpr
@@ -27,7 +26,6 @@ open Pattern
(* Operations for handling terms under a local typing context. *)
type 'a sigma = 'a Evd.sigma;;
-type validation = Proof_type.validation;;
type tactic = Proof_type.tactic;;
val sig_it : 'a sigma -> 'a
@@ -38,7 +36,7 @@ val re_sig : 'a -> evar_map -> 'a sigma
val unpackage : 'a sigma -> evar_map ref * 'a
val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
- evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
+ evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
@@ -90,38 +88,6 @@ val pf_conv_x_leq : goal sigma -> constr -> constr -> bool
val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map
val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-type transformation_tactic = proof_tree -> (goal list * validation)
-
-val frontier : transformation_tactic
-
-
-(*s Functions for handling the state of the proof editor. *)
-
-type pftreestate = Refiner.pftreestate
-
-val proof_of_pftreestate : pftreestate -> proof_tree
-val cursor_of_pftreestate : pftreestate -> int list
-val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> evar_map
-val top_goal_of_pftreestate : pftreestate -> goal sigma
-val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
-val traverse : int -> pftreestate -> pftreestate
-val weak_undo_pftreestate : pftreestate -> pftreestate
-val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
-val solve_pftreestate : tactic -> pftreestate -> pftreestate
-val mk_pftreestate : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
-val extract_pftreestate : pftreestate -> constr
-val first_unproven : pftreestate -> pftreestate
-val last_unproven : pftreestate -> pftreestate
-val nth_unproven : int -> pftreestate -> pftreestate
-val node_prev_unproven : int -> pftreestate -> pftreestate
-val node_next_unproven : int -> pftreestate -> pftreestate
-val next_unproven : pftreestate -> pftreestate
-val prev_unproven : pftreestate -> pftreestate
-val top_of_tree : pftreestate -> pftreestate
-val change_constraints_pftreestate :
- evar_map -> pftreestate -> pftreestate
(*s The most primitive tactics. *)
@@ -159,7 +125,7 @@ val rename_hyp : (identifier*identifier) list -> tactic
type validation_list = proof_tree list -> proof_tree list
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+type tactic_list = Refiner.tactic_list
val first_goal : 'a list sigma -> 'a sigma
val goal_goal_list : 'a sigma -> 'a list sigma
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index ea8ab5b625..f6b2ce4525 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -36,8 +36,18 @@ let explain_logic_error = ref (fun e -> mt())
let explain_logic_error_no_anomaly = ref (fun e -> mt())
(* Prints the goal *)
+
+let db_pr_goal g =
+ let env = Refiner.pf_env g in
+ let penv = print_named_context env in
+ let pc = print_constr_env env (Goal.V82.concl (Refiner.project g) (Refiner.sig_it g)) in
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
+
let db_pr_goal g =
- msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
+ msgnl (str "Goal:" ++ fnl () ++ db_pr_goal g)
+
(* Prints the commands *)
let help () =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 05:39:40 +0000