diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-21 11:16:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-21 11:16:27 +0000 |
| commit | 554a6c8066d764192eac5f82cc14f71d349abbad (patch) | |
| tree | 93047d34727a9ec4c5131c717e439648ef778fc1 | |
| parent | fe8751f3d9372e88ad861b55775f912e92ae7016 (diff) | |
Generic support for open terms in tactics
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
33 files changed, 423 insertions, 439 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index ef7c3e864..664ed43f0 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -195,11 +195,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type +val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type +val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type diff --git a/lib/option.ml b/lib/option.ml index 2a530b89b..942fff48a 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -97,6 +97,12 @@ let fold_right f x a = | Some y -> f y a | _ -> a +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +let fold_map f a x = + match x with + | Some y -> let a, z = f a y in a, Some z + | _ -> a, None + (** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) let cata f a = function | Some c -> f c diff --git a/lib/option.mli b/lib/option.mli index 8002a7ea2..ef2e311a6 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -66,6 +66,9 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option + (** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1fde7b245..fe7038d3a 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -246,10 +246,10 @@ let rec pr_generic prc prlc prtac x = pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x) | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> - let (c,b) = out_gen wit_constr_with_bindings x in - pr_with_bindings prc prlc (c,out_bindings b) + let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in + pr_with_bindings prc prlc (c,b) | BindingsArgType -> - pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x)) + pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it | List0ArgType _ -> hov 0 (pr_sequence (pr_generic prc prlc prtac) (fold_list0 (fun a l -> a::l) x [])) @@ -288,7 +288,7 @@ let pr_raw_extend prc prlc prtac = let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac) + pr_extend_gen (pr_generic prc prlc prtac) (**********************************************************************) (* The tactic printer *) @@ -1008,12 +1008,12 @@ let strip_prod_binders_rawterm n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n (sigma,ty) = +let strip_prod_binders_constr n ty = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, (sigma,ty)) else + if n=0 then (List.rev acc, ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b + strip_ty (([dummy_loc,na],a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1059,8 +1059,8 @@ and pr_glob_match_rule env t = let typed_printers = (pr_glob_tactic_level, - pr_open_constr_env, - pr_open_lconstr_env, + pr_constr_env, + pr_lconstr_env, pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 7fa33119d..f84a2deb2 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -74,7 +74,7 @@ val pr_glob_extend: string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> string -> typed_generic_argument list -> std_ppcmds diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 64f9403a1..ab6c42035 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -36,7 +36,7 @@ let pr_with_bindings prc prlc (c,bl) = let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -46,12 +46,12 @@ let pr_fun_ind_using prc prlc _ opt_c = let pr_with_bindings_typed prc prlc (c,bl) = prc c ++ - hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + hv 0 (pr_bindings prc prlc bl) let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) ARGUMENT EXTEND fun_ind_using @@ -96,7 +96,7 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction true c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] END (***** debug only ***) TACTIC EXTEND snewfunind @@ -107,7 +107,7 @@ TACTIC EXTEND snewfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction false c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] END diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca608ec0b..8c22265d6 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -24,13 +24,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun (_,c) -> prc c) l + Util.prlist_with_sep spc prc l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -424,7 +424,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -434,7 +434,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 02d70da74..60616845b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1224,7 +1224,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac (inj_open eq1)) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 0beb1e1ae..476724ba6 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -248,7 +248,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac false (Some 1) 1 - (Rawterm.ImplicitBindings [inj_open (mkVar n)]); + (Rawterm.ImplicitBindings [mkVar n]); cont]); ]))) in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a65cc24ff..99e3c4e1d 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -354,7 +354,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, @@ -411,12 +411,11 @@ let clenv_unify_binding_type clenv c t u = | e when precatchable_exception e -> TypeNotProcessed, clenv, c -let clenv_assign_binding clenv k (sigma,c) = +let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let clenv' = { clenv with evd = Evd.merge clenv.evd sigma} in - let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in - let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in - { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } + let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in + { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd } let clenv_match_args bl clenv = if bl = [] then @@ -425,13 +424,13 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,b,(sigma,c as sc)) -> + (fun clenv (loc,b,c) -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else - clenv_assign_binding clenv k sc) + clenv_assign_binding clenv k c) clenv bl let clenv_constrain_last_binding c clenv = @@ -439,7 +438,7 @@ let clenv_constrain_last_binding c clenv = let k = try list_last all_mvs with Failure _ -> anomaly "clenv_constrain_with_bindings" in - clenv_assign_binding clenv k (Evd.empty,c) + clenv_assign_binding clenv k c let clenv_constrain_dep_args hyps_only bl clenv = if bl = [] then diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 5571efbc5..4f7ac4092 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -86,7 +86,7 @@ val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to @@ -107,10 +107,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (* the optional int tells how many prods of the lemma have to be used *) (* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int option -> constr * constr -> open_constr bindings -> + evar_info sigma -> int option -> constr * constr -> constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> open_constr bindings -> clausenv + evar_info sigma -> constr * constr -> constr bindings -> clausenv (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where [lmetas] is a list of metas to be applied to a proof of [t] so that diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index dc1784f40..a33c81b09 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1241,6 +1241,15 @@ let check_evars env initial_sigma evd c = | _ -> iter_constr proc_rec c in proc_rec c +(* This returns the evars of [sigma] that are not in [sigma0] and + [sigma] minus these evars *) + +let subtract_evars sigma0 sigma = + Evd.fold (fun evk ev (sigma,sigma' as acc) -> + if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else + (Evd.remove sigma evk,Evd.add sigma' evk ev)) + sigma (sigma,Evd.empty) + (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr @@ -1376,4 +1385,3 @@ let pr_tycon_type env (abs, t) = let pr_tycon env = function None -> str "None" | Some t -> pr_tycon_type env t - diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4bfef7998..205ca8bd6 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -90,6 +90,7 @@ val solve_simple_eqn : new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_map -> constr -> unit +val subtract_evars : evar_map -> evar_map -> evar_map * evar_map val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5bc86889..b741c9a41 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -703,9 +703,9 @@ let plain_instance s c = empty map). *) -let instance s c = +let instance sigma s c = (* if s = [] then c else *) - local_strong whd_betaiota Evd.empty (plain_instance s c) + local_strong whd_betaiota sigma (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -902,21 +902,21 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv in valrec mv -let meta_instance env b = +let meta_instance sigma b = let c_sigma = List.map - (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) + (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) in - if c_sigma = [] then b.rebus else instance c_sigma b.rebus + if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus -let nf_meta env c = meta_instance env (mk_freelisted c) +let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) @@ -924,7 +924,7 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9e5ced8a2..0b9e69d95 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -210,7 +210,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr val whd_meta : (metavariable * constr) list -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr -val instance : (metavariable * constr) list -> constr -> constr +val instance :evar_map -> (metavariable * constr) list -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function (*s Heuristic for Conversion with Evar *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ff7cf5acc..9bc818e86 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -78,6 +78,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = clenv.env clenv.evd else clenv.evd in + let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index e7bca648c..bc2953408 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -74,7 +74,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -85,7 +85,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 5fa4a44ef..b5c4a234d 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -109,7 +109,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -120,7 +120,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index ff902d880..e853c12b7 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -185,6 +185,11 @@ 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 + 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. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 6a08bda87..59791f011 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -756,7 +756,7 @@ let unify_resolve_nodelta (c,clenv) gl = let unify_resolve flags (c,clenv) gl = let clenv' = connect_clenv gl clenv in let _ = clenv_unique_resolver false ~flags clenv' gl in - h_apply true false [dummy_loc,(inj_open c,NoBindings)] gl + h_apply true false [dummy_loc,(c,NoBindings)] gl let unify_resolve_gen = function | None -> unify_resolve_nodelta @@ -932,7 +932,7 @@ let gen_trivial lems = function let inj_open c = (Evd.empty,c) let h_trivial lems l = - Refiner.abstract_tactic (TacTrivial (List.map inj_open lems,l)) + Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l) (**************************************************************************) @@ -1062,7 +1062,7 @@ let gen_auto n lems dbnames = let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto n lems l = - Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l)) + Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l) (**************************************************************************) @@ -1091,7 +1091,7 @@ let dauto (n,p) lems = let default_dauto = dauto (None,None) [] let h_dauto (n,p) lems = - Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map inj_open lems)) + Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,lems)) (dauto (n,p) lems) (***************************************) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 71817b2c7..9c38362a8 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -17,4 +17,4 @@ open Genarg (*i*) val absurd : constr -> tactic -val contradiction : constr with_ebindings option -> tactic +val contradiction : constr with_bindings option -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml index 935431bf9..cac200f58 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -139,13 +139,13 @@ let decompose_or c gls = let inj_open c = (Evd.empty,c) let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l) + Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c) + Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c) + Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) (* The tactic Double performs a double induction *) diff --git a/tactics/equality.ml b/tactics/equality.ml index a82f50671..62581d74b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -240,19 +240,18 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) (* Main function for dispatching which kind of rewriting it is about *) let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac - ((c,l) : open_constr with_bindings) with_evars gl = + ((c,l) : constr with_bindings) with_evars gl = if occs <> all_occurrences then ( rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl) else let env = pf_env gl in - let sigma, c' = c in - let sigma = Evd.merge sigma (project gl) in - let ctype = get_type_of env sigma c' in + let sigma = project gl in + let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels) + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels) l with_evars dep_proof_ok gl hdcncl | None -> try @@ -264,7 +263,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac match match_with_equality_type t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars dep_proof_ok gl hdcncl | None -> raise e (* error "The provided term does not end with an equality or a declared rewrite relation." *) @@ -273,7 +272,7 @@ let general_rewrite_ebindings = general_rewrite_ebindings_clause None let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) = - general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (inj_open c,inj_ebindings bl) + general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (c,bl) let general_rewrite l2r occs dep_proof_ok ?tac c = general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,NoBindings) false @@ -282,10 +281,10 @@ let general_rewrite_ebindings_in l2r occs dep_proof_ok ?tac id = general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac let general_rewrite_bindings_in l2r occs dep_proof_ok ?tac id (c,bl) = - general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (inj_open c,inj_ebindings bl) + general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,bl) let general_rewrite_in l2r occs dep_proof_ok ?tac id c = - general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (inj_open c,NoBindings) + general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,NoBindings) let general_multi_rewrite l2r with_evars ?tac c cl = let occs_of = on_snd (List.fold_left @@ -321,7 +320,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = let do_hyps gl = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) let ids = - let ids_in_c = Environ.global_vars_set (Global.env()) (snd (fst c)) in + let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in @@ -331,7 +330,10 @@ let general_multi_rewrite l2r with_evars ?tac c cl = do_hyps let general_multi_multi_rewrite with_evars l cl tac = - let do1 l2r c = general_multi_rewrite l2r with_evars ?tac c cl in + let do1 l2r c gl = + Refiner.tclWITHHOLES with_evars + (general_multi_rewrite l2r with_evars ?tac c.it) + (Evd.merge (project gl) c.sigma) cl gl in let rec doN l2r c = function | Precisely n when n <= 0 -> tclIDTAC | Precisely 1 -> do1 l2r c @@ -372,7 +374,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = tclTHENS (assert_as false None eq) [onLastHypId (fun id -> tclTHEN - (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause)) + (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause)) (clear [id])); tclFIRST [assumption; @@ -1398,7 +1400,7 @@ let rewrite_multi_assumption_cond cond_eq_term cl gl = begin try let dir = cond_eq_term t gl in - general_multi_rewrite dir false (inj_open (mkVar id),NoBindings) cl gl + general_multi_rewrite dir false (mkVar id,NoBindings) cl gl with | Failure _ | UserError _ -> arec rest end in diff --git a/tactics/equality.mli b/tactics/equality.mli index b88f376ee..9986d230b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -52,12 +52,12 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic val register_general_rewrite_clause : (identifier option -> orientation -> - occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit -val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> open_constr option) -> unit + occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit +val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit val general_rewrite_ebindings_clause : identifier option -> orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) -> - open_constr with_bindings -> evars_flag -> tactic + constr with_bindings -> evars_flag -> tactic val general_rewrite_bindings_in : orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) -> @@ -67,9 +67,9 @@ val general_rewrite_in : identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : - orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic + orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic val general_multi_multi_rewrite : - evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> + evars_flag -> (bool * multi * constr with_bindings sigma) list -> clause -> (tactic * conditions) option -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic @@ -78,22 +78,22 @@ val replace_in : identifier -> constr -> constr -> tactic val replace_by : constr -> constr -> tactic -> tactic val replace_in_by : identifier -> constr -> constr -> tactic -> tactic -val discr : evars_flag -> constr with_ebindings -> tactic +val discr : evars_flag -> constr with_bindings -> tactic val discrConcl : tactic val discrClause : evars_flag -> clause -> tactic val discrHyp : identifier -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> - constr with_ebindings induction_arg option -> tactic + constr with_bindings induction_arg option -> tactic val inj : intro_pattern_expr located list -> evars_flag -> - constr with_ebindings -> tactic + constr with_bindings -> tactic val injClause : intro_pattern_expr located list -> evars_flag -> - constr with_ebindings induction_arg option -> tactic + constr with_bindings induction_arg option -> tactic val injHyp : identifier -> tactic val injConcl : tactic -val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic -val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic +val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic +val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings induction_arg option -> tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> constr * constr * constr diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index b5d7d10d0..c0043db06 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,6 +21,7 @@ open Rawterm open Tactics open Util open Termops +open Evd (* Equality *) open Equality @@ -54,9 +55,13 @@ let induction_arg_of_quantified_hyp = function ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a ElimOnIdent and not as "constr" *) +let elimOnConstrWithHoles tac with_evars c = + Refiner.tclWITHHOLES with_evars (tac with_evars) + c.sigma (Some (ElimOnConstr c.it)) + TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> - [ dEq false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles dEq false c ] END TACTIC EXTEND simplify_eq [ "simplify_eq" ] -> [ dEq false None ] @@ -65,7 +70,7 @@ TACTIC EXTEND simplify_eq END TACTIC EXTEND esimplify_eq_main | [ "esimplify_eq" constr_with_bindings(c) ] -> - [ dEq true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles dEq true c ] END TACTIC EXTEND esimplify_eq | [ "esimplify_eq" ] -> [ dEq true None ] @@ -75,7 +80,7 @@ END TACTIC EXTEND discriminate_main | [ "discriminate" constr_with_bindings(c) ] -> - [ discr_tac false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles discr_tac false c ] END TACTIC EXTEND discriminate | [ "discriminate" ] -> [ discr_tac false None ] @@ -84,7 +89,7 @@ TACTIC EXTEND discriminate END TACTIC EXTEND ediscriminate_main | [ "ediscriminate" constr_with_bindings(c) ] -> - [ discr_tac true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles discr_tac true c ] END TACTIC EXTEND ediscriminate | [ "ediscriminate" ] -> [ discr_tac true None ] @@ -92,11 +97,12 @@ TACTIC EXTEND ediscriminate [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings) +let h_discrHyp id gl = + h_discriminate_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl TACTIC EXTEND injection_main | [ "injection" constr_with_bindings(c) ] -> - [ injClause [] false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause []) false c ] END TACTIC EXTEND injection | [ "injection" ] -> [ injClause [] false None ] @@ -105,7 +111,7 @@ TACTIC EXTEND injection END TACTIC EXTEND einjection_main | [ "einjection" constr_with_bindings(c) ] -> - [ injClause [] true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause []) true c ] END TACTIC EXTEND einjection | [ "einjection" ] -> [ injClause [] true None ] @@ -113,7 +119,7 @@ TACTIC EXTEND einjection END TACTIC EXTEND injection_as_main | [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ injClause ipat false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause ipat) false c ] END TACTIC EXTEND injection_as | [ "injection" "as" simple_intropattern_list(ipat)] -> @@ -123,7 +129,7 @@ TACTIC EXTEND injection_as END TACTIC EXTEND einjection_as_main | [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ injClause ipat true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause ipat) true c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" simple_intropattern_list(ipat)] -> @@ -132,7 +138,8 @@ TACTIC EXTEND einjection_as [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings) +let h_injHyp id gl = + h_injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -153,8 +160,13 @@ TACTIC EXTEND absurd [ "absurd" constr(c) ] -> [ absurd c ] END +let onSomeWithHoles tac = function + | None -> tac None + | Some c -> Refiner.tclWITHHOLES false tac c.sigma (Some c.it) + TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ] + [ "contradiction" constr_with_bindings_opt(c) ] -> + [ onSomeWithHoles contradiction c ] END (* AutoRewrite *) @@ -194,9 +206,10 @@ END open Extraargs -let rewrite_star clause orient occs c (tac : glob_tactic_expr option) = +let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings) true + Refiner. tclWITHHOLES false + (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings)) sigma true let occurrences_of = function | n::_ as nl when n < 0 -> (false,List.map abs nl) diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 7a5314c36..82006f602 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -15,3 +15,4 @@ val h_injHyp : Names.identifier -> tactic val refine_tac : Evd.open_constr -> tactic +val onSomeWithHoles : ('a option -> tactic) -> 'a Evd.sigma option -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index d642a38db..ba17ac30c 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -19,26 +19,17 @@ open Tacexpr open Tactics open Util -let inj_id id = (dummy_loc,id) -let inj_open c = (Evd.empty,c) -let inj_open_wb (c,b) = ((Evd.empty,c),b) -let inj_ia = function - | ElimOnConstr c -> ElimOnConstr (inj_open_wb c) - | ElimOnIdent id -> ElimOnIdent id - | ElimOnAnonHyp n -> ElimOnAnonHyp n -let inj_occ (occ,c) = (occ,inj_open c) - (* Basic tactics *) let h_intro_move x y = abstract_tactic (TacIntroMove (x, y)) (intro_move x y) let h_intro x = h_intro_move (Some x) no_move let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption -let h_exact c = abstract_tactic (TacExact (inj_open c)) (exact_check c) +let h_exact c = abstract_tactic (TacExact c) (exact_check c) let h_exact_no_check c = - abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c) + abstract_tactic (TacExactNoCheck c) (exact_no_check c) let h_vm_cast_no_check c = - abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) + abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) let h_apply simple ev cb = abstract_tactic (TacApply (simple,ev,List.map snd cb,None)) (apply_with_ebindings_gen simple ev cb) @@ -46,35 +37,35 @@ let h_apply_in simple ev cb (id,ipat as inhyp) = abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp)) (apply_in simple ev id cb ipat) let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) + abstract_tactic (TacElim (ev,cb,cbo)) (elim ev cb cbo) -let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) -let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) -let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c) +let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) +let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb) +let h_case_type c = abstract_tactic (TacCaseType c) (case_type c) let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) let h_mutual_fix b id n l = abstract_tactic - (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l)) + (TacMutualFix (b,id,n,l)) (mutual_fix id n l 0) let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido) let h_mutual_cofix b id l = abstract_tactic - (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l)) + (TacMutualCofix (b,id,l)) (mutual_cofix id l 0) -let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c) +let h_cut c = abstract_tactic (TacCut c) (cut c) let h_generalize_gen cl = - abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl)) + abstract_tactic (TacGeneralize cl) (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) let h_generalize cl = h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous)) cl) let h_generalize_dep c = - abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) + abstract_tactic (TacGeneralizeDep c) (generalize_dep c) let h_let_tac b na c cl = let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in - abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl) + abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl) (* Derived basic tactics *) let h_simple_induction_destruct isrec h = @@ -83,15 +74,14 @@ let h_simple_induction_destruct isrec h = let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let h_induction_destruct isrec ev (l,cl) = - abstract_tactic (TacInductionDestruct (isrec,ev,(List.map (fun (c,e,idl) -> - List.map inj_ia c,Option.map inj_open_wb e,idl) l,cl))) - (induction_destruct ev isrec (l,cl)) +let h_induction_destruct isrec ev lcl = + abstract_tactic (TacInductionDestruct (isrec,ev,lcl)) + (induction_destruct ev isrec lcl) let h_new_induction ev c e idl cl = h_induction_destruct ev true ([c,e,idl],cl) let h_new_destruct ev c e idl cl = h_induction_destruct ev false ([c,e,idl],cl) -let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) -let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) +let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) +let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) (* Context management *) let h_clear b l = abstract_tactic (TacClear (b,l)) @@ -113,26 +103,27 @@ let h_any_constructor t = *) let h_constructor ev n l = abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l) -let h_one_constructor n = h_constructor false n NoBindings +let h_one_constructor n = + abstract_tactic (TacConstructor(false,AI n,NoBindings)) (one_constructor n NoBindings) let h_simplest_left = h_left false NoBindings let h_simplest_right = h_right false NoBindings (* Conversion *) let h_reduce r cl = - abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) + abstract_tactic (TacReduce (r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl)) + abstract_tactic (TacChange (oc,c,cl)) (change (Option.map Redexpr.out_with_occurrences oc) c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = - abstract_tactic (TacTransitivity (Option.map inj_open c)) + abstract_tactic (TacTransitivity c) (intros_transitivity c) -let h_simplest_apply c = h_apply false false [dummy_loc,(inj_open c,NoBindings)] -let h_simplest_eapply c = h_apply false true [dummy_loc,(inj_open c,NoBindings)] +let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)] +let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 86a337678..70eb8dfb3 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -38,15 +38,15 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - open_constr with_bindings located list -> tactic + constr with_bindings located list -> tactic val h_apply_in : advanced_flag -> evars_flag -> - open_constr with_bindings located list -> + constr with_bindings located list -> identifier * intro_pattern_expr located option -> tactic -val h_elim : evars_flag -> constr with_ebindings -> - constr with_ebindings option -> tactic +val h_elim : evars_flag -> constr with_bindings -> + constr with_bindings option -> tactic val h_elim_type : constr -> tactic -val h_case : evars_flag -> constr with_ebindings -> tactic +val h_case : evars_flag -> constr with_bindings -> tactic val h_case_type : constr -> tactic val h_mutual_fix : hidden_flag -> identifier -> int -> @@ -69,19 +69,19 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic val h_new_induction : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic val h_new_destruct : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - (constr with_ebindings induction_arg list * constr with_ebindings option * + (constr with_bindings induction_arg list * constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) list * Tacticals.clause option -> tactic -val h_specialize : int option -> constr with_ebindings -> tactic +val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic (* Automation tactic : see Auto *) @@ -95,10 +95,10 @@ val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic (* Constructors *) -val h_constructor : evars_flag -> int -> open_constr bindings -> tactic -val h_left : evars_flag -> open_constr bindings -> tactic -val h_right : evars_flag -> open_constr bindings -> tactic -val h_split : evars_flag -> open_constr bindings list -> tactic +val h_constructor : evars_flag -> int -> constr bindings -> tactic +val h_left : evars_flag -> constr bindings -> tactic +val h_right : evars_flag -> constr bindings -> tactic +val h_split : evars_flag -> constr bindings list -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index aea8c0ccf..ce6abc93e 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -158,7 +158,7 @@ let is_applied_rewrite_relation env sigma rels t = let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in - Some (sigma, it_mkProd_or_LetIn t rels) + Some (it_mkProd_or_LetIn t rels) with _ -> None) | _ -> None @@ -759,6 +759,8 @@ module Strategies = choice tac (apply_lemma l l2r (false,[]))) fail cs + let inj_open c = (Evd.empty,c) + let old_hints (db : string) : strategy = let rules = Autorewrite.find_rewrites db in lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) @@ -1378,17 +1380,16 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)} -let get_hyp gl evars (evm,c) clause l2r = +let get_hyp gl evars c clause l2r = let hi = decompose_applied_relation (pf_env gl) evars c l2r in let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl let general_rewrite_flags = { under_lambdas = false; on_morphisms = false } -let apply_lemma gl (evm,c) cl l2r occs = +let apply_lemma gl c cl l2r occs = let sigma = project gl in - let evars = Evd.merge sigma evm in - let hypinfo = ref (get_hyp gl evars (evm,c) cl l2r) in + let hypinfo = ref (get_hyp gl sigma c cl l2r) in let app = apply_rule hypinfo occs in let rec aux () = Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env)) @@ -1397,7 +1398,10 @@ let apply_lemma gl (evm,c) cl l2r occs = let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo, strat = apply_lemma gl c cl l2r occs in - try cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl gl + try + tclTHEN + (Refiner.tclEVARS hypinfo.cl.evd) + (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl) gl with Not_found -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 13add4151..8c5f85c21 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1169,18 +1169,19 @@ let coerce_to_ident fresh env = function destVar c | v -> raise (CannotCoerceTo "a fresh identifier") -let interp_ident_gen fresh ist gl id = - let env = pf_env gl in +let interp_ident_gen fresh ist env id = try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id) with Not_found -> id let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true +let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) +let pf_interp_fresh_ident id gl = interp_ident_gen true id (pf_env gl) (* Interprets an optional identifier which must be fresh *) -let interp_fresh_name ist gl = function +let interp_fresh_name ist env = function | Anonymous -> Anonymous - | Name id -> Name (interp_fresh_ident ist gl id) + | Name id -> Name (interp_fresh_ident ist env id) let coerce_to_intro_pattern env = function | VIntroPattern ipat -> ipat @@ -1367,7 +1368,7 @@ let rec extract_ids ids = function let default_fresh_id = id_of_string "H" -let interp_fresh_id ist gl l = +let interp_fresh_id ist env l = let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in let id = @@ -1376,10 +1377,12 @@ let interp_fresh_id ist gl l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l) in + | ArgVar (_,id) -> string_of_id (interp_ident ist env id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in id_of_string s in - Tactics.fresh_id avoid id gl + Tactics.fresh_id_in_env avoid id env + +let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl) (* To retype a list of key*constr with undefined key *) let retype_list sigma env lst = @@ -1446,7 +1449,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c = (* Side-effect *) !evdref,c -let interp_gen kind ist fail_evar use_classes sigma env (c,ce) = +let interp_gen kind ist fail_evar use_classes env sigma (c,ce) = let (ltacvars,unbndltacvars as vars),typs = extract_ltac_vars_data ist sigma env in let c = match ce with @@ -1465,90 +1468,58 @@ let interp_gen kind ist fail_evar use_classes sigma env (c,ce) = (evd,c) (* Interprets a constr; expects evars to be solved *) -let interp_constr_gen kind ist sigma env c = - snd (interp_gen kind ist true true sigma env c) +let interp_constr_gen kind ist env sigma c = + snd (interp_gen kind ist true true env sigma c) let interp_constr = interp_constr_gen (OfType None) let interp_type = interp_constr_gen IsType (* Interprets an open constr *) -let interp_open_constr_gen kind ist sigma env c = - interp_gen kind ist false false sigma env c +let interp_open_constr_gen kind ist = interp_gen kind ist false false let interp_open_constr ccl = interp_open_constr_gen (OfType ccl) (* Interprets a constr expression casted by the current goal *) let pf_interp_casted_constr ist gl c = - interp_constr_gen (OfType (Some (pf_concl gl))) ist (project gl) (pf_env gl) c - -(* Interprets an open constr expression *) -let pf_interp_open_constr casted ist gl cc = - let cl = if casted then Some (pf_concl gl) else None in - interp_open_constr cl ist (project gl) (pf_env gl) cc + interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c (* Interprets a constr expression *) let pf_interp_constr ist gl = - interp_constr ist (project gl) (pf_env gl) + interp_constr ist (pf_env gl) (project gl) let constr_list_of_VList env = function | VList l -> List.map (constr_of_value env) l | _ -> raise Not_found -let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l = - let env = pf_env gl in - let try_expand_ltac_var x = +let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = + let try_expand_ltac_var sigma x = try match dest_fun x with - | RVar (_,id), _ -> - List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) + | RVar (_,id), _ -> + sigma, + List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) | _ -> - raise Not_found + raise Not_found with Not_found -> (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*) - [interp_fun ist gl x] in - List.flatten (List.map try_expand_ltac_var l) + let sigma, c = interp_fun ist env sigma x in + sigma, [c] in + let sigma, l = list_fold_map try_expand_ltac_var sigma l in + sigma, List.flatten l -let pf_interp_constr_list = - pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (fun ist gl -> interp_constr ist (project gl) (pf_env gl)) - -(* -let pf_interp_constr_list_as_list ist gl (c,_ as x) = - match c with - | RVar (_,id) -> - (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun) - with Not_found -> []) - | _ -> [interp_constr ist (project gl) (pf_env gl) x] - -let pf_interp_constr_list ist gl l = - List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l) -*) +let interp_constr_list ist env sigma c = + snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c) let inj_open c = (Evd.empty,c) -let pf_interp_open_constr_list = - pf_interp_constr_in_compound_list inj_open (fun x -> x) - (fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl)) - -(* -let pf_interp_open_constr_list_as_list ist gl (c,_ as x) = - match c with - | RVar (_,id) -> - (try List.map inj_open - (constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)) - with Not_found -> - [interp_open_constr None ist (project gl) (pf_env gl) x]) - | _ -> - [interp_open_constr None ist (project gl) (pf_env gl) x] - -let pf_interp_open_constr_list ist gl l = - List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l) -*) +let interp_open_constr_list = + interp_constr_in_compound_list (fun x -> x) (fun x -> x) + (interp_open_constr None) (* Interprets a type expression *) let pf_interp_type ist gl = - interp_type ist (project gl) (pf_env gl) + interp_type ist (pf_env gl) (project gl) (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = @@ -1561,24 +1532,24 @@ let interp_pattern ist sigma env (occs,c) = (interp_occurrences ist occs, interp_constr ist sigma env c) let pf_interp_constr_with_occurrences ist gl = - interp_pattern ist (project gl) (pf_env gl) + interp_pattern ist (pf_env gl) (project gl) -let pf_interp_constr_with_occurrences_and_name_as_list = - pf_interp_constr_in_compound_list +let interp_constr_with_occurrences_and_name_as_list = + interp_constr_in_compound_list (fun c -> ((all_occurrences_expr,c),Anonymous)) (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c | _ -> raise Not_found) - (fun ist gl (occ_c,na) -> - (interp_pattern ist (project gl) (pf_env gl) occ_c, - interp_fresh_name ist gl na)) + (fun ist env sigma (occ_c,na) -> + sigma, (interp_pattern ist env sigma occ_c, + interp_fresh_name ist env na)) let interp_red_expr ist sigma env = function | Unfold l -> Unfold (List.map (interp_unfold ist env) l) - | Fold l -> Fold (List.map (interp_constr ist sigma env) l) + | Fold l -> Fold (List.map (interp_constr ist env sigma) l) | Cbv f -> Cbv (interp_flag ist env f) | Lazy f -> Lazy (interp_flag ist env f) - | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) - | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o) + | Pattern l -> Pattern (List.map (interp_pattern ist env sigma) l) + | Simpl o -> Simpl (Option.map (interp_pattern ist env sigma) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -1619,12 +1590,6 @@ let interp_constr_may_eval ist gl c = csr end -let inj_may_eval = function - | ConstrTerm c -> ConstrTerm (inj_open c) - | ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c) - | ConstrContext (id,c) -> ConstrContext (id,inj_open c) - | ConstrTypeOf c -> ConstrTypeOf (inj_open c) - let rec message_of_value = function | VVoid -> str "()" | VInteger n -> int n @@ -1661,7 +1626,7 @@ let rec interp_intro_pattern ist gl = function | loc, IntroIdentifier id -> loc, interp_intro_pattern_var loc ist (pf_env gl) id | loc, IntroFresh id -> - loc, IntroFresh (interp_fresh_ident ist gl id) + loc, IntroFresh (interp_fresh_ident ist (pf_env gl) id) | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x @@ -1717,37 +1682,53 @@ let interp_declared_or_quantified_hypothesis ist gl = function (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) with Not_found -> NamedHyp id -let interp_binding ist gl (loc,b,c) = - (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c) - -let interp_bindings ist gl = function -| NoBindings -> NoBindings -| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l) -| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l) - -let interp_constr_with_bindings ist gl (c,bl) = - (pf_interp_constr ist gl c, interp_bindings ist gl bl) - -let interp_open_constr_with_bindings ist gl (c,bl) = - (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl) +let interp_binding ist env sigma (loc,b,c) = + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (loc,interp_binding_name ist b,c) + +let interp_bindings ist env sigma = function +| NoBindings -> + sigma, NoBindings +| ImplicitBindings l -> + let sigma, l = interp_open_constr_list ist env sigma l in + sigma, ImplicitBindings l +| ExplicitBindings l -> + let sigma, l = list_fold_map (interp_binding ist env) sigma l in + sigma, ExplicitBindings l + +let interp_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c,bl) + +let interp_open_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c, bl) let loc_of_bindings = function | NoBindings -> dummy_loc | ImplicitBindings l -> loc_of_rawconstr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) -let interp_open_constr_with_bindings_loc ist gl ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = let loc1 = loc_of_rawconstr c in let loc2 = loc_of_bindings bl in let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in - (loc,interp_open_constr_with_bindings ist gl cb) + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + sigma, (loc,cb) -let interp_induction_arg ist gl = function - | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c) - | ElimOnAnonHyp n as x -> x +let interp_induction_arg ist gl sigma arg = + let env = pf_env gl in + match arg with + | ElimOnConstr c -> + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, ElimOnConstr c + | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try - match List.assoc id ist.lfun with + sigma, + match List.assoc id ist.lfun with | VInteger n -> ElimOnAnonHyp n | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id) | VConstr c -> ElimOnConstr (c,NoBindings) @@ -1756,15 +1737,18 @@ let interp_induction_arg ist gl = function strbrk " neither to a quantified hypothesis nor to a term.") with Not_found -> (* Interactive mode *) - if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr - (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), - NoBindings) + if Tactics.is_quantified_hypothesis id gl then + sigma, ElimOnIdent (loc,id) + else + let c = interp_constr ist env sigma (RVar (loc,id),Some (CRef (Ident (loc,id)))) in + sigma, ElimOnConstr (c,NoBindings) let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c) let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) +let pack_sigma (sigma,c) = {it=c;sigma=sigma} + (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1802,7 +1786,7 @@ and eval_tactic ist = function | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) | TacAbstract (tac,ido) -> fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl + (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl | TacThen (t1,tf,t,tl) -> tclTHENS3PARTS (interp_tactic ist t1) (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) @@ -1859,7 +1843,7 @@ and interp_tacarg ist gl = function | TacExternal (loc,com,req,la) -> interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la) | TacFreshId l -> - let id = interp_fresh_id ist gl l in + let id = pf_interp_fresh_id ist gl l in VIntroPattern (IntroIdentifier id) | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> @@ -2054,7 +2038,7 @@ and interp_genarg ist gl x = (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) | IdentArgType b -> in_gen (wit_ident_gen b) - (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) + (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) | VarArgType -> in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x)) | RefArgType -> @@ -2076,14 +2060,16 @@ and interp_genarg ist gl x = in_gen wit_red_expr (pf_interp_red_expr ist gl (out_gen globwit_red_expr x)) | OpenConstrArgType casted -> in_gen (wit_open_constr_gen casted) - (pf_interp_open_constr casted ist gl + (interp_open_constr (if casted then Some (pf_concl gl) else None) + ist (pf_env gl) (project gl) (snd (out_gen (globwit_open_constr_gen casted) x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings - (interp_constr_with_bindings ist gl (out_gen globwit_constr_with_bindings x)) + (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) + (out_gen globwit_constr_with_bindings x))) | BindingsArgType -> in_gen wit_bindings - (interp_bindings ist gl (out_gen globwit_bindings x)) + (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x))) | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x @@ -2104,12 +2090,12 @@ and interp_genarg ist gl x = and interp_genarg_constr_list0 ist gl x = let lc = out_gen (wit_list0 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list0 wit_constr) lc and interp_genarg_constr_list1 ist gl x = let lc = out_gen (wit_list1 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list1 wit_constr) lc and interp_genarg_var_list0 ist gl x = @@ -2227,59 +2213,68 @@ and interp_tactic ist tac gl = tactic_of_value ist (val_interp ist gl tac) gl (* Interprets a primitive tactic *) -and interp_atomic ist gl = function +and interp_atomic ist gl tac = + let env = pf_env gl and sigma = project gl in + match tac with (* Basic tactics *) | TacIntroPattern l -> h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> - h_intro_move (Option.map (interp_fresh_ident ist gl) ido) + h_intro_move (Option.map (interp_fresh_ident ist env) ido) (interp_move_location ist gl hto) | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) - | TacApply (a,ev,cb,None) -> - h_apply a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb) - | TacApply (a,ev,cb,Some cl) -> - h_apply_in a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb) - (interp_in_hyp_as ist gl cl) + | TacApply (a,ev,cb,cl) -> + let sigma, l = + list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + in + let tac = match cl with + | None -> h_apply a ev + | Some cl -> + (fun l -> h_apply_in a ev l (interp_in_hyp_as ist gl cl)) in + tclWITHHOLES ev tac sigma l | TacElim (ev,cb,cbo) -> - h_elim ev (interp_constr_with_bindings ist gl cb) - (Option.map (interp_constr_with_bindings ist gl) cbo) + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + tclWITHHOLES ev (h_elim ev cb) sigma cbo | TacElimType c -> h_elim_type (pf_interp_type ist gl c) - | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) + | TacCase (ev,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES ev (h_case ev) sigma cb | TacCaseType c -> h_case_type (pf_interp_type ist gl c) - | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n + | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n | TacMutualFix (b,id,n,l) -> - let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c) - in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l) - | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt) + let f (id,n,c) = (interp_fresh_ident ist env id,n,pf_interp_type ist gl c) + in h_mutual_fix b (interp_fresh_ident ist env id) n (List.map f l) + | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt) | TacMutualCofix (b,id,l) -> - let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in - h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l) + let f (id,c) = (interp_fresh_ident ist env id,pf_interp_type ist gl c) in + h_mutual_cofix b (interp_fresh_ident ist env id) (List.map f l) | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> - let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in - abstract_tactic (TacAssert (t,ipat,inj_open c)) + let c = (if t=None then interp_constr else interp_type) ist env sigma c in + abstract_tactic (TacAssert (t,ipat,c)) (Tactics.forward (Option.map (interp_tactic ist) t) (Option.map (interp_intro_pattern ist gl) ipat) c) | TacGeneralize cl -> - h_generalize_gen - (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl) + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + tclWITHHOLES false (h_generalize_gen) sigma cl | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp + h_let_tac b (interp_fresh_name ist env na) (pf_interp_constr ist gl c) clp (* Automation tactics *) | TacTrivial (lems,l) -> - Auto.h_trivial (pf_interp_constr_list ist gl lems) + Auto.h_trivial (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> Auto.h_auto (Option.map (interp_int_or_var ist) n) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) @@ -2287,19 +2282,23 @@ and interp_atomic ist gl = function | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p,lems) -> Auto.h_dauto (Option.map (interp_int_or_var ist) n,p) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) | TacInductionDestruct (isrec,ev,(l,cls)) -> - h_induction_destruct ev isrec - (List.map (fun (lc,cbo,(ipato,ipats)) -> - (List.map (interp_induction_arg ist gl) lc, - Option.map (interp_constr_with_bindings ist gl) cbo, - (Option.map (interp_intro_pattern ist gl) ipato, - Option.map (interp_intro_pattern ist gl) ipats))) l, - Option.map (interp_clause ist gl) cls) + let sigma, l = + list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) -> + let sigma,lc = + list_fold_map (interp_induction_arg ist gl) sigma lc in + let sigma,cbo = + Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + (sigma,(lc,cbo, + (Option.map (interp_intro_pattern ist gl) ipato, + Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + let cls = Option.map (interp_clause ist gl) cls in + tclWITHHOLES ev (h_induction_destruct ev isrec) sigma (l,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2309,8 +2308,9 @@ and interp_atomic ist gl = function | TacDecompose (l,c) -> let l = List.map (interp_inductive ist) l in Elim.h_decompose l (pf_interp_constr ist gl c) - | TacSpecialize (n,l) -> - h_specialize n (interp_constr_with_bindings ist gl l) + | TacSpecialize (n,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES false (h_specialize n) sigma cb | TacLApply c -> h_lapply (pf_interp_constr ist gl c) (* Context management *) @@ -2321,18 +2321,25 @@ and interp_atomic ist gl = function | TacRename l -> h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, - interp_fresh_ident ist gl (snd id2)) l) + interp_fresh_ident ist env (snd id2)) l) | TacRevert l -> h_revert (interp_hyp_list ist gl l) (* Constructors *) - | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl) - | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl) - | TacSplit (ev,_,bll) -> h_split ev (List.map (interp_bindings ist gl) bll) + | TacLeft (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_left ev) sigma bl + | TacRight (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_right ev) sigma bl + | TacSplit (ev,_,bll) -> + let sigma, bll = list_fold_map (interp_bindings ist env) sigma bll in + tclWITHHOLES ev (h_split ev) sigma bll | TacAnyConstructor (ev,t) -> abstract_tactic (TacAnyConstructor (ev,t)) (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) | TacConstructor (ev,n,bl) -> - h_constructor ev (skip_metaid n) (interp_bindings ist gl bl) + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_constructor ev (skip_metaid n)) sigma bl (* Conversion *) | TacReduce (r,cl) -> @@ -2353,10 +2360,13 @@ and interp_atomic ist gl = function (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Equality.general_multi_multi_rewrite ev - (List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l) - (interp_clause ist gl cl) - (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) + let l = List.map (fun (b,m,c) -> + let sigma',c = interp_open_constr_with_bindings ist env sigma c in + let _,sigma' = Evarutil.subtract_evars sigma sigma' in + (b,m,{it=c;sigma=sigma'})) l in + let cl = interp_clause ist gl cl in + Equality.general_multi_multi_rewrite ev l cl + (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (Option.map (interp_intro_pattern ist gl) ids) @@ -2388,7 +2398,7 @@ and interp_atomic ist gl = function VIntroPattern (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType b -> - value_of_ident (interp_fresh_ident ist gl + value_of_ident (interp_fresh_ident ist env (out_gen (globwit_ident_gen b) x)) | VarArgType -> mk_hyp_value ist gl (out_gen globwit_var x) @@ -2420,7 +2430,7 @@ and interp_atomic ist gl = function VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) | List0ArgType (IdentArgType b) -> let wit = wit_list0 (globwit_ident_gen b) in - let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in VList (List.map mk_ident (out_gen wit x)) | List0ArgType IntroPatternArgType -> let wit = wit_list0 globwit_intro_pattern in @@ -2440,7 +2450,7 @@ and interp_atomic ist gl = function VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) | List1ArgType (IdentArgType b) -> let wit = wit_list1 (globwit_ident_gen b) in - let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in VList (List.map mk_ident (out_gen wit x)) | List1ArgType IntroPatternArgType -> let wit = wit_list1 globwit_intro_pattern in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ce8cfa7db..fe4e9f6aa 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -134,8 +134,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> - Evd.open_constr Rawterm.bindings +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dc51c6d0c..332e93c8c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,23 +59,6 @@ let rec nb_prod x = let inj_with_occurrences e = (all_occurrences_expr,e) -let inj_open c = (Evd.empty,c) - -let inj_occ (occ,c) = (occ,inj_open c) - -let inj_red_expr = function - | Simpl lo -> Simpl (Option.map inj_occ lo) - | Fold l -> Fold (List.map inj_open l) - | Pattern l -> Pattern (List.map inj_occ l) - | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c) - -> c - -let inj_ebindings = function - | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map inj_open l) - | ExplicitBindings l -> - ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l) - let dloc = dummy_loc (* Option for 8.2 compatibility *) @@ -191,8 +174,11 @@ let rename_hyp = Tacmach.rename_hyp (* Fresh names *) (**************************************************************) +let fresh_id_in_env avoid id env = + next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env)) + let fresh_id avoid id gl = - next_ident_away_in_goal id (avoid@(pf_ids_of_hyps gl)) + fresh_id_in_env avoid id (pf_env gl) (**************************************************************) (* Fixpoints and CoFixpoints *) @@ -776,7 +762,7 @@ let elimination_clause_scheme with_evars allow_K i elimclause indclause gl = type eliminator = { elimindex : int option; (* None = find it automatically *) - elimbody : constr with_ebindings + elimbody : constr with_bindings } let general_elim_clause_gen elimtac indclause elim gl = @@ -927,26 +913,6 @@ let descend_in_conjunctions sidecond_first with_evars tac exit c gl = (* Resolution tactics *) (****************************************************) -(* Resolution with missing arguments *) - -let check_evars sigma evm 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 - in - if rest <> Evd.empty then - errorlabstrm "apply" (str"Uninstantiated existential "++ - str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ - fnl () ++ pr_evar_map rest);; - -let get_bindings_evars = function - | ImplicitBindings largs -> List.map fst largs - | ExplicitBindings lbind -> List.map (fun x -> fst (pi3 x)) lbind - | NoBindings -> [] - let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in @@ -954,17 +920,13 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = goal. If this fails, then the head constant will be unfolded step by step. *) let concl_nprod = nb_prod (pf_concl gl0) in - let evmc, c = c in - let evm = List.fold_left Evd.merge evmc (get_bindings_evars lbind) in let rec try_main_apply with_destruct c gl = let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in - let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in - if not with_evars then check_evars (fst res).sigma evm gl0; - res + Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> @@ -987,33 +949,27 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = Stdpp.raise_with_loc loc exn in try_red_apply thm_ty0 in - if evm = Evd.empty then try_main_apply with_destruct c gl0 - else - tclTHEN - (tclEVARS (Evd.merge gl0.sigma evm)) - (try_main_apply with_destruct c) gl0 + try_main_apply with_destruct c gl0 let rec apply_with_ebindings_gen b e = function - | [] -> - tclIDTAC + | [] -> tclIDTAC | [cb] -> general_apply b b e cb | cb::cbl -> tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl) -let apply_with_ebindings cb = apply_with_ebindings_gen false false [dloc,cb] -let eapply_with_ebindings cb = apply_with_ebindings_gen false true [dloc,cb] +let apply_with_ebindings cb = + apply_with_ebindings_gen false false [dloc,cb] + +let eapply_with_ebindings cb = + apply_with_ebindings_gen false true [dloc,cb] -let apply_with_bindings (c,bl) = - apply_with_ebindings (inj_open c,inj_ebindings bl) +let apply_with_bindings cb = apply_with_ebindings_gen false false [dloc,cb] -let eapply_with_bindings (c,bl) = - apply_with_ebindings_gen false true [dloc,(inj_open c,inj_ebindings bl)] +let eapply_with_bindings cb = apply_with_ebindings_gen false true [dloc,cb] -let apply c = - apply_with_ebindings (inj_open c,NoBindings) +let apply c = apply_with_ebindings_gen false false [dloc,(c,NoBindings)] -let eapply c = - eapply_with_ebindings (inj_open c,NoBindings) +let eapply c = apply_with_ebindings_gen false true [dloc,(c,NoBindings)] let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1055,25 +1011,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl = aux (make_clenv_binding gl (d,thm) lbind) let apply_in_once sidecond_first with_delta with_destruct with_evars id - (loc,((sigma,d),lbind)) gl0 = + (loc,(d,lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in - let sigma = List.fold_left Evd.merge sigma (get_bindings_evars lbind) in let t' = pf_get_hyp_typ gl0 id in let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in let rec aux with_destruct c gl = try let clause = apply_in_once_main flags innerclause (c,lbind) gl in - let res = clenv_refine_in ~sidecond_first with_evars id clause gl in - if not with_evars then check_evars (fst res).sigma sigma gl0; - res + clenv_refine_in ~sidecond_first with_evars id clause gl with exn when with_destruct -> descend_in_conjunctions sidecond_first true aux (fun _ -> raise exn) c gl in - if sigma = Evd.empty then aux with_destruct d gl0 - else - tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux with_destruct d) gl0 - + aux with_destruct d gl0 (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1176,13 +1126,12 @@ let rec intros_clearing = function (* Modifying/Adding an hypothesis *) let specialize mopt (c,lbind) g = - let evars, term = - if lbind = NoBindings then None, c + let term = + if lbind = NoBindings then c else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in - let (thd,tstack) = - whd_stack clause.evd (clenv_value clause) in + let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> @@ -1193,24 +1142,21 @@ let specialize mopt (c,lbind) g = | t::l -> if occur_meta t then [] else t :: chk l in chk tstack in - let term = applist(thd,tstack) in + let term = applist(thd,List.map (nf_evar clause.evd) tstack) in if occur_meta term then errorlabstrm "" (str "Cannot infer an instance for " ++ pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); - Some clause.evd, term + term in - tclTHEN - (match evars with Some e -> tclEVARS e | _ -> tclIDTAC) - (match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with + match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with | Var id when List.mem id (pf_ids_of_hyps g) -> tclTHENFIRST (fun g -> internal_cut_replace id (pf_type_of g term) g) - (exact_no_check term) + (exact_no_check term) g | _ -> tclTHENLAST (fun g -> cut (pf_type_of g term) g) - (exact_no_check term)) - g + (exact_no_check term) g (* Keeping only a few hypotheses *) @@ -1248,12 +1194,11 @@ let constructor_tac with_evars expctdnumopt i lbind gl = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = - general_apply true false with_evars (dloc,(inj_open cons,lbind)) in + let apply_tac = general_apply true false with_evars (dloc,(cons,lbind)) in (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl -let one_constructor i = constructor_tac false None i +let one_constructor i lbind = constructor_tac false None i lbind (* Try to apply the constructor of the inductive definition followed by a tactic t given as an argument. @@ -1273,18 +1218,17 @@ let any_constructor with_evars tacopt gl = let left_with_ebindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2 -let split_with_ebindings with_evars = - tclMAP (constructor_tac with_evars (Some 1) 1) - -let left l = left_with_ebindings false (inj_ebindings l) -let simplest_left = left NoBindings +let split_with_ebindings with_evars l = + tclMAP (constructor_tac with_evars (Some 1) 1) l -let right l = right_with_ebindings false (inj_ebindings l) -let simplest_right = right NoBindings +let left = left_with_ebindings false +let simplest_left = left NoBindings -let split l = split_with_ebindings false [inj_ebindings l] -let simplest_split = split NoBindings +let right = right_with_ebindings false +let simplest_right = right NoBindings +let split = constructor_tac false (Some 1) 1 +let simplest_split = split NoBindings (*****************************) (* Decomposing introductions *) @@ -1328,7 +1272,7 @@ let intro_or_and_pattern loc b ll l' tac id gl = let rewrite_hyp l2r id gl = let rew_on l2r = - !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in + !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in @@ -1431,7 +1375,7 @@ let prepare_intros s ipat gl = match ipat with | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id] | IntroRewrite l2r -> let id = make_id s gl in - id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl + id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | IntroOrAndPattern ll -> make_id s gl, onLastHypId (intro_or_and_pattern loc true ll [] @@ -1465,7 +1409,7 @@ let assert_tac na = assert_as true (ipat_of_name na) let as_tac id ipat = match ipat with | Some (loc,IntroRewrite l2r) -> - !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl + !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | Some (loc,IntroOrAndPattern ll) -> intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) id @@ -1497,10 +1441,11 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars lemmas) (as_tac id ipat) -let apply_in simple with_evars = general_apply_in false simple simple with_evars +let apply_in simple with_evars id lemmas ipat = + general_apply_in false simple simple with_evars id lemmas ipat let simple_apply_in id c = - apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None + general_apply_in false false false false id [dloc,(c,NoBindings)] None (**************************) (* Generalize tactics *) @@ -2137,7 +2082,7 @@ let cook_sign hyp0_opt indvars env = (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: constr with_ebindings option; + elimc: constr with_bindings option; elimt: types; indref: global_reference option; index: int; (* index of the elimination type in the scheme *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b894628c3..d2cbeb856 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,10 +30,6 @@ open Rawterm open Termops (*i*) -val inj_open : constr -> open_constr -val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen -val inj_ebindings : constr bindings -> open_constr bindings - (* Main tactics. *) (*s General functions. *) @@ -60,6 +56,7 @@ val cofix : identifier option -> tactic (*s Introduction tactics. *) +val fresh_id_in_env : identifier list -> identifier -> env -> identifier val fresh_id : identifier list -> identifier -> goal sigma -> identifier val find_intro_names : rel_context -> goal sigma -> identifier list @@ -103,8 +100,8 @@ val try_intros_until : or a term with bindings *) val onInductionArg : - (constr with_ebindings -> tactic) -> - constr with_ebindings induction_arg -> tactic + (constr with_bindings -> tactic) -> + constr with_bindings induction_arg -> tactic (*s Introduction tactics with eliminations. *) @@ -163,7 +160,7 @@ val clear : identifier list -> tactic val clear_body : identifier list -> tactic val keep : identifier list -> tactic -val specialize : int option -> constr with_ebindings -> tactic +val specialize : int option -> constr with_bindings -> tactic val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier * identifier) list -> tactic @@ -180,21 +177,20 @@ val apply : constr -> tactic val eapply : constr -> tactic val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> open_constr with_ebindings located list -> - tactic + advanced_flag -> evars_flag -> constr with_bindings located list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic -val apply_with_ebindings : open_constr with_ebindings -> tactic -val eapply_with_ebindings : open_constr with_ebindings -> tactic +val apply_with_ebindings : constr with_bindings -> tactic +val eapply_with_ebindings : constr with_bindings -> tactic val cut_and_apply : constr -> tactic val apply_in : - advanced_flag -> evars_flag -> identifier -> - open_constr with_ebindings located list -> - intro_pattern_expr located option -> tactic + advanced_flag -> evars_flag -> identifier -> + constr with_bindings located list -> + intro_pattern_expr located option -> tactic val simple_apply_in : identifier -> constr -> tactic @@ -227,7 +223,7 @@ val simple_apply_in : identifier -> constr -> tactic (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: constr with_ebindings option; + elimc: constr with_bindings option; elimt: types; indref: global_reference option; index: int; (* index of the elimination type in the scheme *) @@ -248,13 +244,13 @@ type elim_scheme = { } -val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme +val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types (* elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (* None = find it automatically *) - elimbody : constr with_ebindings + elimbody : constr with_bindings } val elimination_clause_scheme : evars_flag -> @@ -267,38 +263,38 @@ val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> 'a -> eliminator -> tactic val general_elim : evars_flag -> - constr with_ebindings -> eliminator -> ?allow_K:bool -> tactic + constr with_bindings -> eliminator -> ?allow_K:bool -> tactic val general_elim_in : evars_flag -> - identifier -> constr with_ebindings -> eliminator -> tactic + identifier -> constr with_bindings -> eliminator -> tactic -val default_elim : evars_flag -> constr with_ebindings -> tactic +val default_elim : evars_flag -> constr with_bindings -> tactic val simplest_elim : constr -> tactic val elim : - evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic + evars_flag -> constr with_bindings -> constr with_bindings option -> tactic val simple_induct : quantified_hypothesis -> tactic -val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> +val new_induct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic (*s Case analysis tactics. *) -val general_case_analysis : evars_flag -> constr with_ebindings -> tactic +val general_case_analysis : evars_flag -> constr with_bindings -> tactic val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> +val new_destruct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic (*s Generic case analysis / induction tactics. *) val induction_destruct : rec_flag -> evars_flag -> - (constr with_ebindings induction_arg list * - constr with_ebindings option * + (constr with_bindings induction_arg list * + constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) list * clause option -> tactic @@ -321,17 +317,17 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) val constructor_tac : evars_flag -> int option -> int -> - open_constr bindings -> tactic + constr bindings -> tactic val any_constructor : evars_flag -> tactic option -> tactic -val one_constructor : int -> open_constr bindings -> tactic +val one_constructor : int -> constr bindings -> tactic val left : constr bindings -> tactic val right : constr bindings -> tactic val split : constr bindings -> tactic -val left_with_ebindings : evars_flag -> open_constr bindings -> tactic -val right_with_ebindings : evars_flag -> open_constr bindings -> tactic -val split_with_ebindings : evars_flag -> open_constr bindings list -> tactic +val left_with_ebindings : evars_flag -> constr bindings -> tactic +val right_with_ebindings : evars_flag -> constr bindings -> tactic +val split_with_ebindings : evars_flag -> constr bindings list -> tactic val simplest_left : tactic val simplest_right : tactic @@ -388,4 +384,4 @@ val specialize_hypothesis : identifier -> tactic val dependent_pattern : ?pattern_term:bool -> constr -> tactic val register_general_multi_rewrite : - (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit + (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit |