From 33d54f6692446e6006f9b89d0dfd64408a4051fe Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 17 Nov 2011 22:19:36 +0000 Subject: Fixing bug #2640 and variants of it (inconsistency between when and how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_ltac.ml4 | 16 ++-- parsing/pptactic.ml | 20 ++--- parsing/q_coqast.ml4 | 6 +- parsing/tactic_printer.ml | 2 +- plugins/decl_mode/decl_interp.ml | 2 +- plugins/setoid_ring/Ncring_polynom.v | 6 +- plugins/setoid_ring/newring.ml4 | 16 ++-- plugins/subtac/subtac_utils.ml | 2 +- plugins/xml/dumptree.ml4 | 2 +- plugins/xml/proofTree2Xml.ml4 | 2 +- proofs/tacexpr.ml | 2 +- tactics/tacinterp.ml | 130 ++++++++++++++++------------ tactics/tacinterp.mli | 2 +- test-suite/bugs/closed/shouldsucceed/2640.v | 17 ++++ 14 files changed, 131 insertions(+), 94 deletions(-) create mode 100644 test-suite/bugs/closed/shouldsucceed/2640.v diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index e71d53bf9..2f129637d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -20,7 +20,7 @@ open Tok let fail_default_value = ArgArg 0 let arg_of_expr = function - TacArg a -> a + TacArg (loc,a) -> a | e -> Tacexp (e:raw_tactic_expr) (* Tactics grammar rules *) @@ -85,20 +85,20 @@ GEXTEND Gram | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> - TacArg (TacExternal (loc,com,req,la)) + TacArg (loc,TacExternal (loc,com,req,la)) | st = simple_tactic -> TacAtom (loc,st) - | a = may_eval_arg -> TacArg(a) + | a = may_eval_arg -> TacArg(loc,a) | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(MetaIdArg (loc,false,id)) + TacArg(loc,MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(ConstrMayEval(ConstrTerm c)) + TacArg(loc,ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacArg(IntroPattern ipat) + TacArg(loc,IntroPattern ipat) | r = reference; la = LIST0 tactic_arg -> - TacArg(TacCall (loc,r,la)) ] + TacArg(loc,TacCall (loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a - | a = tactic_atom -> TacArg a ] ] + | a = tactic_atom -> TacArg (loc,a) ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index fd4c1bcea..f55ced809 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -479,7 +479,7 @@ let pr_funvar = function let pr_let_clause k pr (id,(bl,t)) = hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg t)) + str " :=" ++ brk (1,1) ++ pr (TacArg (dummy_loc,t))) let pr_let_clauses recflag pr = function | hd::tl -> @@ -922,20 +922,20 @@ let rec pr_tac inherited tac = latom | TacAtom (loc,t) -> pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom - | TacArg(Tacexp e) -> pr_tac_level (latom,E) e, latom - | TacArg(ConstrMayEval (ConstrTerm c)) -> + | TacArg(_,Tacexp e) -> pr_tac_level (latom,E) e, latom + | TacArg(_,ConstrMayEval (ConstrTerm c)) -> str "constr:" ++ pr_constr c, latom - | TacArg(ConstrMayEval c) -> + | TacArg(_,ConstrMayEval c) -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c, leval - | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom - | TacArg(Integer n) -> int n, latom - | TacArg(TacCall(loc,f,[])) -> pr_ref f, latom - | TacArg(TacCall(loc,f,l)) -> + | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom + | TacArg(_,Integer n) -> int n, latom + | TacArg(_,TacCall(loc,f,[])) -> pr_ref f, latom + | TacArg(_,TacCall(loc,f,l)) -> pr_with_comments loc (hov 1 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall - | TacArg a -> pr_tacarg a, latom + | TacArg (_,a) -> pr_tacarg a, latom in if prec_less prec inherited then strm else str"(" ++ strm ++ str")" @@ -954,7 +954,7 @@ and pr_tacarg = function str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la | (TacCall _|Tacexp _|Integer _) as a -> - str "ltac:" ++ pr_tac (latom,E) (TacArg a) + str "ltac:" ++ pr_tac (latom,E) (TacArg (dummy_loc,a)) in (pr_tac, pr_match_rule) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e184eafe3..7df97a075 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -465,9 +465,9 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacFun ($mlexpr_of_list mlexpr_of_ident_option idol$, $mlexpr_of_tactic body$) >> - | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id - | Tacexpr.TacArg t -> - <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >> + | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id + | Tacexpr.TacArg (_,t) -> + <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >> | Tacexpr.TacComplete t -> <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >> | _ -> failwith "Quotation of tactic expressions: TODO" diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 747d2c738..83dae3dce 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -16,7 +16,7 @@ open Logic open Printer let pr_tactic = function - | TacArg (Tacexp t) -> + | TacArg (_,Tacexp t) -> (*top tactic from tacinterp*) Pptactic.pr_glob_tactic (Global.env()) t | t -> diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 64aa08ff2..b3e076c49 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -27,7 +27,7 @@ let intern_justification_items globs = Option.map (List.map (intern_constr globs)) let intern_justification_method globs = - Option.map (intern_tactic globs) + Option.map (intern_pure_tactic globs) let intern_statement intern_it globs st = {st_label=st.st_label; diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index a3e14b30f..c0d315871 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -23,7 +23,7 @@ Context (C R:Type) `{Rh:Ring_morphism C R}. Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. - Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). + Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm). Ltac add_push := gen_add_push . (* Definition of non commutative multivariable polynomials @@ -298,7 +298,7 @@ reflexivity. induction P;simpl;intros. rewrite ring_morphism_mul. try reflexivity. simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. - repeat rewrite phiCR_comm. Esimpl. Qed. + Qed. Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. Proof. @@ -618,4 +618,4 @@ exact pow_th. apply Peq_ok;trivial. Qed. -End MakeRingPol. \ No newline at end of file +End MakeRingPol. diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index af236bc0f..d189a4e55 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -164,11 +164,11 @@ let decl_constant na c = (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) let ltac_letin (x, e1) e2 = TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2) @@ -624,23 +624,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = (match rk, opp, kind with Abstract, None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) | Abstract, Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Abstract, Some opp, None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Computational _,_,_ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) | Morphism mth,_,_ -> let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = let t = Retyping.get_type_of env Evd.empty c in @@ -657,7 +657,7 @@ let interp_power env pow = match pow with | None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index ae28c9847..546d720c4 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -474,4 +474,4 @@ let tactics_tac s = lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) let tactics_call tac args = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 44a481f44..3c3e54fa3 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -42,7 +42,7 @@ let thin_sign osign sign = ;; let pr_tactic_xml = function - | TacArg (Tacexp t) -> str "" + | TacArg (_,Tacexp t) -> str "" | t -> str "" ;; diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index b0e4fcc69..2f5eb6ac2 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -144,7 +144,7 @@ Pp.ppnl (Pp.(++) (Pp.str Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node in begin match tactic_expr with - | T.TacArg (T.Tacexp _) -> + | T.TacArg (_,T.Tacexp _) -> (* We don't need to keep the level of abstraction introduced at *) (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) aux flat_proof old_hyps diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 9e2acfdd0..b8279b8f9 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -240,7 +240,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast - | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg + | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast = identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 90e4582fa..f9fba20e6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -60,6 +60,9 @@ let error_syntactic_metavariables_not_allowed loc = (loc,"out_ident", str "Syntactic metavariables allowed only in quotations.") +let error_tactic_expected loc = + user_err_loc (loc,"",str "Tactic expected.") + let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid let skip_metaid = function @@ -189,7 +192,7 @@ let _ = (fun (s,t) -> add_primitive_tactic s t) [ "idtac",TacId []; "fail", TacFail(ArgArg 0,[]); - "fresh", TacArg(TacFreshId []) + "fresh", TacArg(dloc,TacFreshId []) ] let lookup_atomic id = Idmap.find id !atomic_mactab @@ -696,7 +699,7 @@ let rec intern_atomic lf ist x = TacMutualCofix (b,intern_ident lf ist id, List.map f l) | TacCut c -> TacCut (intern_type ist c) | TacAssert (otac,ipat,c) -> - TacAssert (Option.map (intern_tactic ist) otac, + TacAssert (Option.map (intern_pure_tactic ist) otac, Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen false (otac<>None) ist c) | TacGeneralize cl -> @@ -758,7 +761,7 @@ let rec intern_atomic lf ist x = | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl) | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl) | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll) - | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t) + | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t) | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl) (* Conversion *) @@ -787,7 +790,7 @@ let rec intern_atomic lf ist x = (ev, List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l, clause_app (intern_hyp_location ist) cl, - Option.map (intern_tactic ist) by) + Option.map (intern_pure_tactic ist) by) | TacInversion (inv,hyp) -> TacInversion (intern_inversion_strength lf ist inv, intern_quantified_hypothesis ist hyp) @@ -800,9 +803,9 @@ let rec intern_atomic lf ist x = let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in TacAlias (loc,s,l,(dir,body)) -and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) +and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac) -and intern_tactic_seq ist = function +and intern_tactic_seq onlytac ist = function | TacAtom (loc,t) -> let lf = ref ist.ltacvars in let t = intern_atomic lf ist t in @@ -812,52 +815,68 @@ and intern_tactic_seq ist = function let (l1,l2) = ist.ltacvars in let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in let l = List.map (fun (n,b) -> - (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in - ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u) + (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in + ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u) + | TacMatchGoal (lz,lr,lmr) -> - ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr) + ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr) | TacMatch (lz,c,lmr) -> - ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr) + ist.ltacvars, + TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) | TacFail (n,l) -> ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l) - | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac) - | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s) + | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) + | TacAbstract (tac,s) -> + ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s) | TacThen (t1,[||],t2,[||]) -> - let lfun', t1 = intern_tactic_seq ist t1 in - let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in + let lfun', t1 = intern_tactic_seq onlytac ist t1 in + let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in lfun'', TacThen (t1,[||],t2,[||]) | TacThen (t1,tf,t2,tl) -> - let lfun', t1 = intern_tactic_seq ist t1 in + let lfun', t1 = intern_tactic_seq onlytac ist t1 in let ist' = { ist with ltacvars = lfun' } in (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *) - lfun', TacThen (t1,Array.map (intern_tactic ist') tf,intern_tactic ist' t2, - Array.map (intern_tactic ist') tl) + lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2, + Array.map (intern_pure_tactic ist') tl) | TacThens (t,tl) -> - let lfun', t = intern_tactic_seq ist t in + let lfun', t = intern_tactic_seq true ist t in let ist' = { ist with ltacvars = lfun' } in (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *) - lfun', TacThens (t, List.map (intern_tactic ist') tl) + lfun', TacThens (t, List.map (intern_pure_tactic ist') tl) | TacDo (n,tac) -> - ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac) + ist.ltacvars, TacDo (intern_or_var ist n,intern_pure_tactic ist tac) + | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac) + | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac) + | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> - ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic ist tac) - | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac) - | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac) - | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac) + ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) | TacOrelse (tac1,tac2) -> - ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2) - | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l) - | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l) - | TacComplete tac -> ist.ltacvars, TacComplete (intern_tactic ist tac) - | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a) + ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) + | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) + | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l) + | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac) + | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a + +and intern_tactic_as_arg loc onlytac ist a = + match intern_tacarg !strict_check onlytac ist a with + | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a) + | Tacexp a -> a + | TacVoid | IntroPattern _ | Integer _ + | ConstrMayEval _ | TacFreshId _ as a -> + if onlytac then error_tactic_expected loc else TacArg (loc,a) + | MetaIdArg _ -> assert false + +and intern_tactic_or_tacarg ist = intern_tactic false ist + +and intern_pure_tactic ist = intern_tactic true ist and intern_tactic_fun ist (var,body) = let (l1,l2) = ist.ltacvars in let lfun' = List.rev_append (Option.List.flatten var) l1 in - (var,intern_tactic { ist with ltacvars = (lfun',l2) } body) + (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body) -and intern_tacarg strict ist = function +and intern_tacarg strict onlytac ist = function | TacVoid -> TacVoid | Reference r -> intern_non_tactic_reference strict ist r | IntroPattern ipat -> @@ -876,28 +895,29 @@ and intern_tacarg strict ist = function | TacCall (loc,f,l) -> TacCall (loc, intern_applied_tactic_reference ist f, - List.map (intern_tacarg !strict_check ist) l) + List.map (intern_tacarg !strict_check false ist) l) | TacExternal (loc,com,req,la) -> - TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la) + TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) - | Tacexp t -> Tacexp (intern_tactic ist t) + | Tacexp t -> Tacexp (intern_tactic onlytac ist t) | TacDynamic(loc,t) as x -> (match Dyn.tag t with - | "tactic" | "value" | "constr" -> x + | "tactic" | "value" -> x + | "constr" -> if onlytac then error_tactic_expected loc else x | s -> anomaly_loc (loc, "", str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) -and intern_match_rule ist = function +and intern_match_rule onlytac ist = function | (All tc)::tl -> - All (intern_tactic ist tc) :: (intern_match_rule ist tl) + All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) | (Pat (rl,mp,tc))::tl -> let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in let ido,metas2,pat = intern_pattern ist lfun mp in let metas = list_uniquize (metas1@metas2) in let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in - Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl) + Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) | [] -> [] and intern_genarg ist x = @@ -953,7 +973,7 @@ and intern_genarg ist x = match tactic_genarg_level s with | Some n -> (* Special treatment of tactic arguments *) - in_gen (globwit_tactic n) (intern_tactic ist + in_gen (globwit_tactic n) (intern_tactic_or_tacarg ist (out_gen (rawwit_tactic n) x)) | None -> lookup_genarg_glob s ist x @@ -1727,7 +1747,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = | TacLetIn (false,l,u) -> interp_letin ist gl l u | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr - | TacArg a -> interp_tacarg ist gl a + | TacArg (loc,a) -> interp_tacarg ist gl a (* Delayed evaluation *) | t -> VFun (ist.trace,ist.lfun,[],t) @@ -1768,7 +1788,7 @@ and eval_tactic ist = function begin match tac with TacAtom (_,_) -> t - | _ -> abstract_tactic_expr (TacArg (Tacexp tac)) t + | _ -> abstract_tactic_expr (TacArg (dloc,Tacexp tac)) t end | TacRepeat tac -> tclREPEAT (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> @@ -1892,7 +1912,7 @@ and eval_with_fail ist is_lazy goal tac = (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = let lref = ref ist.lfun in - let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg b))) llc in + let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in lref := lve@ist.lfun; let ist = { ist with lfun = lve@ist.lfun } in val_interp ist gl u @@ -2055,7 +2075,7 @@ and interp_genarg ist gl x = | Some n -> (* Special treatment of tactic arguments *) in_gen (wit_tactic n) - (TacArg(valueIn(VFun(ist.trace,ist.lfun,[], + (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[], out_gen (globwit_tactic n) x)))) | None -> lookup_interp_genarg s ist gl x @@ -2463,7 +2483,7 @@ let make_empty_glob_sign () = (* Initial call for interpretation *) let interp_tac_gen lfun avoid_ids debug t gl = interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] } - (intern_tactic { + (intern_tactic true { ltacvars = (List.map fst lfun, []); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } t) gl @@ -2476,18 +2496,18 @@ let interp t = interp_tac_gen [] [] (get_debug()) t let eval_ltac_constr gl t = interp_ltac_constr { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl - (intern_tactic (make_empty_glob_sign ()) t ) + (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) (* Hides interpretation for pretty-print *) let hide_interp t ot gl = let ist = { ltacvars = ([],[]); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } in - let te = intern_tactic ist t in + let te = intern_tactic true ist t in let t = eval_tactic te in match ot with - | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl + | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl | Some t' -> - abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl + abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl (***************************************************************************) (* Substitution at module closing time *) @@ -2715,7 +2735,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) - | TacArg a -> TacArg (subst_tacarg subst a) + | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) @@ -2897,7 +2917,7 @@ let add_tacdef local isrec tacl = let gtacl = List.map2 (fun (_,b,def) (id, qid) -> let k = if b then UpdateTac qid else NewTac (Option.get id) in - let t = Flags.with_option strict_check (intern_tactic ist) def in + let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in (k, t)) tacl rfun in let id0 = fst (List.hd rfun) in @@ -2915,11 +2935,11 @@ let add_tacdef local isrec tacl = (* Other entry points *) let glob_tactic x = - Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x + Flags.with_option strict_check (intern_tactic true (make_empty_glob_sign ())) x let glob_tactic_env l env x = Flags.with_option strict_check - (intern_tactic + (intern_pure_tactic { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }) x @@ -2931,7 +2951,7 @@ let interp_redexp env sigma r = (***************************************************************************) (* Embed tactics in raw or glob tactic expr *) -let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) +let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) @@ -2940,7 +2960,7 @@ let tacticIn t = Errors.print e)) let tacticOut = function - | TacArg (TacDynamic (_,d)) -> + | TacArg (_,TacDynamic (_,d)) -> if (Dyn.tag d) = "tactic" then tactic_out d else @@ -2959,6 +2979,6 @@ let _ = Auto.set_extern_interp let _ = Auto.set_extern_intern_tac (fun l -> Flags.with_option strict_check - (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})) + (intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})) let _ = Auto.set_extern_subst_tactic subst_tactic let _ = Dhyp.set_extern_interp eval_tactic diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6d7909b3b..d9dc8094f 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -91,7 +91,7 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -val intern_tactic : +val intern_pure_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr val intern_constr : diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v new file mode 100644 index 000000000..da0cc68a4 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2640.v @@ -0,0 +1,17 @@ +(* Testing consistency of globalization and interpretation in some + extreme cases *) + +Section sect. + + (* Simplification of the initial example *) + Hypothesis Other: True. + + Lemma C2 : True. + proof. + Fail have True using Other. + Abort. + + (* Variant of the same problem *) + Lemma C2 : True. + Fail clear; Other. + Abort. -- cgit v1.2.3