diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /proofs | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'proofs')
36 files changed, 4054 insertions, 2079 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml new file mode 100644 index 00000000..d06c6f2e --- /dev/null +++ b/proofs/clenv.ml @@ -0,0 +1,522 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +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 Glob_term +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_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c + +(******************************************************************) +(* 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_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 = (Conv,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 of the + * template 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 concl are _excluded_ + * If [iter] is also set then all metavariables *recursively* occurring + * in the concl are _excluded_ + + Details of the strategies used for computing the set of unresolved + dependent metavariables + + We typically have a clause of the form + + lem(?T:Type,?T,?U:Type,?V:Type,?x:?T,?y:?U,?z:?V,?H:hyp(?x,?z)) :concl(?y,?z) + + Then, we compute: + A = the set of all unresolved metas + C = the set of metas occurring in concl (here ?y, ?z) + C* = the recursive closure of C wrt types (here ?y, ?z, ?U, ?V) + D = the set of metas occurring in a type of meta (here ?x, ?T, ?z, ?U, ?V) + NL = the set of duplicated metas even if non dependent (here ?T) + (we make the assumption that duplicated metas have internal dependencies) + + Then, for the "apply"-style tactic (hyps_only), missing metas are + A inter ((D minus C) union NL) + + for the optimized "apply"-style tactic (taking in care, f_equal style + lemma, from 2/8/10, Coq > 8.3), missing metas are + A inter (( D minus C* ) union NL) + + for the "elim"-style tactic, missing metas are + A inter (D union C union NL) + + In any case, we respect the order given in A. +*) + +let clenv_metas_in_type_of_meta evd mv = + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas + +let dependent_in_type_of_metas clenv mvs = + List.fold_right + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv)) + mvs Metaset.empty + +let dependent_closure clenv mvs = + let rec aux mvs acc = + Metaset.fold + (fun mv deps -> + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in + aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) + mvs acc in + aux mvs mvs + +let clenv_dependent_gen hyps_only ?(iter=true) clenv = + let all_undefined = undefined_metas clenv.evd in + let deps_in_concl = (mk_freelisted (clenv_type clenv)).freemetas in + let deps_in_hyps = dependent_in_type_of_metas clenv all_undefined in + let deps_in_concl = + if hyps_only && iter then dependent_closure clenv deps_in_concl + else deps_in_concl in + List.filter + (fun mv -> + if hyps_only then + Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl) + else + Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl) + all_undefined + +let clenv_missing ce = clenv_dependent_gen true ce +let clenv_dependent ce = clenv_dependent_gen false ce + +(******************************************************************) + +let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv = + { clenv with + evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + +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 ?(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 CUMUL ~flags (clenv_type clenv) concl + (clenv_unify_meta_types ~flags clenv) + else + clenv_unify CUMUL ~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 = evars_reset_evd ~with_conv_pbs:true gls.sigma 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 fchain_flags = + { default_unify_flags with + allow_K_in_toplevel_higher_order_unification = true } + +let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv = + (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) + let clenv' = + { templval = clenv.templval; + templtyp = clenv.templtyp; + evd = meta_merge 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 ~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 = Metaset.union (dependent_in_type_of_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,(Conv,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 + +exception NoSuchBinding + +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 _ -> raise NoSuchBinding in + clenv_assign_binding clenv k c + +let error_not_right_number_missing_arguments n = + errorlabstrm "" + (strbrk "Not the right number of missing arguments (expected " ++ + int n ++ str ").") + +let clenv_constrain_dep_args hyps_only bl clenv = + if bl = [] then + clenv + else + let occlist = clenv_dependent_gen hyps_only clenv in + if List.length occlist = List.length bl then + List.fold_left2 clenv_assign_binding clenv occlist bl + else + if hyps_only then + (* Tolerance for compatibility <= 8.3 *) + let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in + if List.length occlist' = List.length bl then + List.fold_left2 clenv_assign_binding clenv occlist' bl + else + error_not_right_number_missing_arguments (List.length occlist) + else + error_not_right_number_missing_arguments (List.length occlist) + +(****************************************************************) +(* Clausal environment for an application *) + +let make_clenv_binding_gen hyps_only n env sigma (c,t) = function + | ImplicitBindings largs -> + let clause = mk_clenv_from_env env sigma n (c,t) in + clenv_constrain_dep_args hyps_only largs clause + | ExplicitBindings lbind -> + let clause = mk_clenv_from_env env sigma n + (c,rename_bound_vars_as_displayed [] t) + in clenv_match_args lbind clause + | NoBindings -> + mk_clenv_from_env env sigma n (c,t) + +let make_clenv_binding_env_apply env sigma n = + make_clenv_binding_gen true n env sigma + +let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma +let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma + +(****************************************************************) +(* 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 (Some 2) clenv.evd) diff --git a/proofs/clenv.mli b/proofs/clenv.mli new file mode 100644 index 00000000..abd67236 --- /dev/null +++ b/proofs/clenv.mli @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Term +open Sign +open Environ +open Evd +open Evarutil +open Mod_subst +open Glob_term +open Unification + +(** {6 The Type of Constructions clausale environments.} *) + +type clausenv = { + env : env; (** the typing context *) + evd : evar_map; (** the mapping from metavar and evar numbers to their + types and values *) + templval : constr freelisted; (** the template which we are trying to fill + out *) + templtyp : constr freelisted (** its type *)} + +(** 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 + +(** {6 linking of clenvs } *) + +val connect_clenv : Goal.goal sigma -> clausenv -> clausenv +val clenv_fchain : + ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv + +(** {6 Unification with clenvs } *) + +(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) +val clenv_unify : + ?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 : + ?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 : + ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv + +val clenv_dependent : clausenv -> metavariable list + +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv + +(** {6 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 + +(** for the purpose of inversion tactics *) +exception NoSuchBinding +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_env_apply : + env -> evar_map -> int option -> constr * constr -> constr bindings -> + clausenv + +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 + +(** {6 Pretty-print (debug only) } *) +val pr_clenv : clausenv -> Pp.std_ppcmds + diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7b760859..eb935d05 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenvtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -20,12 +18,11 @@ open Evd open Evarutil open Proof_type open Refiner -open Proof_trees open Logic open Reduction open Reductionops open Tacmach -open Rawterm +open Glob_term open Pattern open Tacexpr open Clenv @@ -64,7 +61,7 @@ let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) let clenv_pose_dependent_evars with_evars clenv = - let dep_mvs = clenv_dependent false clenv in + let dep_mvs = clenv_dependent clenv in if dep_mvs <> [] & not with_evars then raise (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); @@ -84,17 +81,18 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls -let dft = Unification.default_unify_flags +open Unification + +let dft = default_unify_flags -let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls = - clenv_refine with_evars - (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = + clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls let elim_res_pf_THEN_i clenv tac gls = - let clenv' = (clenv_unique_resolver true clenv gls) in + let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls -let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft +let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -102,21 +100,27 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) -open Unification - let fail_quick_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) + frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = false; + modulo_eta = true; + allow_K_in_toplevel_higher_order_unification = false } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify false env CONV ~flags m n evd in + let evd' = w_unify env evd CONV ~flags m n in tclIDTAC {it = gls.it; sigma = evd'} let unify ?(flags=fail_quick_unif_flags) m gls = diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 45e12645..49a961f5 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: clenvtac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term @@ -18,16 +15,15 @@ open Clenv open Proof_type open Tacexpr open Unification -(*i*) -(* Tactics *) +(** Tactics *) val unify : ?flags:unify_flags -> constr -> tactic val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr -(* Compatibility, use res_pf ?with_evars:true instead *) +(** Compatibility, use res_pf ?with_evars:true instead *) val e_res_pf : clausenv -> tactic diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli deleted file mode 100644 index 5c069cdd..00000000 --- a/proofs/decl_expr.mli +++ /dev/null @@ -1,105 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: decl_expr.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - -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 250c1655..00000000 --- a/proofs/decl_mode.ml +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: decl_mode.ml 14641 2011-11-06 11:59:10Z herbelin $ 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 60cb99c1..00000000 --- a/proofs/decl_mode.mli +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: decl_mode.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - -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 69168dbd..36268de1 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,20 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Term open Evd open Evarutil open Sign -open Proof_trees open Refiner (******************************************) @@ -33,7 +30,7 @@ let define_and_solve_constraints evk c evd = let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in fst (List.fold_left (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then Evarconv.evar_conv_x env evd pbty t1 t2 else p) (evd,true) + if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) pbs) with e when Pretype_errors.precatchable_exception e -> error "Instance does not satisfy constraints." @@ -46,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = try Pretyping.Default.understand_ltac true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> - let loc = Rawterm.loc_of_rawconstr rawc in + let loc = Glob_term.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) @@ -55,19 +52,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 69d4853e..8e7c0713 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,29 +1,25 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evar_refiner.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Environ open Evd open Refiner open Pretyping -open Rawterm -(*i*) +open Glob_term -(* Refinement of existential variables. *) +(** Refinement of existential variables. *) val w_refine : evar * evar_info -> - rawconstr_ltac_closure -> evar_map -> evar_map + glob_constr_ltac_closure -> 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] *) +(** 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 00000000..1542267e --- /dev/null +++ b/proofs/goal.ml @@ -0,0 +1,588 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +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. *) + + +let pr_goal {content = e} = str "GOAL:" ++ Pp.int e + +(* 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 = [] + } + + +let uid {content = e} = string_of_int e +let get_by_uid u = + (* this necessarily forget about tags. + when tags are to be implemented, they + should be done another way. + We could use the store in evar_extra, + for instance. *) + build (int_of_string u) + +(* 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, acting only on undefined evars *) + let evar_map_filter_undefined f evm = + Evd.fold_undefined + (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) + + let update_handle handle init_defs post_defs = + (* [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_undefined + (fun ev _ -> 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; + delta_evars + + (* [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 [glob_constr] 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 + ignore(update_handle handle init_defs !rdefs); + open_constr + + let constr_of_open_constr handle check_type (evars, c) env rdefs gl info = + let delta = update_handle handle !rdefs evars in + rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs; + if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info + else c + +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 +(* no handler: this should never be allowed to reach toplevel *) +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_candidates = None; + 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 00000000..e9d23065 --- /dev/null +++ b/proofs/goal.mli @@ -0,0 +1,243 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* 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 + +(* Gives a unique identifier to each goal. The identifier is + guaranteed to contain no space. *) +val uid : goal -> string +(* Returns the goal (even if it has been partially solved) + corresponding to a unique identifier obtained by {!uid}. *) +val get_by_uid : string -> goal + +(* Debugging help *) +val pr_goal : goal -> Pp.std_ppcmds + +(* [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 [glob_constr] 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 -> Glob_term.glob_constr -> Term.constr sensitive + + (* [constr_of_open_constr h check_type] transforms an open constr into a + goal-sensitive constr, adding the undefined variables to the set of subgoals. + If [check_type] is true, the term is coerced to the conclusion of the goal. + It allows to do refinement with already-built terms with holes. + *) + val constr_of_open_constr : handle -> bool -> Evd.open_constr -> 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 d837dca5..a363c6bb 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Pp open Util open Names @@ -21,7 +20,6 @@ open Reductionops open Inductive open Inductiveops open Typing -open Proof_trees open Proof_type open Typeops open Type_errors @@ -48,18 +46,18 @@ exception RefinerError of refiner_error open Pretype_errors let rec catchable_exception = function - | Stdpp.Exc_located(_,e) -> catchable_exception e + | Loc.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ + | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) | RefinerError _ | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* reduction errors *) | Tacred.ReductionTacticError _ (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _|OccurCheck _ - |UnsolvableImplicit _)) -> true + |UnsolvableImplicit _|AbstractionOverMeta _)) -> true | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false @@ -327,53 +325,59 @@ let goal_type_of env sigma c = 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) -> + | Cast (t,k, ty) -> check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; - mk_refgoals sigma goal goalacc ty t + let res = mk_refgoals sigma goal goalacc ty t in + (** we keep the casts (in particular VMcast) except + when they are annotating metas *) + if isMeta t then begin + assert (k <> VMcast); + res + end else + let (gls,cty,sigma,trm) = res in + (gls,cty,sigma,mkCast(trm,k,ty)) | 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 @@ -381,70 +385,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 + try Tacred.find_hnf_rectype 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) = @@ -462,18 +473,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 - (************************************************************************) @@ -481,10 +480,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 -> @@ -492,19 +493,23 @@ let prim_refiner r sigma goal = error ("Variable " ^ string_of_id id ^ " 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 @@ -516,7 +521,10 @@ let prim_refiner r sigma goal = (if !check && mem_named_context id (named_context_of_val sign) then error ("Variable " ^ string_of_id id ^ " 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) -> @@ -546,9 +554,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 = @@ -573,32 +596,56 @@ 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',_) -> + | Convert_concl (cl',k) -> 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 ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev 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 = @@ -607,7 +654,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) -> @@ -615,11 +663,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 && @@ -627,12 +679,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) (************************************************************************) (************************************************************************) @@ -644,27 +703,6 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = - let rec aux p vars = - let _,subst = - List.fold_left (fun (n,l) var -> - let t = match var with - | Anonymous,_ -> l - | Name id, ProofVar -> (id,mkRel n)::l - | Name id, SectionVar id' -> (id,mkVar id')::l in - (n+1,t)) (p,[]) vars - in replace_vars (List.rev subst) - in aux 1 - -let rec rebind id1 id2 = function - | [] -> [Name id2,SectionVar id1] - | (na,k as x)::l -> - if na = Name id1 then (Name id2,k)::l else - let l' = rebind id1 id2 l in - if na = Name id2 then (Anonymous,k)::l' else x::l' - -let add_proof_var id vl = (Name id,ProofVar)::vl - let proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n @@ -672,77 +710,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 da2566a7..420e6374 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,28 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: logic.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Sign open Evd open Environ open Proof_type -(*i*) -(* This suppresses check done in [prim_refiner] for the tactic given in +(** This suppresses check done in [prim_refiner] for the tactic given in argument; works by side-effect *) val with_check : tactic -> tactic -(* [without_check] respectively means:\\ +(** [without_check] respectively means:\\ [Intro]: no check that the name does not exist\\ [Intro_after]: no check that the name does not exist and that variables in its type does not escape their scope\\ @@ -32,19 +28,16 @@ val with_check : tactic -> tactic no check that the name exist and that its type is convertible\\ *) -(* The primitive refiner. *) +(** The primitive refiner. *) 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 -(*s Refiner errors. *) +(** {6 Refiner errors. } *) type refiner_error = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a9799f38..3d507f35 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -20,322 +18,139 @@ 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 *) -(*********************************************************************) - -type lemma_possible_guards = int list list - -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 } - -let proof_edits = - (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t) - -let get_all_proof_names () = Edit.dom proof_edits - -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 refining = Proof_global.there_are_pending_proofs +let check_no_pending_proofs = Proof_global.check_no_pending_proof -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_current_proof_name = Proof_global.get_current_proof_name +let get_all_proof_names = Proof_global.get_all_proof_names -let get_topstate () = snd(get_state()) -let get_pftreestate () = fst(get_state()) +type lemma_possible_guards = Proof_global.lemma_possible_guards -let get_end_tac () = let ts = get_topstate () in ts.top_end_tac +let delete_proof = Proof_global.discard +let delete_current_proof = Proof_global.discard_current +let delete_all_proofs = Proof_global.discard_all -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 undo n = + let p = Proof_global.give_me_the_proof () in + for i = 1 to n do + Proof.undo p + done -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 () = - 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 - -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 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 = +(* [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.mutate proof_edits (fun _ pfs -> f pfs) - with Invalid_argument "Edit.mutate" -> - errorlabstrm "Pfedit.mutate" - (str"No focused proof" ++ msg_proofs true) + undo ((current_proof_depth ()) - n ) + with Proof_global.NoCurrentProof when n=0 -> () -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 set_undo _ = () +let get_undo _ = None -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 +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 -(*********************************************************************) -(* Proof cooking *) -(*********************************************************************) +let restart_proof () = + 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 get_pftreestate () = + Proof_global.give_me_the_proof () -let refining () = [] <> (Edit.dom proof_edits) +let set_end_tac tac = + let tac = Proofview.V82.tactic tac in + Proof_global.set_endline_tactic tac + +let set_used_variables l = + Proof_global.set_used_variables l +let get_used_variables () = + Proof_global.get_used_variables () + +exception NoSuchGoal +let _ = Errors.register_handler begin function + | NoSuchGoal -> Util.error "No such goal." + | _ -> raise Errors.Unhandled +end +let get_nth_V82_goal i = + let p = Proof_global.give_me_the_proof () in + let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in + try + { it=(List.nth goals (i-1)) ; sigma=sigma } + with Failure _ -> raise NoSuchGoal + +let get_goal_context_gen i = + try + let { it=goal ; sigma=sigma } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma }) + with Proof_global.NoCurrentProof -> Util.error "No focused proof." -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_goal_context i = + try get_goal_context_gen i + with NoSuchGoal -> Util.error "No such goal." -let delete_current_proof () = delete_proof_gen (get_current_proof_name ()) +let get_current_goal_context () = + try get_goal_context_gen 1 + with NoSuchGoal -> + (* spiwack: returning empty evar_map, since if there is no goal, under focus, + there is no accessible evar either *) + (Evd.empty, Global.env ()) -let delete_all_proofs () = Edit.clear proof_edits +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 -(*********************************************************************) -(* 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 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 - -(* 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 reset_top_of_tree () = - mutate top_of_tree - -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 *) @@ -355,7 +170,26 @@ let build_constant_by_tactic id sign typ tac = delete_current_proof (); raise e -let build_by_tactic typ tac = +let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in - let sign = Decls.clear_proofs (Global.named_context ()) in + let sign = val_of_named_context (named_context env) in (build_constant_by_tactic id sign typ tac).const_entry_body + +(**********************************************************************) +(* Support for resolution of evars in tactic interpretation, including + resolution by application of tactics *) + +let implicit_tactic = ref None + +let declare_implicit_tactic tac = implicit_tactic := Some tac + +let solve_by_implicit_tactic env sigma (evk,args) = + let evi = Evd.find_undefined sigma evk in + match (!implicit_tactic, snd (evar_source evk sigma)) with + | Some tac, (ImplicitArg _ | QuestionMark _) + when + Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + (Environ.named_context env) -> + (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac) + with e when Logic.catchable_exception e -> raise Exit) + | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 05c329c1..7297b975 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Pp open Names @@ -18,190 +15,179 @@ open Environ open Decl_kinds open Tacmach open Tacexpr -(*i*) -(*s Several proofs can be opened simultaneously but at most one is +(** 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 open proof (something started by vernacular command [Goal], [Lemma] or [Theorem]), and ``goal'' means a subgoal of the current focused proof *) -(*s [refining ()] tells if there is some proof in progress, even if a not +(** {6 ... } *) +(** [refining ()] tells if there is some proof in progress, even if a not focused one *) val refining : unit -> bool -(* [check_no_pending_proofs ()] fails if there is still some proof in +(** [check_no_pending_proofs ()] fails if there is still some proof in progress *) val check_no_pending_proofs : unit -> unit -(*s [delete_proof name] deletes proof of name [name] or fails if no proof +(** {6 ... } *) +(** [delete_proof name] deletes proof of name [name] or fails if no proof has this name *) val delete_proof : identifier located -> unit -(* [delete_current_proof ()] deletes current focused proof or fails if +(** [delete_current_proof ()] deletes current focused proof or fails if no proof is focused *) val delete_current_proof : unit -> unit -(* [delete_all_proofs ()] deletes all open proofs if any *) +(** [delete_all_proofs ()] deletes all open proofs if any *) val delete_all_proofs : unit -> unit -(*s [undo n] undoes the effect of the last [n] tactics applied to the +(** {6 ... } *) +(** [undo n] undoes the effect of the last [n] tactics applied to the current proof; it fails if no proof is focused or if the ``undo'' stack is exhausted *) 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 +(** 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) *) - -val set_undo : int option -> unit -val get_undo : unit -> int option - -(*s [start_proof s str env t hook tac] starts a proof of name [s] and +(** {6 ... } *) +(** [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) *) -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 -> ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> declaration_hook -> unit -(* [restart_proof ()] restarts the current focused proof from the beginning +(** [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) val restart_proof : unit -> unit -(*s [resume_last_proof ()] focus on the last unfocused proof or fails +(** {6 ... } *) +(** [resume_last_proof ()] focus on the last unfocused proof or fails if there is no suspended proofs *) val resume_last_proof : unit -> unit -(* [resume_proof name] focuses on the proof of name [name] or - raises [UserError] if no proof has name [name] *) +(** [resume_proof name] focuses on the proof of name [name] or + raises [NoSuchProof] if no proof has name [name]. + + It doesn't [suspend_proof ()] before. *) val resume_proof : identifier located -> unit -(* [suspend_proof ()] unfocuses the current focused proof or +(** [suspend_proof ()] unfocuses the current focused proof or failed with [UserError] if no proof is currently focused *) val suspend_proof : unit -> unit -(*s [cook_proof opacity] turns the current proof (assumed completed) into +(** {6 ... } *) +(** [cook_proof opacity] turns the current proof (assumed completed) into a constant with its name, kind and possible hook (see [start_proof]); 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 +(** To export completed proofs to xml *) +val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit -(*s [get_pftreestate ()] returns the current focused pending proof or +(** {6 ... } *) +(** [get_Proof.proof ()] returns the current focused pending proof or raises [UserError "no focused proof"] *) -val get_pftreestate : unit -> pftreestate +val get_pftreestate : unit -> Proof.proof -(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) - -val get_end_tac : unit -> tactic option - -(* [get_goal_context n] returns the context of the [n]th subgoal of +(** [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 focused proof or if there is no more subgoals *) val get_goal_context : int -> Evd.evar_map * env -(* [get_current_goal_context ()] works as [get_goal_context 1] *) +(** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : unit -> Evd.evar_map * env -(* [current_proof_statement] *) +(** [current_proof_statement] *) val current_proof_statement : unit -> identifier * goal_kind * types * declaration_hook -(*s [get_current_proof_name ()] return the name of the current focused +(** {6 ... } *) +(** [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) val get_current_proof_name : unit -> identifier -(* [get_all_proof_names ()] returns the list of all pending proof names *) +(** [get_all_proof_names ()] returns the list of all pending proof names *) val get_all_proof_names : unit -> identifier list -(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate +(** {6 ... } *) +(** [set_end_tac tac] applies tactic [tac] to all subgoal generate by [solve_nth] *) val set_end_tac : tactic -> unit -(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the +(** {6 ... } *) +(** [set_used_variables l] declares that section variables [l] will be + used in the proof *) +val set_used_variables : identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + +(** {6 ... } *) +(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the 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 +(** [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 if there is no more subgoals *) val by : tactic -> unit -(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined +(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th existential variable *) 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 +(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) -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 +val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> + Entries.definition_entry +val build_by_tactic : env -> types -> tactic -> constr +(** Declare the default tactic to fill implicit arguments *) -(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) +val declare_implicit_tactic : tactic -> unit -val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic -> - Entries.definition_entry -val build_by_tactic : types -> tactic -> constr +(* Raise Exit if cannot solve *) +val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr diff --git a/proofs/proof.ml b/proofs/proof.ml new file mode 100644 index 00000000..72730495 --- /dev/null +++ b/proofs/proof.ml @@ -0,0 +1,458 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* 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 'a focus_kind = _focus_kind +type focus_info = Obj.t +type unfocusable = + | Cannot + | Loose + | Strict +type _focus_condition = + (_focus_kind -> Proofview.proofview -> unfocusable) * + (_focus_kind -> focus_info -> focus_info) +type 'a focus_condition = _focus_condition + +let next_kind = ref 0 +let new_focus_kind () = + let r = !next_kind in + incr next_kind; + r + +(* Auxiliary function to define conditions: + [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match. + Otherwise it raises [CheckNext] *) +exception CheckNext +(* no handler: confined to this module. *) +let check kind1 kind2 inf = + if kind1=kind2 then inf else raise CheckNext + +(* 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]. *) + +module Cond = struct + (* first attempt at an algebra of condition *) + (* semantics: + - [Cannot] means that the condition is not met + - [Strict] that the condition is meant + - [Loose] that the condition is not quite meant + but authorises to unfocus provided a condition + of a previous focus on the stack is (strictly) + met. + *) + let bool b = + if b then fun _ _ -> Strict + else fun _ _ -> Cannot + let loose c k p = match c k p with + | Cannot -> Loose + | c -> c + let cloose l c = + if l then loose c + else c + let (&&&) c1 c2 k p= + match c1 k p , c2 k p with + | Cannot , _ + | _ , Cannot -> Cannot + | Strict, Strict -> Strict + | _ , _ -> Loose + let kind k0 k p = bool (k0=k) k p + let pdone k p = bool (Proofview.finished p) k p +end + +open Cond +let no_cond ~loose_end k0 = + cloose loose_end (kind k0) +let no_cond ?(loose_end=false) k = no_cond ~loose_end k , check k +(* [done_cond] checks that the unfocusing command uses the right [focus_kind] + and that the focused proofview is complete. *) +let done_cond ~loose_end k0 = + (cloose loose_end (kind k0)) &&& pdone +let done_cond ?(loose_end=false) k = done_cond ~loose_end k , check k + + +(* 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 and the extra information stored while focusing. + The list is empty when the proof is fully unfocused. *) + focus_stack: (_focus_condition*focus_info*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 ; + mutable section_vars : Sign.section_context option; + 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; + (* secondary undo stacks used for transactions *) + mutable transactions : undo_action list list; + info : proof_info + } + + +(*** General proof functions ***) + +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. + Unfocusing is handled in {!return}. *) +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) + + + +(*** 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 cond inf context pr = + pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack } + +exception FullyUnfocused +let _ = Errors.register_handler begin function + | FullyUnfocused -> Util.error "The proof is not focused" + | _ -> raise Errors.Unhandled +end +(* 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 pr = + match pr.transactions with + | [] -> pr.undo_stack <- save::pr.undo_stack + | stack::trans' -> pr.transactions <- (save::stack)::trans' + +(* Auxiliary function to pop and read a [save_state] from the undo stack. *) +exception EmptyUndoStack +let _ = Errors.register_handler begin function + | EmptyUndoStack -> Util.error "Cannot undo: no more undo information" + | _ -> raise Errors.Unhandled +end +let pop_undo pr = + match pr.transactions , pr.undo_stack with + | [] , state::stack -> pr.undo_stack <- stack; state + | (state::stack)::trans', _ -> pr.transactions <- stack::trans'; state + | _ -> raise EmptyUndoStack + + +(* This function focuses the proof [pr] between indices [i] and [j] *) +let _focus cond inf i j pr = + let (focused,context) = Proofview.focus i j pr.state.proofview in + push_focus cond inf context pr; + pr.state <- { pr.state with proofview = focused } + +(* This function unfocuses the proof [pr], it raises [FullyUnfocused], + 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 } + + +let set_used_variables l p = + p.info.section_vars <- Some l + +let get_used_variables p = p.info.section_vars + +(*** 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 + + + +(*** Transactions ***) + +let init_transaction pr = + pr.transactions <- []::pr.transactions + +let commit_stack pr stack = + let push s = push_undo s pr in + List.iter push (List.rev stack) + +(* Invariant: [commit] should be called only when a transaction + is open. It closes the current transaction. *) +let commit pr = + match pr.transactions with + | stack::trans' -> + pr.transactions <- trans'; + commit_stack pr stack + | [] -> assert false + +(* Invariant: [rollback] should be called only when a transaction + is open. It closes the current transaction. *) +let rec rollback pr = + try + undo pr; + rollback pr + with EmptyUndoStack -> + match pr.transactions with + | []::trans' -> pr.transactions <- trans' + | _ -> assert false + + +let transaction pr t = + init_transaction pr; + try t (); commit pr + with e -> rollback pr; raise e + + +(* 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 inf i pr = + save pr; + _focus cond (Obj.repr inf) i i pr + +(* Unfocus command. + Fails if the proof is not focused. *) +exception CannotUnfocusThisWay +let _ = Errors.register_handler begin function + | CannotUnfocusThisWay -> + Util.error "This proof is focused, but cannot be unfocused this way" + | _ -> raise Errors.Unhandled +end + +let rec unfocus kind pr () = + let starting_point = save_state pr in + let cond = cond_of_focus pr in + match fst cond kind pr.state.proofview with + | Cannot -> raise CannotUnfocusThisWay + | Strict -> + (_unfocus pr; + push_undo starting_point pr) + | Loose -> + begin try + _unfocus pr; + push_undo starting_point pr; + unfocus kind pr () + with FullyUnfocused -> raise CannotUnfocusThisWay + end + +let unfocus kind pr = + transaction pr (unfocus kind pr) + +let get_at_point kind ((_,get),inf,_) = get kind inf +exception NoSuchFocus +(* no handler: should not be allowed to reach toplevel. *) +exception GetDone of Obj.t +(* no handler: confined to this module. *) +let get_in_focus_stack kind stack = + try + List.iter begin fun pt -> + try + raise (GetDone (get_at_point kind pt)) + with CheckNext -> () + end stack; + raise NoSuchFocus + with GetDone x -> x +let get_at_focus kind pr = + Obj.magic (get_in_focus_stack kind pr.state.focus_stack) + +let no_focused_goal p = + Proofview.finished p.state.proofview + +(*** Proof Creation/Termination ***) + +let end_of_stack_kind = new_focus_kind () +let end_of_stack = done_cond end_of_stack_kind + +let start goals = + let pr = + { state = { proofview = Proofview.init goals ; + focus_stack = [] ; + intel = Store.empty} ; + undo_stack = [] ; + transactions = [] ; + info = { endline_tactic = Proofview.tclUNIT (); + initial_conclusions = List.map snd goals; + section_vars = None } + } + in + _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr; + pr + +exception UnfinishedProof +exception HasUnresolvedEvar +let _ = Errors.register_handler begin function + | UnfinishedProof -> Util.error "Some goals have not been solved." + | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated." + | _ -> raise Errors.Unhandled +end +let return p = + if not (is_done p) then + raise UnfinishedProof + else if has_unresolved_evar p then + (* spiwack: for compatibility with <= 8.3 proof engine *) + raise HasUnresolvedEvar + else + unfocus end_of_stack_kind p; + Proofview.return 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 + +(*** Commands ***) + +let in_proof p k = + Proofview.in_proofview p.state.proofview k + + +(*** 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 top_evars p = + Proofview.V82.top_evars p.state.proofview + + 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 00000000..12af18f4 --- /dev/null +++ b/proofs/proof.mli @@ -0,0 +1,183 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* 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] if 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. + An undo effect is meant to undo an effect on a proof (a canonical example + of which is {!Proofglobal.set_proof_mode} which changes the current parser for + tactics). Make sure it will work even if the effects have been only partially + applied at the time of failure. *) +val add_undo : (unit -> unit) -> proof -> unit + +(*** Focusing actions ***) + +(* ['a focus_kind] is the type used by focusing and unfocusing + commands to synchronise. Focusing and unfocusing commands use + a particular ['a focus_kind], and if they don't match, the unfocusing command + will fail. + When focusing with an ['a focus_kind], an information of type ['a] is + stored at the focusing point. An example use is the "induction" tactic + of the declarative mode where sub-tactics must be aware of the current + induction argument. *) +type 'a focus_kind +val new_focus_kind : unit -> 'a focus_kind + +(* To be authorized to unfocus one must meet the condition prescribed by + the action which focused. + Conditions always carry a focus kind, and inherit their type parameter + from it.*) +type 'a focus_condition +(* [no_cond] only checks that the unfocusing command uses the right + [focus_kind]. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{- solve_goal. }] because they use a loose-end condition. *) +val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition +(* [done_cond] checks that the unfocusing command uses the right [focus_kind] + and that the focused proofview is complete. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{ - solve_goal. }] because they use a loose-end condition. *) +val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition + +(* 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? *) +val focus : 'a focus_condition -> 'a -> int -> proof -> unit + +exception FullyUnfocused +exception CannotUnfocusThisWay +(* Unfocusing command. + Raises [FullyUnfocused] if the proof is not focused. + Raises [CannotUnfocusThisWay] if the proof the unfocusing condition + is not met. *) +val unfocus : 'a focus_kind -> proof -> unit + +(* [get_at_focus k] gets the information stored at the closest focus point + of kind [k]. + Raises [NoSuchFocus] if there is no focus point of kind [k]. *) +exception NoSuchFocus +val get_at_focus : 'a focus_kind -> proof -> 'a + +(* 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 + +(* Sets the section variables assumed by the proof *) +val set_used_variables : Sign.section_context -> proof -> unit +val get_used_variables : proof -> Sign.section_context option + +(*** 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 + + +(*** Transactions ***) + +(* A transaction chains several commands into a single one. For instance, + a focusing command and a tactic. Transactions are such that if + any of the atomic action fails, the whole transaction fails. + + During a transaction, the undo visible undo stack is constituted only + of the actions performed done during the transaction. + + [transaction p f] can be called on an [f] using, itself, [transaction p].*) +val transaction : proof -> (unit -> unit) -> unit + + +(*** Commands ***) + +val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a + +(*** 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 + + (* returns the existential variable used to start the proof *) + val top_evars : proof -> Evd.evar list + + (* 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 00000000..2745270a --- /dev/null +++ b/proofs/proof_global.ml @@ -0,0 +1,427 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(***********************************************************************) +(* *) +(* This module defines proof facilities relevant to the *) +(* toplevel. In particular it defines the global proof *) +(* environment. *) +(* *) +(***********************************************************************) + +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 find_proof_mode n = + try Hashtbl.find proof_modes n + with Not_found -> + Util.error (Format.sprintf "No proof mode named \"%s\"." n) + +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 _ = + Goptions.declare_string_option {Goptions. + optsync = true ; + optdepr = false; + 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 := find_proof_mode 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 _ = Errors.register_handler begin function + | NoSuchProof -> Util.error "No such proof." + | _ -> raise Errors.Unhandled +end +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 _ = Errors.register_handler begin function + | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)." + | _ -> raise Errors.Unhandled +end +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 + Util.error (Pp.string_of_ppcmds + (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ + str"Use \"Abort All\" first or complete proof(s).")) + 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 = find_proof_mode 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 set_used_variables l = + let p = give_me_the_proof () in + let env = Global.env () in + let ids = List.fold_right Idset.add l Idset.empty in + let ctx = Environ.keep_hyps env ids in + Proof.set_used_variables ctx p + +let get_used_variables () = + Proof.get_used_variables (give_me_the_proof ()) + +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 section_vars = Proof.get_used_variables p in + let entries = List.map + (fun (c,t) -> { Entries.const_entry_body = c; + const_entry_secctx = section_vars; + const_entry_type = Some t; + const_entry_opaque = true }) + 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" + + +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +let maximal_unfocus k p = + begin try while Proof.no_focused_goal p do + Proof.unfocus k p + done + with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> () + end + + +(**********************************************************) +(* *) +(* Bullets *) +(* *) +(**********************************************************) + +module Bullet = struct + + open Store.Field + + + type t = Vernacexpr.bullet + + type behavior = { + name : string; + put : Proof.proof -> t -> unit + } + + let behaviors = Hashtbl.create 4 + let register_behavior b = Hashtbl.add behaviors b.name b + + (*** initial modes ***) + let none = { + name = "None"; + put = fun _ _ -> () + } + let _ = register_behavior none + + module Strict = struct + (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) + let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind) + let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind + + let get_bullets pr = + try Proof.get_at_focus bullet_kind pr + with Proof.NoSuchFocus -> [] + + let has_bullet bul pr = + let rec has_bullet = function + | b'::_ when bul=b' -> true + | _::l -> has_bullet l + | [] -> false + in + has_bullet (get_bullets pr) + + (* precondition: the stack is not empty *) + let pop pr = + match get_bullets pr with + | b::_ -> + Proof.unfocus bullet_kind pr; + (*returns*) b + | _ -> assert false + + let push b pr = + Proof.focus bullet_cond (b::get_bullets pr) 1 pr + + let put p bul = + if has_bullet bul p then + Proof.transaction p begin fun () -> + while bul <> pop p do () done; + push bul p + end + else + push bul p + + let strict = { + name = "Strict Subproofs"; + put = put + } + let _ = register_behavior strict + end + + (* Current bullet behavior, controled by the option *) + let current_behavior = ref Strict.strict + + let _ = + Goptions.declare_string_option {Goptions. + optsync = true; + optdepr = false; + optname = "bullet behavior"; + optkey = ["Bullet";"Behavior"]; + optread = begin fun () -> + (!current_behavior).name + end; + optwrite = begin fun n -> + current_behavior := Hashtbl.find behaviors n + end + } + + let put p b = + (!current_behavior).put p b +end + + +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 00000000..ed6a60c7 --- /dev/null +++ b/proofs/proof_global.mli @@ -0,0 +1,137 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module defines proof facilities relevant to the + toplevel. In particular it defines the global proof + environment. *) + +(** 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) + +exception NoSuchProof + +val suspend : unit -> unit +val resume_last : unit -> unit + +val resume : Names.identifier -> unit +(** @raise NoSuchProof if it doesn't find one. *) + +(** 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 + +(** Sets the section variables assumed by the proof *) +val set_used_variables : Names.identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + +(** Appends the endline tactic of the current proof to a tactic. *) +val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic + +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a + focused goal or that the last focus isn't of kind [k]. *) +val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit + +(**********************************************************) +(* *) +(* Bullets *) +(* *) +(**********************************************************) + +module Bullet : sig + type t = Vernacexpr.bullet + + (** A [behavior] is the data of a put function which + is called when a bullet prefixes a tactic, together + with a name to identify it. *) + type behavior = { + name : string; + put : Proof.proof -> t -> unit + } + + (** A registered behavior can then be accessed in Coq + through the command [Set Bullet Behavior "name"]. + + Two modes are registered originally: + * "Strict Subproofs": + - If this bullet follows another one of its kind, defocuses then focuses + (which fails if the focused subproof is not complete). + - If it is the first bullet of its kind, then focuses a new subproof. + * "None": bullets don't do anything *) + val register_behavior : behavior -> unit + + (** Handles focusing/defocusing with bullets: + *) + val put : Proof.proof -> t -> unit +end + +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 8fe1a4c2..00000000 --- a/proofs/proof_trees.ml +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: proof_trees.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - -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 9e9f5e63..00000000 --- a/proofs/proof_trees.mli +++ /dev/null @@ -1,48 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: proof_trees.mli 14641 2011-11-06 11:59:10Z herbelin $ 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 46fce6ae..e256794a 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (*i*) open Environ open Evd @@ -16,8 +14,8 @@ open Libnames open Term open Util open Tacexpr -open Decl_expr -open Rawterm +(* open Decl_expr *) +open Glob_term open Genarg open Nametab open Pattern @@ -26,6 +24,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 @@ -42,7 +44,6 @@ type prim_rule = | Change_evars type proof_tree = { - open_subgoals : int; goal : goal; ref : (rule * proof_tree list) option } @@ -54,13 +55,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, @@ -100,7 +94,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr - | LtacConstrInterp of rawconstr * + | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) type ltac_trace = (int * loc * ltac_call_kind) list diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 417f75da..2b0a10ba 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Environ open Evd open Names @@ -16,16 +13,18 @@ open Libnames open Term open Util open Tacexpr -open Decl_expr -open Rawterm +open Glob_term open Genarg open Nametab open Pattern -(*i*) -(* This module defines the structure of proof tree and the tactic type. So, it +(** 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 @@ -41,42 +40,39 @@ type prim_rule = | Rename of identifier * identifier | Change_evars -(* The type [goal sigma] is the type of subgoal. It has the following form -\begin{verbatim} - it = { evar_concl = [the conclusion of the subgoal] +(** The type [goal sigma] is the type of subgoal. It has the following form +{v it = \{ evar_concl = [the conclusion of the subgoal] evar_hyps = [the hypotheses of the subgoal] evar_body = Evar_Empty; - evar_info = { pgm : [The Realizer pgm if any] - lc : [Set of evar num occurring in subgoal] }} - sigma = { stamp = [an int chardacterizing the ed field, for quick compare] + evar_info = \{ pgm : [The Realizer pgm if any] + lc : [Set of evar num occurring in subgoal] \}\} + sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare] ed : [A set of existential variables depending in the subgoal] number of first evar, - it = { evar_concl = [the type of first evar] + it = \{ evar_concl = [the type of first evar] evar_hyps = [the context of the evar] evar_body = [the body of the Evar if any] - evar_info = { pgm : [Useless ??] + evar_info = \{ pgm : [Useless ??] lc : [Set of evars occurring - in the type of evar] } }; + in the type of evar] \} \}; ... number of last evar, - it = { evar_concl = [the type of evar] + it = \{ evar_concl = [the type of evar] evar_hyps = [the context of the evar] evar_body = [the body of the Evar if any] - evar_info = { pgm : [Useless ??] + evar_info = \{ pgm : [Useless ??] lc : [Set of evars occurring - in the type of evar] } } } - } -\end{verbatim} + in the type of evar] \} \} \} v} *) -(*s Proof trees. +(** {6 ... } *) +(** Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal and gave [l] as subproofs to be completed. if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof that the goal can be proven if the goals in [l] are solved. *) type proof_tree = { - open_subgoals : int; goal : goal; ref : (rule * proof_tree list) option } @@ -87,15 +83,8 @@ and rule = | Daimon and compound_rule= - (* the boolean of Tactic tells if the default tactic is used *) + (** 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, @@ -135,7 +124,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr - | LtacConstrInterp of rawconstr * + | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) type ltac_trace = (int * loc * ltac_call_kind) list diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 05b86b1a..66001e77 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 00000000..0d50d521 --- /dev/null +++ b/proofs/proofview.ml @@ -0,0 +1,507 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Compat + +(* 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 +(* no handler: should not be allowed to reach toplevel *) + +(* [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"No 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). The first goal has index 1. + 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 +let _ = Errors.register_handler begin function + | SizeMismatch -> Util.error "Incorrect number of goals." + | _ -> raise Errors.Unhandled +end +(* 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 + | Loc.Exc_located(_,e) -> catchable_exception e + | Util.UserError _ + | Type_errors.TypeError _ | PretypeError (_,_,TypingError _) + | 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 + + +(*** Commands ***) + +let in_proofview p k = + k p.solution + +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 = + Evd.has_undefined pv.solution + + (* 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 top_evars { initial=initial } = + let evars_of_initial (c,_) = + Util.Intset.elements (Evarutil.evars_of_term c) + in + List.flatten (List.map evars_of_initial initial) + + 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 00000000..24da9d77 --- /dev/null +++ b/proofs/proofview.mli @@ -0,0 +1,213 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* 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 + +(* Interprets 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 + + +(*** Commands ***) + +val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a + + + + + +(* 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 + + (* returns the existential variable used to start the proof *) + val top_evars : proofview -> Evd.evar list + + (* 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/redexpr.ml b/proofs/redexpr.ml index 7290a92f..0430a239 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: redexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names open Term open Declarations open Libnames -open Rawterm +open Glob_term open Pattern open Reductionops open Tacred @@ -40,12 +38,13 @@ let set_strategy_one ref l = Csymtable.set_opaque_const sp | ConstKey sp, _ -> let cb = Global.lookup_constant sp in - if cb.const_body <> None & cb.const_opaque then - errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - Csymtable.set_transparent_const sp + (match cb.const_body with + | OpaqueDef _ -> + errorlabstrm "set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque."); + | _ -> Csymtable.set_transparent_const sp) | _ -> () let cache_strategy (_,str) = @@ -87,7 +86,10 @@ let discharge_strategy (_,(local,obj)) = if local then None else map_strategy disch_ref obj -let (inStrategy,outStrategy) = +type strategy_obj = + bool * (Conv_oracle.level * evaluable_global_reference list) list + +let inStrategy : strategy_obj -> obj = declare_object {(default_object "STRATEGY") with cache_function = (fun (_,obj) -> cache_strategy obj); load_function = (fun _ (_,obj) -> cache_strategy obj); @@ -213,7 +215,7 @@ let subst_red_expr subs e = (Pattern.subst_pattern subs) e -let (inReduction,_) = +let inReduction : bool * string * red_expr -> obj = declare_object {(default_object "REDUCTION") with cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 9eaa91cc..ae82153d 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: redexpr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names open Term open Closure open Pattern -open Rawterm +open Glob_term open Reductionops open Termops @@ -22,23 +20,24 @@ type red_expr = val out_with_occurrences : 'a with_occurrences -> occurrences * 'a val reduction_of_red_expr : red_expr -> reduction_function * cast_kind -(* [true] if we should use the vm to verify the reduction *) -(* Adding a custom reduction (function to be use at the ML level) +(** [true] if we should use the vm to verify the reduction *) + +(** Adding a custom reduction (function to be use at the ML level) NB: the effect is permanent. *) val declare_reduction : string -> reduction_function -> unit -(* Adding a custom reduction (function to be called a vernac command). +(** Adding a custom reduction (function to be called a vernac command). The boolean flag is the locality. *) val declare_red_expr : bool -> string -> red_expr -> unit -(* Opaque and Transparent commands. *) +(** Opaque and Transparent commands. *) -(* Sets the expansion strategy of a constant. When the boolean is +(** Sets the expansion strategy of a constant. When the boolean is true, the effect is non-synchronous (i.e. it does not survive section and module closure). *) val set_strategy : bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit -(* call by value normalisation function using the virtual machine *) +(** call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a540eef6..5cd85547 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Pp open Util open Term @@ -18,183 +17,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" - - -(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] - gives - [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ; - (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] - *) - -let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) - (l : proof_tree list) = - match nl with - | [] -> [] - | h::t -> - 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 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)) + +let abstract_operation syntax semantics = + semantics let abstract_tactic_expr ?(dflt=false) te tacfun gls = abstract_operation (Tactic(te,dflt)) tacfun gls @@ -207,16 +43,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 +57,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 +73,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 +84,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 +103,22 @@ 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) = +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) +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 +127,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 +140,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 +209,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 @@ -494,15 +239,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let catch_failerror e = if catchable_exception e then check_for_interrupt () else match e with - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) - | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> + | FailError (0,_) | Loc.Exc_located(_, FailError (0,_)) + | Loc.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + | Loc.Exc_located(s,FailError (lvl,s')) -> + raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) + | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> raise - (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) + (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -525,9 +270,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) @@ -587,6 +332,27 @@ let tclDO n t = in dorec n +(* Fails if a tactic hasn't finished after a certain amount of time *) + +exception TacTimeout + +let tclTIMEOUT n t g = + let timeout_handler _ = raise TacTimeout in + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + let restore_timeout () = + ignore (Unix.alarm 0); + Sys.set_signal Sys.sigalrm psh + in + try + let res = t g in + restore_timeout (); + res + with + | TacTimeout | Loc.Exc_located(_,TacTimeout) -> + restore_timeout (); + errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") + | e -> restore_timeout (); raise e (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = @@ -601,14 +367,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 +392,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,42 +416,24 @@ 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 *) -let check_evars env sigma evm gl = +let check_evars env sigma extsigma gl = let origsigma = gl.sigma in let rest = - Evd.fold (fun ev evi acc -> - if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) - then Evd.add acc ev evi else acc) - evm Evd.empty + Evd.fold_undefined (fun evk evi acc -> + if Evd.is_undefined extsigma evk & not (Evd.mem origsigma evk) then + evi::acc + else + acc) + sigma [] in - if rest <> Evd.empty then - let (evk,evi) = List.hd (Evd.to_list rest) in - let (loc,k) = evar_source evk rest in + if rest <> [] then + let evi = List.hd rest in + let (loc,k) = evi.evar_source in let evi = Evarutil.nf_evar_info sigma evi in Pretype_errors.error_unsolvable_implicit loc env sigma evi k None @@ -962,5 +442,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 8167bfb2..75fd6d3d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,23 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: refiner.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Term open Sign open Evd -open Proof_trees open Proof_type open Tacexpr -(*i*) +open Logic -(* The refiner (handles primitive rules and high-level tactics). *) +(** The refiner (handles primitive rules and high-level tactics). *) val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map @@ -28,14 +24,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. *) +(** {6 Hiding the implementation of tactics. } *) -(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under +(** [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,100 +39,84 @@ 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. *) +(** {6 Tacticals. } *) -(* [tclNORMEVAR] forces propagation of evar constraints *) +(** [tclNORMEVAR] forces propagation of evar constraints *) val tclNORMEVAR : tactic -(* [tclIDTAC] is the identity tactic without message printing*) +(** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic -(* [tclEVARS sigma] changes the current evar map *) +(** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies +(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) val tclTHEN : tactic -> tactic -> tactic -(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More +(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More convenient than [tclTHEN] when [n] is large *) val tclTHENLIST : tactic list -> tactic -(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) val tclMAP : ('a -> tactic) -> 'a list -> tactic -(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *) +(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *) val tclTHEN_i : tactic -> (int -> tactic) -> tactic -(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] +(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the last resulting subgoal (previously called [tclTHENL]) *) val tclTHENLAST : tactic -> tactic -> tactic -(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] +(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : tactic -> tactic -> tactic -(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to +(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises an error if the number of resulting subgoals is not [n] *) val tclTHENSV : tactic -> tactic array -> tactic -(* Same with a list of tactics *) +(** Same with a list of tactics *) val tclTHENS : tactic -> tactic list -> tactic -(* [tclTHENST] is renamed [tclTHENSFIRSTn] +(** [tclTHENST] is renamed [tclTHENSFIRSTn] val tclTHENST : tactic -> tactic array -> tactic -> tactic *) -(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] +(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] subgoals and [tac2] to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic -(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the +(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the last [n] resulting subgoals and [tac2] on the remaining first subgoals *) val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then +(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then applies [t1],...,[tn] on the first [n] resulting subgoals and [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, +(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, applies [t1],...,[tn] on the last [n] resulting subgoals and leaves unchanged the other subgoals *) val tclTHENLASTn : tactic -> tactic array -> tactic -(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, +(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, applies [t1],...,[tn] on the first [n] resulting subgoals and leaves unchanged the other subgoals (previously called [tclTHENSI]) *) val tclTHENFIRSTn : tactic -> tactic array -> tactic -(* A special exception for levels for the Fail tactic *) +(** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.std_ppcmds Lazy.t -(* Takes an exception and either raise it at the next +(** Takes an exception and either raise it at the next level or do nothing. *) val catch_failerror : exn -> unit @@ -153,29 +133,28 @@ 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 tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic +val tclPROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclINFO : tactic -> tactic -(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, +(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, if it succeeds, applies [tac2] to the resulting subgoals, and if not applies [tac3] to the initial goal [gls] *) val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic -(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] +(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. Equivalent to [(tac1;try tac2)||tac2] *) val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic -(*s Tactics handling a list of goals. *) +(** {6 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 @@ -185,63 +164,8 @@ val then_tactic_list : tactic_list -> tactic_list -> tactic_list val tactic_list_tactic : tactic_list -> tactic val goal_goal_list : 'a sigma -> 'a list sigma -(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which +(** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which may have unresolved holes; if [solve_holes] these holes must be resolved after application of the tactic; [sigma] must be an 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/tacexpr.ml b/proofs/tacexpr.ml index 563d073a..b8279b8f 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names open Topconstr open Libnames open Nametab -open Rawterm +open Glob_term open Util open Genarg open Pattern @@ -29,7 +27,7 @@ type split_flag = bool (* true = exists false = split *) type hidden_flag = bool (* true = internal use false = user-level *) type letin_flag = bool (* true = use local def false = use Leibniz *) -type raw_red_flag = +type glob_red_flag = | FBeta | FIota | FZeta @@ -107,14 +105,6 @@ type 'id gclause = let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} -let goal_location_of = function -| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> - Some scl -| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> - None -| _ -> - error "Not a simple \"in\" clause (one hypothesis or the conclusion)" - type 'constr induction_clause = ('constr with_bindings induction_arg list * 'constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) @@ -201,7 +191,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = | TacRight of evars_flag * 'constr bindings | TacSplit of evars_flag * split_flag * 'constr bindings list | TacAnyConstructor of evars_flag * 'tac option - | TacConstructor of evars_flag * int or_metaid * 'constr bindings + | TacConstructor of evars_flag * int or_var * 'constr bindings (* Conversion *) | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause @@ -239,6 +229,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option @@ -249,7 +240,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast - | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg + | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast = identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr @@ -272,8 +263,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg = (* Globalized tactics *) and glob_tactic_expr = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -317,8 +308,8 @@ type raw_red_expr = (constr_expr, reference or_by_notation, constr_expr) red_expr_gen type glob_atomic_tactic_expr = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -327,8 +318,8 @@ type glob_atomic_tactic_expr = glevel) gen_atomic_tactic_expr type glob_tactic_arg = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -339,7 +330,7 @@ type glob_tactic_arg = type glob_generic_argument = glevel generic_argument type glob_red_expr = - (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern) + (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern) red_expr_gen type typed_generic_argument = tlevel generic_argument diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3939a78b..5475daa8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -21,7 +19,6 @@ open Evd open Typing open Redexpr open Tacred -open Proof_trees open Proof_type open Logic open Refiner @@ -34,7 +31,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 +42,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 +119,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 +134,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 *) (********************************************) @@ -237,16 +202,20 @@ let rename_hyp l = with_check (rename_hyp_no_check l) open Pp open Tacexpr -open Rawterm +open Glob_term -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 (Some 2) (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)) + hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls)) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6938c320..884a0307 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,33 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacmach.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Sign open Environ open Evd open Reduction -open Proof_trees open Proof_type open Refiner open Redexpr open Tacexpr -open Rawterm +open Glob_term open Pattern -(*i*) -(* Operations for handling terms under a local typing context. *) +(** 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 +32,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,40 +84,8 @@ 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. *) + +(** {6 The most primitive tactics. } *) val refiner : rule -> tactic val introduction_no_check : identifier -> tactic @@ -142,7 +104,7 @@ val mutual_fix : identifier -> int -> (identifier * int * constr) list -> int -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic -(*s The most primitive tactics with consistency and type checking *) +(** {6 The most primitive tactics with consistency and type checking } *) val introduction : identifier -> tactic val internal_cut : bool -> identifier -> types -> tactic @@ -155,11 +117,11 @@ val thin_body : identifier list -> tactic val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier*identifier) list -> tactic -(*s Tactics handling a list of goals. *) +(** {6 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 = Refiner.tactic_list val first_goal : 'a list sigma -> 'a sigma val goal_goal_list : 'a sigma -> 'a list sigma @@ -169,6 +131,6 @@ val tactic_list_tactic : tactic_list -> tactic val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Pretty-printing functions (debug only). *) +(** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds val pr_glls : goal list sigma -> Pp.std_ppcmds diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 7922eeb0..1c2fb278 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactic_debug.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names open Constrextern open Pp @@ -36,8 +34,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 () = @@ -146,11 +154,6 @@ let db_mc_pattern_success debug = msgnl (str "The goal has been successfully matched!" ++ fnl() ++ str "Let us execute the right-hand side part..." ++ fnl()) -let pp_match_pattern env = function - | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c) - | Subterm (b,o,c) -> - Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c)) - (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = if debug <> DebugOff & !skip = 0 then diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index e2606a06..d96f4c74 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactic_debug.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Environ open Pattern open Evd @@ -16,7 +14,7 @@ open Names open Tacexpr open Term -(* This module intends to be a beginning of debugger for tactic expressions. +(** This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) @@ -24,53 +22,53 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit val set_match_pattern_printer : (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit val set_match_rule_printer : - ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> + ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> unit -(* Debug information *) +(** Debug information *) type debug_info = | DebugOn of int | DebugOff -(* Prints the state and waits *) +(** Prints the state and waits *) val debug_prompt : int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a -(* Prints a constr *) +(** Prints a constr *) val db_constr : debug_info -> env -> constr -> unit -(* Prints the pattern rule *) +(** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit + debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit -(* Prints a matched hypothesis *) +(** Prints a matched hypothesis *) val db_matched_hyp : debug_info -> env -> identifier * constr option * constr -> name -> unit -(* Prints the matched conclusion *) +(** Prints the matched conclusion *) val db_matched_concl : debug_info -> env -> constr -> unit -(* Prints a success message when the goal has been matched *) +(** Prints a success message when the goal has been matched *) val db_mc_pattern_success : debug_info -> unit -(* Prints a failure message for an hypothesis pattern *) +(** Prints a failure message for an hypothesis pattern *) val db_hyp_pattern_failure : debug_info -> env -> name * constr_pattern match_pattern -> unit -(* Prints a matching failure message for a rule *) +(** Prints a matching failure message for a rule *) val db_matching_failure : debug_info -> unit -(* Prints an evaluation failure message for a rule *) +(** Prints an evaluation failure message for a rule *) val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit -(* An exception handler *) +(** An exception handler *) val explain_logic_error: (exn -> Pp.std_ppcmds) ref -(* For use in the Ltac debugger: some exception that are usually +(** For use in the Ltac debugger: some exception that are usually consider anomalies are acceptable because they are caught later in the process that is being debugged. One should not require from users that they report these anomalies. *) val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref -(* Prints a logic failure message for a rule *) +(** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit diff --git a/proofs/tmp-src b/proofs/tmp-src deleted file mode 100644 index 1da11fe0..00000000 --- a/proofs/tmp-src +++ /dev/null @@ -1,56 +0,0 @@ - -(********* INSTANTIATE ****************************************************) - -(* existential_type gives the type of an existential *) -let existential_type env k = - let (sp,args) = destConst k in - let evd = Evd.map (evar_map env) sp in - instantiate_constr - (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args) - -(* existential_value gives the value of a defined existential *) -let existential_value env k = - let (sp,args) = destConst k in - if defined_const env k then - let evd = Evd.map (evar_map env) sp in - match evd.evar_body with - | EVAR_DEFINED c -> - instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args) - | _ -> anomalylabstrm "termenv__existential_value" - [< 'sTR"The existential variable code just registered a" ; - 'sPC ; 'sTR"grave internal error." >] - else - failwith "undefined existential" - - -(******* REDUCTION ********************************************************) - - -(************ REDUCTION.MLI **********************************************) - -(*********** TYPEOPS *****************************************************) - - -(* Constants or existentials. *) - -let type_of_constant_or_existential env c = - if is_existential c then - type_of_existential env c - else - type_of_constant env c - - -(******** TYPING **********************************************************) - - | IsMeta n -> - let metaty = - try lookup_meta n env - with Not_found -> error "A variable remains non instanciated" - in - (match kind_of_term metaty with - | IsCast (typ,kind) -> - ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0) - | _ -> - let (jty,cst) = execute mf env metaty in - let k = whd_betadeltaiotaeta env jty.uj_type in - ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst)) |