diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 474 |
1 files changed, 249 insertions, 225 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f4547930..3f8eb0ca 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: tacinterp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Constrintern open Closure @@ -51,13 +51,13 @@ open Pcoq let safe_msgnl s = try msgnl s with e -> msgnl - (str "bug in the debugger : " ++ + (str "bug in the debugger: " ++ str "an exception is raised while printing debug information") let error_syntactic_metavariables_not_allowed loc = user_err_loc (loc,"out_ident", - str "Syntactic metavariables allowed only in quotations") + str "Syntactic metavariables allowed only in quotations.") let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid @@ -72,10 +72,10 @@ type ltac_type = (* Values for interpretation *) type value = - | VTactic of loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *) | VRTactic of (goal list sigma * validation) (* For Match results *) (* Not a true value *) - | VFun of (identifier*value) list * identifier option list * glob_tactic_expr + | VFun of ltac_trace * (identifier*value) list * + identifier option list * glob_tactic_expr | VVoid | VInteger of int | VIntroPattern of intro_pattern_expr (* includes idents which are not *) @@ -86,20 +86,20 @@ type value = | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr -let locate_tactic_call loc = function - | VTactic (_,t) -> VTactic (loc,t) - | v -> v - -let locate_error_in_file dir = function - | Stdpp.Exc_located (loc,e) -> Error_in_file ("",(true,dir,loc),e) - | e -> Error_in_file ("",(true,dir,dummy_loc),e) +let dloc = dummy_loc -let catch_error loc tac g = - try tac g - with e when loc <> dummy_loc -> - match e with - | Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e)) - | e -> raise (Stdpp.Exc_located (loc,e)) +let catch_error call_trace tac g = + if call_trace = [] then tac g else try tac g with + | LtacLocated _ as e -> raise e + | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e + | e -> + let (loc',c),tail = list_sep_last call_trace in + let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in + if tail = [] then + let loc = if loc' = dloc then loc else loc' in + raise (Stdpp.Exc_located(loc,e')) + else + raise (Stdpp.Exc_located(loc',LtacLocated((c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -107,11 +107,11 @@ type interp_sign = avoid_ids : identifier list; (* ids inherited from the call context (needed to get fresh ids) *) debug : debug_info; - last_loc : loc } + trace : ltac_trace } let check_is_value = function | VRTactic _ -> (* These are goals produced by Match *) - error "Immediate match producing tactics not allowed in local definitions" + error "Immediate match producing tactics not allowed in local definitions." | _ -> () (* For tactic_of_value *) @@ -121,16 +121,16 @@ exception NotTactic let constr_of_VConstr_context = function | VConstr_context c -> c | _ -> - errorlabstrm "constr_of_VConstr_context" (str "not a context variable") + errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.") (* Displays a value *) let rec pr_value env = function | VVoid -> str "()" | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern ipat + | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) | VConstr c | VConstr_context c -> (match env with Some env -> pr_lconstr_env env c | _ -> str "a term") - | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "a tactic" + | (VRTactic _ | VFun _ | VRec _) -> str "a tactic" | VList [] -> str "an empty list" | VList (a::_) -> str "a list (first element is " ++ pr_value env a ++ str")" @@ -143,24 +143,13 @@ let constr_of_id env id = construct_reference (Environ.named_context env) id (* To embed tactics *) -let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t), - (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) = +let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), + (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = create "tactic" let ((value_in : value -> Dyn.t), (value_out : Dyn.t -> value)) = create "value" -let tacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) -let tacticOut = function - | TacArg (TacDynamic (_,d)) -> - if (tag d) = "tactic" then - tactic_out d - else - anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") - | ast -> - anomalylabstrm "tacticOut" - (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) - let valueIn t = TacDynamic (dummy_loc,value_in t) let valueOut = function | TacDynamic (_,d) -> @@ -182,8 +171,6 @@ let constrOut = function | ast -> anomalylabstrm "constrOut" (str "Not a Dynamic ast") -let dloc = dummy_loc - (* Globalizes the identifier *) let find_reference env qid = (* We first look for a variable of the current proof *) @@ -195,7 +182,7 @@ let find_reference env qid = let error_not_evaluable s = errorlabstrm "evalref_of_ref" (str "Cannot coerce" ++ spc () ++ s ++ spc () ++ - str "to an evaluable reference") + str "to an evaluable reference.") (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -211,7 +198,7 @@ let _ = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); "compute", TacReduce(Cbv all_flags,nocl); - "intro", TacIntroMove(None,None); + "intro", TacIntroMove(None,no_move); "intros", TacIntroPattern []; "assumption", TacAssumption; "cofix", TacCofix None; @@ -263,7 +250,7 @@ let tac_tab = Hashtbl.create 17 let add_tactic s t = if Hashtbl.mem tac_tab s then errorlabstrm ("Refiner.add_tactic: ") - (str ("Cannot redeclare tactic "^s)); + (str ("Cannot redeclare tactic "^s^".")); Hashtbl.add tac_tab s t let overwriting_add_tactic s t = @@ -278,7 +265,7 @@ let lookup_tactic s = Hashtbl.find tac_tab s with Not_found -> errorlabstrm "Refiner.lookup_tactic" - (str"The tactic " ++ str s ++ str" is not installed") + (str"The tactic " ++ str s ++ str" is not installed.") (* let vernac_tactic (s,args) = let tacfun = lookup_tactic s args in @@ -311,11 +298,17 @@ let lookup_genarg_glob id = let (f,_,_) = lookup_genarg id in f let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f -(* Dynamically check that an argument is a tactic, possibly unboxing VRec *) +let propagate_trace ist loc id = function + | VFun (_,lfun,it,b) -> + let t = if it=[] then b else TacFun (it,b) in + VFun ((loc,LtacVarCall (id,t))::ist.trace,lfun,it,b) + | x -> x + +(* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id = function - | VTactic _ | VFun _ | VRTactic _ as a -> a + | VFun _ | VRTactic _ as a -> a | _ -> user_err_loc - (loc, "", str "variable " ++ pr_id id ++ str " should be bound to a tactic") + (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") (*****************) (* Globalization *) @@ -422,6 +415,11 @@ let intern_constr_reference strict ist = function let loc,_ as lqid = qualid_of_reference r in RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) +let intern_move_location ist = function + | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) + | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id) + | MoveToEnd toleft as x -> x + (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = @@ -432,7 +430,7 @@ let intern_isolated_global_tactic_reference r = | Ident (_,id) -> Tacexp (lookup_atomic id) | _ -> raise Not_found -let intern_isolated_tactic_reference ist r = +let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) try Reference (intern_ltac_variable ist r) with Not_found -> @@ -440,7 +438,7 @@ let intern_isolated_tactic_reference ist r = try intern_isolated_global_tactic_reference r with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference true ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) error_global_not_found_loc (qualid_of_reference r) @@ -475,7 +473,7 @@ let intern_non_tactic_reference strict ist r = with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with - | Ident (_,id) when not strict -> IntroPattern (IntroIdentifier id) + | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id) | _ -> (* Reference not found *) error_global_not_found_loc (qualid_of_reference r) @@ -487,13 +485,14 @@ let intern_message_token ist = function let intern_message ist = List.map (intern_message_token ist) let rec intern_intro_pattern lf ist = function - | IntroOrAndPattern l -> - IntroOrAndPattern (intern_case_intro_pattern lf ist l) - | IntroIdentifier id -> - IntroIdentifier (intern_ident lf ist id) - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x - -and intern_case_intro_pattern lf ist = + | loc, IntroOrAndPattern l -> + loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) + | loc, IntroIdentifier id -> + loc, IntroIdentifier (intern_ident lf ist id) + | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) + as x -> x + +and intern_or_and_intro_pattern lf ist = List.map (List.map (intern_intro_pattern lf ist)) let intern_quantified_hypothesis ist = function @@ -602,10 +601,10 @@ let intern_red_expr ist = function let intern_inversion_strength lf ist = function | NonDepInversion (k,idl,ids) -> NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl, - intern_intro_pattern lf ist ids) + Option.map (intern_intro_pattern lf ist) ids) | DepInversion (k,copt,ids) -> DepInversion (k, Option.map (intern_constr ist) copt, - intern_intro_pattern lf ist ids) + Option.map (intern_intro_pattern lf ist) ids) | InversionUsing (c,idl) -> InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) @@ -642,9 +641,9 @@ let internalise_tacarg ch = G_xml.parse_tactic_arg ch let extern_tacarg ch env sigma = function | VConstr c -> !print_xml_term ch env sigma c - | VTactic _ | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ + | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ | VIntroPattern _ | VRec _ | VList _ -> - error "Only externing of terms is implemented" + error "Only externing of terms is implemented." let extern_request ch req gl la = output_string ch "<REQUEST req=\""; output_string ch req; @@ -652,11 +651,11 @@ let extern_request ch req gl la = List.iter (pf_apply (extern_tacarg ch) gl) la; output_string ch "</REQUEST>\n" -(* Reads the hypotheses of a Match Context rule *) -let rec intern_match_context_hyps sigma env lfun = function +(* Reads the hypotheses of a "match goal" rule *) +let rec intern_match_goal_hyps sigma env lfun = function | (Hyp ((_,na) as locna,mp))::tl -> let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in - let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in + let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in let lfun' = name_cons na (Option.List.cons ido lfun) in lfun', metas1@metas2, Hyp (locna,pat)::hyps | [] -> lfun, [], [] @@ -667,7 +666,7 @@ let extract_let_names lrc = (fun ((loc,name),_) l -> if List.mem name l then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times"); + (loc, "glob_tactic", str "This variable is bound several times."); name::l) lrc [] @@ -684,14 +683,15 @@ let rec intern_atomic lf ist x = | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) - | TacIntroMove (ido,ido') -> + | TacIntroMove (ido,hto) -> TacIntroMove (Option.map (intern_ident lf ist) ido, - Option.map (intern_hyp ist) ido') + intern_move_location ist hto) | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) - | TacApply (a,ev,cb) -> TacApply (a,ev,intern_constr_with_bindings ist cb) + | TacApply (a,ev,cb) -> + TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb) | TacElim (ev,cb,cbo) -> TacElim (ev,intern_constr_with_bindings ist cb, Option.map (intern_constr_with_bindings ist) cbo) @@ -735,20 +735,15 @@ let rec intern_atomic lf ist x = List.map (intern_constr ist) lems) (* Derived basic tactics *) - | TacSimpleInduction h -> - TacSimpleInduction (intern_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids,cls) -> - TacNewInduction (ev,List.map (intern_induction_arg ist) lc, - Option.map (intern_constr_with_bindings ist) cbo, - intern_intro_pattern lf ist ids, - Option.map (clause_app (intern_hyp_location ist)) cls) - | TacSimpleDestruct h -> - TacSimpleDestruct (intern_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids,cls) -> - TacNewDestruct (ev,List.map (intern_induction_arg ist) c, + | TacSimpleInductionDestruct (isrec,h) -> + TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h) + | TacInductionDestruct (ev,isrec,l) -> + TacInductionDestruct (ev,isrec,List.map (fun (lc,cbo,(ipato,ipats),cls) -> + (List.map (intern_induction_arg ist) lc, Option.map (intern_constr_with_bindings ist) cbo, - intern_intro_pattern lf ist ids, - Option.map (clause_app (intern_hyp_location ist)) cls) + (Option.map (intern_intro_pattern lf ist) ipato, + Option.map (intern_intro_pattern lf ist) ipats), + Option.map (clause_app (intern_hyp_location ist)) cls)) l) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in @@ -764,7 +759,7 @@ let rec intern_atomic lf ist x = | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l) | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) | TacMove (dep,id1,id2) -> - TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2) + TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> intern_hyp_or_metaid ist id1, @@ -812,8 +807,7 @@ let rec intern_atomic lf ist x = TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l) | TacAlias (loc,s,l,(dir,body)) -> let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in - try TacAlias (loc,s,l,(dir,body)) - with e -> raise (locate_error_in_file (string_of_dirpath dir) e) + TacAlias (loc,s,l,(dir,body)) and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) @@ -829,8 +823,8 @@ and intern_tactic_seq ist = function 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) - | TacMatchContext (lz,lr,lmr) -> - ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr) + | TacMatchGoal (lz,lr,lmr) -> + ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr) | TacMatch (lz,c,lmr) -> ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) @@ -885,7 +879,7 @@ and intern_tacarg strict ist = function if istac then Reference (ArgVar (adjust_loc loc,id)) else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None)) else error_syntactic_metavariables_not_allowed loc - | TacCall (loc,f,[]) -> intern_isolated_tactic_reference ist f + | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f | TacCall (loc,f,l) -> TacCall (loc, intern_applied_tactic_reference ist f, @@ -906,7 +900,7 @@ and intern_match_rule ist = function All (intern_tactic ist tc) :: (intern_match_rule ist tl) | (Pat (rl,mp,tc))::tl -> let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in - let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in + let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in let ido,metas2,pat = intern_pattern sigma env lfun mp in let metas = list_uniquize (metas1@metas2) in let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in @@ -1006,23 +1000,23 @@ let read_pattern lfun = function (* Reads the hypotheses of a Match Context rule *) let cons_and_check_name id l = if List.mem id l then - user_err_loc (dloc,"read_match_context_hyps", - str ("Hypothesis pattern-matching variable "^(string_of_id id)^ - " used twice in the same pattern")) + user_err_loc (dloc,"read_match_goal_hyps", + strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ + " used twice in the same pattern.")) else id::l -let rec read_match_context_hyps lfun lidh = function +let rec read_match_goal_hyps lfun lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> let lidh' = name_fold cons_and_check_name na lidh in Hyp (locna,read_pattern lfun mp):: - (read_match_context_hyps lfun lidh' tl) + (read_match_goal_hyps lfun lidh' tl) | [] -> [] (* Reads the rules of a Match Context or a Match *) let rec read_match_rule lfun = function | (All tc)::tl -> (All tc)::(read_match_rule lfun tl) | (Pat (rl,mp,tc))::tl -> - Pat (read_match_context_hyps lfun [] rl, read_pattern lfun mp,tc) + Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc) :: read_match_rule lfun tl | [] -> [] @@ -1110,8 +1104,8 @@ let debugging_exception_step ist signal_anomaly e pp = let error_ltac_variable loc id env v s = user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ - str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s) + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") exception CannotCoerceTo of string @@ -1153,8 +1147,8 @@ let coerce_to_intro_pattern env = function IntroIdentifier (destVar c) | v -> raise (CannotCoerceTo "an introduction pattern") -let interp_intro_pattern_var ist env id = - try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env)(dloc,id) +let interp_intro_pattern_var loc ist env id = + try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id) with Not_found -> IntroIdentifier id let coerce_to_hint_base = function @@ -1171,8 +1165,9 @@ let coerce_to_int = function let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid - with Not_found -> user_err_loc(fst locid,"interp_int", - str "Unbound variable" ++ pr_id (snd locid)) + with Not_found -> + user_err_loc(fst locid,"interp_int", + str "Unbound variable " ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -1209,7 +1204,7 @@ let interp_hyp ist gl (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found") + else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.") let hyp_list_of_VList env = function | VList l -> List.map (coerce_to_hyp env) l @@ -1227,11 +1222,16 @@ let interp_clause_pattern ist gl (l,occl) = | (hyp,l) :: rest -> let hyp = interp_hyp ist gl hyp in if List.mem hyp acc then - error ("Hypothesis "^(string_of_id hyp)^" occurs twice"); + error ("Hypothesis "^(string_of_id hyp)^" occurs twice."); (hyp,l)::(check (hyp::acc) rest) | [] -> [] in (l,check [] occl) +let interp_move_location ist gl = function + | MoveAfter id -> MoveAfter (interp_hyp ist gl id) + | MoveBefore id -> MoveBefore (interp_hyp ist gl id) + | MoveToEnd toleft as x -> x + (* Interprets a qualified name *) let coerce_to_reference env v = try match v with @@ -1309,7 +1309,7 @@ let rec constr_list_aux env = function let constr_list ist env = constr_list_aux env ist.lfun (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids = function +let rec intropattern_ids (loc,pat) = match pat with | IntroIdentifier id -> [id] | IntroOrAndPattern ll -> List.flatten (List.map intropattern_ids (List.flatten ll)) @@ -1317,7 +1317,7 @@ let rec intropattern_ids = function let rec extract_ids ids = function | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> - intropattern_ids ipat @ extract_ids ids tl + intropattern_ids (dloc,ipat) @ extract_ids ids tl | _::tl -> extract_ids ids tl | [] -> [] @@ -1388,7 +1388,7 @@ let solve_remaining_evars env initial_sigma evd c = proc_rec c let interp_gen kind ist sigma env (c,ce) = - let (ltacvars,unbndltacvars) = constr_list ist env in + let (ltacvars,unbndltacvars as vars) = constr_list ist env in let typs = retype_list sigma env ltacvars in let c = match ce with | None -> c @@ -1398,7 +1398,8 @@ let interp_gen kind ist sigma env (c,ce) = | Some c -> let ltacdata = (List.map fst ltacvars,unbndltacvars) in intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in - understand_ltac sigma env (typs,unbndltacvars) kind c + let trace = (dloc,LtacConstrInterp (c,vars))::ist.trace in + catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c (* Interprets a constr and solve remaining evars with default tactic *) let interp_econstr kind ist sigma env cc = @@ -1532,7 +1533,7 @@ let interp_may_eval f ist gl = function with | Not_found -> user_err_loc (loc, "interp_may_eval", - str "Unbound context identifier" ++ pr_id s)) + str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) | ConstrTerm c -> try @@ -1565,31 +1566,38 @@ let inj_may_eval = function let message_of_value = function | VVoid -> str "()" | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern ipat + | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) | VConstr_context c | VConstr c -> pr_constr c - | VRec _ | VTactic _ | VRTactic _ | VFun _ -> str "<tactic>" + | VRec _ | VRTactic _ | VFun _ -> str "<tactic>" | VList _ -> str "<list>" -let rec interp_message ist = function - | [] -> mt() - | MsgString s :: l -> pr_arg str s ++ interp_message ist l - | MsgInt n :: l -> pr_arg int n ++ interp_message ist l - | MsgIdent (loc,id) :: l -> +let rec interp_message_token ist = function + | MsgString s -> str s + | MsgInt n -> int n + | MsgIdent (loc,id) -> let v = try List.assoc id ist.lfun - with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found") in - pr_arg message_of_value v ++ interp_message ist l + with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in + message_of_value v let rec interp_message_nl ist = function | [] -> mt() - | l -> interp_message ist l ++ fnl() + | l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl() -let rec interp_intro_pattern ist gl = function - | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l) - | IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x +let interp_message ist l = + (* Force evaluation of interp_message_token so that potential errors + are raised now and not at printing time *) + prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l) -and interp_case_intro_pattern ist gl = +let rec interp_intro_pattern ist gl = function + | loc, IntroOrAndPattern l -> + loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l) + | loc, IntroIdentifier id -> + loc, interp_intro_pattern_var loc ist (pf_env gl) id + | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) + as x -> x + +and interp_or_and_intro_pattern ist gl = List.map (List.map (interp_intro_pattern ist gl)) (* Quantified named or numbered hypothesis or hypothesis in context *) @@ -1663,14 +1671,14 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = let value_interp ist = match tac with (* Immediate evaluation *) - | TacFun (it,body) -> VFun (ist.lfun,it,body) + | TacFun (it,body) -> VFun (ist.trace,ist.lfun,it,body) | TacLetIn (true,l,u) -> interp_letrec ist gl l u | TacLetIn (false,l,u) -> interp_letin ist gl l u - | TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr + | 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 (* Delayed evaluation *) - | t -> VTactic (ist.last_loc,eval_tactic ist t) + | t -> VFun (ist.trace,ist.lfun,[],t) in check_for_interrupt (); match ist.debug with @@ -1679,9 +1687,16 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = | _ -> value_interp ist and eval_tactic ist = function - | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl + | TacAtom (loc,t) -> + fun gl -> + let box = ref None in abstract_tactic_box := box; + let call = LtacAtomCall (t,box) in + let tac = (* catch error in the interpretation *) + catch_error ((dloc,call)::ist.trace) (interp_atomic ist gl) t in + (* catch error in the evaluation *) + catch_error ((loc,call)::ist.trace) tac gl | TacFun _ | TacLetIn _ -> assert false - | TacMatchContext _ | TacMatch _ -> assert false + | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s) | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s) | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) @@ -1714,31 +1729,33 @@ and force_vrec ist gl = function | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body | v -> v -and interp_ltac_reference isapplied mustbetac ist gl = function +and interp_ltac_reference loc' mustbetac ist gl = function | ArgVar (loc,id) -> let v = List.assoc id ist.lfun in let v = force_vrec ist gl v in + let v = propagate_trace ist loc id v in if mustbetac then coerce_to_tactic loc id v else v | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in + let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in let ist = { lfun=[]; debug=ist.debug; avoid_ids=ids; - last_loc = if isapplied then ist.last_loc else loc } in + trace = loc_info::ist.trace } in val_interp ist gl (lookup r) and interp_tacarg ist gl = function | TacVoid -> VVoid - | Reference r -> interp_ltac_reference false false ist gl r + | Reference r -> interp_ltac_reference dloc false ist gl r | Integer n -> VInteger n - | IntroPattern ipat -> VIntroPattern (interp_intro_pattern ist gl ipat) + | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat)) | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) | MetaIdArg (loc,_,id) -> assert false - | TacCall (loc,r,[]) -> interp_ltac_reference false true ist gl r + | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r | TacCall (loc,f,l) -> - let fv = interp_ltac_reference true true ist gl f + let fv = interp_ltac_reference loc true ist gl f and largs = List.map (interp_tacarg ist gl) l in List.iter check_is_value largs; - interp_app ist gl fv largs loc + interp_app loc ist gl fv largs | TacExternal (loc,com,req,la) -> interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la) | TacFreshId l -> @@ -1748,12 +1765,7 @@ and interp_tacarg ist gl = function | TacDynamic(_,t) -> let tg = (tag t) in if tg = "tactic" then - let f = (tactic_out t) in - val_interp ist gl - (intern_tactic { - ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = []; - gsigma = project gl; genv = pf_env gl } - (f ist)) + val_interp ist gl (tactic_out t ist) else if tg = "value" then value_out t else if tg = "constr" then @@ -1763,48 +1775,54 @@ and interp_tacarg ist gl = function (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) (* Interprets an application node *) -and interp_app ist gl fv largs loc = +and interp_app loc ist gl fv largs = match fv with - | VFun(olfun,var,body) -> + | VFun(trace,olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then let v = try - let lloc = if lval=[] then loc else ist.last_loc in - val_interp { ist with lfun=newlfun@olfun; last_loc=lloc } gl body + catch_error trace + (val_interp { ist with lfun=newlfun@olfun; trace=trace } gl) body with e -> debugging_exception_step ist false e (fun () -> str "evaluation"); raise e in debugging_step ist (fun () -> str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v); - if lval=[] then v else interp_app ist gl v lval loc + if lval=[] then v else interp_app loc ist gl v lval else - VFun(newlfun@olfun,lvar,body) + VFun(trace,newlfun@olfun,lvar,body) | _ -> user_err_loc (loc, "Tacinterp.interp_app", - (str"Illegal tactic application")) + (str"Illegal tactic application.")) (* Gives the tactic corresponding to the tactic value *) -and tactic_of_value vle g = +and tactic_of_value ist vle g = match vle with | VRTactic res -> res - | VTactic (loc,tac) -> catch_error loc tac g - | VFun _ -> error "A fully applied tactic is expected" + | VFun (trace,lfun,[],t) -> + let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in + catch_error trace tac g + | VFun _ -> error "A fully applied tactic is expected." | _ -> raise NotTactic (* Evaluation with FailError catching *) and eval_with_fail ist is_lazy goal tac = try (match val_interp ist goal tac with - | VTactic (loc,tac) when not is_lazy -> VRTactic (catch_error loc tac goal) + | VFun (trace,lfun,[],t) when not is_lazy -> + let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in + VRTactic (catch_error trace tac goal) | a -> a) with - | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) -> + | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) + | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> raise (Eval_fail s) - | Stdpp.Exc_located (s',FailError (lvl,s)) -> - raise (Stdpp.Exc_located (s',FailError (lvl - 1, s))) - | FailError (lvl,s) -> - raise (FailError (lvl - 1, s)) + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located(s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = @@ -1822,14 +1840,14 @@ and interp_letin ist gl llc u = val_interp ist gl u (* Interprets the Match Context expressions *) -and interp_match_context ist g lz lr lmr = +and interp_match_goal ist g lz lr lmr = let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps = let (lgoal,ctxt) = match_subterm nocc c csr in let lctxt = give_context ctxt id in try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps with e when is_match_catchable e -> apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in - let rec apply_match_context ist env goal nrs lex lpt = + let rec apply_match_goal ist env goal nrs lex lpt = begin if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); match lpt with @@ -1838,7 +1856,7 @@ and interp_match_context ist g lz lr lmr = db_mc_pattern_success ist.debug; try eval_with_fail ist lz goal t with e when is_match_catchable e -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl + apply_match_goal ist env goal (nrs+1) (List.tl lex) tl end | (Pat (mhyps,mgoal,mt))::tl -> let hyps = make_hyps (pf_hyps goal) in @@ -1856,21 +1874,21 @@ and interp_match_context ist g lz lr lmr = | PatternMatchingFailure -> db_matching_failure ist.debug | Eval_fail s -> db_eval_failure ist.debug s | _ -> db_logic_failure ist.debug e); - apply_match_context ist env goal (nrs+1) (List.tl lex) tl) + apply_match_goal ist env goal (nrs+1) (List.tl lex) tl) | Subterm (id,mg) -> (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps with | PatternMatchingFailure -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) + apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" + errorlabstrm "Tacinterp.apply_match_goal" (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Set Ltac Debug\" for more info)" - else mt()))) + else mt()) ++ str".")) end in let env = pf_env g in - apply_match_context ist env g 0 lmr + apply_match_goal ist env g 0 lmr (read_match_rule (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) @@ -2023,7 +2041,7 @@ and interp_match ist g lz constr lmr = with PatternMatchingFailure -> apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for match") in + "No matching clauses for match.") in let csr = try interp_ltac_constr ist g constr with e -> debugging_exception_step ist true e @@ -2058,9 +2076,8 @@ and interp_ltac_constr ist gl e = str "offending expression: " ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++ (match result with - VTactic _ -> str "VTactic" | VRTactic _ -> str "VRTactic" - | VFun (il,ul,b) -> + | VFun (_,il,ul,b) -> (str "VFun with body " ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ str "instantiated arguments " ++ fnl() ++ @@ -2074,20 +2091,19 @@ and interp_ltac_constr ist gl e = (match opt_id with Some id -> str (string_of_id id) | None -> str "_") ++ str ", " ++ s) - ul (str "")) + ul (mt())) | VVoid -> str "VVoid" | VInteger _ -> str "VInteger" | VConstr _ -> str "VConstr" | VIntroPattern _ -> str "VIntroPattern" | VConstr_context _ -> str "VConstrr_context" | VRec _ -> str "VRec" - | VList _ -> str "VList")) + | VList _ -> str "VList") ++ str".") (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = - try tactic_of_value (val_interp ist gl tac) gl - with NotTactic -> - errorlabstrm "" (str "Must be a command or must give a tactic value") + try tactic_of_value ist (val_interp ist gl tac) gl + with NotTactic -> errorlabstrm "" (str "Not a tactic.") (* Interprets a primitive tactic *) and interp_atomic ist gl = function @@ -2096,14 +2112,15 @@ and interp_atomic ist gl = function h_intro_patterns (List.map (interp_intro_pattern ist gl) l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) - | TacIntroMove (ido,ido') -> + | TacIntroMove (ido,hto) -> h_intro_move (Option.map (interp_fresh_ident ist gl) ido) - (Option.map (interp_hyp ist gl) 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) -> h_apply a ev (interp_constr_with_bindings ist gl cb) + | TacApply (a,ev,cb) -> + h_apply a ev (List.map (interp_constr_with_bindings ist gl) cb) | TacElim (ev,cb,cbo) -> h_elim ev (interp_constr_with_bindings ist gl cb) (Option.map (interp_constr_with_bindings ist gl) cbo) @@ -2149,20 +2166,16 @@ and interp_atomic ist gl = function (pf_interp_constr_list ist gl lems) (* Derived basic tactics *) - | TacSimpleInduction h -> - h_simple_induction (interp_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids,cls) -> - h_new_induction ev (List.map (interp_induction_arg ist gl) lc) - (Option.map (interp_constr_with_bindings ist gl) cbo) - (interp_intro_pattern ist gl ids) - (Option.map (interp_clause ist gl) cls) - | TacSimpleDestruct h -> - h_simple_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids,cls) -> - h_new_destruct ev (List.map (interp_induction_arg ist gl) c) - (Option.map (interp_constr_with_bindings ist gl) cbo) - (interp_intro_pattern ist gl ids) - (Option.map (interp_clause ist gl) cls) + | TacSimpleInductionDestruct (isrec,h) -> + h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) + | TacInductionDestruct (isrec,ev,l) -> + h_induction_destruct ev isrec + (List.map (fun (lc,cbo,(ipato,ipats),cls) -> + (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), + Option.map (interp_clause ist gl) cls)) l) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2180,7 +2193,7 @@ and interp_atomic ist gl = function | TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l) | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l) | TacMove (dep,id1,id2) -> - h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2) + h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) | TacRename l -> h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, @@ -2222,11 +2235,11 @@ and interp_atomic ist gl = function (Option.map (interp_tactic ist) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) - (interp_intro_pattern ist gl ids) + (Option.map (interp_intro_pattern ist gl) ids) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Inv.inv_clause k - (interp_intro_pattern ist gl ids) + (Option.map (interp_intro_pattern ist gl) ids) (interp_hyp_list ist gl idl) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (InversionUsing (c,idl),hyp) -> @@ -2237,10 +2250,9 @@ and interp_atomic ist gl = function (* For extensions *) | TacExtend (loc,opn,l) -> let tac = lookup_tactic opn in - fun gl -> - let args = List.map (interp_genarg ist gl) l in - abstract_extended_tactic opn args (tac args) gl - | TacAlias (loc,_,l,(_,body)) -> fun gl -> + let args = List.map (interp_genarg ist gl) l in + abstract_extended_tactic opn args (tac args) + | TacAlias (loc,s,l,(_,body)) -> fun gl -> let rec f x = match genarg_tag x with | IntArgType -> VInteger (out_gen globwit_int x) @@ -2250,7 +2262,7 @@ and interp_atomic ist gl = function failwith "pre-identifiers cannot be bound" | IntroPatternArgType -> VIntroPattern - (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) + (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType -> VIntroPattern (IntroIdentifier @@ -2301,14 +2313,12 @@ and interp_atomic ist gl = function | ExtraArgType _ | BindingsArgType | OptArgType _ | PairArgType _ | List0ArgType _ | List1ArgType _ - -> error "This generic type is not supported in alias" + -> error "This generic type is not supported in alias." in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in - let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body) - in - try tactic_of_value v gl - with NotTactic -> user_err_loc (loc,"",str "not a tactic") + let trace = (loc,LtacNotationCall s)::ist.trace in + interp_tactic { ist with lfun=lfun; trace=trace } body gl let make_empty_glob_sign () = { ltacvars = ([],[]); ltacrecvars = []; @@ -2316,20 +2326,20 @@ 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; last_loc=dloc } + interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] } (intern_tactic { ltacvars = (List.map fst lfun, []); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } t) gl let eval_tactic t gls = - interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc } + interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } t gls let interp t = interp_tac_gen [] [] (get_debug()) t let eval_ltac_constr gl t = interp_ltac_constr - { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc } gl + { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl (intern_tactic (make_empty_glob_sign ()) t ) (* Hides interpretation for pretty-print *) @@ -2392,7 +2402,7 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (eq_constr (constr_of_global ref') t') then - ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++ + ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' @@ -2430,10 +2440,10 @@ let subst_match_pattern subst = function | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc) | Term pc -> Term (subst_pattern subst pc) -let rec subst_match_context_hyps subst = function +let rec subst_match_goal_hyps subst = function | Hyp (locs,mp) :: tl -> Hyp (locs,subst_match_pattern subst mp) - :: subst_match_context_hyps subst tl + :: subst_match_goal_hyps subst tl | [] -> [] let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with @@ -2443,7 +2453,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacExact c -> TacExact (subst_rawconstr subst c) | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) - | TacApply (a,ev,cb) -> TacApply (a,ev,subst_raw_with_bindings subst cb) + | TacApply (a,ev,cb) -> + TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, Option.map (subst_raw_with_bindings subst) cbo) @@ -2474,14 +2485,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems) (* Derived basic tactics *) - | TacSimpleInduction h as x -> x - | TacNewInduction (ev,lc,cbo,ids,cls) -> - TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - Option.map (subst_raw_with_bindings subst) cbo, ids, cls) - | TacSimpleDestruct h as x -> x - | TacNewDestruct (ev,c,cbo,ids,cls) -> - TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - Option.map (subst_raw_with_bindings subst) cbo, ids, cls) + | TacSimpleInductionDestruct (isrec,h) as x -> x + | TacInductionDestruct (isrec,ev,l) -> + TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) -> + List.map (subst_induction_arg subst) lc, + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2540,8 +2548,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacLetIn (r,l,u) -> let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in TacLetIn (r,l,subst_tactic subst u) - | TacMatchContext (lz,lr,lmr) -> - TacMatchContext(lz,lr, subst_match_rule subst lmr) + | TacMatchGoal (lz,lr,lmr) -> + TacMatchGoal(lz,lr, subst_match_rule subst lmr) | TacMatch (lz,c,lmr) -> TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr) | TacId _ | TacFail _ as x -> x @@ -2588,7 +2596,7 @@ and subst_match_rule subst = function | (All tc)::tl -> (All (subst_tactic subst tc))::(subst_match_rule subst tl) | (Pat (rl,mp,tc))::tl -> - let hyps = subst_match_context_hyps subst rl in + let hyps = subst_match_goal_hyps subst rl in let pat = subst_match_pattern subst mp in Pat (hyps,pat,subst_tactic subst tc) ::(subst_match_rule subst tl) @@ -2707,12 +2715,12 @@ let print_ltac id = try let kn = Nametab.locate_tactic id in let t = lookup kn in - str "Ltac" ++ spc() ++ pr_qualid id ++ str ":=" ++ spc() ++ + str "Ltac" ++ spc() ++ pr_qualid id ++ str " :=" ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t with Not_found -> errorlabstrm "print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic") + (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") open Libnames @@ -2729,14 +2737,14 @@ let make_absolute_name ident repl = if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is already an Ltac named " ++ pr_reference ident) + str "There is already an Ltac named " ++ pr_reference ident ++ str".") else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_reference ident) + str "Reserved Ltac name " ++ pr_reference ident ++ str".") else id, kn with Not_found -> user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_reference ident) + str "There is no Ltac named " ++ pr_reference ident ++ str".") let rec filter_map f l = let rec aux acc = function @@ -2782,17 +2790,33 @@ let glob_tactic_env l env x = x let interp_redexp env sigma r = - let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); last_loc=dloc } in + let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); trace=[] } in let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in interp_red_expr ist sigma env (intern_red_expr gist r) (***************************************************************************) +(* Embed tactics in raw or glob tactic expr *) + +let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) +let tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist)) + +let tacticOut = function + | TacArg (TacDynamic (_,d)) -> + if (tag d) = "tactic" then + tactic_out d + else + anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") + | ast -> + anomalylabstrm "tacticOut" + (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) + +(***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = Auto.set_extern_interp (fun l -> let l = List.map (fun (id,c) -> (id,VConstr c)) l in - interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); last_loc=dloc}) + interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]}) let _ = Auto.set_extern_intern_tac (fun l -> Flags.with_option strict_check |