From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- tactics/auto.ml | 70 +++++++++++++++++--------------------- tactics/auto.mli | 4 +-- tactics/autorewrite.ml | 9 +++-- tactics/equality.ml | 83 ++++++++++++++++++++++++---------------------- tactics/extraargs.mli | 2 +- tactics/extratactics.ml4 | 12 +++---- tactics/extratactics.mli | 2 +- tactics/hiddentac.mli | 6 ++-- tactics/setoid_replace.mli | 2 +- tactics/tacinterp.ml | 69 ++++++++++++++++++++++++++------------ tactics/tacticals.mli | 4 +-- tactics/tactics.ml | 14 ++++---- tactics/tactics.mli | 3 +- 13 files changed, 151 insertions(+), 129 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index d087420a..b530178e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml,v 1.63.2.1 2004/07/16 19:30:51 herbelin Exp $ *) +(* $Id: auto.ml,v 1.63.2.2 2004/12/06 11:25:21 herbelin Exp $ *) open Pp open Util @@ -199,8 +199,12 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) = in if eapply & (nmiss <> 0) then begin if verbose then + if !Options.v7 then warn (str "the hint: EApply " ++ prterm c ++ - str " will only be used by EAuto"); + str " will only be used by EAuto") + else + warn (str "the hint: eapply " ++ prterm c ++ + str " will only be used by eauto"); (hd, { hname = name; pri = nb_hyp cty + nmiss; @@ -281,40 +285,8 @@ let add_hint dbname hintlist = let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist -(* let recalc_hints hintlist = - let env = Global.env() and sigma = Evd.empty in - let recalc_hint ((_,data) as hint) = - match data.code with - | Res_pf (c,_) -> - let c' = Term.subst_mps subst c in - if c==c' then hint else - make_apply_entry env sigma (false,false) - data.hname (c', type_of env sigma c') - | ERes_pf (c,_) -> - let c' = Term.subst_mps subst c in - if c==c' then hint else - make_apply_entry env sigma (true,false) - data.hname (c', type_of env sigma c') - | Give_exact c -> - let c' = Term.subst_mps subst c in - if c==c' then hint else - make_exact_entry data.hname (c',type_of env sigma c') - | Res_pf_THEN_trivial_fail (c,_) -> - let c' = Term.subst_mps subst c in - if c==c' then hint else - make_trivial env sigma (data.hname,c') - | Unfold_nth ref -> - let ref' = subst_global subst ref in - if ref==ref' then hint else - make_unfold (data.hname,ref') - | Extern _ -> - anomaly "Extern hints cannot be substituted!!!" - in - list_smartmap recalc_hint hintlist -*) - let forward_subst_tactic = - ref (fun _ -> failwith "subst_tactic is not installed for Auto") + ref (fun _ -> failwith "subst_tactic is not installed for auto") let set_extern_subst_tactic f = forward_subst_tactic := f @@ -430,7 +402,7 @@ let add_trivials env sigma l local dbnames = dbnames let forward_intern_tac = - ref (fun _ -> failwith "intern_tac is not installed for Auto") + ref (fun _ -> failwith "intern_tac is not installed for auto") let set_extern_intern_tac f = forward_intern_tac := f @@ -492,7 +464,9 @@ let add_hints local dbnames0 h = (* Functions for printing the hints *) (**************************************************************************) -let fmt_autotactic = function +let fmt_autotactic = + if !Options.v7 then + function | Res_pf (c,clenv) -> (str"Apply " ++ prterm c) | ERes_pf (c,clenv) -> (str"EApply " ++ prterm c) | Give_exact c -> (str"Exact " ++ prterm c) @@ -500,6 +474,16 @@ let fmt_autotactic = function (str"Apply " ++ prterm c ++ str" ; Trivial") | Unfold_nth c -> (str"Unfold " ++ pr_global c) | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac) + else + function + | Res_pf (c,clenv) -> (str"apply " ++ prterm c) + | ERes_pf (c,clenv) -> (str"eapply " ++ prterm c) + | Give_exact c -> (str"exact " ++ prterm c) + | Res_pf_THEN_trivial_fail (c,clenv) -> + (str"apply " ++ prterm c ++ str" ; trivial") + | Unfold_nth c -> (str"unfold " ++ pr_global c) + | Extern tac -> + (str "(external) " ++ Pptacticnew.pr_glob_tactic (Global.env()) tac) let fmt_hint v = (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) @@ -631,7 +615,7 @@ si apr (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) let forward_interp_tactic = - ref (fun _ -> failwith "interp_tactic is not installed for Auto") + ref (fun _ -> failwith "interp_tactic is not installed for auto") let set_extern_interp f = forward_interp_tactic := f @@ -700,7 +684,10 @@ let trivial dbnames gl = try searchtable_map x with Not_found -> - error ("Trivial: "^x^": No such Hint database")) + if !Options.v7 then + error ("Trivial: "^x^": No such Hint database") + else + error ("trivial: "^x^": No such Hint database")) ("core"::dbnames) in tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl @@ -799,7 +786,10 @@ let auto n dbnames gl = try searchtable_map x with Not_found -> - error ("Auto: "^x^": No such Hint database")) + if !Options.v7 then + error ("Auto: "^x^": No such Hint database") + else + error ("auto: "^x^": No such Hint database")) ("core"::dbnames) in let hyps = pf_hyps gl in diff --git a/tactics/auto.mli b/tactics/auto.mli index ef6b85ea..ec8c0d71 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto.mli,v 1.22.2.1 2004/07/16 19:30:51 herbelin Exp $ i*) +(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) (*i*) open Util @@ -105,7 +105,7 @@ val make_resolves : (* [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; - Never raises an User_exception; + Never raises a user exception; If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 7c134b89..5706e134 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -22,7 +22,7 @@ open Vernacinterp open Tacexpr (* Rewriting rules *) -type rew_rule = constr * bool * tactic +type rew_rule = constr * bool * glob_tactic_expr (* Summary and Object declaration *) let rewtab = @@ -39,7 +39,6 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -(* Rewriting rules before tactic interpretation *) type raw_rew_rule = constr * bool * raw_tactic_expr (* Applies all the rules of one base *) @@ -51,6 +50,7 @@ let one_base tac_main bas = errorlabstrm "AutoRewrite" (str ("Rewriting base "^(bas)^" does not exist")) in + let lrul = List.map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> tclTHEN tac (tclREPEAT_MAIN @@ -65,12 +65,11 @@ let autorewrite tac_main lbas = (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrl in let l = try - List.rev_append l (Stringmap.find rbase !rewtab) + lrl @ Stringmap.find rbase !rewtab with - | Not_found -> List.rev l + | Not_found -> lrl in rewtab:=Stringmap.add rbase l !rewtab diff --git a/tactics/equality.ml b/tactics/equality.ml index dd9054f5..994abb9d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml,v 1.120.2.1 2004/07/16 19:30:53 herbelin Exp $ *) +(* $Id: equality.ml,v 1.120.2.4 2004/11/21 22:24:09 herbelin Exp $ *) open Pp open Util @@ -18,6 +18,7 @@ open Termops open Inductive open Inductiveops open Environ +open Libnames open Reductionops open Instantiate open Typeops @@ -327,8 +328,11 @@ let descend_then sigma env head dirn = (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> - let arign,_ = get_arity env indf in - let p = it_mkLambda_or_LetIn (lift mip.mind_nrealargs resty) arign in + let arsign,_ = get_arity env indf in + let depind = build_dependent_inductive env indf in + let deparsign = (Anonymous,None,depind)::arsign in + let p = + it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in let build_branch i = let result = if i = dirn then dirnval else dfltval in it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in @@ -371,7 +375,9 @@ let construct_discriminator sigma env dirn c sort = let (mib,mip) = lookup_mind_specif env ind in let arsign,arsort = get_arity env indf in let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in - let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in + let depind = build_dependent_inductive env indf in + let deparsign = (Anonymous,None,depind)::arsign in + let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in let cstrs = get_constructors env indf in let build_branch i = let endpt = if i = dirn then true_0 else false_0 in @@ -419,14 +425,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = exception NotDiscriminable -let discr id gls = - let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in +let discrEq (lbeq,(t,t1,t2)) id gls = let sort = pf_type_of gls (pf_concl gls) in - let (lbeq,(t,t1,t2)) = - try find_eq_data_decompose eqn - with PatternMatchingFailure -> - errorlabstrm "discr" (pr_id id ++ str": not a primitive equality here") - in let sigma = project gls in let env = pf_env gls in (match find_positions env sigma t1 t2 with @@ -445,24 +445,40 @@ let discr id gls = ([onLastHyp gen_absurdity; refine (mkApp (pf, [| mkVar id |]))]))) gls) - let not_found_message id = (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++ str" was not found in the current environment") +let onEquality tac id gls = + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + let eq = + try find_eq_data_decompose eqn + with PatternMatchingFailure -> + errorlabstrm "" (pr_id id ++ str": not a primitive equality") + in tac eq id gls + +let check_equality tac id gls = + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in + let eq = + try find_eq_data_decompose eqn + with PatternMatchingFailure -> + errorlabstrm "" (str "The goal should negate an equality") + in tac eq id gls + let onNegatedEquality tac gls = - if is_matching_not (pf_concl gls) then - (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp tac)) gls - else if is_matching_imp_False (pf_concl gls)then - (tclTHEN intro (onLastHyp tac)) gls - else + if is_matching_not (pf_concl gls) then + (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp(check_equality tac))) gls + else if is_matching_imp_False (pf_concl gls)then + (tclTHEN intro (onLastHyp (check_equality tac))) gls + else errorlabstrm "extract_negated_equality_then" (str"The goal should negate an equality") - let discrSimpleClause = function - | None -> onNegatedEquality discr - | Some (id,_,_) -> discr id + | None -> onNegatedEquality discrEq + | Some (id,_,_) -> onEquality discrEq id + +let discr = onEquality discrEq let discrClause = onClauses discrSimpleClause @@ -566,7 +582,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let isevars = Evarutil.create_evar_defs sigma in let rec sigrec_clausal_form siglen p_i = if siglen = 0 then - if Evarconv.the_conv_x env isevars p_i dFLTty then + if Evarconv.the_conv_x_leq env isevars dFLTty p_i then (* the_conv_x had a side-effect on isevars *) dFLT else @@ -695,13 +711,7 @@ let try_delta_expand env sigma t = expands then only when the whdnf has a constructor of an inductive type in hd position, otherwise delta expansion is not done *) -let inj id gls = - let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in - let (eq,(t,t1,t2))= - try find_eq_data_decompose eqn - with PatternMatchingFailure -> - errorlabstrm "Inj" (pr_id id ++ str": not a primitive equality here") - in +let injEq (eq,(t,t1,t2)) id gls = let sigma = project gls in let env = pf_env gls in match find_positions env sigma t1 t2 with @@ -749,17 +759,17 @@ let inj id gls = in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) injectors gls - + +let inj = onEquality injEq + let injClause = function - | None -> onNegatedEquality inj + | None -> onNegatedEquality injEq | Some id -> try_intros_until inj id let injConcl gls = injClause None gls let injHyp id gls = injClause (Some id) gls -let decompEqThen ntac id gls = - let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in - let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in +let decompEqThen ntac (lbeq,(t,t1,t2)) id gls = let sort = pf_type_of gls (pf_concl gls) in let sigma = project gls in let env = pf_env gls in @@ -806,17 +816,12 @@ let decompEqThen ntac id gls = (ntac (List.length injectors))) gls)) -let decompEq = decompEqThen (fun x -> tclIDTAC) - let dEqThen ntac = function | None -> onNegatedEquality (decompEqThen ntac) - | Some id -> try_intros_until (decompEqThen ntac) id + | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id let dEq = dEqThen (fun x -> tclIDTAC) -let dEqConcl gls = dEq None gls -let dEqHyp id gls = dEq (Some id) gls - let rewrite_msg = function | None -> str "passed term is not a primitive equality" | Some id -> pr_id id ++ str "does not satisfy preconditions " diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 60a1ddc5..2b4746ae 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: extraargs.mli,v 1.3.2.1 2004/07/16 19:30:53 herbelin Exp $ *) +(*i $Id: extraargs.mli,v 1.3.2.2 2005/01/21 17:14:10 herbelin Exp $ i*) open Tacexpr open Term diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1dbf84ab..237f0a0d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4,v 1.21.2.1 2004/07/16 19:30:53 herbelin Exp $ *) +(* $Id: extratactics.ml4,v 1.21.2.2 2004/11/15 11:06:49 herbelin Exp $ *) open Pp open Pcoq @@ -202,21 +202,21 @@ open Rawterm VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] - -> [ add_inversion_lemma_exn na c s false half_inv_tac ] + -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (RProp Null) false half_inv_tac ] + -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ] | [ "Derive" "Inversion" ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ] + -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_tac ] | [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal n na id Term.mk_Prop false half_inv_tac ] + -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] - -> [ add_inversion_lemma_exn na c s true half_dinv_tac ] + -> [ add_inversion_lemma_exn na c s true dinv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversionClear diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index a714c8dd..78a94190 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: extratactics.mli,v 1.3.10.1 2004/07/16 19:30:53 herbelin Exp $ *) +(*i $Id: extratactics.mli,v 1.3.10.2 2005/01/21 17:14:10 herbelin Exp $ i*) open Names open Term diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 816678ae..1b37291c 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hiddentac.mli,v 1.19.2.1 2004/07/16 19:30:53 herbelin Exp $ i*) +(*i $Id: hiddentac.mli,v 1.19.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) (*i*) open Names @@ -78,9 +78,9 @@ val h_rename : identifier -> identifier -> tactic (* Constructors *) -(* +(*i val h_any_constructor : tactic -> tactic -*) +i*) val h_constructor : int -> constr bindings -> tactic val h_left : constr bindings -> tactic val h_right : constr bindings -> tactic diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 565ae169..854fa478 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: setoid_replace.mli,v 1.3.6.1 2004/07/16 19:30:55 herbelin Exp $ *) +(*i $Id: setoid_replace.mli,v 1.3.6.2 2005/01/21 17:14:11 herbelin Exp $ i*) open Term open Proof_type diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2080b5dc..4f8e7d7c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml,v 1.84.2.4 2004/07/16 19:30:55 herbelin Exp $ *) +(* $Id: tacinterp.ml,v 1.84.2.8 2005/01/15 14:56:54 herbelin Exp $ *) open Constrintern open Closure @@ -552,8 +552,7 @@ let intern_redexp ist = function | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o) - | (Red _ | Hnf as r) -> r - | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let intern_inversion_strength lf ist = function | NonDepInversion (k,idl,ids) -> @@ -879,9 +878,12 @@ and intern_genarg ist x = in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x)) | TacticArgType -> in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x)) + | OpenConstrArgType -> + in_gen globwit_open_constr + ((),intern_constr ist (snd (out_gen rawwit_open_constr x))) | CastedOpenConstrArgType -> in_gen globwit_casted_open_constr - (intern_constr ist (out_gen rawwit_casted_open_constr x)) + ((),intern_constr ist (snd (out_gen rawwit_casted_open_constr x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) @@ -964,6 +966,10 @@ let is_match_catchable = function | No_match | Eval_fail _ -> true | e -> is_failure e or Logic.catchable_exception e +let hack_fail_level_shift = ref 0 +let hack_fail_level n = + if n >= !hack_fail_level_shift then n - !hack_fail_level_shift else 0 + (* Verifies if the matched list is coherent with respect to lcm *) let rec verify_metas_coherence gl lcm = function | (num,csr)::tl -> @@ -1202,12 +1208,12 @@ let interp_constr ist sigma env c = interp_casted_constr None ist sigma env c (* Interprets an open constr expression casted by the current goal *) -let pf_interp_casted_openconstr ist gl (c,ce) = +let pf_interp_openconstr_gen casted ist gl (c,ce) = let sigma = project gl in let env = pf_env gl in let (ltacvars,l) = constr_list ist env in let typs = retype_list sigma env ltacvars in - let ocl = Some (pf_concl gl) in + let ocl = if casted then Some (pf_concl gl) else None in match ce with | None -> Pretyping.understand_gen_tcc sigma env typs ocl c @@ -1216,6 +1222,9 @@ let pf_interp_casted_openconstr ist gl (c,ce) = intros/lettac/inversion hypothesis names *) | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl +let pf_interp_casted_openconstr = pf_interp_openconstr_gen true +let pf_interp_openconstr = pf_interp_openconstr_gen false + (* Interprets a constr expression *) let pf_interp_constr ist gl = interp_constr ist (project gl) (pf_env gl) @@ -1242,8 +1251,7 @@ let redexp_interp ist sigma env = function | Lazy f -> Lazy (interp_flag ist env f) | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o) - | (Red _ | Hnf as r) -> r - | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl) @@ -1349,7 +1357,7 @@ and eval_tactic ist = function | TacMatchContext _ -> assert false | TacMatch (c,lmr) -> assert false | TacId s -> tclIDTAC_MESSAGE s - | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s + | TacFail (n,s) -> tclFAIL (hack_fail_level (interp_int_or_var ist n)) s | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac) | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2) @@ -1494,7 +1502,7 @@ and interp_match_context ist g lr lmr = let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in eval_with_fail { ist with lfun=lgoal@lctxt@ist.lfun } mt goal else - apply_hyps_context ist env goal mt lgoal mhyps hyps + apply_hyps_context ist env goal mt lctxt lgoal mhyps hyps with | e when is_failure e -> raise e | NextOccurrence _ -> raise No_match @@ -1508,7 +1516,9 @@ and interp_match_context ist g lr lmr = begin db_mc_pattern_success ist.debug; try eval_with_fail ist t goal - with e when is_match_catchable e -> + with + | e when is_failure e -> raise e + | e when is_match_catchable e -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl end | (Pat (mhyps,mgoal,mt))::tl -> @@ -1529,9 +1539,10 @@ and interp_match_context ist g lr lmr = eval_with_fail {ist with lfun=lgoal@ist.lfun} mt goal end else - apply_hyps_context ist env goal mt lgoal mhyps hyps + apply_hyps_context ist env goal mt [] lgoal mhyps hyps end) with + | e when is_failure e -> raise e | e when is_match_catchable e -> begin (match e with @@ -1542,7 +1553,9 @@ and interp_match_context ist g lr lmr = end) | Subterm (id,mg) -> (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps - with e when is_match_catchable e -> + with + | e when is_failure e -> raise e + | e when is_match_catchable e -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> errorlabstrm "Tacinterp.apply_match_context" (str @@ -1557,7 +1570,7 @@ and interp_match_context ist g lr lmr = (read_match_rule (project g) env (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context ist env goal mt lgmatch mhyps hyps = +and apply_hyps_context ist env goal mt lctxt lgmatch mhyps hyps = let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function | Hyp ((_,hypname),mhyp)::tl as mhyps -> let (lids,lm,hyp_match,next) = @@ -1578,7 +1591,7 @@ and apply_hyps_context ist env goal mt lgmatch mhyps hyps = db_mc_pattern_success ist.debug; eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} mt goal in - apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps + apply_hyps_context_rec lctxt lgmatch hyps (hyps,0) mhyps (* Interprets extended tactic generic arguments *) and interp_genarg ist goal x = @@ -1617,9 +1630,12 @@ and interp_genarg ist goal x = | RedExprArgType -> in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x)) | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x) + | OpenConstrArgType -> + in_gen wit_open_constr + (pf_interp_openconstr ist goal (snd (out_gen globwit_open_constr x))) | CastedOpenConstrArgType -> in_gen wit_casted_open_constr - (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x)) + (pf_interp_casted_openconstr ist goal (snd (out_gen globwit_casted_open_constr x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x)) @@ -1641,6 +1657,8 @@ and interp_match ist g constr lmr = let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in val_interp {ist with lfun=lm@lctxt@ist.lfun} g mt with | NextOccurrence _ -> raise No_match + | e when is_match_catchable e -> + apply_sub_match ist (nocc + 1) (id,c) csr mt in let rec apply_match ist csr = function | (All t)::_ -> @@ -1668,7 +1686,14 @@ and interp_match ist g constr lmr = errorlabstrm "Tacinterp.apply_match" (str "Argument of match does not evaluate to a term") in let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in - apply_match ist csr ilr + try + incr hack_fail_level_shift; + let x = apply_match ist csr ilr in + decr hack_fail_level_shift; + x + with e -> + decr hack_fail_level_shift; + raise e (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = @@ -1829,7 +1854,7 @@ and interp_atomic ist gl = function | TacticArgType -> val_interp ist gl (out_gen globwit_tactic x) | StringArgType | BoolArgType - | QuantHypArgType | RedExprArgType + | QuantHypArgType | RedExprArgType | OpenConstrArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ -> error "This generic type is not supported in alias" @@ -1926,8 +1951,7 @@ let subst_redexp subst = function | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o) - | (Red _ | Hnf as r) -> r - | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let subst_raw_may_eval subst = function | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c) @@ -2120,9 +2144,12 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) | TacticArgType -> in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x)) + | OpenConstrArgType -> + in_gen globwit_open_constr + ((),subst_rawconstr subst (snd (out_gen globwit_open_constr x))) | CastedOpenConstrArgType -> in_gen globwit_casted_open_constr - (subst_rawconstr subst (out_gen globwit_casted_open_constr x)) + ((),subst_rawconstr subst (snd (out_gen globwit_casted_open_constr x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x)) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2cb63b40..111a5e2d 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli,v 1.38.2.1 2004/07/16 19:30:55 herbelin Exp $ i*) +(*i $Id: tacticals.mli,v 1.38.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) (*i*) open Names @@ -127,7 +127,7 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -(* Useful for "as intro_pattern" modifier *) +(* Useful for [as intro_pattern] modifier *) val compute_induction_names : int -> intro_pattern_expr option -> intro_pattern_expr list array diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cab4f025..b6eaf015 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml,v 1.162.2.2 2004/07/16 19:30:55 herbelin Exp $ *) +(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *) open Pp open Util @@ -654,7 +654,7 @@ let occurrences_of_hyp id cls = let occurrences_of_goal cls = if cls.onconcl then Some cls.concl_occs else None -let everywhere cls = (cls=allClauses) +let in_every_hyp cls = (cls.onhyps = None) (* (* Implementation with generalisation then re-intro: introduces noise *) @@ -721,8 +721,8 @@ let letin_abstract id c occs gl = | None -> depdecls | Some occ -> let newdecl = subst_term_occ_decl occ c d in - if d = newdecl then - if not (everywhere occs) + if occ = [] & d = newdecl then + if not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls else @@ -1175,7 +1175,7 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in if Options.do_translate() & id7 <> id8 then force := true; let id = if !Options.v7 then id7 else id8 in rnames := !rnames @ [IntroIdentifier id]; @@ -1192,12 +1192,12 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in let id8 = fresh_id avoid8 (default_id gl (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in if Options.do_translate() & id7 <> id8 then force := true; let id = if !Options.v7 then id7 else id8 in let avoid = if !Options.v7 then avoid7 else avoid8 in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6e67a9cd..1155d845 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli,v 1.59.2.1 2004/07/16 19:30:55 herbelin Exp $ i*) +(*i $Id: tactics.mli,v 1.59.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) (*i*) open Names @@ -26,6 +26,7 @@ open Genarg open Tacexpr open Nametab open Rawterm +(*i*) (* Main tactics. *) -- cgit v1.2.3