diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 4620 |
1 files changed, 1908 insertions, 2712 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e5575a2c..23de47d5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1,1001 +1,287 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Constrintern -open Closure -open RedFlags -open Declarations -open Entries -open Libobject -open Pattern -open Matching +open Patternops open Pp +open Genredexpr open Glob_term -open Sign +open Glob_ops open Tacred +open Errors open Util open Names open Nameops open Libnames +open Globnames open Nametab -open Smartlocate open Pfedit open Proof_type open Refiner open Tacmach open Tactic_debug -open Topconstr +open Constrexpr open Term open Termops open Tacexpr -open Safe_typing -open Typing -open Hiddentac open Genarg -open Decl_kinds -open Mod_subst +open Stdarg +open Constrarg open Printer -open Inductiveops -open Syntax_def open Pretyping -open Pretyping.Default -open Extrawit -open Pcoq -open Compat +module Monad_ = Monad open Evd +open Misctypes +open Locus +open Tacintern +open Taccoerce +open Proofview.Notations let safe_msgnl s = - try msgnl s with e when Errors.noncritical 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 - (loc,"out_ident", - str "Syntactic metavariables allowed only in quotations.") - -let error_tactic_expected loc = - user_err_loc (loc,"",str "Tactic expected.") - -let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid - -let skip_metaid = function - | AI x -> x - | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc + Proofview.NonLogical.catch + (Proofview.NonLogical.print (s++fnl())) + (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) + +type value = tlevel generic_argument + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.kernel_name * typed_generic_argument list) list + (** For calls to global constants, some may alias other. *) +let push_appl appl args = + match appl with + | UnnamedAppl -> UnnamedAppl + | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) +let pr_generic arg = + let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in + try + Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg + with e when Errors.noncritical e -> str"<generic>" +let pr_appl h vs = + Pptactic.pr_ltac_constant h ++ spc () ++ + Pp.prlist_with_sep spc pr_generic vs +let rec name_with_list appl t = + match appl with + | [] -> t + | (h,vs)::l -> Proofview.Trace.name_tactic (fun () -> pr_appl h vs) (name_with_list l t) +let name_if_glob appl t = + match appl with + | UnnamedAppl -> t + | GlbAppl l -> name_with_list l t +let combine_appl appl1 appl2 = + match appl1,appl2 with + | UnnamedAppl,a | a,UnnamedAppl -> a + | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1) (* Values for interpretation *) -type value = - | VRTactic of (goal list sigma) (* For Match results *) - (* Not a true value *) - | 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_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 - -let dloc = dummy_loc - -let catch_error call_trace tac g = - if call_trace = [] then tac g else try tac g with - | LtacLocated _ as e -> raise e - | Loc.Exc_located (_,LtacLocated _) as e -> raise e - | e when Errors.noncritical e -> - let (nrep,loc',c),tail = list_sep_last call_trace in - let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in - if tail = [] then - let loc = if loc = dloc then loc' else loc in - raise (Loc.Exc_located(loc,e')) - else - raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) - -(* Signature for interpretation: val_interp and interpretation functions *) -type interp_sign = - { lfun : (identifier * value) list; - avoid_ids : identifier list; (* ids inherited from the call context - (needed to get fresh ids) *) - debug : debug_info; - trace : ltac_trace } - -let check_is_value = function - | VRTactic _ -> (* These are goals produced by Match *) - error "Immediate match producing tactics not allowed in local definitions." - | _ -> () - -(* Gives the constr corresponding to a Constr_context tactic_arg *) -let constr_of_VConstr_context = function - | VConstr_context c -> c - | _ -> - errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.") - -(* Displays a value *) -let rec pr_value env = function - | VVoid -> str "()" - | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) - | 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" - | VList (a::_) -> - str "a list (first element is " ++ pr_value env a ++ str")" - -(* Transforms an id into a constr if possible, or fails with Not_found *) -let constr_of_id env id = - Term.mkVar (let _ = Environ.lookup_named id env in id) +type tacvalue = + | VFun of appl*ltac_trace * value Id.Map.t * + Id.t option list * glob_tactic_expr + | VRec of value Id.Map.t ref * glob_tactic_expr -(* To embed tactics *) -let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), - (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = - Dyn.create "tactic" +let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) = + Genarg.create_arg None "tacvalue" -let ((value_in : value -> Dyn.t), - (value_out : Dyn.t -> value)) = Dyn.create "value" +let of_tacvalue v = in_gen (topwit wit_tacvalue) v +let to_tacvalue v = out_gen (topwit wit_tacvalue) v -let valueIn t = TacDynamic (dummy_loc,value_in t) -let valueOut = function - | TacDynamic (_,d) -> - if (Dyn.tag d) = "value" then - value_out d - else - anomalylabstrm "valueOut" (str "Dynamic tag should be value") - | ast -> - anomalylabstrm "valueOut" (str "Not a Dynamic ast: ") +(** More naming applications *) +let name_vfun appl vle = + let vle = Value.normalize vle in + if has_type vle (topwit wit_tacvalue) then + match to_tacvalue vle with + | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) + | _ -> vle + else vle -(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) -let atomic_mactab = ref Idmap.empty -let add_primitive_tactic s tac = - let id = id_of_string s in - atomic_mactab := Idmap.add id tac !atomic_mactab +module TacStore = Geninterp.TacStore -let _ = - let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in - List.iter - (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t))) - [ "red", TacReduce(Red false,nocl); - "hnf", TacReduce(Hnf,nocl); - "simpl", TacReduce(Simpl None,nocl); - "compute", TacReduce(Cbv all_flags,nocl); - "intro", TacIntroMove(None,no_move); - "intros", TacIntroPattern []; - "assumption", TacAssumption; - "cofix", TacCofix None; - "trivial", TacTrivial (Off,[],None); - "auto", TacAuto(Off,None,[],None); - "left", TacLeft(false,NoBindings); - "eleft", TacLeft(true,NoBindings); - "right", TacRight(false,NoBindings); - "eright", TacRight(true,NoBindings); - "split", TacSplit(false,false,[NoBindings]); - "esplit", TacSplit(true,false,[NoBindings]); - "constructor", TacAnyConstructor (false,None); - "econstructor", TacAnyConstructor (true,None); - "reflexivity", TacReflexivity; - "symmetry", TacSymmetry nocl - ]; - List.iter - (fun (s,t) -> add_primitive_tactic s t) - [ "idtac",TacId []; - "fail", TacFail(ArgArg 0,[]); - "fresh", TacArg(dloc,TacFreshId []) - ] - -let lookup_atomic id = Idmap.find id !atomic_mactab -let is_atomic_kn kn = - let (_,_,l) = repr_kn kn in - Idmap.mem (id_of_label l) !atomic_mactab - -(* Summary and Object declaration *) -let mactab = ref Gmap.empty - -let lookup r = Gmap.find r !mactab +let f_avoid_ids : Id.t list TacStore.field = TacStore.field () +(* ids inherited from the call context (needed to get fresh ids) *) +let f_debug : debug_info TacStore.field = TacStore.field () +let f_trace : ltac_trace TacStore.field = TacStore.field () -let _ = - let init () = mactab := Gmap.empty in - let freeze () = !mactab in - let unfreeze fs = mactab := fs in - Summary.declare_summary "tactic-definition" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - -(* Tactics table (TacExtend). *) - -let tac_tab = Hashtbl.create 17 - -let add_tactic s t = - if Hashtbl.mem tac_tab s then - errorlabstrm ("Refiner.add_tactic: ") - (str ("Cannot redeclare tactic "^s^".")); - Hashtbl.add tac_tab s t - -let overwriting_add_tactic s t = - if Hashtbl.mem tac_tab s then begin - Hashtbl.remove tac_tab s; - msg_warn ("Overwriting definition of tactic "^s) - end; - Hashtbl.add tac_tab s t - -let lookup_tactic s = - try - Hashtbl.find tac_tab s - with Not_found -> - errorlabstrm "Refiner.lookup_tactic" - (str"The tactic " ++ str s ++ str" is not installed.") -(* -let vernac_tactic (s,args) = - let tacfun = lookup_tactic s args in - abstract_extended_tactic s args tacfun -*) -(* Interpretation of extra generic arguments *) -type glob_sign = { - ltacvars : identifier list * identifier list; - (* ltac variables and the subset of vars introduced by Intro/Let/... *) - ltacrecvars : (identifier * ltac_constant) list; - (* ltac recursive names *) - gsigma : Evd.evar_map; - genv : Environ.env } - -type interp_genarg_type = - (glob_sign -> raw_generic_argument -> glob_generic_argument) * - (interp_sign -> goal sigma -> glob_generic_argument -> - Evd.evar_map * typed_generic_argument) * - (substitution -> glob_generic_argument -> glob_generic_argument) - -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 = - try Gmap.find id !extragenargtab - with Not_found -> - let msg = "No interpretation function found for entry " ^ id in - msg_warn 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 (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 - (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") - -(*****************) -(* Globalization *) -(*****************) +(* Signature for interpretation: val_interp and interpretation functions *) +type interp_sign = Geninterp.interp_sign = { + lfun : value Id.Map.t; + extra : TacStore.t } -(* We have identifier <| global_reference <| constr *) +let extract_trace ist = match TacStore.get ist.extra f_trace with +| None -> [] +| Some l -> l -let find_ident id ist = - List.mem id (fst ist.ltacvars) or - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) +module Value = struct -let find_recvar qid ist = List.assoc qid ist.ltacrecvars + include Taccoerce.Value -(* a "var" is a ltac var or a var introduced by an intro tactic *) -let find_var id ist = List.mem id (fst ist.ltacvars) + let of_closure ist tac = + let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in + of_tacvalue closure -(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *) -let find_ctxvar id ist = List.mem id (snd ist.ltacvars) +end -(* a "ltacvar" is an ltac var (Let-In/Fun/...) *) -let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist) +let dloc = Loc.ghost -let find_hyp id ist = - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) +let catching_error call_trace fail (e, info) = + let inner_trace = + Option.default [] (Exninfo.get info ltac_trace_info) + in + if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info) + else begin + assert (Errors.noncritical e); (* preserved invariant *) + let new_trace = inner_trace @ call_trace in + let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in + fail located_exc + end -(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *) -(* be fresh in which case it is binding later on *) -let intern_ident l ist id = - (* We use identifier both for variables and new names; thus nothing to do *) - if not (find_ident id ist) then l:=(id::fst !l,id::snd !l); - id +let catch_error call_trace f x = + try f x + with e when Errors.noncritical e -> + let e = Errors.push e in + catching_error call_trace iraise e -let intern_name l ist = function - | Anonymous -> Anonymous - | Name id -> Name (intern_ident l ist id) +let catch_error_tac call_trace tac = + Proofview.tclORELSE + tac + (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) -let strict_check = ref false +let curr_debug ist = match TacStore.get ist.extra f_debug with +| None -> DebugOff +| Some level -> level -let adjust_loc loc = if !strict_check then dloc else loc +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) -(* Globalize a name which must be bound -- actually just check it is bound *) -let intern_hyp ist (loc,id as locid) = - if not !strict_check then - locid - else if find_ident id ist then - (dloc,id) +(* Displays a value *) +let pr_value env v = + let v = Value.normalize v in + if has_type v (topwit wit_tacvalue) then str "a tactic" + else if has_type v (topwit wit_constr_context) then + let c = out_gen (topwit wit_constr_context) v in + match env with + | Some (env,sigma) -> pr_lconstr_env env sigma c + | _ -> str "a term" + else if has_type v (topwit wit_constr) then + let c = out_gen (topwit wit_constr) v in + match env with + | Some (env,sigma) -> pr_lconstr_env env sigma c + | _ -> str "a term" + else if has_type v (topwit wit_constr_under_binders) then + let c = out_gen (topwit wit_constr_under_binders) v in + match env with + | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c + | _ -> str "a term" else - Pretype_errors.error_var_not_found_loc loc id - -let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id) - -let intern_or_var ist = function - | ArgVar locid -> ArgVar (intern_hyp ist locid) - | ArgArg _ as x -> x - -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) - | r -> ArgArg (intern_inductive_or_by_notation r) - -let intern_global_reference ist = function - | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) - | r -> - let loc,_ as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> - error_global_not_found_loc lqid - -let intern_ltac_variable ist = function - | Ident (loc,id) -> - if find_ltacvar id ist then - (* A local variable of any type *) - ArgVar (loc,id) - else - (* A recursive variable *) - ArgArg (loc,find_recvar id ist) - | _ -> - raise Not_found - -let intern_constr_reference strict ist = function - | Ident (_,id) as r when not strict & find_hyp id ist -> - GVar (dloc,id), Some (CRef r) - | Ident (_,id) as r when find_ctxvar id ist -> - GVar (dloc,id), if strict then None else Some (CRef r) - | r -> - let loc,_ as lqid = qualid_of_reference r in - GRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) - -let intern_move_location ist = function - | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) - | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id) - | MoveToEnd toleft as x -> x - -(* Internalize an isolated reference in position of tactic *) - -let intern_isolated_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in - try TacCall (loc,ArgArg (loc,locate_tactic qid),[]) - with Not_found -> - match r with - | Ident (_,id) -> Tacexp (lookup_atomic id) - | _ -> raise Not_found + str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v) + +let pr_closure env ist body = + let pp_body = Pptactic.pr_glob_tactic env body in + let pr_sep () = fnl () in + let pr_iarg (id, arg) = + let arg = pr_argument_type (genarg_tag arg) in + hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg) + in + let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in + pp_body ++ fnl() ++ str "in environment " ++ fnl() ++ pp_iargs + +let pr_inspect env expr result = + let pp_expr = Pptactic.pr_glob_tactic env expr in + let pp_result = + if has_type result (topwit wit_tacvalue) then + match to_tacvalue result with + | VFun (_,_, ist, ul, b) -> + let body = if List.is_empty ul then b else (TacFun (ul, b)) in + str "a closure with body " ++ fnl() ++ pr_closure env ist body + | VRec (ist, body) -> + str "a recursive closure" ++ fnl () ++ pr_closure env !ist body + else + let pp_type = pr_argument_type (genarg_tag result) in + str "an object of type" ++ spc () ++ pp_type + in + pp_expr ++ fnl() ++ str "this is " ++ pp_result -let intern_isolated_tactic_reference strict ist r = - (* An ltac reference *) - try Reference (intern_ltac_variable ist r) - with Not_found -> - (* A global tactic *) - try intern_isolated_global_tactic_reference r - with Not_found -> - (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) - with Not_found -> - (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) +(* Transforms an id into a constr if possible, or fails with Not_found *) +let constr_of_id env id = + Term.mkVar (let _ = Environ.lookup_named id env in id) -(* Internalize an applied tactic reference *) +(* To embed tactics *) -let intern_applied_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in - ArgArg (loc,locate_tactic qid) +let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), + (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = + Dyn.create "tactic" -let intern_applied_tactic_reference ist r = - (* An ltac reference *) - try intern_ltac_variable ist r - with Not_found -> - (* A global tactic *) - try intern_applied_global_tactic_reference r - with Not_found -> - (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) +let ((value_in : value -> Dyn.t), + (value_out : Dyn.t -> value)) = Dyn.create "value" -(* Intern a reference parsed in a non-tactic entry *) +let valueIn t = TacDynamic (Loc.ghost, value_in t) + +(** Generic arguments : table of interpretation functions *) + +let push_trace call ist = match TacStore.get ist.extra f_trace with +| None -> [call] +| Some trace -> call :: trace + +let propagate_trace ist loc id v = + let v = Value.normalize v in + if has_type v (topwit wit_tacvalue) then + let tacv = to_tacvalue v in + match tacv with + | VFun (appl,_,lfun,it,b) -> + let t = if List.is_empty it then b else TacFun (it,b) in + let ans = VFun (appl,push_trace(loc,LtacVarCall (id,t)) ist,lfun,it,b) in + of_tacvalue ans + | _ -> v + else v + +let append_trace trace v = + let v = Value.normalize v in + if has_type v (topwit wit_tacvalue) then + match to_tacvalue v with + | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) + | _ -> v + else v -let intern_non_tactic_reference strict ist r = - (* An ltac reference *) - try Reference (intern_ltac_variable ist r) - with Not_found -> - (* A constr reference *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) - with Not_found -> - (* Tolerance for compatibility, allow not to use "ltac:" *) - try intern_isolated_global_tactic_reference r - with Not_found -> - (* By convention, use IntroIdentifier for unbound ident, when not in a def *) - match r with - | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id) - | _ -> - (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) - -let intern_message_token ist = function - | (MsgString _ | MsgInt _ as x) -> x - | MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id) - -let intern_message ist = List.map (intern_message_token ist) - -let rec intern_intro_pattern lf ist = function - | loc, IntroOrAndPattern l -> - loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) - | loc, IntroIdentifier id -> - loc, IntroIdentifier (intern_ident lf ist id) - | 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 = - List.map (List.map (intern_intro_pattern lf ist)) - -let intern_quantified_hypothesis ist = function - | AnonHyp n -> AnonHyp n - | 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 - and if a term w/o ltac vars, check the name is indeed quantified *) - x - -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 ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c +(* Dynamically check that an argument is a tactic *) +let coerce_to_tactic loc id v = + let v = Value.normalize v in + let fail () = user_err_loc + (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") in - (c',if !strict_check then None else Some c) - -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) = - (loc,intern_binding_name ist b,intern_constr ist c) - -let intern_bindings ist = function - | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l) - | ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l) - -let intern_constr_with_bindings ist (c,bl) = - (intern_constr ist c, intern_bindings ist bl) - - (* TODO: catch ltac vars *) -let intern_induction_arg ist = function - | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) -> - if !strict_check then - (* If in a defined tactic, no intros-until *) - match intern_constr ist (CRef (Ident (dloc,id))) with - | GVar (loc,id),_ -> ElimOnIdent (loc,id) - | c -> ElimOnConstr (c,NoBindings) - else - ElimOnIdent (loc,id) + let v = Value.normalize v in + if has_type v (topwit wit_tacvalue) then + let tacv = to_tacvalue v in + match tacv with + | VFun _ -> v + | _ -> fail () + else fail () -let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) - | _ -> None +let value_of_ident id = + in_gen (topwit wit_intro_pattern) + (Loc.ghost, IntroNaming (IntroIdentifier id)) -let intern_evaluable_global_reference ist r = - let lqid = qualid_of_reference r in - 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 -> EvalVarRef id - | _ -> error_global_not_found_loc lqid - -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 ist.genv - (Notation.interp_notation_as_global_reference loc - (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) - -(* Globalize a reduction expression *) -let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) - | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist -> - ArgArg (EvalVarRef id, Some (loc,id)) - | AN (Ident (loc,id)) when find_ctxvar id ist -> - ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id)) - | r -> - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) - -let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) - -let intern_flag ist red = - { red with rConst = List.map (intern_evaluable ist) red.rConst } - -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 glob_constr 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) - -(* This seems fairly hacky, but it's the first way I've found to get proper - globalization of [unfold]. --adamc *) -let dump_glob_red_expr = function - | Unfold occs -> List.iter (fun (_, r) -> - try - Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) - (Smartlocate.smart_global r) - with e when Errors.noncritical e -> ()) occs - | Cbv grf | Lazy grf -> - List.iter (fun r -> - try - Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) - (Smartlocate.smart_global r) - with e when Errors.noncritical e -> ()) grf.rConst - | _ -> () - -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_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) - -let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist) - -let intern_inversion_strength lf ist = function - | NonDepInversion (k,idl,ids) -> - NonDepInversion (k,intern_hyp_list ist idl, - Option.map (intern_intro_pattern lf ist) ids) - | DepInversion (k,copt,ids) -> - DepInversion (k, Option.map (intern_constr ist) copt, - Option.map (intern_intro_pattern lf ist) ids) - | InversionUsing (c,idl) -> - InversionUsing (intern_constr ist c, intern_hyp_list ist idl) - -(* Interprets an hypothesis name *) -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 ist ?(as_type=false) lfun = function - | Subterm (b,ido,pc) -> - let ltacvars = (lfun,[]) in - let (metas,pc) = intern_constr_pattern ist ltacvars pc in - ido, metas, Subterm (b,ido,pc) - | Term pc -> - let ltacvars = (lfun,[]) in - 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) - | ConstrContext (locid,c) -> - ConstrContext (intern_hyp ist locid,intern_constr ist c) - | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c) - | ConstrTerm c -> ConstrTerm (intern_constr ist c) - -(* External tactics *) -let print_xml_term = ref (fun _ -> failwith "print_xml_term unset") -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 - | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ - | 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; - output_string ch "\">\n"; - List.iter (pf_apply (extern_tacarg ch) gl) la; - output_string ch "</REQUEST>\n" - -let value_of_ident id = VIntroPattern (IntroIdentifier id) +let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 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 + let of_cub c = match c with + | [], c -> Value.of_constr c + | _ -> in_gen (topwit wit_constr_under_binders) c + 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 ist lfun = function - | (Hyp ((_,na) as locna,mp))::tl -> - 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 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 - (fun ((loc,name),_) l -> - if List.mem name l then - user_err_loc - (loc, "glob_tactic", str "This variable is bound several times."); - name::l) - lrc [] - -let clause_app f = function - { onhyps=None; concl_occs=nl } -> - { onhyps=None; concl_occs=nl } - | { onhyps=Some l; concl_occs=nl } -> - { onhyps=Some(List.map f l); concl_occs=nl} - -(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) -let rec intern_atomic lf ist x = - match (x:raw_atomic_tactic_expr) with - (* Basic tactics *) - | TacIntroPattern l -> - TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) - | TacIntroMove (ido,hto) -> - TacIntroMove (Option.map (intern_ident lf ist) ido, - intern_move_location ist hto) - | TacAssumption -> TacAssumption - | TacExact c -> TacExact (intern_constr ist c) - | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) - | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) - | TacApply (a,ev,cb,inhyp) -> - TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb, - Option.map (intern_in_hyp_as ist lf) inhyp) - | TacElim (ev,cb,cbo) -> - TacElim (ev,intern_constr_with_bindings ist cb, - Option.map (intern_constr_with_bindings ist) cbo) - | TacElimType c -> TacElimType (intern_type ist c) - | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb) - | TacCaseType c -> TacCaseType (intern_type ist c) - | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) - | TacMutualFix (b,id,n,l) -> - let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in - TacMutualFix (b,intern_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt) - | TacMutualCofix (b,id,l) -> - let f (id,c) = (intern_ident lf ist id,intern_type ist c) in - TacMutualCofix (b,intern_ident lf ist id, List.map f l) - | TacCut c -> TacCut (intern_type ist c) - | TacAssert (otac,ipat,c) -> - TacAssert (Option.map (intern_pure_tactic ist) otac, - Option.map (intern_intro_pattern lf ist) ipat, - intern_constr_gen false (otac<>None) ist c) - | TacGeneralize cl -> - TacGeneralize (List.map (fun (c,na) -> - intern_constr_with_occurrences ist c, - intern_name lf ist na) cl) - | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (na,c,cls,b,eqpat) -> - let na = intern_name lf ist na in - TacLetTac (na,intern_constr ist c, - (clause_app (intern_hyp_location ist) cls),b, - (Option.map (intern_intro_pattern lf ist) eqpat)) - - (* Automation tactics *) - | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l) - | TacAuto (d,n,lems,l) -> - TacAuto (d,Option.map (intern_or_var ist) n, - List.map (intern_constr ist) lems,l) - - (* Derived basic tactics *) - | TacSimpleInductionDestruct (isrec,h) -> - TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h) - | TacInductionDestruct (ev,isrec,(l,el,cls)) -> - TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) -> - (intern_induction_arg ist c, - (Option.map (intern_intro_pattern lf ist) ipato, - Option.map (intern_intro_pattern lf ist) ipats))) l, - Option.map (intern_constr_with_bindings ist) el, - 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 - TacDoubleInduction (h1,h2) - | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c) - | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c) - | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in - TacDecompose (l,intern_constr ist c) - | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l) - | TacLApply c -> TacLApply (intern_constr ist c) - - (* Context management *) - | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l) - | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) - | TacMove (dep,id1,id2) -> - TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2) - | 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,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll) - | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t) - | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl) - - (* Conversion *) - | TacReduce (r,cl) -> - dump_glob_red_expr r; - TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) - | 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 (clause_app (intern_hyp_location ist) idopt) - | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c) - - (* Equality and inversion *) - | 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_pure_tactic ist) by) - | TacInversion (inv,hyp) -> - TacInversion (intern_inversion_strength lf ist inv, - intern_quantified_hypothesis ist hyp) - - (* For extensions *) - | TacExtend (loc,opn,l) -> - let _ = lookup_tactic opn in - TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l) - | TacAlias (loc,s,l,(dir,body)) -> - let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in - TacAlias (loc,s,l,(dir,body)) - -and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac) - -and intern_tactic_seq onlytac ist = function - | TacAtom (loc,t) -> - let lf = ref ist.ltacvars in - let t = intern_atomic lf ist t in - !lf, TacAtom (adjust_loc loc, t) - | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun) - | 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) -> - (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in - ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u) - - | TacMatchGoal (lz,lr,lmr) -> - ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr) - | TacMatch (lz,c,lmr) -> - ist.ltacvars, - TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) - | TacId l -> ist.ltacvars, TacId (intern_message ist l) - | TacFail (n,l) -> - ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l) - | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) - | TacAbstract (tac,s) -> - ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s) - | TacThen (t1,[||],t2,[||]) -> - let lfun', t1 = intern_tactic_seq onlytac ist t1 in - let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in - lfun'', TacThen (t1,[||],t2,[||]) - | TacThen (t1,tf,t2,tl) -> - let lfun', t1 = intern_tactic_seq onlytac ist t1 in - let ist' = { ist with ltacvars = lfun' } in - (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *) - lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2, - Array.map (intern_pure_tactic ist') tl) - | TacThens (t,tl) -> - let lfun', t = intern_tactic_seq true ist t in - let ist' = { ist with ltacvars = lfun' } in - (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *) - lfun', TacThens (t, List.map (intern_pure_tactic ist') tl) - | TacDo (n,tac) -> - ist.ltacvars, TacDo (intern_or_var ist n,intern_pure_tactic ist tac) - | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac) - | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac) - | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) - | TacTimeout (n,tac) -> - ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) - | TacOrelse (tac1,tac2) -> - ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) - | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) - | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l) - | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac) - | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a - -and intern_tactic_as_arg loc onlytac ist a = - match intern_tacarg !strict_check onlytac ist a with - | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a) - | Tacexp a -> a - | TacVoid | IntroPattern _ | Integer _ - | ConstrMayEval _ | TacFreshId _ as a -> - if onlytac then error_tactic_expected loc else TacArg (loc,a) - | MetaIdArg _ -> assert false - -and intern_tactic_or_tacarg ist = intern_tactic false ist - -and intern_pure_tactic ist = intern_tactic true ist - -and intern_tactic_fun ist (var,body) = - let (l1,l2) = ist.ltacvars in - let lfun' = List.rev_append (Option.List.flatten var) l1 in - (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body) - -and intern_tacarg strict onlytac ist = function - | TacVoid -> TacVoid - | Reference r -> intern_non_tactic_reference strict ist r - | 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 - | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | MetaIdArg (loc,istac,s) -> - (* $id can occur in Grammar tactic... *) - let id = id_of_string s in - if find_ltacvar id ist then - if istac then Reference (ArgVar (adjust_loc loc,id)) - else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None)) - else error_syntactic_metavariables_not_allowed loc - | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f - | TacCall (loc,f,l) -> - TacCall (loc, - intern_applied_tactic_reference ist f, - List.map (intern_tacarg !strict_check false ist) l) - | TacExternal (loc,com,req,la) -> - TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) - | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) - | Tacexp t -> Tacexp (intern_tactic onlytac ist t) - | TacDynamic(loc,t) as x -> - (match Dyn.tag t with - | "tactic" | "value" -> x - | "constr" -> if onlytac then error_tactic_expected loc else x - | s -> anomaly_loc (loc, "", - str "Unknown dynamic: <" ++ str s ++ str ">")) - -(* Reads the rules of a Match Context or a Match *) -and intern_match_rule onlytac ist = function - | (All tc)::tl -> - All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) - | (Pat (rl,mp,tc))::tl -> - let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in - let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in - let ido,metas2,pat = intern_pattern ist lfun mp in - let metas = list_uniquize (metas1@metas2) in - let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in - Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) - | [] -> [] - -and intern_genarg ist x = - match genarg_tag x with - | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x) - | IntArgType -> in_gen globwit_int (out_gen rawwit_int x) - | IntOrVarArgType -> - in_gen globwit_int_or_var - (intern_or_var ist (out_gen rawwit_int_or_var x)) - | StringArgType -> - in_gen globwit_string (out_gen rawwit_string x) - | PreIdentArgType -> - in_gen globwit_pre_ident (out_gen rawwit_pre_ident x) - | IntroPatternArgType -> - let lf = ref ([],[]) in - (* how to know which names are bound by the intropattern *) - in_gen globwit_intro_pattern - (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x)) - | IdentArgType b -> - let lf = ref ([],[]) in - 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)) - | RefArgType -> - in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x)) - | SortArgType -> - in_gen globwit_sort (out_gen rawwit_sort x) - | ConstrArgType -> - in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x)) - | ConstrMayEvalArgType -> - in_gen globwit_constr_may_eval - (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x)) - | QuantHypArgType -> - in_gen globwit_quant_hyp - (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x)) - | RedExprArgType -> - in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x)) - | OpenConstrArgType (b1,b2) -> - in_gen (globwit_open_constr_gen (b1,b2)) - ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x))) - | ConstrWithBindingsArgType -> - in_gen globwit_constr_with_bindings - (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) - | BindingsArgType -> - in_gen globwit_bindings - (intern_bindings ist (out_gen rawwit_bindings x)) - | List0ArgType _ -> app_list0 (intern_genarg ist) x - | List1ArgType _ -> app_list1 (intern_genarg ist) x - | OptArgType _ -> app_opt (intern_genarg ist) x - | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x - | ExtraArgType s -> - match tactic_genarg_level s with - | Some n -> - (* Special treatment of tactic arguments *) - in_gen (globwit_tactic n) (intern_tactic_or_tacarg ist - (out_gen (rawwit_tactic n) x)) - | None -> - lookup_genarg_glob s ist x - -(************* End globalization ************) + let accu = Id.Map.map value_of_ident ln in + let accu = lfun +++ accu in + Id.Map.fold (fun id c accu -> Id.Map.add id (of_cub c) accu) lm accu (***************************************************************************) (* Evaluation/interpretation *) let is_variable env id = - List.mem id (ids_of_named_context (Environ.named_context env)) + Id.List.mem id (ids_of_named_context (Environ.named_context env)) (* Debug reference *) let debug = ref DebugOff @@ -1006,11 +292,10 @@ let set_debug pos = debug := pos (* Gives the state of debug *) let get_debug () = !debug -let debugging_step ist pp = - match ist.debug with +let debugging_step ist pp = match curr_debug ist with | DebugOn lev -> safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp () ++ fnl()) - | _ -> () + | _ -> Proofview.NonLogical.return () let debugging_exception_step ist signal_anomaly e pp = let explain_exc = @@ -1024,63 +309,40 @@ let error_ltac_variable loc id env v s = strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") -exception CannotCoerceTo of string - (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env (loc,id) = - let v = List.assoc id ist.lfun in + let v = Id.Map.find id ist.lfun in try coerce v with CannotCoerceTo s -> error_ltac_variable loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly ("Detected '" ^ (string_of_id (snd locid)) ^ "' as ltac var at interning time") - -(* 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)) -> - (* 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 env id = - try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id) + with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") + +let interp_ident_gen fresh ist env sigma id = + try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some (env,sigma)) (dloc,id) with Not_found -> id let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true -let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) -let pf_interp_fresh_ident id gl = interp_ident_gen true id (pf_env gl) +let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) (project gl) (* Interprets an optional identifier which must be fresh *) -let interp_fresh_name ist env = function +let interp_fresh_name ist env sigma = function | Anonymous -> Anonymous - | Name id -> Name (interp_fresh_ident ist env id) - -let coerce_to_intro_pattern env = function - | VIntroPattern ipat -> ipat - | 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) - | v -> raise (CannotCoerceTo "an introduction pattern") - -let interp_intro_pattern_var loc ist env id = - try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id) - with Not_found -> IntroIdentifier id + | Name id -> Name (interp_fresh_ident ist env sigma id) -let coerce_to_hint_base = function - | VIntroPattern (IntroIdentifier id) -> string_of_id id - | _ -> raise (CannotCoerceTo "a hint base name") +let interp_intro_pattern_var loc ist env sigma id = + try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id) + with Not_found -> IntroNaming (IntroIdentifier id) + +let interp_intro_pattern_naming_var loc ist env sigma id = + try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id) + with Not_found -> IntroIdentifier id let interp_hint_base ist s = - try try_interp_ltac_var coerce_to_hint_base ist None (dloc,id_of_string s) + try try_interp_ltac_var coerce_to_hint_base ist None (dloc,Id.of_string s) with Not_found -> s -let coerce_to_int = function - | VInteger n -> n - | v -> raise (CannotCoerceTo "an integer") - let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> @@ -1091,252 +353,313 @@ let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid | ArgArg n -> n -let int_or_var_list_of_VList = function - | VList l -> List.map (fun n -> ArgArg (coerce_to_int n)) l - | _ -> raise Not_found - let interp_int_or_var_as_list ist = function | ArgVar (_,id as locid) -> - (try int_or_var_list_of_VList (List.assoc id ist.lfun) + (try coerce_to_int_or_var_list (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) | ArgArg n as x -> [x] let interp_int_or_var_list ist l = List.flatten (List.map (interp_int_or_var_as_list ist) l) -let constr_of_value env = function - | VConstr csr -> csr - | 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 - | VIntroPattern (IntroIdentifier id) when is_variable env id -> id - | _ -> raise (CannotCoerceTo "a variable") - (* Interprets a bound variable (especially an existing hypothesis) *) -let interp_hyp ist gl (loc,id as locid) = - let env = pf_env gl in +let interp_hyp ist env sigma (loc,id as locid) = (* Look first in lfun for a value coercible to a variable *) - try try_interp_ltac_var (coerce_to_hyp env) ist (Some env) locid + try try_interp_ltac_var (coerce_to_hyp env) ist (Some (env,sigma)) locid with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable", - str "No such hypothesis: " ++ pr_id id ++ str ".") - -let hyp_list_of_VList env = function - | VList l -> List.map (coerce_to_hyp env) l - | _ -> raise Not_found + else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id)) -let interp_hyp_list_as_list ist gl (loc,id as x) = - try hyp_list_of_VList (pf_env gl) (List.assoc id ist.lfun) - with Not_found | CannotCoerceTo _ -> [interp_hyp ist gl x] +let interp_hyp_list_as_list ist env sigma (loc,id as x) = + try coerce_to_hyp_list env (Id.Map.find id ist.lfun) + with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] -let interp_hyp_list ist gl l = - List.flatten (List.map (interp_hyp_list_as_list ist gl) l) +let interp_hyp_list ist env sigma l = + List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l) -let interp_move_location ist gl = function - | MoveAfter id -> MoveAfter (interp_hyp ist gl id) - | MoveBefore id -> MoveBefore (interp_hyp ist gl id) - | MoveToEnd toleft as x -> x +let interp_move_location ist env sigma = function + | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id) + | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id) + | MoveFirst -> MoveFirst + | MoveLast -> MoveLast -(* Interprets a qualified name *) -let coerce_to_reference env v = - try match v with - | 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 +let interp_reference ist env sigma = function | ArgArg (_,r) -> r - | 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 - | _ -> raise (CannotCoerceTo "an inductive type") - -let interp_inductive ist = function - | ArgArg r -> r - | ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid - -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) - -> EvalVarRef id - | _ -> raise (CannotCoerceTo "an evaluable reference") - in - if not (Tacred.is_evaluable env ev) then - raise (CannotCoerceTo "an evaluable reference") - else - ev + | ArgVar (loc, id) -> + try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id) + with Not_found -> + try + let (v, _, _) = Environ.lookup_named id env in + VarRef v + with Not_found -> error_global_not_found_loc loc (qualid_of_ident id) -let interp_evaluable ist env = function +let try_interp_evaluable env (loc, id) = + let v = Environ.lookup_named id env in + match v with + | (_, Some _, _) -> EvalVarRef id + | _ -> error_not_evaluable (VarRef id) + +let interp_evaluable ist env sigma = function | ArgArg (r,Some (loc,id)) -> - (* Maybe [id] has been introduced by Intro-like tactics *) - (try match Environ.lookup_named id env with - | (_,Some _,_) -> EvalVarRef id - | _ -> error_not_evaluable (VarRef id) - with Not_found -> - match r with - | EvalConstRef _ -> r - | _ -> error_global_not_found_loc (loc,qualid_of_ident id)) + (* Maybe [id] has been introduced by Intro-like tactics *) + begin + try try_interp_evaluable env (loc, id) + with Not_found -> + match r with + | EvalConstRef _ -> r + | _ -> error_global_not_found_loc loc (qualid_of_ident id) + end | ArgArg (r,None) -> r - | ArgVar locid -> - interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid + | ArgVar (loc, id) -> + try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id) + with Not_found -> + try try_interp_evaluable env (loc, id) + with Not_found -> error_global_not_found_loc loc (qualid_of_ident id) (* Interprets an hypothesis name *) -let interp_occurrences ist (b,occs) = - (b,interp_int_or_var_list ist occs) +let interp_occurrences ist occs = + Locusops.occurrences_map (interp_int_or_var_list ist) occs + +let interp_hyp_location ist env sigma ((occs,id),hl) = + ((interp_occurrences ist occs,interp_hyp ist env sigma id),hl) -let interp_hyp_location ist gl ((occs,id),hl) = - ((interp_occurrences ist occs,interp_hyp ist gl id),hl) +let interp_hyp_location_list_as_list ist env sigma ((occs,id),hl as x) = + match occs,hl with + | AllOccurrences,InHyp -> + List.map (fun id -> ((AllOccurrences,id),InHyp)) + (interp_hyp_list_as_list ist env sigma id) + | _,_ -> [interp_hyp_location ist env sigma x] -let interp_clause ist gl { onhyps=ol; concl_occs=occs } = - { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol; +let interp_hyp_location_list ist env sigma l = + List.flatten (List.map (interp_hyp_location_list_as_list ist env sigma) l) + +let interp_clause ist env sigma { onhyps=ol; concl_occs=occs } : clause = + { onhyps=Option.map (interp_hyp_location_list ist env sigma) ol; concl_occs=interp_occurrences ist occs } (* Interpretation of constructions *) (* Extract the constr list from lfun *) 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 -> - let ido = match v with - | VIntroPattern (IntroIdentifier id0) -> Some id0 - | _ -> None in - (l1,(id,ido)::l2)) - | [] -> ([],[]) in - aux ist.lfun + let fold id v accu = + try + let c = coerce_to_constr env v in + Id.Map.add id c accu + with CannotCoerceTo _ -> accu + in + Id.Map.fold fold ist.lfun Id.Map.empty +(** ppedrot: I have changed the semantics here. Before this patch, closure was + implemented as a list and a variable could be bound several times with + different types, resulting in its possible appearance on both sides. This + could barely be defined as a feature... *) (* 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 -> + | IntroNaming (IntroIdentifier id) -> [id] + | IntroAction (IntroOrAndPattern ll) -> List.flatten (List.map intropattern_ids (List.flatten ll)) - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ + | IntroAction (IntroInjection l) -> + List.flatten (List.map intropattern_ids l) + | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat + | IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _) | IntroForthcoming _ -> [] -let rec extract_ids ids = function - | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> - intropattern_ids (dloc,ipat) @ extract_ids ids tl - | _::tl -> extract_ids ids tl - | [] -> [] +let extract_ids ids lfun = + let fold id v accu = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + let (_, ipat) = out_gen (topwit wit_intro_pattern) v in + if Id.List.mem id ids then accu + else accu @ intropattern_ids (dloc, ipat) + else accu + in + Id.Map.fold fold lfun [] -let default_fresh_id = id_of_string "H" +let default_fresh_id = Id.of_string "H" -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 interp_fresh_id ist env sigma l = + let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in + let avoid = match TacStore.get ist.extra f_avoid_ids with + | None -> [] + | Some l -> l + in + let avoid = (extract_ids ids ist.lfun) @ avoid in let id = - if l = [] then default_fresh_id + if List.is_empty l then default_fresh_id else let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> string_of_id (interp_ident ist env id)) l) in + | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in - id_of_string s in + Id.of_string s in Tactics.fresh_id_in_env avoid id env -let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl) -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 + +(* Extract the uconstr list from lfun *) +let extract_ltac_constr_context ist env = + let open Glob_term in + let add_uconstr id env v map = + try Id.Map.add id (coerce_to_uconstr env v) map + with CannotCoerceTo _ -> map + in + let add_constr id env v map = + try Id.Map.add id (coerce_to_constr env v) map + with CannotCoerceTo _ -> map + in + let add_ident id env v map = + try Id.Map.add id (coerce_to_ident false env v) map + with CannotCoerceTo _ -> map + in + let fold id v {idents;typed;untyped} = + let idents = add_ident id env v idents in + let typed = add_constr id env v typed in + let untyped = add_uconstr id env v untyped in + { idents ; typed ; untyped } + in + let empty = { idents = Id.Map.empty ;typed = Id.Map.empty ; untyped = Id.Map.empty } in + Id.Map.fold fold ist.lfun empty + +(** Significantly simpler than [interp_constr], to interpret an + untyped constr, it suffices to adjoin a closure environment. *) +let interp_uconstr ist env = function + | (term,None) -> + { closure = extract_ltac_constr_context ist env ; term } + | (_,Some ce) -> + let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env in + let ltacvars = { + Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); + ltac_bound = Id.Map.domain ist.lfun; + } in + { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } + +let interp_gen kind ist allow_patvar flags env sigma (c,ce) = + let constrvars = extract_ltac_constr_context ist env in + let vars = { + Pretyping.ltac_constrs = constrvars.typed; + Pretyping.ltac_uconstrs = constrvars.untyped; + Pretyping.ltac_idents = constrvars.idents; + Pretyping.ltac_genargs = ist.lfun; + } in let c = match ce with | None -> c (* If at toplevel (ce<>None), the error can be due to an incorrect context at globalization time: we retype with the now known intros/lettac/inversion hypothesis names *) | Some c -> - let ltacdata = (List.map fst ltacvars,unbndltacvars) in - intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c + let constr_context = + Id.Set.union + (Id.Map.domain constrvars.typed) + (Id.Set.union + (Id.Map.domain constrvars.untyped) + (Id.Map.domain constrvars.idents)) + in + let ltacvars = { + ltac_vars = constr_context; + ltac_bound = Id.Map.domain ist.lfun; + } in + intern_gen kind ~allow_patvar ~ltacvars env c in - let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in - let evdc = - catch_error trace - (understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c in + let trace = + push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in let (evd,c) = - if expand_evar then - solve_remaining_evars fail_evar use_classes - solve_by_implicit_tactic env sigma evdc - else - evdc in - db_constr ist.debug env c; + catch_error trace (understand_ltac flags env sigma vars kind) c + in + (* spiwack: to avoid unnecessary modifications of tacinterp, as this + function already use effect, I call [run] hoping it doesn't mess + up with any assumption. *) + Proofview.NonLogical.run (db_constr (curr_debug ist) env c); (evd,c) +let constr_flags = { + use_typeclasses = true; + use_unif_heuristics = true; + use_hook = Some solve_by_implicit_tactic; + fail_evar = true; + expand_evars = true } + (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = - interp_gen kind ist false true true true env sigma c + interp_gen kind ist false constr_flags env sigma c -let interp_constr = interp_constr_gen (OfType None) +let interp_constr = interp_constr_gen WithoutTypeConstraint let interp_type = interp_constr_gen IsType -(* Interprets an open constr *) -let interp_open_constr_gen kind ist = - interp_gen kind ist false true false false +let open_constr_use_classes_flags = { + use_typeclasses = true; + use_unif_heuristics = true; + use_hook = Some solve_by_implicit_tactic; + fail_evar = false; + expand_evars = true } + +let open_constr_no_classes_flags = { + use_typeclasses = false; + use_unif_heuristics = true; + use_hook = Some solve_by_implicit_tactic; + fail_evar = false; + expand_evars = true } + +let pure_open_constr_flags = { + use_typeclasses = false; + use_unif_heuristics = true; + use_hook = None; + fail_evar = false; + expand_evars = false } -(* wTC is for retrocompatibility: TC resolution started only if needed *) -let interp_open_constr ccl wTC ist e s t = - try interp_gen (OfType ccl) ist false true false (ccl<>None) e s t - with ex when Pretype_errors.precatchable_exception ex && ccl = None && wTC -> - interp_gen (OfType ccl) ist false true false true e s t +(* Interprets an open constr *) +let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist = + let flags = + if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags + else open_constr_use_classes_flags in + interp_gen expected_type ist false flags let interp_pure_open_constr ist = - interp_gen (OfType None) ist false false false false + interp_gen WithoutTypeConstraint ist false pure_open_constr_flags 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 + interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in + pattern_of_constr env sigma c (* Interprets a constr expression casted by the current goal *) let pf_interp_casted_constr ist gl c = - interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c + interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c (* Interprets a constr expression *) let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) -let constr_list_of_VList env = function - | VList l -> List.map (closed_constr_of_value env) l - | _ -> raise Not_found +let new_interp_constr ist c k = + let open Proofview in + Proofview.Goal.enter begin fun gl -> + let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) + end 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 - | GVar (_,id), _ -> - sigma, - List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) + | GVar (_,id), _ -> + let v = Id.Map.find id ist.lfun in + sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> raise Not_found - with Not_found -> - (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*) + with CannotCoerceTo _ | Not_found -> + (* dest_fun, List.assoc may raise Not_found *) 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 + let sigma, l = List.fold_map try_expand_ltac_var sigma l in sigma, List.flatten l let interp_constr_list ist env sigma c = interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_constr ist env sigma c let interp_open_constr_list = - interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (interp_open_constr None false) + interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr let interp_auto_lemmas ist env sigma lems = let local_sigma, lems = interp_open_constr_list ist env sigma lems in @@ -1347,154 +670,231 @@ let pf_interp_type ist gl = interp_type ist (pf_env gl) (project gl) (* Interprets a reduction expression *) -let interp_unfold ist env (occs,qid) = - (interp_occurrences ist occs,interp_evaluable ist env qid) +let interp_unfold ist env sigma (occs,qid) = + (interp_occurrences ist occs,interp_evaluable ist env sigma qid) -let interp_flag ist env red = - { red with rConst = List.map (interp_evaluable ist env) red.rConst } +let interp_flag ist env sigma red = + { red with rConst = List.map (interp_evaluable ist env sigma) red.rConst } -let interp_constr_with_occurrences ist sigma env (occs,c) = - let (sigma,c_interp) = interp_constr ist sigma env c in +let interp_constr_with_occurrences ist env sigma (occs,c) = + let (sigma,c_interp) = interp_constr ist env sigma c in sigma , (interp_occurrences ist occs, c_interp) -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 interp_closed_typed_pattern_with_occurrences ist env sigma occl = - snd (interp_typed_pattern_with_occurrences ist env sigma occl) +let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = + let p = match a with + | Inl b -> Inl (interp_evaluable ist env sigma b) + | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in + interp_occurrences ist occs, p 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 + (fun c -> ((AllOccurrences,c),Anonymous)) + (function ((occs,c),Anonymous) when occs == AllOccurrences -> c | _ -> raise Not_found) (fun ist env sigma (occ_c,na) -> let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in sigma, (c_interp, - interp_fresh_name ist env na)) + interp_fresh_name ist env sigma na)) -let interp_red_expr ist sigma env = function - | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env) l) +let interp_red_expr ist env sigma = function + | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l) | Fold l -> let (sigma,l_interp) = interp_constr_list ist env sigma l in sigma , Fold l_interp - | Cbv f -> sigma , Cbv (interp_flag ist env f) - | Lazy f -> sigma , Lazy (interp_flag ist env f) + | Cbv f -> sigma , Cbv (interp_flag ist env sigma f) + | Cbn f -> sigma , Cbn (interp_flag ist env sigma f) + | Lazy f -> sigma , Lazy (interp_flag ist env sigma f) | Pattern l -> - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma c in - sigma , c_interp :: acc - end l (sigma,[]) - in - sigma , Pattern l_interp - | Simpl o -> - sigma , Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) - | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> sigma , r - -let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) - -let interp_may_eval f ist gl = function + let (sigma,l_interp) = + Evd.MonadR.List.map_right + (fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma + in + sigma , Pattern l_interp + | Simpl (f,o) -> + sigma , Simpl (interp_flag ist env sigma f, + Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | CbvVm o -> + sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | CbvNative o -> + sigma , CbvNative (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> sigma , r + +let interp_may_eval f ist env sigma = function | ConstrEval (r,c) -> - let (sigma,redexp) = pf_interp_red_expr ist gl r in - let (sigma,c_interp) = f ist { gl with sigma=sigma } c in - sigma , pf_reduction_of_red_expr gl redexp c_interp + let (sigma,redexp) = interp_red_expr ist env sigma r in + let (sigma,c_interp) = f ist env sigma c in + (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp) | ConstrContext ((loc,s),c) -> (try - let (sigma,ic) = f ist gl c - and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in - sigma , subst_meta [special_meta,ic] ctxt + let (sigma,ic) = f ist env sigma c in + let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in + let evdref = ref sigma in + let c = subst_meta [Constr_matching.special_meta,ic] ctxt in + let c = Typing.solve_evars env evdref c in + !evdref , c with | Not_found -> user_err_loc (loc, "interp_may_eval", str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> - let (sigma,c_interp) = f ist gl c in - sigma , pf_type_of gl c_interp + let (sigma,c_interp) = f ist env sigma c in + Typing.e_type_of ~refresh:true env sigma c_interp | ConstrTerm c -> try - f ist gl c + f ist env sigma c with reraise -> - debugging_exception_step ist false reraise (fun () -> - str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c)); - raise reraise + let reraise = Errors.push reraise in + (* spiwack: to avoid unnecessary modifications of tacinterp, as this + function already use effect, I call [run] hoping it doesn't mess + up with any assumption. *) + Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> + str"interpretation of term " ++ pr_glob_constr_env env (fst c))); + iraise reraise (* Interprets a constr expression possibly to first evaluate *) -let interp_constr_may_eval ist gl c = +let interp_constr_may_eval ist env sigma c = let (sigma,csr) = try - interp_may_eval pf_interp_constr ist gl c + interp_may_eval interp_constr ist env sigma c with reraise -> - debugging_exception_step ist false reraise (fun () -> - str"evaluation of term"); - raise reraise + let reraise = Errors.push reraise in + (* spiwack: to avoid unnecessary modifications of tacinterp, as this + function already use effect, I call [run] hoping it doesn't mess + up with any assumption. *) + Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term")); + iraise reraise in begin - db_constr ist.debug (pf_env gl) csr; + (* spiwack: to avoid unnecessary modifications of tacinterp, as this + function already use effect, I call [run] hoping it doesn't mess + up with any assumption. *) + Proofview.NonLogical.run (db_constr (curr_debug ist) env csr); sigma , csr end -let rec message_of_value gl = function - | VVoid -> str "()" - | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) - | 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 l -> prlist_with_sep spc (message_of_value gl) l - -let rec interp_message_token ist gl = function - | MsgString s -> str s - | MsgInt n -> int n +(** TODO: should use dedicated printers *) +let rec message_of_value v = + let v = Value.normalize v in + let open Tacmach.New in + let open Ftactic in + if has_type v (topwit wit_tacvalue) then + Ftactic.return (str "<tactic>") + else if has_type v (topwit wit_constr) then + let v = out_gen (topwit wit_constr) v in + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end + else if has_type v (topwit wit_constr_under_binders) then + let c = out_gen (topwit wit_constr_under_binders) v in + Ftactic.nf_enter begin fun gl -> + Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c) + end + else if has_type v (topwit wit_unit) then + Ftactic.return (str "()") + else if has_type v (topwit wit_int) then + Ftactic.return (int (out_gen (topwit wit_int) v)) + else if has_type v (topwit wit_intro_pattern) then + let p = out_gen (topwit wit_intro_pattern) v in + let print env sigma c = pr_constr_env env sigma (snd (c env Evd.empty)) in + Ftactic.nf_enter begin fun gl -> + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p) + end + else if has_type v (topwit wit_constr_context) then + let c = out_gen (topwit wit_constr_context) v in + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end + else if has_type v (topwit wit_uconstr) then + let c = out_gen (topwit wit_uconstr) v in + Ftactic.nf_enter begin fun gl -> + Ftactic.return (pr_closed_glob_env (pf_env gl) + (Proofview.Goal.sigma gl) c) + end + else match Value.to_list v with + | Some l -> + Ftactic.List.map message_of_value l >>= fun l -> + Ftactic.return (prlist_with_sep spc (fun x -> x) l) + | None -> + let tag = pr_argument_type (genarg_tag v) in + Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) + +let interp_message_token ist = function + | MsgString s -> Ftactic.return (str s) + | MsgInt n -> Ftactic.return (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 gl v - -let rec interp_message_nl ist gl = function - | [] -> mt() - | l -> prlist_with_sep spc (interp_message_token ist gl) l ++ fnl() - -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 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, 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 (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) + let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in + match v with + | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (pr_id id ++ str" not found.")) + | Some v -> message_of_value v + +let interp_message ist l = + let open Ftactic in + Ftactic.List.map (interp_message_token ist) l >>= fun l -> + Ftactic.return (prlist_with_sep spc (fun x -> x) l) + +let interp_message ist l = + let open Ftactic in + Ftactic.List.map (interp_message_token ist) l >>= fun l -> + Ftactic.return (prlist_with_sep spc (fun x -> x) l) + +let rec interp_intro_pattern ist env sigma = function + | loc, IntroAction pat -> + let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in + sigma, (loc, IntroAction pat) + | loc, IntroNaming (IntroIdentifier id) -> + sigma, (loc, interp_intro_pattern_var loc ist env sigma id) + | loc, IntroNaming pat -> + sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env sigma pat)) + | loc, IntroForthcoming _ as x -> sigma, x + +and interp_intro_pattern_naming loc ist env sigma = function + | IntroFresh id -> IntroFresh (interp_fresh_ident ist env sigma id) + | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env sigma id + | IntroAnonymous as x -> x + +and interp_intro_pattern_action ist env sigma = function + | IntroOrAndPattern l -> + let (sigma,l) = interp_or_and_intro_pattern ist env sigma l in + sigma, IntroOrAndPattern l + | IntroInjection l -> + let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in + sigma, IntroInjection l + | IntroApplyOn (c,ipat) -> + let c = fun env sigma -> interp_constr ist env sigma c in + let sigma,ipat = interp_intro_pattern ist env sigma ipat in + sigma, IntroApplyOn (c,ipat) + | IntroWildcard | IntroRewrite _ as x -> sigma, x + +and interp_or_and_intro_pattern ist env sigma = + List.fold_map (interp_intro_pattern_list_as_list ist env) sigma + +and interp_intro_pattern_list_as_list ist env sigma = function + | [loc,IntroNaming (IntroIdentifier id)] as l -> + (try sigma, coerce_to_intro_pattern_list loc env (Id.Map.find 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) - -(* Quantified named or numbered hypothesis or hypothesis in context *) -(* (as in Inversion) *) -let coerce_to_quantified_hypothesis = function - | VInteger n -> AnonHyp n - | VIntroPattern (IntroIdentifier id) -> NamedHyp id - | v -> raise (CannotCoerceTo "a quantified hypothesis") + List.fold_map (interp_intro_pattern ist env) sigma l) + | l -> List.fold_map (interp_intro_pattern ist env) sigma l + +let interp_intro_pattern_naming_option ist env sigma = function + | None -> None + | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env sigma pat) + +let interp_or_and_intro_pattern_option ist env sigma = function + | None -> sigma, None + | Some (ArgVar (loc,id)) -> + (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with + | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) + | _ -> + raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern")) + | Some (ArgArg (loc,l)) -> + let sigma,l = interp_or_and_intro_pattern ist env sigma l in + sigma, Some (loc,l) + +let interp_intro_pattern_option ist env sigma = function + | None -> sigma, None + | Some ipat -> + let sigma, ipat = interp_intro_pattern ist env sigma ipat in + sigma, Some ipat + +let interp_in_hyp_as ist env sigma (clear,id,ipat) = + let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in + sigma,(clear,interp_hyp ist env sigma id,ipat) let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n @@ -1511,25 +911,15 @@ let interp_binding_name ist = function try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) with Not_found -> NamedHyp id -(* Quantified named or numbered hypothesis or hypothesis in context *) -(* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env = function - | VInteger n -> AnonHyp n - | v -> - try NamedHyp (coerce_to_hyp env v) - with CannotCoerceTo _ -> - raise (CannotCoerceTo "a declared or quantified hypothesis") - -let interp_declared_or_quantified_hypothesis ist gl = function +let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> - let env = pf_env gl in try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) + (coerce_to_decl_or_quant_hyp env) ist (Some (env,sigma)) (dloc,id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,b,c) = - let sigma, c = interp_open_constr None false ist env sigma c in + let sigma, c = interp_open_constr ist env sigma c in sigma, (loc,interp_binding_name ist b,c) let interp_bindings ist env sigma = function @@ -1539,63 +929,85 @@ let interp_bindings ist env sigma = function 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 + 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 false ist env sigma c in + let sigma, c = interp_open_constr ist env sigma c in sigma, (c,bl) -let interp_open_constr_with_bindings wTC ist env sigma (c,bl) = +let interp_constr_with_bindings_arg ist env sigma (keep,c) = + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, (keep,c) + +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 wTC ist env sigma c in + let sigma, c = interp_open_constr ist env sigma c in sigma, (c, bl) +let interp_open_constr_with_bindings_arg ist env sigma (keep,c) = + let sigma, c = interp_open_constr_with_bindings ist env sigma c in + sigma,(keep,c) + let loc_of_bindings = function -| NoBindings -> dummy_loc -| ImplicitBindings l -> loc_of_glob_constr (fst (list_last l)) -| ExplicitBindings l -> pi1 (list_last l) +| NoBindings -> Loc.ghost +| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) +| ExplicitBindings l -> pi1 (List.last l) -let interp_open_constr_with_bindings_loc wTC ist env sigma ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr 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 wTC ist env sigma cb in - sigma, (loc,cb) + let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in + let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + (loc,f) let interp_induction_arg ist gl arg = - let env = pf_env gl and sigma = project gl in match arg with - | ElimOnConstr c -> - ElimOnConstr (interp_constr_with_bindings ist env sigma c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) -> + | keep,ElimOnConstr c -> + keep,ElimOnConstr (fun env sigma -> interp_constr_with_bindings ist env sigma c) + | keep,ElimOnAnonHyp n as x -> x + | keep,ElimOnIdent (loc,id) -> + let error () = user_err_loc (loc, "", + strbrk "Cannot coerce " ++ pr_id id ++ + strbrk " neither to a quantified hypothesis nor to a term.") + in + let try_cast_id id' = + if Tactics.is_quantified_hypothesis id' gl + then keep,ElimOnIdent (loc,id') + else + (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings)) + with Not_found -> + user_err_loc (loc,"", + pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")) + in try - match List.assoc id ist.lfun with - | VInteger n -> - ElimOnAnonHyp n - | VIntroPattern (IntroIdentifier id') -> - if Tactics.is_quantified_hypothesis id' gl - then ElimOnIdent (loc,id') - else - (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings)) - with Not_found -> - user_err_loc (loc,"", - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")) - | VConstr ([],c) -> - ElimOnConstr (sigma,(c,NoBindings)) - | _ -> user_err_loc (loc,"", - strbrk "Cannot coerce " ++ pr_id id ++ - strbrk " neither to a quantified hypothesis nor to a term.") + (** FIXME: should be moved to taccoerce *) + let v = Id.Map.find id ist.lfun in + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + let v = out_gen (topwit wit_intro_pattern) v in + match v with + | _, IntroNaming (IntroIdentifier id) -> try_cast_id id + | _ -> error () + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + try_cast_id id + else if has_type v (topwit wit_int) then + keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) + else match Value.to_constr v with + | None -> error () + | Some c -> keep,ElimOnConstr (fun env sigma -> sigma,(c,NoBindings)) with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - ElimOnIdent (loc,id) + keep,ElimOnIdent (loc,id) else - let c = (GVar (loc,id),Some (CRef (Ident (loc,id)))) in - let (sigma,c) = interp_constr ist env sigma c in - ElimOnConstr (sigma,(c,NoBindings)) + let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in + let f env sigma = + let (sigma,c) = interp_open_constr ist env sigma c in + sigma,(c,NoBindings) in + keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and values *) @@ -1609,12 +1021,11 @@ let head_with_value (lvar,lval) = | (vr,[]) -> (lacc,vr,[]) | ([],ve) -> (lacc,[],ve) in - head_with_value_rec [] (lvar,lval) + 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] +(** [interp_context ctxt] interprets a context (as in + {!Matching.matching_result}) into a context value of Ltac. *) +let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt (* Reads a pattern by substituting vars of lfun *) let use_types = false @@ -1623,7 +1034,7 @@ 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 + instantiate_pattern env 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) @@ -1631,9 +1042,9 @@ let read_pattern lfun ist env sigma = function (* Reads the hypotheses of a Match Context rule *) let cons_and_check_name id l = - if List.mem id l then + if Id.List.mem id l then user_err_loc (dloc,"read_match_goal_hyps", - strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ + strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^ " used twice in the same pattern.")) else id::l @@ -1656,1532 +1067,1267 @@ let rec read_match_rule lfun ist env sigma = function :: 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 = let (sigma,c_interp) = pf_interp_constr ist gl c in - sigma,VConstr ([],c_interp) -let mk_open_constr_value wTC ist gl c = - let (sigma,c_interp) = pf_apply (interp_open_constr None wTC ist) gl c in - sigma,VConstr ([],c_interp) -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} + sigma, Value.of_constr c_interp +let mk_open_constr_value ist gl c = + let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in + sigma, Value.of_constr c_interp +let mk_hyp_value ist env sigma c = + Value.of_constr (mkVar (interp_hyp ist env sigma c)) +let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c) -let extend_gl_hyps { it=gl ; sigma=sigma } sign = - Goal.V82.new_goal_with sigma gl sign +let pack_sigma (sigma,c) = {it=c;sigma=sigma;} (* Interprets an l-tac expression into a value *) -let rec val_interp ist gl (tac:glob_tactic_expr) = +let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : typed_generic_argument Ftactic.t = + (* The name [appl] of applied top-level Ltac names is ignored in + [value_interp]. It is installed in the second step by a call to + [name_vfun], because it gives more opportunities to detect a + [VFun]. Otherwise a [Ltac t := let x := .. in tac] would never + register its name since it is syntactically a let, not a + function. *) let value_interp ist = match tac with - (* Immediate evaluation *) - | TacFun (it,body) -> project gl , 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 - | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr - | TacArg (loc,a) -> interp_tacarg ist gl a - (* Delayed evaluation *) - | t -> project gl , VFun (ist.trace,ist.lfun,[],t) - - in check_for_interrupt (); - match ist.debug with - | DebugOn lev -> - debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v}) - | _ -> value_interp ist - -and eval_tactic ist = function + | TacFun (it, body) -> + Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, it, body))) + | TacLetIn (true,l,u) -> interp_letrec ist l u + | TacLetIn (false,l,u) -> interp_letin ist l u + | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr + | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr + | TacArg (loc,a) -> interp_tacarg ist a + | t -> + (** Delayed evaluation *) + Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t))) + in + let open Ftactic in + Control.check_for_interrupt (); + match curr_debug ist with + | DebugOn lev -> + let eval v = + let ist = { ist with extra = TacStore.set ist.extra f_debug v } in + value_interp ist >>= fun v -> return (name_vfun appl v) + in + Ftactic.debug_prompt lev tac eval + | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) + + +and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> - fun gl -> - let box = ref None in abstract_tactic_box := box; - let call = LtacAtomCall (t,box) in - let tac = (* catch error in the interpretation *) - catch_error (push_trace(dloc,call)ist.trace) - (interp_atomic ist gl) t in - (* catch error in the evaluation *) - catch_error (push_trace(loc,call)ist.trace) tac gl + let call = LtacAtomCall t in + catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t) | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false - | TacId s -> fun gl -> - let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in - db_breakpoint ist.debug s; res - | 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) + | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) + | TacId s -> + let msgnl = + let open Ftactic in + interp_message ist s >>= fun msg -> + return (hov 0 msg , hov 0 msg) + in + let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in + let log (msg,_) = Proofview.Trace.log (fun () -> msg) in + let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in + Ftactic.run msgnl begin fun msgnl -> + print msgnl <*> log msgnl <*> break + end + | TacFail (g,n,s) -> + let msg = interp_message ist s in + let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in + let tac = + match g with + | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l) + | TacGlobal -> tac + in + Ftactic.run msg tac + | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) + | TacShowHyps tac -> + Proofview.V82.tactic begin + tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) + end | TacAbstract (tac,ido) -> - fun gl -> Tactics.tclABSTRACT - (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl - | TacThen (t1,tf,t,tl) -> - tclTHENS3PARTS (interp_tactic ist t1) + Proofview.Goal.nf_enter begin fun gl -> Tactics.tclABSTRACT + (Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac) + end + | TacThen (t1,t) -> + Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) + | TacDispatch tl -> + Proofview.tclDISPATCH (List.map (interp_tactic ist) tl) + | TacExtendTac (tf,t,tl) -> + Proofview.tclEXTEND (Array.map_to_list (interp_tactic ist) tf) + (interp_tactic ist t) + (Array.map_to_list (interp_tactic ist) tl) + | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) + | TacThens3parts (t1,tf,t,tl) -> + Tacticals.New.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) - | TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) - | TacTry tac -> tclTRY (interp_tactic ist tac) - | TacRepeat tac -> tclREPEAT (interp_tactic ist tac) + | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTime (s,tac) -> Tacticals.New.tclTIME s (interp_tactic ist tac) + | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) + | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) + | TacOr (tac1,tac2) -> + Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacOnce tac -> + Tacticals.New.tclONCE (interp_tactic ist tac) + | TacExactlyOnce tac -> + Tacticals.New.tclEXACTLY_ONCE (interp_tactic ist tac) + | TacIfThenCatch (t,tt,te) -> + Tacticals.New.tclIFCATCH + (interp_tactic ist t) + (fun () -> interp_tactic ist tt) + (fun () -> interp_tactic ist te) | TacOrelse (tac1,tac2) -> - tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) - | 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) + Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) + | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) + | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> msg_warning - (str "The general \"info\" tactic is currently not working.\n" ++ - str "Some specific verbose tactics may exist instead, such as\n" ++ - str "info_trivial, info_auto, info_eauto."); + (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ + strbrk "There is an \"Info\" command to replace it." ++fnl () ++ + strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto."); eval_tactic ist tac - -and force_vrec ist gl = function - | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body - | v -> project gl , v - -and interp_ltac_reference loc' mustbetac ist gl = function + (* For extensions *) + | TacAlias (loc,s,l) -> + let body = Tacenv.interp_alias s in + let rec f x = match genarg_tag x with + | QuantHypArgType | RedExprArgType + | ConstrWithBindingsArgType + | BindingsArgType + | OptArgType _ | PairArgType _ -> (** generic handler *) + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let goal = Proofview.Goal.goal gl in + let (sigma, arg) = interp_genarg ist env sigma concl goal x in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg) + end + | _ as tag -> (** Special treatment. TODO: use generic handler *) + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + match tag with + | IntOrVarArgType -> + Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) + | IdentArgType -> + Ftactic.return (value_of_ident (interp_fresh_ident ist env sigma + (out_gen (glbwit wit_ident) x))) + | VarArgType -> + Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x)) + | GenArgType -> f (out_gen (glbwit wit_genarg) x) + | ConstrArgType -> + let (sigma,v) = + Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl + in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) + | OpenConstrArgType -> + let (sigma,v) = + Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) + | ConstrMayEvalArgType -> + let (sigma,c_interp) = + interp_constr_may_eval ist env sigma + (out_gen (glbwit wit_constr_may_eval) x) + in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + | ListArgType ConstrArgType -> + let wit = glbwit (wit_list wit_constr) in + let (sigma,l_interp) = Tacmach.New.of_old begin fun gl -> + Evd.MonadR.List.map_right + (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c) + (out_gen wit x) + (project gl) + end gl in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) + | ListArgType VarArgType -> + let wit = glbwit (wit_list wit_var) in + Ftactic.return ( + let ans = List.map (mk_hyp_value ist env sigma) (out_gen wit x) in + in_gen (topwit (wit_list wit_genarg)) ans + ) + | ListArgType IntOrVarArgType -> + let wit = glbwit (wit_list wit_int_or_var) in + let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in + Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + | ListArgType IdentArgType -> + let wit = glbwit (wit_list wit_ident) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env sigma x) in + let ans = List.map mk_ident (out_gen wit x) in + Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + | ListArgType t -> + let open Ftactic in + let list_unpacker wit l = + let map x = + f (in_gen (glbwit wit) x) >>= fun v -> + Ftactic.return (out_gen (topwit wit) v) + in + Ftactic.List.map map (glb l) >>= fun l -> + Ftactic.return (in_gen (topwit (wit_list wit)) l) + in + list_unpack { list_unpacker } x + | ExtraArgType _ -> + (** Special treatment of tactics *) + if has_type x (glbwit wit_tactic) then + let tac = out_gen (glbwit wit_tactic) x in + val_interp ist tac + else + let goal = Proofview.Goal.goal gl in + let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in + Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v) + | _ -> assert false + end + in + let (>>=) = Ftactic.bind in + let interp_vars = + Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l + in + let addvar (x, v) accu = Id.Map.add x v accu in + let tac l = + let lfun = List.fold_right addvar l ist.lfun in + let trace = push_trace (loc,LtacNotationCall s) ist in + let ist = { + lfun = lfun; + extra = TacStore.set ist.extra f_trace trace; } in + val_interp ist body >>= fun v -> + Ftactic.lift (tactic_of_value ist v) + in + let tac = + Ftactic.with_env interp_vars >>= fun (env,l) -> + let name () = Pptactic.pr_tactic env (TacAlias(loc,s,l)) in + Proofview.Trace.name_tactic name (tac l) + (* spiwack: this use of name_tactic is not robust to a + change of implementation of [Ftactic]. In such a situation, + some more elaborate solution will have to be used. *) + in + Ftactic.run tac (fun () -> Proofview.tclUNIT ()) + + | TacML (loc,opn,l) when List.for_all global_genarg l -> + let trace = push_trace (loc,LtacMLCall tac) ist in + let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in + (* spiwack: a special case for tactics (from TACTIC EXTEND) when + every argument can be interpreted without a + [Proofview.Goal.nf_enter]. *) + let tac = Tacenv.interp_ml_tactic opn in + (* dummy values, will be ignored *) + let env = Environ.empty_env in + let sigma = Evd.empty in + let concl = Term.mkRel (-1) in + let goal = Evar.unsafe_of_int (-1) in + (* /dummy values *) + let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in + let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in + Proofview.Trace.name_tactic name + (catch_error_tac trace (tac args ist)) + | TacML (loc,opn,l) -> + let trace = push_trace (loc,LtacMLCall tac) ist in + let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let goal_sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let goal = Proofview.Goal.goal gl in + let tac = Tacenv.interp_ml_tactic opn in + let (sigma,args) = + Evd.MonadR.List.map_right + (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma + in + Proofview.Unsafe.tclEVARS sigma <*> + let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in + Proofview.Trace.name_tactic name + (catch_error_tac trace (tac args ist)) + end + +and force_vrec ist v : typed_generic_argument Ftactic.t = + let v = Value.normalize v in + if has_type v (topwit wit_tacvalue) then + let v = to_tacvalue v in + match v with + | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body + | v -> Ftactic.return (of_tacvalue v) + else Ftactic.return v + +and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic.t = + match r with | ArgVar (loc,id) -> - let v = List.assoc id ist.lfun in - let (sigma,v) = force_vrec ist gl v in + let v = + try Id.Map.find id ist.lfun + with Not_found -> in_gen (topwit wit_var) id + in + Ftactic.bind (force_vrec ist v) begin fun v -> let v = propagate_trace ist loc id v in - sigma , if mustbetac then coerce_to_tactic loc id v else v + if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v + end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in - let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in - let ist = - { lfun=[]; debug=ist.debug; avoid_ids=ids; - trace = push_trace loc_info ist.trace } in - val_interp ist gl (lookup r) - -and interp_tacarg ist gl arg = - let evdref = ref (project gl) in - let v = match arg with - | TacVoid -> VVoid - | Reference r -> - let (sigma,v) = interp_ltac_reference dloc false ist gl r in - evdref := sigma; - v - | Integer n -> VInteger n - | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat)) - | ConstrMayEval c -> - let (sigma,c_interp) = interp_constr_may_eval ist gl c in - evdref := sigma; - VConstr ([],c_interp) - | MetaIdArg (loc,_,id) -> assert false - | TacCall (loc,r,[]) -> - let (sigma,v) = interp_ltac_reference loc true ist gl r in - evdref := sigma; - v - | TacCall (loc,f,l) -> - let (sigma,fv) = interp_ltac_reference loc true ist gl f in - let (sigma,largs) = - List.fold_right begin fun a (sigma',acc) -> - let (sigma', a_interp) = interp_tacarg ist gl a in - sigma' , a_interp::acc - end l (sigma,[]) - in - List.iter check_is_value largs; - let (sigma,v) = interp_app loc ist { gl with sigma=sigma } fv largs in - evdref:= sigma; - v - | TacExternal (loc,com,req,la) -> - let (sigma,la_interp) = - List.fold_right begin fun a (sigma,acc) -> - let (sigma,a_interp) = interp_tacarg ist {gl with sigma=sigma} a in - sigma , a_interp::acc - end la (project gl,[]) - in - let (sigma,v) = interp_external loc ist { gl with sigma=sigma } com req la_interp in - evdref := sigma; - v - | TacFreshId l -> - let id = pf_interp_fresh_id ist gl l in - VIntroPattern (IntroIdentifier id) - | Tacexp t -> - let (sigma,v) = val_interp ist gl t in - evdref := sigma; - v - | TacDynamic(_,t) -> - let tg = (Dyn.tag t) in - if tg = "tactic" then - let (sigma,v) = val_interp ist gl (tactic_out t ist) in - evdref := sigma; - v - else if tg = "value" then - value_out t - else if tg = "constr" then - VConstr ([],constr_out t) - else - anomaly_loc (dloc, "Tacinterp.val_interp", - (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) - in - !evdref , v + let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in + let extra = TacStore.set ist.extra f_avoid_ids ids in + let extra = TacStore.set extra f_trace (push_trace loc_info ist) in + let ist = { lfun = Id.Map.empty; extra = extra; } in + let appl = GlbAppl[r,[]] in + val_interp ~appl ist (Tacenv.interp_ltac r) + +and interp_tacarg ist arg : typed_generic_argument Ftactic.t = + match arg with + | TacGeneric arg -> + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let goal = Proofview.Goal.goal gl in + let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) + end + | Reference r -> interp_ltac_reference dloc false ist r + | ConstrMayEval c -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + end + | UConstr c -> + Ftactic.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Ftactic.return (Value.of_uconstr (interp_uconstr ist env c)) + end + | MetaIdArg (loc,_,id) -> assert false + | TacCall (loc,r,[]) -> + interp_ltac_reference loc true ist r + | TacCall (loc,f,l) -> + let (>>=) = Ftactic.bind in + interp_ltac_reference loc true ist f >>= fun fv -> + Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> + interp_app loc ist fv largs + | TacFreshId l -> + Ftactic.enter begin fun gl -> + let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in + Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) + end + | TacPretype c -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let {closure;term} = interp_uconstr ist env c in + let vars = { + Pretyping.ltac_constrs = closure.typed; + Pretyping.ltac_uconstrs = closure.untyped; + Pretyping.ltac_idents = closure.idents; + Pretyping.ltac_genargs = ist.lfun; + } in + let (sigma,c_interp) = + Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term + in + Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) + end + | TacNumgoals -> + Ftactic.lift begin + let open Proofview.Notations in + Proofview.numgoals >>= fun i -> + Proofview.tclUNIT (Value.of_int i) + end + | Tacexp t -> val_interp ist t + | TacDynamic(_,t) -> + let tg = (Dyn.tag t) in + if String.equal tg "tactic" then + val_interp ist (tactic_out t ist) + else if String.equal tg "value" then + Ftactic.return (value_out t) + else if String.equal tg "constr" then + Ftactic.return (Value.of_constr (constr_out t)) + else + Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" + (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">") (* Interprets an application node *) -and interp_app loc ist gl fv largs = - match fv with +and interp_app loc ist fv largs : typed_generic_argument Ftactic.t = + let (>>=) = Ftactic.bind in + let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in + let fv = Value.normalize fv in + if has_type fv (topwit wit_tacvalue) then + match to_tacvalue fv with (* 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), + | (VFun(appl,trace,olfun,(_::_ as var),body) + |VFun(appl,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 (sigma,v) = - try - catch_error trace - (val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body - with reraise -> - debugging_exception_step ist false reraise - (fun () -> str "evaluation"); - raise reraise - in - let gl = { gl with sigma=sigma } in + let (extfun,lvar,lval)=head_with_value (var,largs) in + let fold accu (id, v) = Id.Map.add id v accu in + let newlfun = List.fold_left fold olfun extfun in + if List.is_empty lvar then + begin Proofview.tclORELSE + begin + let ist = { + lfun = newlfun; + extra = TacStore.set ist.extra f_trace []; } in + catch_error_tac trace (val_interp ist body) >>= fun v -> + Ftactic.return (name_vfun (push_appl appl largs) v) + end + begin fun (e, info) -> + Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*> + Proofview.tclZERO ~info e + end + end >>= fun v -> + (* No errors happened, we propagate the trace *) + let v = append_trace trace v in + Proofview.tclLIFT begin debugging_step ist (fun () -> - str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v); - if lval=[] then sigma,v else interp_app loc ist gl v lval - else - project gl , VFun(trace,newlfun@olfun,lvar,body) - | _ -> - user_err_loc (loc, "Tacinterp.interp_app", - (str"Illegal tactic application.")) + str"evaluation returns"++fnl()++pr_value None v) + end <*> + if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval + else + Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body))) + | _ -> fail + else fail (* Gives the tactic corresponding to the tactic value *) -and tactic_of_value ist vle g = - match vle with - | VRTactic res -> res - | VFun (trace,lfun,[],t) -> - let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in - catch_error trace tac g - | (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 = - try - let (sigma,v) = val_interp ist goal tac in - sigma , - (match v with - | VFun (trace,lfun,[],t) when not is_lazy -> - let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in - VRTactic (catch_error trace tac { goal with sigma=sigma }) - | a -> a) - with - | FailError (0,s) | Loc.Exc_located(_, FailError (0,s)) - | Loc.Exc_located(_,LtacLocated (_,FailError (0,s))) -> - raise (Eval_fail (Lazy.force s)) - | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Loc.Exc_located(s,FailError (lvl,s')) -> - raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) - | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> - raise (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) +and tactic_of_value ist vle = + let vle = Value.normalize vle in + if has_type vle (topwit wit_tacvalue) then + match to_tacvalue vle with + | VFun (appl,trace,lfun,[],t) -> + let ist = { + lfun = lfun; + extra = TacStore.set ist.extra f_trace []; } in + let tac = name_if_glob appl (eval_tactic ist t) in + catch_error_tac trace tac + | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected.")) + else if has_type vle (topwit wit_tactic) then + let tac = out_gen (topwit wit_tactic) vle in + eval_tactic ist tac + else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic.")) (* Interprets the clauses of a recursive LetIn *) -and interp_letrec ist gl llc u = +and interp_letrec ist llc u = + Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in - lref := lve@ist.lfun; - let ist = { ist with lfun = lve@ist.lfun } in - val_interp ist gl u + let fold accu ((_, id), b) = + let v = of_tacvalue (VRec (lref, TacArg (dloc, b))) in + Id.Map.add id v accu + in + let lfun = List.fold_left fold ist.lfun llc in + let () = lref := lfun in + let ist = { ist with lfun } in + val_interp ist u (* Interprets the clauses of a LetIn *) -and interp_letin ist gl llc u = - let (sigma,lve) = - List.fold_right begin fun ((_,id),body) (sigma,acc) -> - let (sigma,v) = interp_tacarg ist { gl with sigma=sigma } body in - check_is_value v; - sigma, (id,v)::acc - end llc (project gl,[]) +and interp_letin ist llc u = + let rec fold lfun = function + | [] -> + let ist = { ist with lfun } in + val_interp ist u + | ((_, id), body) :: defs -> + Ftactic.bind (interp_tacarg ist body) (fun v -> + fold (Id.Map.add id v lfun) defs) in - let ist = { ist with lfun = lve@ist.lfun } in - val_interp ist { gl with sigma=sigma } u + fold ist.lfun llc + +(** [interp_match_success lz ist succ] interprets a single matching success + (of type {!Tactic_matching.t}). *) +and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = + let (>>=) = Ftactic.bind in + let lctxt = Id.Map.map interp_context context in + let hyp_subst = Id.Map.map Value.of_constr terms in + let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in + let ist = { ist with lfun } in + val_interp ist lhs >>= fun v -> + if has_type v (topwit wit_tacvalue) then match to_tacvalue v with + | VFun (appl,trace,lfun,[],t) -> + let ist = { + lfun = lfun; + extra = TacStore.set ist.extra f_trace trace; } in + let tac = eval_tactic ist t in + let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in + catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) + | _ -> Ftactic.return v + else Ftactic.return v + + +(** [interp_match_successes lz ist s] interprets the stream of + matching of successes [s]. If [lz] is set to true, then only the + first success is considered, otherwise further successes are tried + if the left-hand side fails. *) +and interp_match_successes lz ist s = + let general = + let break (e, info) = match e with + | FailError (0, _) -> None + | FailError (n, s) -> Some (FailError (pred n, s), info) + | _ -> None + in + Proofview.tclBREAK break s >>= fun ans -> interp_match_success ist ans + in + match lz with + | General -> + general + | Select -> + begin + (** Only keep the first matching result, we don't backtrack on it *) + let s = Proofview.tclONCE s in + s >>= fun ans -> interp_match_success ist ans + end + | Once -> + (** Once a tactic has succeeded, do not backtrack anymore *) + Proofview.tclONCE general + +(* Interprets the Match expressions *) +and interp_match ist lz constr lmr = + let (>>=) = Ftactic.bind in + begin Proofview.tclORELSE + (interp_ltac_constr ist constr) + begin function + | (e, info) -> + Proofview.tclLIFT (debugging_exception_step ist true e + (fun () -> str "evaluation of the matched expression")) <*> + Proofview.tclZERO ~info e + end + end >>= fun constr -> + Ftactic.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in + interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) + end (* Interprets the Match Context expressions *) -and interp_match_goal ist goal lz lr lmr = - let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in - let goal = { it = gl ; sigma = sigma } in - let hyps = pf_hyps goal in - let hyps = if lr then List.rev hyps else hyps in - let concl = pf_concl goal in - let env = pf_env goal in - let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps = - 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 (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 = - begin - if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); - match lpt with - | (All t)::tl -> - begin - db_mc_pattern_success ist.debug; - try eval_with_fail ist lz goal t - with e when is_match_catchable e -> - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl - end - | (Pat (mhyps,mgoal,mt))::tl -> - let mhyps = List.rev mhyps (* Sens naturel *) in - (match mgoal with - | Term mg -> - (try - let lmatch = extended_matches mg concl in - db_matched_concl ist.debug env concl; - apply_hyps_context ist env lz goal mt [] lmatch mhyps hyps - with e when is_match_catchable e -> - (match e with - | PatternMatchingFailure -> db_matching_failure ist.debug - | Eval_fail s -> db_eval_failure ist.debug s - | _ -> db_logic_failure ist.debug e); - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl) - | Subterm (b,id,mg) -> - (try apply_goal_sub b ist (id,mg) concl mt mhyps hyps - with - | PatternMatchingFailure -> - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)) - | _ -> - errorlabstrm "Tacinterp.apply_match_goal" - (v 0 (str "No matching clauses for match goal" ++ - (if ist.debug=DebugOff then - fnl() ++ str "(use \"Set Ltac Debug\" for more info)" - else mt()) ++ str".")) - end in - apply_match_goal ist env goal 0 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 = - let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function - | hyp_pat::tl -> - let (hypname, _, _ as hyp_pat) = - match hyp_pat with - | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp - | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp - in - let rec match_next_pattern find_next = - let (lids,lm,hyp_match,find_next') = find_next () in - db_matched_hyp ist.debug (pf_env goal) hyp_match hypname; - try - 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 -> - match_next_pattern find_next' in - let init_match_pattern () = - apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in - match_next_pattern init_match_pattern - | [] -> - let lfun = extend_values_with_bindings lmatch (lfun@ist.lfun) in - db_mc_pattern_success ist.debug; - eval_with_fail {ist with lfun=lfun} lz goal mt - in - apply_hyps_context_rec lctxt lgmatch hyps mhyps - -and interp_external loc ist gl com req la = - let f ch = extern_request ch req gl la in - let g ch = internalise_tacarg ch in - interp_tacarg ist gl (System.connect f g com) - - (* Interprets extended tactic generic arguments *) -and interp_genarg ist gl x = - let evdref = ref (project gl) in - let rec interp_genarg ist gl x = - let gl = { gl with sigma = !evdref } in +and interp_match_goal ist lz lr lmr = + Ftactic.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let hyps = Proofview.Goal.hyps gl in + let hyps = if lr then List.rev hyps else hyps in + let concl = Proofview.Goal.concl gl in + let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in + interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) + end + +(* Interprets extended tactic generic arguments *) +(* spiwack: interp_genarg has an argument [concl] for the case of + "casted open constr". And [gl] for [Geninterp]. I haven't changed + the interface for geninterp yet as it is used by ARGUMENT EXTEND + (in turn used by plugins). At the time I'm writing this comment + though, the only concerned plugins are the declarative mode (which + needs the [extra] field of goals to interprete rules) and ssreflect + (a handful of time). I believe we'd need to address "casted open + constr" and the declarative mode rules to provide a reasonable + interface. *) +and interp_genarg ist env sigma concl gl x = + let evdref = ref sigma in + let rec interp_genarg x = match genarg_tag x with - | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x) - | IntArgType -> in_gen wit_int (out_gen globwit_int x) | IntOrVarArgType -> - in_gen wit_int_or_var - (ArgArg (interp_int_or_var ist (out_gen globwit_int_or_var x))) - | StringArgType -> - in_gen wit_string (out_gen globwit_string x) - | PreIdentArgType -> - in_gen wit_pre_ident (out_gen globwit_pre_ident x) - | IntroPatternArgType -> - in_gen wit_intro_pattern - (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) - | IdentArgType b -> - in_gen (wit_ident_gen b) - (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) + in_gen (topwit wit_int_or_var) + (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) + | IdentArgType -> + in_gen (topwit wit_ident) + (interp_fresh_ident ist env sigma (out_gen (glbwit wit_ident) 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 (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x)) + | GenArgType -> + in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x)) + | ConstrArgType -> let (sigma,c_interp) = - pf_interp_constr ist gl - (GSort (dloc,out_gen globwit_sort x), None) + interp_constr ist env !evdref (out_gen (glbwit wit_constr) x) in evdref := sigma; - in_gen wit_sort - (destSort c_interp) - | ConstrArgType -> - let (sigma,c_interp) = pf_interp_constr ist gl (out_gen globwit_constr x) in - evdref := sigma; - in_gen wit_constr c_interp + in_gen (topwit wit_constr) c_interp | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in + let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (out_gen (glbwit wit_constr_may_eval) x) in evdref := sigma; - in_gen wit_constr_may_eval c_interp + in_gen (topwit wit_constr_may_eval) c_interp | QuantHypArgType -> - in_gen wit_quant_hyp - (interp_declared_or_quantified_hypothesis ist gl - (out_gen globwit_quant_hyp x)) + in_gen (topwit wit_quant_hyp) + (interp_declared_or_quantified_hypothesis ist env sigma + (out_gen (glbwit wit_quant_hyp) x)) | RedExprArgType -> - let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in + let (sigma,r_interp) = + interp_red_expr ist env !evdref (out_gen (glbwit wit_red_expr) x) + in evdref := sigma; - in_gen wit_red_expr r_interp - | OpenConstrArgType (casted,wTC) -> - in_gen (wit_open_constr_gen (casted,wTC)) - (interp_open_constr (if casted then Some (pf_concl gl) else None) wTC - ist (pf_env gl) (project gl) - (snd (out_gen (globwit_open_constr_gen (casted,wTC)) x))) + in_gen (topwit wit_red_expr) r_interp + | OpenConstrArgType -> + let expected_type = WithoutTypeConstraint in + in_gen (topwit wit_open_constr) + (interp_open_constr ~expected_type + ist env !evdref + (snd (out_gen (glbwit wit_open_constr) x))) | ConstrWithBindingsArgType -> - in_gen wit_constr_with_bindings - (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) - (out_gen globwit_constr_with_bindings x))) + in_gen (topwit wit_constr_with_bindings) + (pack_sigma (interp_constr_with_bindings ist env !evdref + (out_gen (glbwit wit_constr_with_bindings) x))) | BindingsArgType -> - in_gen wit_bindings - (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x))) - | List0ArgType ConstrArgType -> - let (sigma,v) = interp_genarg_constr_list0 ist gl x in - evdref := sigma; - v - | List1ArgType ConstrArgType -> - let (sigma,v) = interp_genarg_constr_list1 ist gl x in + in_gen (topwit wit_bindings) + (pack_sigma (interp_bindings ist env !evdref (out_gen (glbwit wit_bindings) x))) + | ListArgType ConstrArgType -> + let (sigma,v) = interp_genarg_constr_list ist env !evdref x in evdref := sigma; v - | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x - | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x - | List0ArgType _ -> app_list0 (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 + | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x + | ListArgType _ -> + let list_unpacker wit l = + let map x = + out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) + in + in_gen (topwit (wit_list wit)) (List.map map (glb l)) + in + list_unpack { list_unpacker } x + | OptArgType _ -> + let opt_unpacker wit o = match glb o with + | None -> in_gen (topwit (wit_opt wit)) None + | Some x -> + let x = out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) in + in_gen (topwit (wit_opt wit)) (Some x) + in + opt_unpack { opt_unpacker } x + | PairArgType _ -> + let pair_unpacker wit1 wit2 o = + let (p, q) = glb o in + let p = out_gen (topwit wit1) (interp_genarg (in_gen (glbwit wit1) p)) in + let q = out_gen (topwit wit2) (interp_genarg (in_gen (glbwit wit2) q)) in + in_gen (topwit (wit_pair wit1 wit2)) (p, q) + in + pair_unpack { pair_unpacker } x | ExtraArgType s -> - match tactic_genarg_level s with - | Some n -> - (* Special treatment of tactic arguments *) - in_gen (wit_tactic n) - (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[], - out_gen (globwit_tactic n) x)))) - | None -> - let (sigma,v) = lookup_interp_genarg s ist gl x in + let (sigma,v) = Geninterp.generic_interp ist { Evd.it=gl;sigma=(!evdref) } x in evdref:=sigma; v in - let v = interp_genarg ist gl x in + let v = interp_genarg x in !evdref , v -and interp_genarg_constr_list0 ist gl x = - let lc = out_gen (wit_list0 globwit_constr) x in - let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in - sigma , 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 (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in - sigma , in_gen (wit_list1 wit_constr) lc +(** returns [true] for genargs which have the same meaning + independently of goals. *) -and interp_genarg_var_list0 ist gl x = - let lc = out_gen (wit_list0 globwit_var) x in - let lc = interp_hyp_list ist gl lc in - in_gen (wit_list0 wit_var) lc +and global_genarg = + let rec global_tag = function + | IntOrVarArgType | GenArgType -> true + | ListArgType t | OptArgType t -> global_tag t + | PairArgType (t1,t2) -> global_tag t1 && global_tag t2 + | _ -> false + in + fun x -> global_tag (genarg_tag x) -and interp_genarg_var_list1 ist gl x = - let lc = out_gen (wit_list1 globwit_var) x in - let lc = interp_hyp_list ist gl lc in - in_gen (wit_list1 wit_var) lc +and interp_genarg_constr_list ist env sigma x = + let lc = out_gen (glbwit (wit_list wit_constr)) x in + let (sigma,lc) = interp_constr_list ist env sigma lc in + sigma , in_gen (topwit (wit_list wit_constr)) lc -(* Interprets the Match expressions *) -and interp_match ist g lz constr lmr = - let rec apply_match_subterm app ist (id,c) csr mt = - 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 (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 - match_next_pattern (fun () -> match_subterm_gen app c csr) () in - let rec apply_match ist sigma csr = let g = { g with sigma=sigma } in function - | (All t)::tl -> - (try eval_with_fail ist lz g t - with e when is_match_catchable e -> apply_match ist sigma csr tl) - | (Pat ([],Term c,mt))::tl -> - (try - let lmatch = - try extended_matches c csr - with reraise -> - debugging_exception_step ist false reraise (fun () -> - str "matching with pattern" ++ fnl () ++ - pr_constr_pattern_env (pf_env g) c); - raise reraise - in - try - let lfun = extend_values_with_bindings lmatch ist.lfun in - eval_with_fail { ist with lfun=lfun } lz g mt - with reraise -> - debugging_exception_step ist false reraise (fun () -> - str "rule body for pattern" ++ - pr_constr_pattern_env (pf_env g) c); - raise reraise - with e when is_match_catchable e -> - debugging_step ist (fun () -> str "switching to the next rule"); - apply_match ist sigma csr tl) - - | (Pat ([],Subterm (b,id,c),mt))::tl -> - (try apply_match_subterm b ist (id,c) csr mt - with PatternMatchingFailure -> apply_match ist sigma csr tl) - | _ -> - errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for match.") in - let (sigma,csr) = - try interp_ltac_constr ist g constr with reraise -> - debugging_exception_step ist true reraise - (fun () -> str "evaluation of the matched expression"); - raise reraise in - let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in - let res = - try apply_match ist sigma csr ilr with reraise -> - debugging_exception_step ist true reraise - (fun () -> str "match expression"); - raise reraise in - debugging_step ist (fun () -> - str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res)); - res +and interp_genarg_var_list ist env sigma x = + let lc = out_gen (glbwit (wit_list wit_var)) x in + let lc = interp_hyp_list ist env sigma lc in + in_gen (topwit (wit_list wit_var)) lc (* Interprets tactic expressions : returns a "constr" *) -and interp_ltac_constr ist gl e = - let (sigma, 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); - raise Not_found in +and interp_ltac_constr ist e : constr Ftactic.t = + let (>>=) = Ftactic.bind in + begin Proofview.tclORELSE + (val_interp ist e) + begin function (err, info) -> match err with + | Not_found -> + Ftactic.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.tclLIFT begin + debugging_step ist (fun () -> + str "evaluation failed for" ++ fnl() ++ + Pptactic.pr_glob_tactic env e) + end + <*> Proofview.tclZERO Not_found + end + | err -> Proofview.tclZERO ~info err + end + end >>= fun result -> + Ftactic.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let result = Value.normalize result in try - 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() ++ - pr_constr_under_binders_env (pf_env gl) cresult); - if fst cresult <> [] then raise Not_found; - sigma , snd cresult - with Not_found -> - errorlabstrm "" + let cresult = coerce_to_closed_constr env result in + Proofview.tclLIFT begin + debugging_step ist (fun () -> + Pptactic.pr_glob_tactic env e ++ fnl() ++ + str " has value " ++ fnl() ++ + pr_constr_env env sigma cresult) + end <*> + Ftactic.return cresult + with CannotCoerceTo _ -> + let env = Proofview.Goal.env gl in + Proofview.tclZERO (UserError ( "", + errorlabstrm "" (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 - | VRTactic _ -> str "VRTactic" - | VFun (_,il,ul,b) -> - (str "VFun with body " ++ fnl() ++ - Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ - str "instantiated arguments " ++ fnl() ++ - List.fold_right - (fun p s -> - let (i,v) = p in str (string_of_id i) ++ str ", " ++ s) - il (str "") ++ - str "uninstantiated arguments " ++ fnl() ++ - List.fold_right - (fun opt_id s -> - (match opt_id with - Some id -> str (string_of_id id) - | None -> str "_") ++ str ", " ++ s) - ul (mt())) - | VVoid -> str "VVoid" - | VInteger _ -> str "VInteger" - | VConstr _ -> str "VConstr" - | VIntroPattern _ -> str "VIntroPattern" - | VConstr_context _ -> str "VConstrr_context" - | VRec _ -> str "VRec" - | VList _ -> str "VList") ++ str".") + str "offending expression: " ++ fnl() ++ pr_inspect env e result))) + end + (* Interprets tactic expressions : returns a "tactic" *) -and interp_tactic ist tac gl = - let (sigma,v) = val_interp ist gl tac in - tactic_of_value ist v { gl with sigma=sigma } +and interp_tactic ist tac : unit Proofview.tactic = + Ftactic.run (val_interp ist tac) (fun v -> tactic_of_value ist v) + +(* Provides a "name" for the trace to atomic tactics *) +and name_atomic ?env tacexpr tac : unit Proofview.tactic = + begin match env with + | Some e -> Proofview.tclUNIT e + | None -> Proofview.tclENV + end >>= fun env -> + let name () = Pptactic.pr_tactic env (TacAtom (Loc.ghost,tacexpr)) in + Proofview.Trace.name_tactic name tac (* Interprets a primitive tactic *) -and interp_atomic ist gl tac = - let env = pf_env gl and sigma = project gl in +and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern l -> - h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) - | TacIntrosUntil hyp -> - h_intros_until (interp_quantified_hypothesis ist hyp) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacIntroPattern l) + (* spiwack: print uninterpreted, not sure if it is the + expected behaviour. *) + (Tactics.intros_patterns l') + end | TacIntroMove (ido,hto) -> - h_intro_move (Option.map (interp_fresh_ident ist env) ido) - (interp_move_location ist gl hto) - | TacAssumption -> h_assumption + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let mloc = interp_move_location ist env sigma hto in + let ido = Option.map (interp_fresh_ident ist env sigma) ido in + name_atomic ~env + (TacIntroMove(ido,mloc)) + (Tactics.intro_move ido mloc) + end | TacExact c -> - let (sigma,c_interp) = pf_interp_casted_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_exact c_interp) - | TacExactNoCheck c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_exact_no_check c_interp) - | TacVmCastNoCheck c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_vm_cast_no_check c_interp) + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_casted_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (Tactics.exact_no_check c_interp) + gl + end + end | TacApply (a,ev,cb,cl) -> - let sigma, l = - list_fold_map (interp_open_constr_with_bindings_loc true 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) -> - 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 -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_elim_type c_interp) - | TacCase (ev,cb) -> - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - tclWITHHOLES ev (h_case ev) sigma cb - | TacCaseType c -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_case_type c_interp) - | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n - | TacMutualFix (b,id,n,l) -> - let f sigma (id,n,c) = - let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,n,c_interp) in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = f sigma c in - sigma , c_interp::acc - end l (project gl,[]) - in - tclTHEN - (tclEVARS sigma) - (h_mutual_fix b (interp_fresh_ident ist env id) n l_interp) - | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt) - | TacMutualCofix (b,id,l) -> - let f sigma (id,c) = - let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,c_interp) in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = f sigma c in - sigma , c_interp::acc - end l (project gl,[]) - in - tclTHEN - (tclEVARS sigma) - (h_mutual_cofix b (interp_fresh_ident ist env id) l_interp) - | TacCut c -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_cut c_interp) - | TacAssert (t,ipat,c) -> - let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in - tclTHEN - (tclEVARS sigma) - (abstract_tactic (TacAssert (t,ipat,c)) - (Tactics.forward (Option.map (interp_tactic ist) t) - (Option.map (interp_intro_pattern ist gl) ipat) c)) + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let l = List.map (fun (k,c) -> + let loc, f = interp_open_constr_with_bindings_loc ist c in + (k,(loc,f))) cb + in + let sigma,tac = match cl with + | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l + | Some cl -> + let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in + sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in + Tacticals.New.tclWITHHOLES ev tac sigma l + end + end + | TacElim (ev,(keep,cb),cbo) -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + 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 + let named_tac cbo = + let tac = Tactics.elim ev keep cb cbo in + name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac + in + Tacticals.New.tclWITHHOLES ev named_tac sigma cbo + end + | TacCase (ev,(keep,cb)) -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let named_tac cb = + let tac = Tactics.general_case_analysis ev keep cb in + name_atomic ~env (TacCase(ev,(keep,cb))) tac + in + Tacticals.New.tclWITHHOLES ev named_tac sigma cb + end + | TacFix (idopt,n) -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in + name_atomic ~env + (TacFix(idopt,n)) + (Proofview.V82.tactic (Tactics.fix idopt n)) + end + | TacMutualFix (id,n,l) -> + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin + Proofview.V82.tactic begin fun gl -> + let env = pf_env gl in + let f sigma (id,n,c) = + let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in + sigma , (interp_fresh_ident ist env sigma id,n,c_interp) in + let (sigma,l_interp) = + Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) + in + tclTHEN + (tclEVARS sigma) + (Tactics.mutual_fix (interp_fresh_ident ist env sigma id) n l_interp 0) + gl + end + end + | TacCofix idopt -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in + name_atomic ~env + (TacCofix (idopt)) + (Proofview.V82.tactic (Tactics.cofix idopt)) + end + | TacMutualCofix (id,l) -> + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin + Proofview.V82.tactic begin fun gl -> + let env = pf_env gl in + let f sigma (id,c) = + let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in + sigma , (interp_fresh_ident ist env sigma id,c_interp) in + let (sigma,l_interp) = + Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) + in + tclTHEN + (tclEVARS sigma) + (Tactics.mutual_cofix (interp_fresh_ident ist env sigma id) l_interp 0) + gl + end + end + | TacAssert (b,t,ipat,c) -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let (sigma,c) = + (if Option.is_empty t then interp_constr else interp_type) ist env sigma c + in + let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in + let tac = Option.map (interp_tactic ist) t in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacAssert(b,t,ipat,c)) + (Tactics.forward b tac ipat' c) + end | TacGeneralize cl -> - let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - tclWITHHOLES false (h_generalize_gen) sigma cl + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacGeneralize cl) + (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl)) + end | TacGeneralizeDep c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_generalize_dep c_interp) + (new_interp_constr ist c) (fun c -> + name_atomic (* spiwack: probably needs a goal environment *) + (TacGeneralizeDep c) + (Proofview.V82.tactic (Tactics.generalize_dep c)) + ) | TacLetTac (na,c,clp,b,eqpat) -> - let clp = interp_clause ist gl clp in - let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in - if clp = nowhere then + Proofview.V82.nf_evar_goals <*> + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let clp = interp_clause ist env sigma clp in + let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in + if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat) - else + let (sigma,c_interp) = + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl + in + let let_tac b na c cl eqpat = + let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let with_eq = if b then None else Some (true,id) in + Tactics.letin_tac with_eq na c None cl + in + Proofview.Unsafe.tclEVARS sigma <*> + let na = interp_fresh_name ist env sigma na in + name_atomic ~env + (TacLetTac(na,c_interp,clp,b,eqpat)) + (let_tac b na c_interp clp eqpat) + else (* We try to keep the pattern structure as much as possible *) - h_let_pat_tac b (interp_fresh_name ist env na) - (interp_pure_open_constr ist env sigma c) clp eqpat + let let_pat_tac b na c cl eqpat = + let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let with_eq = if b then None else Some (true,id) in + Tactics.letin_pat_tac with_eq na c cl + in + let (sigma',c) = interp_pure_open_constr ist env sigma c in + name_atomic ~env + (TacLetTac(na,c,clp,b,eqpat)) + (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) + (let_pat_tac b (interp_fresh_name ist env sigma na) + ((sigma,sigma'),c) clp) sigma' eqpat) + end (* Automation tactics *) | TacTrivial (debug,lems,l) -> - Auto.h_trivial ~debug - (interp_auto_lemmas ist env sigma lems) - (Option.map (List.map (interp_hint_base ist)) l) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let lems = interp_auto_lemmas ist env sigma lems in + name_atomic ~env + (TacTrivial(debug,List.map snd lems,l)) + (Auto.h_trivial ~debug + lems + (Option.map (List.map (interp_hint_base ist)) l)) + end | TacAuto (debug,n,lems,l) -> - Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) - (interp_auto_lemmas ist env sigma lems) - (Option.map (List.map (interp_hint_base ist)) l) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let lems = interp_auto_lemmas ist env sigma lems in + name_atomic ~env + (TacAuto(debug,n,List.map snd lems,l)) + (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) + lems + (Option.map (List.map (interp_hint_base ist)) l)) + end (* Derived basic tactics *) - | TacSimpleInductionDestruct (isrec,h) -> - h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) - | TacInductionDestruct (isrec,ev,(l,el,cls)) -> - let sigma, l = - list_fold_map (fun sigma (c,(ipato,ipats)) -> - let c = interp_induction_arg ist gl c in - (sigma,(c, - (Option.map (interp_intro_pattern ist gl) ipato, - Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in - let sigma,el = - Option.fold_map (interp_constr_with_bindings ist env) sigma el in - let cls = Option.map (interp_clause ist gl) cls in - tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) + | TacInductionDestruct (isrec,ev,(l,el)) -> + (* spiwack: some unknown part of destruct needs the goal to be + prenormalised. *) + Proofview.V82.nf_evar_goals <*> + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma,l = + List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> + (* TODO: move sigma as a side-effect *) + (* spiwack: the [*p] variants are for printing *) + let cp = c in + let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in + let ipato = interp_intro_pattern_naming_option ist env sigma ipato in + let ipatsp = ipats in + let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in + let cls = Option.map (interp_clause ist env sigma) cls in + sigma,((c,(ipato,ipats),cls),(cp,(ipato,ipatsp),cls)) + end sigma l + in + let l,lp = List.split l in + let sigma,el = + Option.fold_map (interp_constr_with_bindings ist env) sigma el in + name_atomic ~env + (TacInductionDestruct(isrec,ev,(lp,el))) + (Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (Tactics.induction_destruct isrec ev (l,el))) + end | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in - Elim.h_double_induction h1 h2 - | TacDecomposeAnd c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Elim.h_decompose_and c_interp) - | TacDecomposeOr c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Elim.h_decompose_or c_interp) - | TacDecompose (l,c) -> - let l = List.map (interp_inductive ist) l in - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Elim.h_decompose l c_interp) - | TacSpecialize (n,cb) -> - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - tclWITHHOLES false (h_specialize n) sigma cb - | TacLApply c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_lapply c_interp) - + name_atomic + (TacDoubleInduction (h1,h2)) + (Elim.h_double_induction h1 h2) (* Context management *) - | TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l) - | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l) - | TacMove (dep,id1,id2) -> - h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) + | TacClear (b,l) -> + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + let l = interp_hyp_list ist env sigma l in + if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) + else + (* spiwack: until the tactic is in the monad *) + let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in + Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac + end + | TacClearBody l -> + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + let l = interp_hyp_list ist env sigma l in + name_atomic ~env + (TacClearBody l) + (Tactics.clear_body l) + end + | TacMove (id1,id2) -> + Proofview.V82.tactic begin fun gl -> + Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) + (interp_move_location ist (pf_env gl) (project gl) id2) + gl + end | TacRename 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) + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + let l = + List.map (fun (id1,id2) -> + interp_hyp ist env sigma id1, + interp_fresh_ident ist env sigma (snd id2)) l + in + name_atomic ~env + (TacRename l) + (Tactics.rename_hyp l) + end (* Constructors *) - | 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) -> - let sigma, bl = interp_bindings ist env sigma bl in - tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl - + | TacSplit (ev,bll) -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in + let named_tac bll = + let tac = Tactics.split_with_bindings ev bll in + name_atomic ~env (TacSplit (ev, bll)) tac + in + Tacticals.New.tclWITHHOLES ev named_tac sigma bll + end (* Conversion *) | TacReduce (r,cl) -> - let (sigma,r_interp) = pf_interp_red_expr ist gl r in - tclTHEN - (tclEVARS sigma) - (h_reduce r_interp (interp_clause ist gl cl)) + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin + Proofview.V82.tactic begin fun gl -> + let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in + tclTHEN + (tclEVARS sigma) + (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) + gl + end + end | TacChange (None,c,cl) -> - let (sigma,c_interp) = - 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 - else pf_interp_constr ist gl c - in - tclTHEN - (tclEVARS sigma) - (h_change None c_interp (interp_clause ist gl cl)) + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin + Proofview.V82.nf_evar_goals <*> + Proofview.V82.tactic begin fun gl -> + let is_onhyps = match cl.onhyps with + | None | Some [] -> true + | _ -> false + in + let is_onconcl = match cl.concl_occs with + | AllOccurrences | NoOccurrences -> true + | _ -> false + in + let c_interp sigma = + if is_onhyps && is_onconcl + then interp_type ist (pf_env gl) sigma c + else interp_constr ist (pf_env gl) sigma c + in + (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) + gl + end + end | TacChange (Some op,c,cl) -> - let sign,op = interp_typed_pattern ist env sigma op in - (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr - is dropped as the evar_map taken as input (from - extend_gl_hyps) is incorrect. This means that evar - instantiated by pf_interp_constr may be lost, there. *) - let (_,c_interp) = - try pf_interp_constr ist (extend_gl_hyps gl sign) c - with Not_found | Anomaly _ (* Hack *) -> - errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - in - tclTHEN - (tclEVARS sigma) - (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl)) + (* spiwack: until the tactic is in the monad *) + Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin + Proofview.V82.nf_evar_goals <*> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Proofview.V82.tactic begin fun gl -> + let sign,op = interp_typed_pattern ist env sigma op in + let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in + let env' = Environ.push_named_context sign env in + let c_interp sigma = + try interp_constr ist env' sigma c + with e when to_catch e (* Hack *) -> + errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") + in + (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) + gl + end + end + end (* Equivalence relations *) - | TacReflexivity -> h_reflexivity - | TacSymmetry c -> h_symmetry (interp_clause ist gl c) - | TacTransitivity c -> - begin match c with - | None -> h_transitivity None - | Some c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_transitivity (Some c_interp)) - end + | TacSymmetry c -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let cl = interp_clause ist env sigma c in + name_atomic ~env + (TacSymmetry cl) + (Tactics.intros_symmetry cl) + end (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - let l = List.map (fun (b,m,c) -> - let f env sigma = interp_open_constr_with_bindings false 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) + Proofview.Goal.enter begin fun gl -> + let l' = List.map (fun (b,m,(keep,c)) -> + let f env sigma = interp_open_constr_with_bindings ist env sigma c in + (b,m,keep,f)) l in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let cl = interp_clause ist env sigma cl in + name_atomic ~env + (TacRewrite (ev,l,cl,by)) + (Equality.general_multi_rewrite ev l' cl + (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), + Equality.Naive) + by)) + end | TacInversion (DepInversion (k,c,ids),hyp) -> - let (sigma,c_interp) = - match c with - | None -> sigma , None - | Some c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - sigma , Some c_interp - in - Inv.dinv k c_interp - (Option.map (interp_intro_pattern ist gl) ids) - (interp_declared_or_quantified_hypothesis ist gl hyp) + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let (sigma,c_interp) = + match c with + | None -> sigma , None + | Some c -> + let (sigma,c_interp) = + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl + in + sigma , Some c_interp + in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in + let sigma,ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) + (Inv.dinv k c_interp ids_interp dqhyps) + end | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - 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) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let hyps = interp_hyp_list ist env sigma idl in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in + let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) + (Inv.inv_clause k ids_interp hyps dqhyps) + end | TacInversion (InversionUsing (c,idl),hyp) -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp) - c_interp - (interp_hyp_list ist gl idl) - - (* For extensions *) - | TacExtend (loc,opn,l) -> - let tac = lookup_tactic opn in - let (sigma,args) = - List.fold_right begin fun a (sigma,acc) -> - let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in - sigma , a_interp::acc - end l (project gl,[]) - in - abstract_extended_tactic opn args (tac args) - | TacAlias (loc,s,l,(_,body)) -> fun gl -> - let evdref = ref gl.sigma in - let rec f x = match genarg_tag x with - | 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 - (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) - | IdentArgType b -> - 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 - (pf_interp_reference ist gl (out_gen globwit_ref x))) - | SortArgType -> - VConstr ([],mkSort (interp_sort (out_gen globwit_sort x))) - | ConstrArgType -> - let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in - evdref := sigma; - v - | OpenConstrArgType (false,true) -> - let (sigma,v) = mk_open_constr_value true ist gl (snd (out_gen globwit_open_constr_wTC x)) in - evdref := sigma; - v - | OpenConstrArgType (false,false) -> - let (sigma,v) = mk_open_constr_value false ist gl (snd (out_gen globwit_open_constr x)) in - evdref := sigma; - v - | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in - evdref := sigma; - VConstr ([],c_interp) - | ExtraArgType s when tactic_genarg_level s <> None -> - (* Special treatment of tactic arguments *) - let (sigma,v) = val_interp ist gl - (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x) - in - evdref := sigma; - v - | List0ArgType ConstrArgType -> - let wit = wit_list0 globwit_constr in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in - sigma , c_interp::acc - end (out_gen wit x) (project gl,[]) - in - evdref := sigma; - VList (l_interp) - | List0ArgType VarArgType -> - let wit = wit_list0 globwit_var in - VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) - | List0ArgType IntArgType -> - let wit = wit_list0 globwit_int in - VList (List.map (fun x -> VInteger x) (out_gen wit x)) - | List0ArgType IntOrVarArgType -> - let wit = wit_list0 globwit_int_or_var in - VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) - | List0ArgType (IdentArgType b) -> - let wit = wit_list0 (globwit_ident_gen b) in - let mk_ident x = value_of_ident (interp_fresh_ident ist 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 - let (sigma, l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in - sigma , c_interp::acc - end (out_gen wit x) (project gl,[]) - in - evdref:=sigma; - VList l_interp - | List1ArgType VarArgType -> - let wit = wit_list1 globwit_var in - VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) - | List1ArgType IntArgType -> - let wit = wit_list1 globwit_int in - VList (List.map (fun x -> VInteger x) (out_gen wit x)) - | 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 _ - -> error "This argument type is not supported in tactic notations." - - in - let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in - let trace = push_trace (loc,LtacNotationCall s) ist.trace in - let gl = { gl with sigma = !evdref } in - interp_tactic { ist with lfun=lfun; trace=trace } body gl - -let make_empty_glob_sign () = - { ltacvars = ([],[]); ltacrecvars = []; - gsigma = Evd.empty; genv = Global.env() } - -let fully_empty_glob_sign = - { ltacvars = ([],[]); ltacrecvars = []; - gsigma = Evd.empty; genv = Environ.empty_env } + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let (sigma,c_interp) = interp_constr ist env sigma c in + let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in + let hyps = interp_hyp_list ist env sigma idl in + Proofview.Unsafe.tclEVARS sigma <*> + name_atomic ~env + (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) + (Leminv.lemInv_clause dqhyps c_interp hyps) + end (* Initial call for interpretation *) -let interp_tac_gen lfun avoid_ids debug t gl = - interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] } - (intern_tactic true { - ltacvars = (List.map fst lfun, []); ltacrecvars = []; - gsigma = project gl; genv = pf_env gl } t) gl - -let eval_tactic t gls = - db_initialize (); - interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } - t gls - -let interp t = interp_tac_gen [] [] (get_debug()) t - -let eval_ltac_constr gl t = - interp_ltac_constr - { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl - (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) - -(* Hides interpretation for pretty-print *) -let hide_interp t ot gl = - let ist = { ltacvars = ([],[]); ltacrecvars = []; - gsigma = project gl; genv = pf_env gl } in - let te = intern_tactic true ist t in - let t = eval_tactic te in - match ot with - | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl - | Some t' -> - abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl - -(***************************************************************************) -(* Substitution at module closing time *) - -let subst_quantified_hypothesis _ x = x - -let subst_declared_or_quantified_hypothesis _ x = x - -let subst_glob_constr_and_expr subst (c,e) = - assert (e=None); (* e<>None only for toplevel tactics *) - (Detyping.subst_glob_constr subst c,None) - -let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) - -let subst_binding subst (loc,b,c) = - (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c) - -let subst_bindings subst = function - | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map (subst_glob_constr subst) l) - | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l) - -let subst_glob_with_bindings subst (c,bl) = - (subst_glob_constr subst c, subst_bindings subst bl) - -let subst_induction_arg subst = function - | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent id as x -> x - -let subst_and_short_name f (c,n) = -(* assert (n=None); *)(* since tacdef are strictly globalized *) - (f c,None) - -let subst_or_var f = function - | ArgVar _ as x -> x - | ArgArg x -> ArgArg (f x) - -let subst_located f (_loc,id) = (dloc,f id) - -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 = - let subst_global ref = - let ref',t' = subst_global subst ref in - if not (eq_constr (constr_of_global ref') t') then - ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; - ref' - in - subst_or_var (subst_located subst_global) - -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) = - (l,subst_evaluable subst e) - -let subst_flag subst red = - { red with rConst = List.map (subst_evaluable subst) red.rConst } - -let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) - -let subst_glob_constr_or_pattern subst (c,p) = - (subst_glob_constr subst c,subst_pattern subst p) - -let subst_pattern_with_occurrences subst (l,p) = - (l,subst_glob_constr_or_pattern subst p) - -let subst_redexp subst = function - | Unfold l -> Unfold (List.map (subst_unfold subst) l) - | Fold l -> Fold (List.map (subst_glob_constr 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_pattern_with_occurrences subst) o) - | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r - -let subst_raw_may_eval subst = function - | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c) - | ConstrContext (locid,c) -> ConstrContext (locid,subst_glob_constr subst c) - | ConstrTypeOf c -> ConstrTypeOf (subst_glob_constr subst c) - | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) - -let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) - | Term pc -> Term (subst_glob_constr_or_pattern subst pc) - -let rec subst_match_goal_hyps subst = function - | Hyp (locs,mp) :: tl -> - Hyp (locs,subst_match_pattern subst mp) - :: subst_match_goal_hyps subst tl - | Def (locs,mv,mp) :: tl -> - Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp) - :: subst_match_goal_hyps subst tl - | [] -> [] - -let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with - (* Basic tactics *) - | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x - | TacAssumption as x -> x - | TacExact c -> TacExact (subst_glob_constr subst c) - | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c) - | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c) - | TacApply (a,ev,cb,cl) -> - TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl) - | TacElim (ev,cb,cbo) -> - TacElim (ev,subst_glob_with_bindings subst cb, - Option.map (subst_glob_with_bindings subst) cbo) - | TacElimType c -> TacElimType (subst_glob_constr subst c) - | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb) - | TacCaseType c -> TacCaseType (subst_glob_constr subst c) - | TacFix (idopt,n) as x -> x - | TacMutualFix (b,id,n,l) -> - TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) - | TacCofix idopt as x -> x - | TacMutualCofix (b,id,l) -> - TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacCut c -> TacCut (subst_glob_constr subst c) - | TacAssert (b,na,c) -> - TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c) - | TacGeneralize cl -> - TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) - (* Automation tactics *) - | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l) - | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l) - - (* Derived basic tactics *) - | TacSimpleInductionDestruct (isrec,h) as x -> x - | TacInductionDestruct (isrec,ev,(l,el,cls)) -> - let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in - let el' = Option.map (subst_glob_with_bindings subst) el in - TacInductionDestruct (isrec,ev,(l',el',cls)) - | TacDoubleInduction (h1,h2) as x -> x - | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c) - | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c) - | TacDecompose (l,c) -> - let l = List.map (subst_or_var (subst_inductive subst)) l in - TacDecompose (l,subst_glob_constr subst c) - | TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l) - | TacLApply c -> TacLApply (subst_glob_constr subst c) - - (* Context management *) - | TacClear _ as x -> x - | TacClearBody l as x -> x - | TacMove (dep,id1,id2) as x -> x - | TacRename l as x -> x - | TacRevert _ as x -> x - - (* Constructors *) - | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl) - | TacRight (ev,bl) -> TacRight (ev,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 (op,c,cl) -> - TacChange (Option.map (subst_glob_constr_or_pattern subst) op, - subst_glob_constr subst c, cl) - - (* Equivalence relations *) - | TacReflexivity | TacSymmetry _ as x -> x - | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c) - - (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - TacRewrite (ev, - List.map (fun (b,m,c) -> - b,m,subst_glob_with_bindings subst c) l, - cl,Option.map (subst_tactic subst) by) - | TacInversion (DepInversion (k,c,l),hyp) -> - TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp) - | TacInversion (NonDepInversion _,_) as x -> x - | TacInversion (InversionUsing (c,cl),hyp) -> - TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp) - - (* For extensions *) - | TacExtend (_loc,opn,l) -> - TacExtend (dloc,opn,List.map (subst_genarg subst) l) - | TacAlias (_,s,l,(dir,body)) -> - TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l, - (dir,subst_tactic subst body)) - -and subst_tactic subst (t:glob_tactic_expr) = match t with - | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t) - | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun) - | TacLetIn (r,l,u) -> - let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in - TacLetIn (r,l,subst_tactic subst u) - | TacMatchGoal (lz,lr,lmr) -> - TacMatchGoal(lz,lr, subst_match_rule subst lmr) - | TacMatch (lz,c,lmr) -> - TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr) - | TacId _ | TacFail _ as x -> x - | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr) - | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s) - | TacThen (t1,tf,t2,tl) -> - TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf, - subst_tactic subst t2,Array.map (subst_tactic subst) tl) - | TacThens (t,tl) -> - TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) - | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac) - | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac) - | TacTry tac -> TacTry (subst_tactic subst tac) - | TacInfo tac -> TacInfo (subst_tactic subst tac) - | TacRepeat tac -> TacRepeat (subst_tactic subst tac) - | TacOrelse (tac1,tac2) -> - TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) - | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) - | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) - | TacComplete tac -> TacComplete (subst_tactic subst tac) - | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) - -and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) - -and subst_tacarg subst = function - | Reference r -> Reference (subst_reference subst r) - | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | 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,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 Dyn.tag t with - | "tactic" | "value" -> x - | "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 ">")) - -(* Reads the rules of a Match Context or a Match *) -and subst_match_rule subst = function - | (All tc)::tl -> - (All (subst_tactic subst tc))::(subst_match_rule subst tl) - | (Pat (rl,mp,tc))::tl -> - let hyps = subst_match_goal_hyps subst rl in - let pat = subst_match_pattern subst mp in - Pat (hyps,pat,subst_tactic subst tc) - ::(subst_match_rule subst tl) - | [] -> [] +let default_ist () = + let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in + { lfun = Id.Map.empty; extra = extra } + +let eval_tactic t = + Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *) + Proofview.tclLIFT db_initialize <*> + interp_tactic (default_ist ()) t + +let eval_tactic_ist ist t = + Proofview.tclLIFT db_initialize <*> + interp_tactic ist t + +(* globalization + interpretation *) + + +let interp_tac_gen lfun avoid_ids debug t = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let extra = TacStore.set TacStore.empty f_debug debug in + let extra = TacStore.set extra f_avoid_ids avoid_ids in + let ist = { lfun = lfun; extra = extra } in + let ltacvars = Id.Map.domain lfun in + interp_tactic ist + (intern_pure_tactic { + ltacvars; ltacrecvars = Id.Map.empty; + genv = env } t) + end -and subst_genarg subst (x:glob_generic_argument) = - match genarg_tag x with - | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x) - | IntArgType -> in_gen globwit_int (out_gen globwit_int x) - | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x) - | StringArgType -> in_gen globwit_string (out_gen globwit_string x) - | 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 -> - 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 - (out_gen globwit_ref x)) - | SortArgType -> - in_gen globwit_sort (out_gen globwit_sort x) - | ConstrArgType -> - in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x)) - | ConstrMayEvalArgType -> - 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 - (out_gen globwit_quant_hyp x)) - | RedExprArgType -> - in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) - | OpenConstrArgType (b1,b2) -> - in_gen (globwit_open_constr_gen (b1,b2)) - ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen (b1,b2)) x))) - | ConstrWithBindingsArgType -> - in_gen globwit_constr_with_bindings - (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x)) - | BindingsArgType -> - in_gen globwit_bindings - (subst_bindings subst (out_gen globwit_bindings x)) - | List0ArgType _ -> app_list0 (subst_genarg subst) x - | List1ArgType _ -> app_list1 (subst_genarg subst) x - | OptArgType _ -> app_opt (subst_genarg subst) x - | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x - | ExtraArgType s -> - match tactic_genarg_level s with - | Some n -> - (* Special treatment of tactic arguments *) - in_gen (globwit_tactic n) - (subst_tactic subst (out_gen (globwit_tactic n) x)) - | None -> - lookup_genarg_subst s subst x +let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t +let _ = Proof_global.set_interp_tac interp + +(* Used to hide interpretation for pretty-print, now just launch tactics *) +(* [global] means that [t] should be internalized outside of goals. *) +let hide_interp global t ot = + let hide_interp env = + let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; + genv = env } in + let te = intern_pure_tactic ist t in + let t = eval_tactic te in + match ot with + | None -> t + | Some t' -> Tacticals.New.tclTHEN t t' + in + if global then + Proofview.tclENV >>= fun env -> + hide_interp env + else + Proofview.Goal.enter begin fun gl -> + hide_interp (Proofview.Goal.env gl) + end (***************************************************************************) -(* Tactic registration *) - -(* Declaration of the TAC-DEFINITION object *) -let add (kn,td) = mactab := Gmap.add kn td !mactab -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),(local,defs)) = - let dp,_ = repr_path sp in - let mp,dir,_ = repr_kn kn in - List.iter (fun (id,t) -> - match id with - NewTac id -> - let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in - Nametab.push_tactic (Until i) sp kn; - add (kn,t) - | UpdateTac kn -> replace (kn,t)) 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) -> - match id with - NewTac id -> - let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in - Nametab.push_tactic (Exactly i) sp kn - | UpdateTac kn -> ()) defs - -let cache_md x = load_md 1 x - -let subst_kind subst id = - match id with - | NewTac _ -> id - | 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 classify_md (local,defs as o) = - if local then Dispose else Substitute o - -let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj = - declare_object {(default_object "TAC-DEFINITION") with - cache_function = cache_md; - load_function = load_md; - open_function = open_md; - subst_function = subst_md; - classify_function = classify_md} - -let rec split_ltac_fun = function - | TacFun (l,t) -> (l,t) - | t -> ([],t) - -let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - -let print_ltac id = - try - let kn = Nametab.locate_tactic id in - let l,t = split_ltac_fun (lookup kn) in - hv 2 ( - hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ - prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) - with - Not_found -> - errorlabstrm "print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") - -open Libnames +(** Register standard arguments *) + +let def_intern ist x = (ist, x) +let def_subst _ x = x +let def_interp ist gl x = (project gl, x) + +let declare_uniform t = + Genintern.register_intern0 t def_intern; + Genintern.register_subst0 t def_subst; + Geninterp.register_interp0 t def_interp + +let () = + declare_uniform wit_unit + +let () = + declare_uniform wit_int + +let () = + declare_uniform wit_bool + +let () = + declare_uniform wit_string + +let () = + declare_uniform wit_pre_ident + +let () = + let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) (project gl) ref) in + Geninterp.register_interp0 wit_ref interp; + let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in + Geninterp.register_interp0 wit_intro_pattern interp; + let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) (project gl) pat) in + Geninterp.register_interp0 wit_clause_dft_concl interp; + let interp ist gl s = interp_sort (project gl) s in + Geninterp.register_interp0 wit_sort interp + +let () = + let interp ist gl tac = + let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in + (project gl, TacArg (dloc, valueIn (of_tacvalue f))) + in + Geninterp.register_interp0 wit_tactic interp -(* 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 = - if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident)) - 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 - user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_reference ident ++ str".") - else id, kn - with Not_found -> - user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_reference ident ++ str".") - -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 list_map_filter - (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun - else []} in - let gtacl = - List.map2 (fun (_,b,def) (id, qid) -> - let k = if b then UpdateTac qid else NewTac (Option.get id) in - let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in - (k, t)) - tacl rfun in - let id0 = fst (List.hd rfun) 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 ++ - (if b then str " is redefined" - else str " is defined"))) - tacl +let () = + Geninterp.register_interp0 wit_uconstr (fun ist gl c -> + project gl , interp_uconstr ist (pf_env gl) c + ) (***************************************************************************) (* Other entry points *) -let glob_tactic x = - Flags.with_option strict_check (intern_tactic true (make_empty_glob_sign ())) x +let val_interp ist tac k = Ftactic.run (val_interp ist tac) k -let glob_tactic_env l env x = - Flags.with_option strict_check - (intern_pure_tactic - { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }) - x +let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k 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) + let ist = default_ist () in + let gist = { fully_empty_glob_sign with genv = env; } in + interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) (* Embed tactics in raw or glob tactic expr *) @@ -3190,30 +2336,80 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) - with e when Errors.noncritical e -> - anomalylabstrm "tacticIn" + with e when Errors.noncritical e -> anomaly ~label:"tacticIn" (str "Incorrect tactic expression. Received exception is:" ++ Errors.print e)) -let tacticOut = function - | TacArg (_,TacDynamic (_,d)) -> - if (Dyn.tag d) = "tactic" then - tactic_out d - else - anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") - | ast -> - anomalylabstrm "tacticOut" - (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) - (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) -let _ = Auto.set_extern_interp - (fun l -> - let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in - interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]}) -let _ = Auto.set_extern_intern_tac +let _ = + let eval ty env sigma lfun arg = + let ist = { lfun = lfun; extra = TacStore.empty; } in + if has_type arg (glbwit wit_tactic) then + let tac = out_gen (glbwit wit_tactic) arg in + let tac = interp_tactic ist tac in + (** Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) + let eff = Evd.eval_side_effects sigma in + let sigma = Evd.drop_side_effects sigma in + (** Start a proof *) + let prf = Proof.start sigma [env, ty] in + let (prf, _) = + try Proof.run_tactic env tac prf + with Logic_monad.TacticFailure e as src -> + (** Catch the inner error of the monad tactic *) + let (_, info) = Errors.push src in + iraise (e, info) + in + (** Plug back the retrieved sigma *) + let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let ans = match Proof.initial_goals prf with + | [c, _] -> c + | _ -> assert false + in + let ans = Reductionops.nf_evar sigma ans in + (** [neff] contains the freshly generated side-effects *) + let neff = Evd.eval_side_effects sigma in + (** Reset the old side-effects *) + let sigma = Evd.drop_side_effects sigma in + let sigma = Evd.emit_side_effects eff sigma in + (** Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) + let ans = Term_typing.handle_side_effects env ans neff in + ans, sigma + else + failwith "not a tactic" + in + Hook.set Pretyping.genarg_interp_hook eval + +let _ = Hook.set Auto.extern_interp (fun l -> - Flags.with_option strict_check - (intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})) -let _ = Auto.set_extern_subst_tactic subst_tactic + let lfun = Id.Map.map (fun c -> Value.of_constr c) l in + let ist = { (default_ist ()) with lfun; } in + interp_tactic ist) + +(** Used in tactic extension **) + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let map = function + | None -> None + | Some id -> + let c = Id.Map.find id ist.lfun in + try Some (coerce_to_closed_constr env c) + with CannotCoerceTo ty -> + error_ltac_variable Loc.ghost dummy_id (Some (env,sigma)) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac |