diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 1516 |
1 files changed, 818 insertions, 698 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5c891c58..87c88b9d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,14 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *) +(* $Id$ *) open Constrintern open Closure open RedFlags open Declarations open Entries -open Dyn open Libobject open Pattern open Matching @@ -26,6 +25,7 @@ open Names open Nameops open Libnames open Nametab +open Smartlocate open Pfedit open Proof_type open Refiner @@ -46,16 +46,17 @@ open Inductiveops open Syntax_def open Pretyping open Pretyping.Default +open Extrawit open Pcoq let safe_msgnl s = - try msgnl s with e -> - msgnl + try msgnl s with e -> + msgnl (str "bug in the debugger: " ++ str "an exception is raised while printing debug information") let error_syntactic_metavariables_not_allowed loc = - user_err_loc + user_err_loc (loc,"out_ident", str "Syntactic metavariables allowed only in quotations.") @@ -74,14 +75,15 @@ type ltac_type = type value = | VRTactic of (goal list sigma * validation) (* For Match results *) (* Not a true value *) - | VFun of ltac_trace * (identifier*value) list * + | 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 *) (* bound as in "Intro H" but which may be bound *) (* later, as in "tac" in "Intro H; tac" *) - | VConstr of constr (* includes idents known to be bound and references *) + | VConstr of constr_under_binders + (* includes idents known to be bound and references *) | VConstr_context of constr | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr @@ -93,13 +95,13 @@ let catch_error call_trace tac g = | 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 (nrep,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'))) + raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -114,9 +116,6 @@ let check_is_value = function error "Immediate match producing tactics not allowed in local definitions." | _ -> () -(* For tactic_of_value *) -exception NotTactic - (* Gives the constr corresponding to a Constr_context tactic_arg *) let constr_of_VConstr_context = function | VConstr_context c -> c @@ -128,7 +127,10 @@ let rec pr_value env = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) - | VConstr c | VConstr_context c -> + | VConstr c -> + (match env with Some env -> + pr_lconstr_under_binders_env env c | _ -> str "a term") + | VConstr_context c -> (match env with Some env -> pr_lconstr_env env c | _ -> str "a term") | (VRTactic _ | VFun _ | VRec _) -> str "a tactic" | VList [] -> str "an empty list" @@ -136,21 +138,21 @@ let rec pr_value env = function str "a list (first element is " ++ pr_value env a ++ str")" (* Transforms an id into a constr if possible, or fails *) -let constr_of_id env id = +let constr_of_id env id = construct_reference (Environ.named_context env) id (* To embed tactics *) let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = - create "tactic" + Dyn.create "tactic" let ((value_in : value -> Dyn.t), - (value_out : Dyn.t -> value)) = create "value" + (value_out : Dyn.t -> value)) = Dyn.create "value" let valueIn t = TacDynamic (dummy_loc,value_in t) let valueOut = function | TacDynamic (_,d) -> - if (tag d) = "value" then + if (Dyn.tag d) = "value" then value_out d else anomalylabstrm "valueOut" (str "Dynamic tag should be value") @@ -176,11 +178,6 @@ let find_reference env qid = -> VarRef id | _ -> Nametab.locate qid -let error_not_evaluable s = - errorlabstrm "evalref_of_ref" - (str "Cannot coerce" ++ spc () ++ s ++ spc () ++ - str "to an evaluable reference.") - (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty let add_primitive_tactic s tac = @@ -205,8 +202,8 @@ let _ = "eleft", TacLeft(true,NoBindings); "right", TacRight(false,NoBindings); "eright", TacRight(true,NoBindings); - "split", TacSplit(false,false,NoBindings); - "esplit", TacSplit(true,false,NoBindings); + "split", TacSplit(false,false,[NoBindings]); + "esplit", TacSplit(true,false,[NoBindings]); "constructor", TacAnyConstructor (false,None); "econstructor", TacAnyConstructor (true,None); "reflexivity", TacReflexivity; @@ -218,7 +215,7 @@ let _ = "fail", TacFail(ArgArg 0,[]); "fresh", TacArg(TacFreshId []) ] - + let lookup_atomic id = Idmap.find id !atomic_mactab let is_atomic_kn kn = let (_,_,l) = repr_kn kn in @@ -236,9 +233,7 @@ let _ = Summary.declare_summary "tactic-definition" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* Tactics table (TacExtend). *) @@ -246,7 +241,7 @@ let tac_tab = Hashtbl.create 17 let add_tactic s t = if Hashtbl.mem tac_tab s then - errorlabstrm ("Refiner.add_tactic: ") + errorlabstrm ("Refiner.add_tactic: ") (str ("Cannot redeclare tactic "^s^".")); Hashtbl.add tac_tab s t @@ -258,9 +253,9 @@ let overwriting_add_tactic s t = Hashtbl.add tac_tab s t let lookup_tactic s = - try + try Hashtbl.find tac_tab s - with Not_found -> + with Not_found -> errorlabstrm "Refiner.lookup_tactic" (str"The tactic " ++ str s ++ str" is not installed.") (* @@ -279,7 +274,7 @@ type glob_sign = { type interp_genarg_type = (glob_sign -> raw_generic_argument -> glob_generic_argument) * - (interp_sign -> goal sigma -> glob_generic_argument -> + (interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) @@ -287,24 +282,34 @@ let extragenargtab = ref (Gmap.empty : (string,interp_genarg_type) Gmap.t) let add_interp_genarg id f = extragenargtab := Gmap.add id f !extragenargtab -let lookup_genarg id = +let lookup_genarg id = try Gmap.find id !extragenargtab - with Not_found -> failwith ("No interpretation function found for entry "^id) + with Not_found -> + let msg = "No interpretation function found for entry " ^ id in + warning msg; + let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in + add_interp_genarg id f; + f + 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 +let push_trace (loc,ck) = function + | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl + | trl -> (1,loc,ck)::trl + 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) + VFun (push_trace(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 | VFun _ | VRTactic _ as a -> a - | _ -> user_err_loc + | _ -> user_err_loc (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") (*****************) @@ -313,23 +318,23 @@ let coerce_to_tactic loc id = function (* We have identifier <| global_reference <| constr *) -let find_ident id sign = - List.mem id (fst sign.ltacvars) or - List.mem id (ids_of_named_context (Environ.named_context sign.genv)) +let find_ident id ist = + List.mem id (fst ist.ltacvars) or + List.mem id (ids_of_named_context (Environ.named_context ist.genv)) -let find_recvar qid sign = List.assoc qid sign.ltacrecvars +let find_recvar qid ist = List.assoc qid ist.ltacrecvars (* a "var" is a ltac var or a var introduced by an intro tactic *) -let find_var id sign = List.mem id (fst sign.ltacvars) +let find_var id ist = List.mem id (fst ist.ltacvars) (* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *) -let find_ctxvar id sign = List.mem id (snd sign.ltacvars) +let find_ctxvar id ist = List.mem id (snd ist.ltacvars) (* a "ltacvar" is an ltac var (Let-In/Fun/...) *) -let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign) +let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist) -let find_hyp id sign = - List.mem id (ids_of_named_context (Environ.named_context sign.genv)) +let find_hyp id ist = + List.mem id (ids_of_named_context (Environ.named_context ist.genv)) (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *) (* be fresh in which case it is binding later on *) @@ -348,7 +353,7 @@ let vars_of_ist (lfun,_,_,env) = let get_current_context () = try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> + with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) let strict_check = ref false @@ -370,17 +375,7 @@ let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg _ as x -> x -let loc_of_by_notation f = function - | AN c -> f c - | ByNotation (loc,s,_) -> loc - -let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" - -let intern_inductive_or_by_notation = function - | AN r -> Nametab.inductive_of_reference r - | ByNotation (loc,ntn,sc) -> - destIndRef (Notation.interp_notation_as_global_reference loc - (function IndRef ind -> true | _ -> false) ntn sc) +let intern_inductive_or_by_notation = smart_global_inductive let intern_inductive ist = function | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) @@ -388,10 +383,10 @@ let intern_inductive ist = function let intern_global_reference ist = function | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) - | r -> + | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> + with Not_found -> error_global_not_found_loc lqid let intern_ltac_variable ist = function @@ -486,7 +481,9 @@ let rec intern_intro_pattern lf ist = function 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 _) + | loc, IntroFresh id -> + loc, IntroFresh (intern_ident lf ist id) + | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x and intern_or_and_intro_pattern lf ist = @@ -497,22 +494,22 @@ let intern_quantified_hypothesis ist = function | NamedHyp id -> (* Uncomment to disallow "intros until n" in ltac when n is not bound *) NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*)) - + let intern_binding_name ist x = (* We use identifier both for variables and binding names *) - (* Todo: consider the body of the lemma to which the binding refer + (* Todo: consider the body of the lemma to which the binding refer and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in - let c' = - warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c + let c' = + warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c in (c',if !strict_check then None else Some c) -let intern_constr = intern_constr_gen false -let intern_type = intern_constr_gen true +let intern_constr = intern_constr_gen false false +let intern_type = intern_constr_gen false true (* Globalize bindings *) let intern_binding ist (loc,b,c) = @@ -545,38 +542,33 @@ let intern_induction_arg ist = function else ElimOnIdent (loc,id) -let evaluable_of_global_reference = function - | ConstRef c -> EvalConstRef c - | VarRef c -> EvalVarRef c - | r -> error_not_evaluable (pr_global r) - let short_name = function | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) | _ -> None -let interp_global_reference r = +let intern_evaluable_global_reference ist r = let lqid = qualid_of_reference r in - try locate_global_with_alias lqid + try evaluable_of_global_reference ist.genv (locate_global_with_alias lqid) with Not_found -> - match r with - | Ident (loc,id) when not !strict_check -> VarRef id + match r with + | Ident (loc,id) when not !strict_check -> EvalVarRef id | _ -> error_global_not_found_loc lqid -let intern_evaluable_reference_or_by_notation = function - | AN r -> evaluable_of_global_reference (interp_global_reference r) +let intern_evaluable_reference_or_by_notation ist = function + | AN r -> intern_evaluable_global_reference ist r | ByNotation (loc,ntn,sc) -> - evaluable_of_global_reference + evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) -(* Globalizes a reduction expression *) +(* Globalize a reduction expression *) let intern_evaluable ist = function | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) | AN (Ident (_,id)) when (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> ArgArg (EvalVarRef id, None) | r -> - let e = intern_evaluable_reference_or_by_notation r in + let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in ArgArg (e,na) @@ -587,15 +579,31 @@ let intern_flag ist red = let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) +let intern_constr_pattern ist ltacvars pc = + let metas,pat = + Constrintern.intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in + let c = intern_constr_gen true false ist pc in + metas,(c,pat) + +let intern_typed_pattern ist p = + let dummy_pat = PRel 0 in + (* we cannot ensure in non strict mode that the pattern is closed *) + (* keeping a constr_expr copy is too complicated and we want anyway to *) + (* type it, so we remember the pattern as a rawconstr only *) + (intern_constr_gen true false ist p,dummy_pat) + +let intern_typed_pattern_with_occurrences ist (l,p) = + (l,intern_typed_pattern ist p) + let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map (intern_constr ist) l) | Cbv f -> Cbv (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) - | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o) + | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r - + let intern_in_hyp_as ist lf (id,ipat) = (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat) @@ -616,15 +624,15 @@ let intern_hyp_location ist (((b,occs),id),hl) = (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl) (* Reads a pattern *) -let intern_pattern sigma env ?(as_type=false) lfun = function +let intern_pattern ist ?(as_type=false) lfun = function | Subterm (b,ido,pc) -> let ltacvars = (lfun,[]) in - let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in - ido, metas, Subterm (b,ido,pat) + let (metas,pc) = intern_constr_pattern ist ltacvars pc in + ido, metas, Subterm (b,ido,pc) | Term pc -> let ltacvars = (lfun,[]) in - let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in - None, metas, Term pat + let (metas,pc) = intern_constr_pattern ist ltacvars pc in + None, metas, Term pc let intern_constr_may_eval ist = function | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c) @@ -640,10 +648,10 @@ let declare_xml_printer f = print_xml_term := f 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 + | VConstr ([],c) -> !print_xml_term ch env sigma c | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ - | VIntroPattern _ | VRec _ | VList _ -> - error "Only externing of terms is implemented." + | VIntroPattern _ | VRec _ | VList _ | VConstr _ -> + error "Only externing of closed terms is implemented." let extern_request ch req gl la = output_string ch "<REQUEST req=\""; output_string ch req; @@ -651,24 +659,33 @@ let extern_request ch req gl la = List.iter (pf_apply (extern_tacarg ch) gl) la; output_string ch "</REQUEST>\n" +let value_of_ident id = VIntroPattern (IntroIdentifier id) + +let extend_values_with_bindings (ln,lm) lfun = + let lnames = List.map (fun (id,id') ->(id,value_of_ident id')) ln in + let lmatch = List.map (fun (id,(ids,c)) -> (id,VConstr (ids,c))) lm in + (* For compatibility, bound variables are visible only if no other + binding of the same name exists *) + lmatch@lfun@lnames + (* Reads the hypotheses of a "match goal" rule *) -let rec intern_match_goal_hyps sigma env lfun = function +let rec intern_match_goal_hyps ist 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_goal_hyps sigma env lfun tl in + let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in + let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in let lfun' = name_cons na (Option.List.cons ido lfun) in lfun', metas1@metas2, Hyp (locna,pat)::hyps | (Def ((_,na) as locna,mv,mp))::tl -> - let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in - let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in - let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in + let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in + let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in + let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps | [] -> lfun, [], [] (* Utilities *) let extract_let_names lrc = - List.fold_right + List.fold_right (fun ((loc,name),_) l -> if List.mem name l then user_err_loc @@ -684,7 +701,7 @@ let clause_app f = function (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) let rec intern_atomic lf ist x = - match (x:raw_atomic_tactic_expr) with + match (x:raw_atomic_tactic_expr) with (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) @@ -717,7 +734,7 @@ let rec intern_atomic lf ist x = | TacAssert (otac,ipat,c) -> TacAssert (Option.map (intern_tactic ist) otac, Option.map (intern_intro_pattern lf ist) ipat, - intern_constr_gen (otac<>None) ist c) + intern_constr_gen false (otac<>None) ist c) | TacGeneralize cl -> TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, @@ -744,13 +761,13 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | 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) -> + | TacInductionDestruct (ev,isrec,(l,cls)) -> + TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) -> (List.map (intern_induction_arg ist) lc, Option.map (intern_constr_with_bindings ist) cbo, (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) + Option.map (intern_intro_pattern lf ist) ipats))) l, + Option.map (clause_app (intern_hyp_location ist)) cls)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in @@ -767,40 +784,43 @@ let rec intern_atomic lf ist x = | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) | TacMove (dep,id1,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, + | TacRename l -> + TacRename (List.map (fun (id1,id2) -> + intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2) l) | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l) - + (* Constructors *) | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl) | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl) - | TacSplit (ev,b,bl) -> TacSplit (ev,b,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) | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) - | TacChange (occl,c,cl) -> - TacChange (Option.map (intern_constr_with_occurrences ist) occl, - (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) & + | TacChange (None,c,cl) -> + TacChange (None, + (if (cl.onhyps = None or cl.onhyps = Some []) & (cl.concl_occs = all_occurrences_expr or cl.concl_occs = no_occurrences_expr) then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) + | TacChange (Some p,c,cl) -> + TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, + clause_app (intern_hyp_location ist) cl) (* Equivalence relations *) | TacReflexivity -> TacReflexivity - | TacSymmetry idopt -> + | TacSymmetry idopt -> TacSymmetry (clause_app (intern_hyp_location ist) idopt) - | TacTransitivity c -> TacTransitivity (intern_constr ist c) + | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c) (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - TacRewrite - (ev, + | TacRewrite (ev,l,cl,by) -> + TacRewrite + (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) @@ -827,7 +847,7 @@ and intern_tactic_seq ist = function | TacLetIn (isrec,l,u) -> 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) -> + 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) | TacMatchGoal (lz,lr,lmr) -> @@ -835,7 +855,7 @@ and intern_tactic_seq ist = function | 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) - | TacFail (n,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) @@ -854,7 +874,7 @@ and intern_tactic_seq ist = function 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) - | TacDo (n,tac) -> + | TacDo (n,tac) -> ist.ltacvars, TacDo (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) @@ -866,7 +886,7 @@ and intern_tactic_seq ist = function | TacComplete tac -> ist.ltacvars, TacComplete (intern_tactic ist tac) | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a) -and intern_tactic_fun ist (var,body) = +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) @@ -874,7 +894,7 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict ist = function | TacVoid -> TacVoid | Reference r -> intern_non_tactic_reference strict ist r - | IntroPattern ipat -> + | IntroPattern ipat -> let lf = ref([],[]) in (*How to know what names the intropattern binds?*) IntroPattern (intern_intro_pattern lf ist ipat) | Integer n -> Integer n @@ -891,12 +911,12 @@ and intern_tacarg strict ist = function TacCall (loc, intern_applied_tactic_reference ist f, List.map (intern_tacarg !strict_check ist) l) - | TacExternal (loc,com,req,la) -> + | TacExternal (loc,com,req,la) -> TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | Tacexp t -> Tacexp (intern_tactic ist t) | TacDynamic(loc,t) as x -> - (match tag t with + (match Dyn.tag t with | "tactic" | "value" | "constr" -> x | s -> anomaly_loc (loc, "", str "Unknown dynamic: <" ++ str s ++ str ">")) @@ -907,8 +927,8 @@ 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_goal_hyps sigma env lfun rl in - let ido,metas2,pat = intern_pattern sigma env lfun mp 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) @@ -932,7 +952,7 @@ and intern_genarg ist x = (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x)) | IdentArgType b -> let lf = ref ([],[]) in - in_gen (globwit_ident_gen b) + in_gen (globwit_ident_gen b) (intern_ident lf ist (out_gen (rawwit_ident_gen b) x)) | VarArgType -> in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x)) @@ -943,7 +963,7 @@ and intern_genarg ist x = | ConstrArgType -> in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x)) | ConstrMayEvalArgType -> - in_gen globwit_constr_may_eval + in_gen globwit_constr_may_eval (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x)) | QuantHypArgType -> in_gen globwit_quant_hyp @@ -965,7 +985,7 @@ and intern_genarg ist x = | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x | ExtraArgType s -> match tactic_genarg_level s with - | Some n -> + | Some n -> (* Special treatment of tactic arguments *) in_gen (globwit_tactic n) (intern_tactic ist (out_gen (rawwit_tactic n) x)) @@ -977,159 +997,8 @@ and intern_genarg ist x = (***************************************************************************) (* Evaluation/interpretation *) -(* Associates variables with values and gives the remaining variables and - values *) -let head_with_value (lvar,lval) = - let rec head_with_value_rec lacc = function - | ([],[]) -> (lacc,[],[]) - | (vr::tvr,ve::tve) -> - (match vr with - | None -> head_with_value_rec lacc (tvr,tve) - | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) - | (vr,[]) -> (lacc,vr,[]) - | ([],ve) -> (lacc,[],ve) - in - head_with_value_rec [] (lvar,lval) - -(* Gives a context couple if there is a context identifier *) -let give_context ctxt = function - | None -> [] - | Some id -> [id,VConstr_context ctxt] - -(* Reads a pattern by substituting vars of lfun *) -let eval_pattern lfun c = - let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr c))) lfun in - instantiate_pattern lvar c - -let read_pattern lfun = function - | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc) - | Term pc -> Term (eval_pattern lfun pc) - -let value_of_ident id = VIntroPattern (IntroIdentifier id) - -let extend_values_with_bindings (ln,lm) lfun = - let lnames = List.map (fun (id,id') ->(id,value_of_ident id')) ln in - let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lm in - (* For compatibility, bound variables are visible only if no other - binding of the same name exists *) - lmatch@lfun@lnames - -(* 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_goal_hyps", - strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ - " used twice in the same pattern.")) - else id::l - -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_goal_hyps lfun lidh' tl) - | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in - Def (locna,read_pattern lfun mv, read_pattern lfun mp):: - (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_goal_hyps lfun [] rl, read_pattern lfun mp,tc) - :: read_match_rule lfun tl - | [] -> [] - -(* For Match Context and Match *) -exception Not_coherent_metas -exception Eval_fail of std_ppcmds - -let is_match_catchable = function - | PatternMatchingFailure | Eval_fail _ -> true - | e -> Logic.catchable_exception e - -(* Verifies if the matched list is coherent with respect to lcm *) -(* While non-linear matching is modulo eq_constr in matches, merge of *) -(* different instances of the same metavars is here modulo conversion... *) -let verify_metas_coherence gl (ln1,lcm) (ln,lm) = - let rec aux = function - | (num,csr)::tl -> - if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then - (num,csr)::aux tl - else - raise Not_coherent_metas - | [] -> lcm in - (ln@ln1,aux lm) - -(* Tries to match one hypothesis pattern with a list of hypotheses *) -let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = - let get_id_couple id = function - | Name idpat -> [idpat,VConstr (mkVar id)] - | Anonymous -> [] in - let match_pat lmatch hyp pat = - match pat with - | Term t -> - let lmeta = extended_matches t hyp in - (try - let lmeta = verify_metas_coherence gl lmatch lmeta in - ([],lmeta,(fun () -> raise PatternMatchingFailure)) - with - | Not_coherent_metas -> raise PatternMatchingFailure); - | Subterm (b,ic,t) -> - let rec match_next_pattern find_next () = - let (lmeta,ctxt,find_next') = find_next () in - try - let lmeta = verify_metas_coherence gl lmatch lmeta in - (give_context ctxt ic,lmeta,match_next_pattern find_next') - with - | Not_coherent_metas -> match_next_pattern find_next' () in - match_next_pattern(fun () -> match_subterm_gen b t hyp) () in - let rec apply_one_mhyp_context_rec = function - | (id,b,hyp as hd)::tl -> - (match patv with - | None -> - let rec match_next_pattern find_next () = - try - let (ids, lmeta, find_next') = find_next () in - (get_id_couple id hypname@ids, lmeta, hd, - match_next_pattern find_next') - with - | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in - match_next_pattern (fun () -> - let hyp = if b<>None then refresh_universes_strict hyp else hyp in - match_pat lmatch hyp pat) () - | Some patv -> - match b with - | Some body -> - let rec match_next_pattern_in_body next_in_body () = - try - let (ids,lmeta,next_in_body') = next_in_body() in - let rec match_next_pattern_in_typ next_in_typ () = - try - let (ids',lmeta',next_in_typ') = next_in_typ() in - (get_id_couple id hypname@ids@ids', lmeta', hd, - match_next_pattern_in_typ next_in_typ') - with - | PatternMatchingFailure -> - match_next_pattern_in_body next_in_body' () in - match_next_pattern_in_typ - (fun () -> - let hyp = refresh_universes_strict hyp in - match_pat lmeta hyp pat) () - with PatternMatchingFailure -> apply_one_mhyp_context_rec tl - in - match_next_pattern_in_body - (fun () -> match_pat lmatch body patv) () - | None -> apply_one_mhyp_context_rec tl) - | [] -> - db_hyp_pattern_failure ist.debug env (hypname,pat); - raise PatternMatchingFailure - in - apply_one_mhyp_context_rec lhyps - let constr_to_id loc = function - | VConstr c when isVar c -> destVar c + | VConstr ([],c) when isVar c -> destVar c | _ -> invalid_arg_loc (loc, "Not an identifier") let constr_to_qid loc c = @@ -1158,12 +1027,12 @@ let debugging_exception_step ist signal_anomaly e pp = let explain_exc = if signal_anomaly then explain_logic_error else explain_logic_error_no_anomaly in - debugging_step ist (fun () -> + debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e) let error_ltac_variable loc id env v s = - user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ - strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") exception CannotCoerceTo of string @@ -1180,27 +1049,28 @@ let interp_ltac_var coerce ist env locid = (* Interprets an identifier which must be fresh *) let coerce_to_ident fresh env = function | VIntroPattern (IntroIdentifier id) -> id - | VConstr c when isVar c & not (fresh & is_variable env (destVar c)) -> + | VConstr ([],c) when isVar c & not (fresh & is_variable env (destVar c)) -> (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *) destVar c | v -> raise (CannotCoerceTo "a fresh identifier") -let interp_ident_gen fresh ist gl id = - let env = pf_env gl in +let interp_ident_gen fresh ist env id = try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id) with Not_found -> id -let interp_ident = interp_ident_gen false +let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true +let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) +let pf_interp_fresh_ident id gl = interp_ident_gen true id (pf_env gl) (* Interprets an optional identifier which must be fresh *) -let interp_fresh_name ist gl = function +let interp_fresh_name ist env = function | Anonymous -> Anonymous - | Name id -> Name (interp_fresh_ident ist gl id) + | Name id -> Name (interp_fresh_ident ist env id) let coerce_to_intro_pattern env = function | VIntroPattern ipat -> ipat - | VConstr c when isVar c -> + | VConstr ([],c) when isVar c -> (* This happens e.g. in definitions like "Tac H = clear H; intro H" *) (* but also in "destruct H as (H,H')" *) IntroIdentifier (destVar c) @@ -1237,7 +1107,7 @@ let int_or_var_list_of_VList = function | _ -> raise Not_found let interp_int_or_var_as_list ist = function - | ArgVar (_,id as locid) -> + | ArgVar (_,id as locid) -> (try int_or_var_list_of_VList (List.assoc id ist.lfun) with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) | ArgArg n as x -> [x] @@ -1247,11 +1117,16 @@ let interp_int_or_var_list ist l = let constr_of_value env = function | VConstr csr -> csr - | VIntroPattern (IntroIdentifier id) -> constr_of_id env id + | VIntroPattern (IntroIdentifier id) -> ([],constr_of_id env id) | _ -> raise Not_found +let closed_constr_of_value env v = + let ids,c = constr_of_value env v in + if ids <> [] then raise Not_found; + c + let coerce_to_hyp env = function - | VConstr c when isVar c -> destVar c + | VConstr ([],c) when isVar c -> destVar c | VIntroPattern (IntroIdentifier id) when is_variable env id -> id | _ -> raise (CannotCoerceTo "a variable") @@ -1260,7 +1135,7 @@ let interp_hyp ist gl (loc,id as locid) = let env = pf_env gl in (* Look first in lfun for a value coercible to a variable *) try try_interp_ltac_var (coerce_to_hyp env) ist (Some env) locid - with Not_found -> + 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.") @@ -1294,19 +1169,19 @@ let interp_move_location ist gl = function (* Interprets a qualified name *) let coerce_to_reference env v = try match v with - | VConstr c -> global_of_constr c (* may raise Not_found *) + | VConstr ([],c) -> global_of_constr c (* may raise Not_found *) | _ -> raise Not_found with Not_found -> raise (CannotCoerceTo "a reference") let interp_reference ist env = function | ArgArg (_,r) -> r - | ArgVar locid -> + | ArgVar locid -> interp_ltac_var (coerce_to_reference env) ist (Some env) locid let pf_interp_reference ist gl = interp_reference ist (pf_env gl) let coerce_to_inductive = function - | VConstr c when isInd c -> destInd c + | VConstr ([],c) when isInd c -> destInd c | _ -> raise (CannotCoerceTo "an inductive type") let interp_inductive ist = function @@ -1315,9 +1190,9 @@ let interp_inductive ist = function let coerce_to_evaluable_ref env v = let ev = match v with - | VConstr c when isConst c -> EvalConstRef (destConst c) - | VConstr c when isVar c -> EvalVarRef (destVar c) - | VIntroPattern (IntroIdentifier id) when List.mem id (ids_of_context env) + | VConstr ([],c) when isConst c -> EvalConstRef (destConst c) + | VConstr ([],c) when isVar c -> EvalVarRef (destVar c) + | VIntroPattern (IntroIdentifier id) when List.mem id (ids_of_context env) -> EvalVarRef id | _ -> raise (CannotCoerceTo "an evaluable reference") in @@ -1331,13 +1206,13 @@ let interp_evaluable ist env = function (* Maybe [id] has been introduced by Intro-like tactics *) (try match Environ.lookup_named id env with | (_,Some _,_) -> EvalVarRef id - | _ -> error_not_evaluable (pr_id id) + | _ -> error_not_evaluable (VarRef id) with Not_found -> match r with | EvalConstRef _ -> r | _ -> Pretype_errors.error_var_not_found_loc loc id) | ArgArg (r,None) -> r - | ArgVar locid -> + | ArgVar locid -> interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid (* Interprets an hypothesis name *) @@ -1354,25 +1229,26 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } = (* Interpretation of constructions *) (* Extract the constr list from lfun *) -let rec constr_list_aux env = function - | (id,v)::tl -> - let (l1,l2) = constr_list_aux env tl in +let extract_ltac_constr_values ist env = + let rec aux = function + | (id,v)::tl -> + let (l1,l2) = aux tl in (try ((id,constr_of_value env v)::l1,l2) - with Not_found -> + with Not_found -> let ido = match v with | VIntroPattern (IntroIdentifier id0) -> Some id0 | _ -> None in (l1,(id,ido)::l2)) - | [] -> ([],[]) - -let constr_list ist env = constr_list_aux env ist.lfun + | [] -> ([],[]) in + aux ist.lfun (* Extract the identifier list from lfun: join all branches (what to do else?)*) let rec intropattern_ids (loc,pat) = match pat with | IntroIdentifier id -> [id] - | IntroOrAndPattern ll -> + | IntroOrAndPattern ll -> List.flatten (List.map intropattern_ids (List.flatten ll)) - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> [] + | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ + | IntroForthcoming _ -> [] let rec extract_ids ids = function | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> @@ -1382,33 +1258,21 @@ let rec extract_ids ids = function let default_fresh_id = id_of_string "H" -let interp_fresh_id ist gl l = +let interp_fresh_id ist env l = let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in - let id = - if l = [] then default_fresh_id + let id = + if l = [] then default_fresh_id else let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l) in + | ArgVar (_,id) -> string_of_id (interp_ident ist env id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in id_of_string s in - Tactics.fresh_id avoid id gl - -(* To retype a list of key*constr with undefined key *) -let retype_list sigma env lst = - List.fold_right (fun (x,csr) a -> - try (x,Retyping.get_judgment_of env sigma csr)::a with - | Anomaly _ -> a) lst [] + Tactics.fresh_id_in_env avoid id env -let extract_ltac_vars_data ist sigma env = - let (ltacvars,_ as vars) = constr_list ist env in - vars, retype_list sigma env ltacvars - -let extract_ltac_vars ist sigma env = - let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in - typs,unbndltacvars +let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl) let implicit_tactic = ref None @@ -1416,11 +1280,11 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac open Evd -let solvable_by_tactic env evi (ev,args) src = +let solvable_by_tactic env evi (ev,args) src = match (!implicit_tactic, src) with | Some tac, (ImplicitArg _ | QuestionMark _) - when - Environ.named_context_of_val evi.evar_hyps = + when + Environ.named_context_of_val evi.evar_hyps = Environ.named_context env -> let id = id_of_string "H" in start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl @@ -1428,35 +1292,42 @@ let solvable_by_tactic env evi (ev,args) src = begin try by (tclCOMPLETE tac); - let _,(const,_,_,_) = cook_proof ignore in + let _,(const,_,_,_) = cook_proof ignore in delete_current_proof (); const.const_entry_body - with e when Logic.catchable_exception e -> + with e when Logic.catchable_exception e -> delete_current_proof(); raise Exit end | _ -> raise Exit -let solve_remaining_evars env initial_sigma evd c = - let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in +let solve_remaining_evars fail_evar use_classes env initial_sigma evd c = + let evdref = + if use_classes then ref (Typeclasses.resolve_typeclasses ~fail:true env evd) + else ref evd in let rec proc_rec c = - match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with + let c = Reductionops.whd_evar !evdref c in + match kind_of_term c with | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) -> let (loc,src) = evar_source ev !evdref in - let sigma = evars_of !evdref in + let sigma = !evdref in let evi = Evd.find sigma ev in - (try + (try let c = solvable_by_tactic env evi k src in - evdref := Evd.evar_define ev c !evdref; + evdref := Evd.define ev c !evdref; c with Exit -> - Pretype_errors.error_unsolvable_implicit loc env sigma evi src None) - | _ -> map_constr proc_rec c + if fail_evar then + Pretype_errors.error_unsolvable_implicit loc env sigma evi src None + else + c) + | _ -> map_constr proc_rec c in - proc_rec (Evarutil.nf_isevar !evdref c) + let c = proc_rec c in + (* Side-effect *) + !evdref,c -let interp_gen kind ist sigma env (c,ce) = - let (ltacvars,unbndltacvars as vars),typs = - extract_ltac_vars_data ist sigma env in +let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) = + let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in let c = match ce with | None -> c (* If at toplevel (ce<>None), the error can be due to an incorrect @@ -1464,100 +1335,78 @@ let interp_gen kind ist sigma env (c,ce) = intros/lettac/inversion hypothesis names *) | Some c -> let ltacdata = (List.map fst ltacvars,unbndltacvars) in - intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in - let trace = (dloc,LtacConstrInterp (c,vars))::ist.trace in - catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c + intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c + in + let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in + let evd,c = + catch_error trace (understand_ltac expand_evar sigma env vars kind) c in + let evd,c = + if expand_evar then + solve_remaining_evars fail_evar use_classes env sigma evd c + else + evd,c in + db_constr ist.debug env c; + (evd,c) -(* Interprets a constr and solve remaining evars with default tactic *) -let interp_econstr kind ist sigma env cc = - let evars,c = interp_gen kind ist sigma env cc in - let csr = solve_remaining_evars env sigma evars c in - db_constr ist.debug env csr; - csr +(* Interprets a constr; expects evars to be solved *) +let interp_constr_gen kind ist env sigma c = + snd (interp_gen kind ist false true true true env sigma c) -(* Interprets an open constr *) -let interp_open_constr ccl ist sigma env cc = - let evd,c = interp_gen (OfType ccl) ist sigma env cc in - (evars_of evd,c) +let interp_constr = interp_constr_gen (OfType None) + +let interp_type = interp_constr_gen IsType -let interp_open_type ccl ist sigma env cc = - let evd,c = interp_gen IsType ist sigma env cc in - (evars_of evd,c) +(* Interprets an open constr *) +let interp_open_constr_gen kind ist = + interp_gen kind ist false true false false -let interp_constr = interp_econstr (OfType None) +let interp_open_constr ccl = + interp_open_constr_gen (OfType ccl) -let interp_type = interp_econstr IsType +let interp_typed_pattern ist env sigma (c,_) = + let sigma, c = + interp_gen (OfType None) ist true false false false env sigma c in + pattern_of_constr sigma c (* Interprets a constr expression casted by the current goal *) -let pf_interp_casted_constr ist gl cc = - interp_econstr (OfType (Some (pf_concl gl))) ist (project gl) (pf_env gl) cc - -(* Interprets an open constr expression *) -let pf_interp_open_constr casted ist gl cc = - let cl = if casted then Some (pf_concl gl) else None in - interp_open_constr cl ist (project gl) (pf_env gl) cc +let pf_interp_casted_constr ist gl c = + interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c (* Interprets a constr expression *) let pf_interp_constr ist gl = - interp_constr ist (project gl) (pf_env gl) + interp_constr ist (pf_env gl) (project gl) let constr_list_of_VList env = function - | VList l -> List.map (constr_of_value env) l + | VList l -> List.map (closed_constr_of_value env) l | _ -> raise Not_found -let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l = - let env = pf_env gl in - let try_expand_ltac_var x = +let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = + let try_expand_ltac_var sigma x = try match dest_fun x with - | RVar (_,id), _ -> - List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) + | RVar (_,id), _ -> + sigma, + List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) | _ -> - raise Not_found + raise Not_found with Not_found -> (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*) - [interp_fun ist gl x] in - List.flatten (List.map try_expand_ltac_var l) + let sigma, c = interp_fun ist env sigma x in + sigma, [c] in + let sigma, l = list_fold_map try_expand_ltac_var sigma l in + sigma, List.flatten l -let pf_interp_constr_list = - pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (fun ist gl -> interp_constr ist (project gl) (pf_env gl)) - -(* -let pf_interp_constr_list_as_list ist gl (c,_ as x) = - match c with - | RVar (_,id) -> - (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun) - with Not_found -> []) - | _ -> [interp_constr ist (project gl) (pf_env gl) x] - -let pf_interp_constr_list ist gl l = - List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l) -*) +let interp_constr_list ist env sigma c = + snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c) let inj_open c = (Evd.empty,c) -let pf_interp_open_constr_list = - pf_interp_constr_in_compound_list inj_open (fun x -> x) - (fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl)) - -(* -let pf_interp_open_constr_list_as_list ist gl (c,_ as x) = - match c with - | RVar (_,id) -> - (try List.map inj_open - (constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)) - with Not_found -> - [interp_open_constr None ist (project gl) (pf_env gl) x]) - | _ -> - [interp_open_constr None ist (project gl) (pf_env gl) x] - -let pf_interp_open_constr_list ist gl l = - List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l) -*) +let interp_open_constr_list = + interp_constr_in_compound_list (fun x -> x) (fun x -> x) + (interp_open_constr None) (* Interprets a type expression *) let pf_interp_type ist gl = - interp_type ist (project gl) (pf_env gl) + interp_type ist (pf_env gl) (project gl) (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = @@ -1566,28 +1415,34 @@ let interp_unfold ist env (occs,qid) = let interp_flag ist env red = { red with rConst = List.map (interp_evaluable ist env) red.rConst } -let interp_pattern ist sigma env (occs,c) = +let interp_constr_with_occurrences ist sigma env (occs,c) = (interp_occurrences ist occs, interp_constr ist sigma env c) -let pf_interp_constr_with_occurrences ist gl = - interp_pattern ist (project gl) (pf_env gl) +let interp_typed_pattern_with_occurrences ist env sigma (occs,c) = + let sign,p = interp_typed_pattern ist env sigma c in + sign, (interp_occurrences ist occs, p) -let pf_interp_constr_with_occurrences_and_name_as_list = - pf_interp_constr_in_compound_list +let interp_closed_typed_pattern_with_occurrences ist env sigma occl = + snd (interp_typed_pattern_with_occurrences ist env sigma occl) + +let interp_constr_with_occurrences_and_name_as_list = + interp_constr_in_compound_list (fun c -> ((all_occurrences_expr,c),Anonymous)) - (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c + (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c | _ -> raise Not_found) - (fun ist gl (occ_c,na) -> - (interp_pattern ist (project gl) (pf_env gl) occ_c, - interp_fresh_name ist gl na)) + (fun ist env sigma (occ_c,na) -> + sigma, (interp_constr_with_occurrences ist env sigma occ_c, + interp_fresh_name ist env na)) let interp_red_expr ist sigma env = function | Unfold l -> Unfold (List.map (interp_unfold ist env) l) - | Fold l -> Fold (List.map (interp_constr ist sigma env) l) + | Fold l -> Fold (List.map (interp_constr ist env sigma) l) | Cbv f -> Cbv (interp_flag ist env f) | Lazy f -> Lazy (interp_flag ist env f) - | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) - | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o) + | Pattern l -> + Pattern (List.map (interp_constr_with_occurrences ist env sigma) l) + | Simpl o -> + Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -1606,17 +1461,17 @@ let interp_may_eval f ist gl = function user_err_loc (loc, "interp_may_eval", str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) - | ConstrTerm c -> - try + | ConstrTerm c -> + try f ist gl c with e -> debugging_exception_step ist false e (fun () -> str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c)); - raise e + raise e (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist gl c = - let csr = + let csr = try interp_may_eval pf_interp_constr ist gl c with e -> @@ -1628,48 +1483,56 @@ let interp_constr_may_eval ist gl c = csr end -let inj_may_eval = function - | ConstrTerm c -> ConstrTerm (inj_open c) - | ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c) - | ConstrContext (id,c) -> ConstrContext (id,inj_open c) - | ConstrTypeOf c -> ConstrTypeOf (inj_open c) - -let message_of_value = function +let rec message_of_value gl = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) - | VConstr_context c | VConstr c -> pr_constr c + | VConstr_context c -> pr_constr_env (pf_env gl) c + | VConstr c -> pr_constr_under_binders_env (pf_env gl) c | VRec _ | VRTactic _ | VFun _ -> str "<tactic>" - | VList _ -> str "<list>" + | VList l -> prlist_with_sep spc (message_of_value gl) l -let rec interp_message_token ist = function +let rec interp_message_token ist gl = 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 - message_of_value v + message_of_value gl v -let rec interp_message_nl ist = function +let rec interp_message_nl ist gl = function | [] -> mt() - | l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl() + | l -> prlist_with_sep spc (interp_message_token ist gl) l ++ fnl() -let interp_message ist l = - (* Force evaluation of interp_message_token so that potential errors +let interp_message ist gl 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) + prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist gl) l) + +let intro_pattern_list_of_Vlist loc env = function + | VList l -> List.map (fun a -> loc,coerce_to_intro_pattern env a) l + | _ -> raise Not_found 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 _) + | loc, IntroFresh id -> + loc, IntroFresh (interp_fresh_ident ist (pf_env gl) id) + | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x and interp_or_and_intro_pattern ist gl = - List.map (List.map (interp_intro_pattern ist gl)) + List.map (interp_intro_pattern_list_as_list ist gl) + +and interp_intro_pattern_list_as_list ist gl = function + | [loc,IntroIdentifier id] as l -> + (try intro_pattern_list_of_Vlist loc (pf_env gl) (List.assoc id ist.lfun) + with Not_found | CannotCoerceTo _ -> + List.map (interp_intro_pattern ist gl) l) + | l -> List.map (interp_intro_pattern ist gl) l let interp_in_hyp_as ist gl (id,ipat) = (interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat) @@ -1700,56 +1563,249 @@ let interp_binding_name ist = function (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env = function | VInteger n -> AnonHyp n - | v -> + | v -> try NamedHyp (coerce_to_hyp env v) - with CannotCoerceTo _ -> + with CannotCoerceTo _ -> raise (CannotCoerceTo "a declared or quantified hypothesis") let interp_declared_or_quantified_hypothesis ist gl = function | AnonHyp n -> AnonHyp n | NamedHyp id -> let env = pf_env gl in - try try_interp_ltac_var + try try_interp_ltac_var (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) with Not_found -> NamedHyp id -let interp_binding ist gl (loc,b,c) = - (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c) - -let interp_bindings ist gl = function -| NoBindings -> NoBindings -| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l) -| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l) - -let interp_constr_with_bindings ist gl (c,bl) = - (pf_interp_constr ist gl c, interp_bindings ist gl bl) - -let interp_open_constr_with_bindings ist gl (c,bl) = - (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl) - -let interp_induction_arg ist gl = function - | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c) - | ElimOnAnonHyp n as x -> x +let interp_binding ist env sigma (loc,b,c) = + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (loc,interp_binding_name ist b,c) + +let interp_bindings ist env sigma = function +| NoBindings -> + sigma, NoBindings +| ImplicitBindings l -> + let sigma, l = interp_open_constr_list ist env sigma l in + sigma, ImplicitBindings l +| ExplicitBindings l -> + let sigma, l = list_fold_map (interp_binding ist env) sigma l in + sigma, ExplicitBindings l + +let interp_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c,bl) + +let interp_open_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c, bl) + +let loc_of_bindings = function +| NoBindings -> dummy_loc +| ImplicitBindings l -> loc_of_rawconstr (fst (list_last l)) +| ExplicitBindings l -> pi1 (list_last l) + +let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = + let loc1 = loc_of_rawconstr c in + let loc2 = loc_of_bindings bl in + let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + sigma, (loc,cb) + +let interp_induction_arg ist gl sigma arg = + let env = pf_env gl in + match arg with + | ElimOnConstr c -> + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, ElimOnConstr c + | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try - match List.assoc id ist.lfun with + sigma, + match List.assoc id ist.lfun with | VInteger n -> ElimOnAnonHyp n | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id) - | VConstr c -> ElimOnConstr (c,NoBindings) + | VConstr ([],c) -> ElimOnConstr (c,NoBindings) | _ -> user_err_loc (loc,"", strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") with Not_found -> (* Interactive mode *) - if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr - (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), - NoBindings) + if Tactics.is_quantified_hypothesis id gl then + sigma, ElimOnIdent (loc,id) + else + let c = interp_constr ist env sigma (RVar (loc,id),Some (CRef (Ident (loc,id)))) in + sigma, ElimOnConstr (c,NoBindings) + +(* Associates variables with values and gives the remaining variables and + values *) +let head_with_value (lvar,lval) = + let rec head_with_value_rec lacc = function + | ([],[]) -> (lacc,[],[]) + | (vr::tvr,ve::tve) -> + (match vr with + | None -> head_with_value_rec lacc (tvr,tve) + | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) + | (vr,[]) -> (lacc,vr,[]) + | ([],ve) -> (lacc,[],ve) + in + head_with_value_rec [] (lvar,lval) + +(* Gives a context couple if there is a context identifier *) +let give_context ctxt = function + | None -> [] + | Some id -> [id,VConstr_context ctxt] + +(* Reads a pattern by substituting vars of lfun *) +let use_types = false -let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c) -let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c)) +let eval_pattern lfun ist env sigma (_,pat as c) = + if use_types then + snd (interp_typed_pattern ist env sigma c) + else + instantiate_pattern sigma lfun pat + +let read_pattern lfun ist env sigma = function + | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Term c -> Term (eval_pattern lfun ist env sigma c) + +(* 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_goal_hyps", + strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ + " used twice in the same pattern.")) + else id::l + +let rec read_match_goal_hyps lfun ist env sigma 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 ist env sigma mp):: + (read_match_goal_hyps lfun ist env sigma lidh' tl) + | (Def ((loc,na) as locna,mv,mp))::tl -> + let lidh' = name_fold cons_and_check_name na lidh in + Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: + (read_match_goal_hyps lfun ist env sigma lidh' tl) + | [] -> [] + +(* Reads the rules of a Match Context or a Match *) +let rec read_match_rule lfun ist env sigma = function + | (All tc)::tl -> (All tc)::(read_match_rule lfun ist env sigma tl) + | (Pat (rl,mp,tc))::tl -> + Pat (read_match_goal_hyps lfun ist env sigma [] rl, read_pattern lfun ist env sigma mp,tc) + :: read_match_rule lfun ist env sigma tl + | [] -> [] + +(* For Match Context and Match *) +exception Not_coherent_metas +exception Eval_fail of std_ppcmds + +let is_match_catchable = function + | PatternMatchingFailure | Eval_fail _ -> true + | e -> Logic.catchable_exception e + +let equal_instances gl (ctx',c') (ctx,c) = + (* How to compare instances? Do we want the terms to be convertible? + unifiable? Do we want the universe levels to be relevant? + (historically, conv_x is used) *) + ctx = ctx' & pf_conv_x gl c' c + +(* Verifies if the matched list is coherent with respect to lcm *) +(* While non-linear matching is modulo eq_constr in matches, merge of *) +(* different instances of the same metavars is here modulo conversion... *) +let verify_metas_coherence gl (ln1,lcm) (ln,lm) = + let rec aux = function + | (id,c as x)::tl -> + if List.for_all (fun (id',c') -> id'<>id or equal_instances gl c' c) lcm + then + x :: aux tl + else + raise Not_coherent_metas + | [] -> lcm in + (ln@ln1,aux lm) + +let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc) + +(* Tries to match one hypothesis pattern with a list of hypotheses *) +let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = + let get_id_couple id = function + | Name idpat -> [idpat,VConstr ([],mkVar id)] + | Anonymous -> [] in + let match_pat lmatch hyp pat = + match pat with + | Term t -> + let lmeta = extended_matches t hyp in + (try + let lmeta = verify_metas_coherence gl lmatch lmeta in + ([],lmeta,(fun () -> raise PatternMatchingFailure)) + with + | Not_coherent_metas -> raise PatternMatchingFailure); + | Subterm (b,ic,t) -> + let rec match_next_pattern find_next () = + let (lmeta,ctxt,find_next') = find_next () in + try + let lmeta = verify_metas_coherence gl lmatch (adjust lmeta) in + (give_context ctxt ic,lmeta,match_next_pattern find_next') + with + | Not_coherent_metas -> match_next_pattern find_next' () in + match_next_pattern (fun () -> match_subterm_gen b t hyp) () in + let rec apply_one_mhyp_context_rec = function + | (id,b,hyp as hd)::tl -> + (match patv with + | None -> + let rec match_next_pattern find_next () = + try + let (ids, lmeta, find_next') = find_next () in + (get_id_couple id hypname@ids, lmeta, hd, + match_next_pattern find_next') + with + | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in + match_next_pattern (fun () -> + let hyp = if b<>None then refresh_universes_strict hyp else hyp in + match_pat lmatch hyp pat) () + | Some patv -> + match b with + | Some body -> + let rec match_next_pattern_in_body next_in_body () = + try + let (ids,lmeta,next_in_body') = next_in_body() in + let rec match_next_pattern_in_typ next_in_typ () = + try + let (ids',lmeta',next_in_typ') = next_in_typ() in + (get_id_couple id hypname@ids@ids', lmeta', hd, + match_next_pattern_in_typ next_in_typ') + with + | PatternMatchingFailure -> + match_next_pattern_in_body next_in_body' () in + match_next_pattern_in_typ + (fun () -> + let hyp = refresh_universes_strict hyp in + match_pat lmeta hyp pat) () + with PatternMatchingFailure -> apply_one_mhyp_context_rec tl + in + match_next_pattern_in_body + (fun () -> match_pat lmatch body patv) () + | None -> apply_one_mhyp_context_rec tl) + | [] -> + db_hyp_pattern_failure ist.debug env (hypname,pat); + raise PatternMatchingFailure + in + apply_one_mhyp_context_rec lhyps + +(* misc *) + +let mk_constr_value ist gl c = VConstr ([],pf_interp_constr ist gl c) +let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) +let pack_sigma (sigma,c) = {it=c;sigma=sigma} + +let extend_gl_hyps gl sign = + { gl with + it = { gl.it with + evar_hyps = + List.fold_right Environ.push_named_context_val sign gl.it.evar_hyps } } + (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1758,13 +1814,13 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = | 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 - | TacMatchGoal (lz,lr,lmr) -> interp_match_goal 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 -> VFun (ist.trace,ist.lfun,[],t) - in check_for_interrupt (); + in check_for_interrupt (); match ist.debug with | DebugOn lev -> debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v}) @@ -1776,26 +1832,27 @@ and eval_tactic ist = function 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 (push_trace(dloc,call)ist.trace) + (interp_atomic ist gl) t in (* catch error in the evaluation *) - catch_error ((loc,call)::ist.trace) tac gl + catch_error (push_trace(loc,call)ist.trace) tac gl | TacFun _ | TacLetIn _ -> 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) + | TacId s -> fun gl -> tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl + | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) | TacAbstract (tac,ido) -> fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl - | TacThen (t1,tf,t,tl) -> + (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl + | TacThen (t1,tf,t,tl) -> tclTHENS3PARTS (interp_tactic ist t1) (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac) | TacTry tac -> tclTRY (interp_tactic ist tac) - | TacInfo tac -> + | TacInfo tac -> let t = (interp_tactic ist tac) in - tclINFO + tclINFO begin match tac with TacAtom (_,_) -> t @@ -1807,7 +1864,7 @@ and eval_tactic ist = function | TacFirst l -> tclFIRST (List.map (interp_tactic ist) l) | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> tclCOMPLETE (interp_tactic ist tac) - | TacArg a -> assert false + | TacArg a -> interp_tactic ist (TacArg a) and force_vrec ist gl = function | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body @@ -1822,9 +1879,9 @@ and interp_ltac_reference loc' mustbetac ist gl = function | 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 = + let ist = { lfun=[]; debug=ist.debug; avoid_ids=ids; - trace = loc_info::ist.trace } in + trace = push_trace loc_info ist.trace } in val_interp ist gl (lookup r) and interp_tacarg ist gl = function @@ -1832,7 +1889,7 @@ and interp_tacarg ist gl = function | Reference r -> interp_ltac_reference dloc false ist gl r | Integer n -> VInteger n | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat)) - | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) + | ConstrMayEval c -> VConstr ([],interp_constr_may_eval ist gl c) | MetaIdArg (loc,_,id) -> assert false | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r | TacCall (loc,f,l) -> @@ -1842,18 +1899,18 @@ and interp_tacarg ist gl = function 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 -> - let id = interp_fresh_id ist gl l in + | TacFreshId l -> + let id = pf_interp_fresh_id ist gl l in VIntroPattern (IntroIdentifier id) | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> - let tg = (tag t) in + let tg = (Dyn.tag t) in if tg = "tactic" then val_interp ist gl (tactic_out t ist) else if tg = "value" then value_out t else if tg = "constr" then - VConstr (constr_out t) + VConstr ([],constr_out t) else anomaly_loc (dloc, "Tacinterp.val_interp", (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) @@ -1861,21 +1918,28 @@ and interp_tacarg ist gl = function (* Interprets an application node *) and interp_app loc ist gl fv largs = match fv with - | VFun(trace,olfun,var,body) -> - let (newlfun,lvar,lval)=head_with_value (var,largs) in - if lvar=[] then - let v = - try - 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 loc ist gl v lval - else - VFun(trace,newlfun@olfun,lvar,body) + (* if var=[] and body has been delayed by val_interp, then body + is not a tactic that expects arguments. + Otherwise Ltac goes into an infinite loop (val_interp puts + a VFun back on body, and then interp_app is called again...) *) + | (VFun(trace,olfun,(_::_ as var),body) + |VFun(trace,olfun,([] as var), + (TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) -> + let (newlfun,lvar,lval)=head_with_value (var,largs) in + if lvar=[] then + let v = + try + 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 loc ist gl v lval + else + VFun(trace,newlfun@olfun,lvar,body) | _ -> user_err_loc (loc, "Tacinterp.interp_app", (str"Illegal tactic application.")) @@ -1887,8 +1951,13 @@ and tactic_of_value ist vle g = | 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 + | (VFun _|VRec _) -> error "A fully applied tactic is expected." + | VConstr _ -> errorlabstrm "" (str"Value is a term. Expected a tactic.") + | VConstr_context _ -> + errorlabstrm "" (str"Value is a term context. Expected a tactic.") + | VIntroPattern _ -> + errorlabstrm "" (str"Value is an intro pattern. Expected a tactic.") + | _ -> errorlabstrm "" (str"Expression does not evaluate to a tactic.") (* Evaluation with FailError catching *) and eval_with_fail ist is_lazy goal tac = @@ -1899,9 +1968,9 @@ and eval_with_fail ist is_lazy goal tac = VRTactic (catch_error trace tac goal) | a -> a) with - | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) + | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> - raise (Eval_fail s) + raise (Eval_fail (Lazy.force 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'))) @@ -1933,10 +2002,10 @@ and interp_match_goal ist goal lz lr lmr = let rec match_next_pattern find_next () = let (lgoal,ctxt,find_next') = find_next () in let lctxt = give_context ctxt id in - try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps + try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps with e when is_match_catchable e -> match_next_pattern find_next' () in match_next_pattern (fun () -> match_subterm_gen app c csr) () in - let rec apply_match_goal 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 @@ -1974,7 +2043,8 @@ and interp_match_goal ist goal lz lr lmr = else mt()) ++ str".")) end in apply_match_goal ist env goal 0 lmr - (read_match_rule (fst (constr_list ist env)) lmr) + (read_match_rule (fst (extract_ltac_constr_values ist env)) + ist env (project goal) lmr) (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = @@ -1992,7 +2062,7 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = let id_match = pi1 hyp_match in let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in apply_hyps_context_rec (lfun@lids) lm nextlhyps tl - with e when is_match_catchable e -> + with e when is_match_catchable e -> match_next_pattern find_next' in let init_match_pattern () = apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in @@ -2026,15 +2096,15 @@ and interp_genarg ist gl x = (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) | IdentArgType b -> in_gen (wit_ident_gen b) - (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) + (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) | VarArgType -> in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x)) | RefArgType -> in_gen wit_ref (pf_interp_reference ist gl (out_gen globwit_ref x)) | SortArgType -> in_gen wit_sort - (destSort - (pf_interp_constr ist gl + (destSort + (pf_interp_constr ist gl (RSort (dloc,out_gen globwit_sort x), None))) | ConstrArgType -> in_gen wit_constr (pf_interp_constr ist gl (out_gen globwit_constr x)) @@ -2047,15 +2117,17 @@ and interp_genarg ist gl x = | RedExprArgType -> in_gen wit_red_expr (pf_interp_red_expr ist gl (out_gen globwit_red_expr x)) | OpenConstrArgType casted -> - in_gen (wit_open_constr_gen casted) - (pf_interp_open_constr casted ist gl + in_gen (wit_open_constr_gen casted) + (interp_open_constr (if casted then Some (pf_concl gl) else None) + ist (pf_env gl) (project gl) (snd (out_gen (globwit_open_constr_gen casted) x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings - (interp_constr_with_bindings ist gl (out_gen globwit_constr_with_bindings x)) + (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) + (out_gen globwit_constr_with_bindings x))) | BindingsArgType -> in_gen wit_bindings - (interp_bindings ist gl (out_gen globwit_bindings x)) + (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x))) | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x @@ -2064,22 +2136,24 @@ and interp_genarg ist gl x = | List1ArgType _ -> app_list1 (interp_genarg ist gl) x | OptArgType _ -> app_opt (interp_genarg ist gl) x | PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x - | ExtraArgType s -> + | ExtraArgType s -> match tactic_genarg_level s with - | Some n -> + | Some n -> (* Special treatment of tactic arguments *) - in_gen (wit_tactic n) (out_gen (globwit_tactic n) x) - | None -> + in_gen (wit_tactic n) + (TacArg(valueIn(VFun(ist.trace,ist.lfun,[], + out_gen (globwit_tactic n) x)))) + | None -> lookup_interp_genarg s ist gl x and interp_genarg_constr_list0 ist gl x = let lc = out_gen (wit_list0 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list0 wit_constr) lc and interp_genarg_constr_list1 ist gl x = let lc = out_gen (wit_list1 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list1 wit_constr) lc and interp_genarg_var_list0 ist gl x = @@ -2098,7 +2172,7 @@ and interp_match ist g lz constr lmr = let rec match_next_pattern find_next () = let (lmatch,ctxt,find_next') = find_next () in let lctxt = give_context ctxt id in - let lfun = extend_values_with_bindings lmatch (lctxt@ist.lfun) in + let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in try eval_with_fail {ist with lfun=lfun} lz g mt with e when is_match_catchable e -> match_next_pattern find_next' () in @@ -2109,7 +2183,7 @@ and interp_match ist g lz constr lmr = with e when is_match_catchable e -> apply_match ist csr []) | (Pat ([],Term c,mt))::tl -> (try - let lmatch = + let lmatch = try extended_matches c csr with e -> debugging_exception_step ist false e (fun () -> @@ -2134,14 +2208,14 @@ and interp_match ist g lz constr lmr = | _ -> errorlabstrm "Tacinterp.apply_match" (str "No matching clauses for match.") in - let csr = + let csr = try interp_ltac_constr ist g constr with e -> debugging_exception_step ist true e (fun () -> str "evaluation of the matched expression"); raise e in - let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in - let res = - try apply_match ist csr ilr with e -> + let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) (project g) lmr in + let res = + try apply_match ist csr ilr with e -> debugging_exception_step ist true e (fun () -> str "match expression"); raise e in debugging_step ist (fun () -> @@ -2150,8 +2224,8 @@ and interp_match ist g lz constr lmr = (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist gl e = - let result = - try val_interp ist gl e with Not_found -> + let result = + try val_interp ist gl e with Not_found -> debugging_step ist (fun () -> str "evaluation failed for" ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) e); @@ -2160,11 +2234,13 @@ and interp_ltac_constr ist gl e = let cresult = constr_of_value (pf_env gl) result in debugging_step ist (fun () -> Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ - str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult); - cresult + str " has value " ++ fnl() ++ + pr_constr_under_binders_env (pf_env gl) cresult); + if fst cresult <> [] then raise Not_found; + snd cresult with Not_found -> errorlabstrm "" - (str "Must evaluate to a term" ++ fnl() ++ + (str "Must evaluate to a closed term" ++ fnl() ++ str "offending expression: " ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++ (match result with @@ -2173,7 +2249,7 @@ and interp_ltac_constr ist gl e = (str "VFun with body " ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ str "instantiated arguments " ++ fnl() ++ - List.fold_right + List.fold_right (fun p s -> let (i,v) = p in str (string_of_id i) ++ str ", " ++ s) il (str "") ++ @@ -2194,63 +2270,71 @@ and interp_ltac_constr ist gl e = (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = - try tactic_of_value ist (val_interp ist gl tac) gl - with NotTactic -> errorlabstrm "" (str "Not a tactic.") + tactic_of_value ist (val_interp ist gl tac) gl (* Interprets a primitive tactic *) -and interp_atomic ist gl = function +and interp_atomic ist gl tac = + let env = pf_env gl and sigma = project gl in + match tac with (* Basic tactics *) | TacIntroPattern l -> - h_intro_patterns (List.map (interp_intro_pattern ist gl) l) + h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> - h_intro_move (Option.map (interp_fresh_ident ist gl) ido) + h_intro_move (Option.map (interp_fresh_ident ist env) ido) (interp_move_location ist gl hto) | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) - | TacApply (a,ev,cb,None) -> - h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb) - | TacApply (a,ev,cb,Some cl) -> - h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb) - (interp_in_hyp_as ist gl cl) + | TacApply (a,ev,cb,cl) -> + let sigma, l = + list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + in + let tac = match cl with + | None -> h_apply a ev + | Some cl -> + (fun l -> h_apply_in a ev l (interp_in_hyp_as ist gl cl)) in + tclWITHHOLES ev tac sigma l | TacElim (ev,cb,cbo) -> - h_elim ev (interp_constr_with_bindings ist gl cb) - (Option.map (interp_constr_with_bindings ist gl) cbo) + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + tclWITHHOLES ev (h_elim ev cb) sigma cbo | TacElimType c -> h_elim_type (pf_interp_type ist gl c) - | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) + | TacCase (ev,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES ev (h_case ev) sigma cb | TacCaseType c -> h_case_type (pf_interp_type ist gl c) - | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n + | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n | TacMutualFix (b,id,n,l) -> - let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c) - in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l) - | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt) + let f (id,n,c) = (interp_fresh_ident ist env id,n,pf_interp_type ist gl c) + in h_mutual_fix b (interp_fresh_ident ist env id) n (List.map f l) + | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt) | TacMutualCofix (b,id,l) -> - let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in - h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l) + let f (id,c) = (interp_fresh_ident ist env id,pf_interp_type ist gl c) in + h_mutual_cofix b (interp_fresh_ident ist env id) (List.map f l) | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> - let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in - abstract_tactic (TacAssert (t,ipat,inj_open c)) + let c = (if t=None then interp_constr else interp_type) ist env sigma c in + abstract_tactic (TacAssert (t,ipat,c)) (Tactics.forward (Option.map (interp_tactic ist) t) (Option.map (interp_intro_pattern ist gl) ipat) c) | TacGeneralize cl -> - h_generalize_gen - (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl) + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + tclWITHHOLES false (h_generalize_gen) sigma cl | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp + h_let_tac b (interp_fresh_name ist env na) (pf_interp_constr ist gl c) clp (* Automation tactics *) - | TacTrivial (lems,l) -> - Auto.h_trivial (pf_interp_constr_list ist gl lems) + | TacTrivial (lems,l) -> + Auto.h_trivial (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> Auto.h_auto (Option.map (interp_int_or_var ist) n) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) @@ -2258,19 +2342,23 @@ and interp_atomic ist gl = function | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p,lems) -> Auto.h_dauto (Option.map (interp_int_or_var ist) n,p) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) - | TacInductionDestruct (isrec,ev,l) -> - 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) + | TacInductionDestruct (isrec,ev,(l,cls)) -> + let sigma, l = + list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) -> + let sigma,lc = + list_fold_map (interp_induction_arg ist gl) sigma lc in + let sigma,cbo = + Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + (sigma,(lc,cbo, + (Option.map (interp_intro_pattern ist gl) ipato, + Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + let cls = Option.map (interp_clause ist gl) cls in + tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2280,8 +2368,9 @@ and interp_atomic ist gl = function | TacDecompose (l,c) -> let l = List.map (interp_inductive ist) l in Elim.h_decompose l (pf_interp_constr ist gl c) - | TacSpecialize (n,l) -> - h_specialize n (interp_constr_with_bindings ist gl l) + | TacSpecialize (n,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES false (h_specialize n) sigma cb | TacLApply c -> h_lapply (pf_interp_constr ist gl c) (* Context management *) @@ -2290,50 +2379,64 @@ and interp_atomic ist gl = function | TacMove (dep,id1,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, - interp_fresh_ident ist gl (snd id2)) l) + h_rename (List.map (fun (id1,id2) -> + interp_hyp ist gl id1, + interp_fresh_ident ist env (snd id2)) l) | TacRevert l -> h_revert (interp_hyp_list ist gl l) (* Constructors *) - | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl) - | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl) - | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl) + | TacLeft (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_left ev) sigma bl + | TacRight (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_right ev) sigma bl + | TacSplit (ev,_,bll) -> + let sigma, bll = list_fold_map (interp_bindings ist env) sigma bll in + tclWITHHOLES ev (h_split ev) sigma bll | TacAnyConstructor (ev,t) -> abstract_tactic (TacAnyConstructor (ev,t)) (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) | TacConstructor (ev,n,bl) -> - h_constructor ev (skip_metaid n) (interp_bindings ist gl bl) + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_constructor ev (skip_metaid n)) sigma bl (* Conversion *) | TacReduce (r,cl) -> h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) - | TacChange (occl,c,cl) -> - h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl) - (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) & + | TacChange (None,c,cl) -> + h_change None + (if (cl.onhyps = None or cl.onhyps = Some []) & (cl.concl_occs = all_occurrences_expr or cl.concl_occs = no_occurrences_expr) - then pf_interp_type ist gl c + then pf_interp_type ist gl c else pf_interp_constr ist gl c) (interp_clause ist gl cl) + | TacChange (Some op,c,cl) -> + let sign,op = interp_typed_pattern ist env sigma op in + h_change (Some op) + (pf_interp_constr ist (extend_gl_hyps gl sign) c) + (interp_clause ist gl cl) (* Equivalence relations *) | TacReflexivity -> h_reflexivity | TacSymmetry c -> h_symmetry (interp_clause ist gl c) - | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) + | TacTransitivity c -> h_transitivity (Option.map (pf_interp_constr ist gl) c) (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - Equality.general_multi_multi_rewrite ev - (List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l) - (interp_clause ist gl cl) - (Option.map (interp_tactic ist) by) + | TacRewrite (ev,l,cl,by) -> + let l = List.map (fun (b,m,c) -> + let f env sigma = interp_open_constr_with_bindings ist env sigma c in + (b,m,f)) l in + let cl = interp_clause ist gl cl in + Equality.general_multi_multi_rewrite ev l cl + (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (Option.map (interp_intro_pattern ist gl) ids) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - Inv.inv_clause k + Inv.inv_clause k (Option.map (interp_intro_pattern ist gl) ids) (interp_hyp_list ist gl idl) (interp_declared_or_quantified_hypothesis ist gl hyp) @@ -2349,79 +2452,94 @@ and interp_atomic ist gl = function abstract_extended_tactic opn args (tac args) | TacAlias (loc,s,l,(_,body)) -> fun gl -> let rec f x = match genarg_tag x with - | IntArgType -> + | IntArgType -> VInteger (out_gen globwit_int x) | IntOrVarArgType -> mk_int_or_var_value ist (out_gen globwit_int_or_var x) | PreIdentArgType -> failwith "pre-identifiers cannot be bound" | IntroPatternArgType -> - VIntroPattern + VIntroPattern (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType b -> - VIntroPattern - (IntroIdentifier - (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))) + value_of_ident (interp_fresh_ident ist env + (out_gen (globwit_ident_gen b) x)) | VarArgType -> mk_hyp_value ist gl (out_gen globwit_var x) - | RefArgType -> - VConstr (constr_of_global + | RefArgType -> + VConstr ([],constr_of_global (pf_interp_reference ist gl (out_gen globwit_ref x))) - | SortArgType -> - VConstr (mkSort (interp_sort (out_gen globwit_sort x))) + | SortArgType -> + VConstr ([],mkSort (interp_sort (out_gen globwit_sort x))) | ConstrArgType -> mk_constr_value ist gl (out_gen globwit_constr x) | ConstrMayEvalArgType -> VConstr - (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) + ([],interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) | ExtraArgType s when tactic_genarg_level s <> None -> (* Special treatment of tactic arguments *) - val_interp ist gl + val_interp ist gl (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x) - | List0ArgType ConstrArgType -> + | List0ArgType ConstrArgType -> let wit = wit_list0 globwit_constr in VList (List.map (mk_constr_value ist gl) (out_gen wit x)) - | List0ArgType VarArgType -> + | List0ArgType VarArgType -> let wit = wit_list0 globwit_var in VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) - | List0ArgType IntArgType -> + | List0ArgType IntArgType -> let wit = wit_list0 globwit_int in VList (List.map (fun x -> VInteger x) (out_gen wit x)) - | List0ArgType IntOrVarArgType -> + | List0ArgType IntOrVarArgType -> let wit = wit_list0 globwit_int_or_var in VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) - | List1ArgType ConstrArgType -> + | List0ArgType (IdentArgType b) -> + let wit = wit_list0 (globwit_ident_gen b) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in + VList (List.map mk_ident (out_gen wit x)) + | List0ArgType IntroPatternArgType -> + let wit = wit_list0 globwit_intro_pattern in + let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in + VList (List.map mk_ipat (out_gen wit x)) + | List1ArgType ConstrArgType -> let wit = wit_list1 globwit_constr in VList (List.map (mk_constr_value ist gl) (out_gen wit x)) - | List1ArgType VarArgType -> + | List1ArgType VarArgType -> let wit = wit_list1 globwit_var in VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) - | List1ArgType IntArgType -> + | List1ArgType IntArgType -> let wit = wit_list1 globwit_int in VList (List.map (fun x -> VInteger x) (out_gen wit x)) - | List1ArgType IntOrVarArgType -> + | List1ArgType IntOrVarArgType -> let wit = wit_list1 globwit_int_or_var in VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) + | List1ArgType (IdentArgType b) -> + let wit = wit_list1 (globwit_ident_gen b) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in + VList (List.map mk_ident (out_gen wit x)) + | List1ArgType IntroPatternArgType -> + let wit = wit_list1 globwit_intro_pattern in + let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in + VList (List.map mk_ipat (out_gen wit x)) | StringArgType | BoolArgType - | QuantHypArgType | RedExprArgType - | OpenConstrArgType _ | ConstrWithBindingsArgType - | ExtraArgType _ | BindingsArgType - | OptArgType _ | PairArgType _ - | List0ArgType _ | List1ArgType _ + | QuantHypArgType | RedExprArgType + | OpenConstrArgType _ | ConstrWithBindingsArgType + | ExtraArgType _ | BindingsArgType + | OptArgType _ | PairArgType _ + | List0ArgType _ | List1ArgType _ -> 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 trace = (loc,LtacNotationCall s)::ist.trace in + let trace = push_trace (loc,LtacNotationCall s) ist.trace in interp_tactic { ist with lfun=lfun; trace=trace } body gl let make_empty_glob_sign () = - { ltacvars = ([],[]); ltacrecvars = []; + { ltacvars = ([],[]); ltacrecvars = []; gsigma = Evd.empty; genv = Global.env() } (* 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=[] } +let interp_tac_gen lfun avoid_ids debug t gl = + 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 @@ -2433,17 +2551,17 @@ let eval_tactic t gls = let interp t = interp_tac_gen [] [] (get_debug()) t let eval_ltac_constr gl t = - interp_ltac_constr + interp_ltac_constr { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl (intern_tactic (make_empty_glob_sign ()) t ) (* Hides interpretation for pretty-print *) let hide_interp t ot gl = - let ist = { ltacvars = ([],[]); ltacrecvars = []; + let ist = { ltacvars = ([],[]); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } in let te = intern_tactic ist t in let t = eval_tactic te in - match ot with + match ot with | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl | Some t' -> abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl @@ -2487,13 +2605,13 @@ let subst_or_var f = function let subst_located f (_loc,id) = (dloc,f id) -let subst_reference subst = +let subst_reference subst = subst_or_var (subst_located (subst_kn subst)) (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as - Print. It is also used for non-evaluable references. *) -let subst_global_reference subst = + Print. It is also used for non-evaluable references. *) +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 @@ -2508,7 +2626,7 @@ let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in subst_or_var (subst_and_short_name subst_eval_ref) -let subst_unfold subst (l,e) = +let subst_unfold subst (l,e) = (l,subst_evaluable subst e) let subst_flag subst red = @@ -2516,13 +2634,19 @@ let subst_flag subst red = let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c) +let subst_rawconstr_or_pattern subst (c,p) = + (subst_rawconstr subst c,subst_pattern subst p) + +let subst_pattern_with_occurrences subst (l,p) = + (l,subst_rawconstr_or_pattern subst p) + let subst_redexp subst = function | Unfold l -> Unfold (List.map (subst_unfold subst) l) | Fold l -> Fold (List.map (subst_rawconstr subst) l) | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) - | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o) + | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function @@ -2532,8 +2656,8 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc) - | Term pc -> Term (subst_pattern subst pc) + | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_rawconstr_or_pattern subst pc)) + | Term pc -> Term (subst_rawconstr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function | Hyp (locs,mp) :: tl -> @@ -2584,10 +2708,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) as x -> x - | TacInductionDestruct (isrec,ev,l) -> - TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) -> + | TacInductionDestruct (isrec,ev,(l,cls)) -> + TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) -> List.map (subst_induction_arg subst) lc, - Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l) + Option.map (subst_raw_with_bindings subst) cbo, ids) l, cls)) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2607,23 +2731,23 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Constructors *) | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl) | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl) - | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl) + | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll) | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t) | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) - | TacChange (occl,c,cl) -> - TacChange (Option.map (subst_constr_with_occurrences subst) occl, + | TacChange (op,c,cl) -> + TacChange (Option.map (subst_rawconstr_or_pattern subst) op, subst_rawconstr subst c, cl) (* Equivalence relations *) | TacReflexivity | TacSymmetry _ as x -> x - | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) + | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c) (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - TacRewrite (ev, + | TacRewrite (ev,l,cl,by) -> + TacRewrite (ev, List.map (fun (b,m,c) -> b,m,subst_raw_with_bindings subst c) l, cl,Option.map (subst_tactic subst) by) @@ -2677,14 +2801,14 @@ and subst_tacarg subst = function | MetaIdArg (_loc,_,_) -> assert false | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) - | TacExternal (_loc,com,req,la) -> + | TacExternal (_loc,com,req,la) -> TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) | TacDynamic(the_loc,t) as x -> - (match tag t with + (match Dyn.tag t with | "tactic" | "value" -> x - | "constr" -> + | "constr" -> TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) | s -> anomaly_loc (dloc, "Tacinterp.val_interp", str "Unknown dynamic: <" ++ str s ++ str ">")) @@ -2709,11 +2833,11 @@ and subst_genarg subst (x:glob_generic_argument) = | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x) | IntroPatternArgType -> in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x) - | IdentArgType b -> + | IdentArgType b -> in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x) | VarArgType -> in_gen globwit_var (out_gen globwit_var x) | RefArgType -> - in_gen globwit_ref (subst_global_reference subst + in_gen globwit_ref (subst_global_reference subst (out_gen globwit_ref x)) | SortArgType -> in_gen globwit_sort (out_gen globwit_sort x) @@ -2723,7 +2847,7 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x)) | QuantHypArgType -> in_gen globwit_quant_hyp - (subst_declared_or_quantified_hypothesis subst + (subst_declared_or_quantified_hypothesis subst (out_gen globwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) @@ -2742,11 +2866,11 @@ and subst_genarg subst (x:glob_generic_argument) = | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x | ExtraArgType s -> match tactic_genarg_level s with - | Some n -> + | Some n -> (* Special treatment of tactic arguments *) in_gen (globwit_tactic n) (subst_tactic subst (out_gen (globwit_tactic n) x)) - | None -> + | None -> lookup_genarg_subst s subst x (***************************************************************************) @@ -2764,10 +2888,10 @@ let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) type tacdef_kind = | NewTac of identifier | UpdateTac of ltac_constant -let load_md i ((sp,kn),defs) = +let load_md i ((sp,kn),(local,defs)) = let dp,_ = repr_path sp in let mp,dir,_ = repr_kn kn in - List.iter (fun (id,t) -> + List.iter (fun (id,t) -> match id with NewTac id -> let sp = Libnames.make_path dp id in @@ -2775,11 +2899,11 @@ let load_md i ((sp,kn),defs) = Nametab.push_tactic (Until i) sp kn; add (kn,t) | UpdateTac kn -> replace (kn,t)) defs - -let open_md i((sp,kn),defs) = + +let open_md i ((sp,kn),(local,defs)) = let dp,_ = repr_path sp in let mp,dir,_ = repr_kn kn in - List.iter (fun (id,t) -> + List.iter (fun (id,t) -> match id with NewTac id -> let sp = Libnames.make_path dp id in @@ -2789,13 +2913,17 @@ let open_md i((sp,kn),defs) = let cache_md x = load_md 1 x -let subst_kind subst id = +let subst_kind subst id = match id with | NewTac _ -> id - | UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn) + | UpdateTac kn -> UpdateTac (subst_kn subst kn) + +let subst_md (subst,(local,defs)) = + (local, + List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs) -let subst_md (_,subst,defs) = - List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs +let classify_md (local,defs as o) = + if local then Dispose else Substitute o let (inMD,outMD) = declare_object {(default_object "TAC-DEFINITION") with @@ -2803,8 +2931,7 @@ let (inMD,outMD) = load_function = load_md; open_function = open_md; subst_function = subst_md; - classify_function = (fun (_,o) -> Substitute o); - export_function = (fun x -> Some x)} + classify_function = classify_md} let print_ltac id = try @@ -2822,18 +2949,18 @@ open Libnames (* Adds a definition for tactics in the table *) let make_absolute_name ident repl = let loc = loc_of_reference ident in - try - let id, kn = + try + let id, kn = if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident)) - else let id = Pcoq.coerce_global_to_id ident in - Some id, Lib.make_kn id + else let id = coerce_reference_to_id ident in + Some id, Lib.make_kn id in if Gmap.mem kn !mactab then if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", str "There is already an Ltac named " ++ pr_reference ident ++ str".") - else if is_atomic_kn kn then + else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", str "Reserved Ltac name " ++ pr_reference ident ++ str".") else id, kn @@ -2841,21 +2968,12 @@ let make_absolute_name ident repl = user_err_loc (loc,"Tacinterp.add_tacdef", str "There is no Ltac named " ++ pr_reference ident ++ str".") -let rec filter_map f l = - let rec aux acc = function - [] -> acc - | hd :: tl -> - match f hd with - Some x -> aux (x :: acc) tl - | None -> aux acc tl - in aux [] l - -let add_tacdef isrec tacl = +let add_tacdef local isrec tacl = let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in let ist = - {(make_empty_glob_sign()) with ltacrecvars = - if isrec then filter_map - (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun + {(make_empty_glob_sign()) with ltacrecvars = + if isrec then list_map_filter + (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun else []} in let gtacl = List.map2 (fun (_,b,def) (id, qid) -> @@ -2864,11 +2982,12 @@ let add_tacdef isrec tacl = (k, t)) tacl rfun in let id0 = fst (List.hd rfun) in - let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl)) - | _ -> Lib.add_anonymous_leaf (inMD gtacl) in + let _ = match id0 with + | Some id0 -> ignore(Lib.add_leaf id0 (inMD (local,gtacl))) + | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl)) in List.iter - (fun (id,b,_) -> - Flags.if_verbose msgnl (Libnames.pr_reference id ++ + (fun (id,b,_) -> + Flags.if_verbose msgnl (Libnames.pr_reference id ++ (if b then str " is redefined" else str " is defined"))) tacl @@ -2879,13 +2998,13 @@ let add_tacdef isrec tacl = let glob_tactic x = Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x -let glob_tactic_env l env x = +let glob_tactic_env l env x = Flags.with_option strict_check (intern_tactic { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }) x -let interp_redexp env sigma r = +let interp_redexp env sigma r = 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) @@ -2894,11 +3013,14 @@ 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 tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist)) +let tacticIn t = + globTacticIn (fun ist -> + try glob_tactic (t ist) + with e -> raise (AnomalyOnError ("Incorrect tactic expression", e))) let tacticOut = function | TacArg (TacDynamic (_,d)) -> - if (tag d) = "tactic" then + if (Dyn.tag d) = "tactic" then tactic_out d else anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") @@ -2910,14 +3032,12 @@ let tacticOut = function (* 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 + (fun l -> + let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]}) -let _ = Auto.set_extern_intern_tac +let _ = Auto.set_extern_intern_tac (fun l -> Flags.with_option strict_check (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})) let _ = Auto.set_extern_subst_tactic subst_tactic let _ = Dhyp.set_extern_interp eval_tactic -let _ = Dhyp.set_extern_intern_tac - (fun t -> intern_tactic (make_empty_glob_sign()) t) |