summaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /tactics/tacinterp.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml2236
1 files changed, 2236 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
new file mode 100644
index 00000000..2080b5dc
--- /dev/null
+++ b/tactics/tacinterp.ml
@@ -0,0 +1,2236 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: tacinterp.ml,v 1.84.2.4 2004/07/16 19:30:55 herbelin Exp $ *)
+
+open Constrintern
+open Closure
+open RedFlags
+open Declarations
+open Entries
+open Dyn
+open Libobject
+open Pattern
+open Matching
+open Pp
+open Rawterm
+open Sign
+open Tacred
+open Util
+open Names
+open Nameops
+open Libnames
+open Nametab
+open Pfedit
+open Proof_type
+open Refiner
+open Tacmach
+open Tactic_debug
+open Topconstr
+open Ast
+open Term
+open Termops
+open Tacexpr
+open Safe_typing
+open Typing
+open Hiddentac
+open Genarg
+open Decl_kinds
+
+let strip_meta id = (* For Grammar v7 compatibility *)
+ let s = string_of_id id in
+ if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+ else id
+
+let error_syntactic_metavariables_not_allowed loc =
+ user_err_loc
+ (loc,"out_ident",
+ str "Syntactic metavariables allowed only in quotations")
+
+let skip_metaid = function
+ | AI x -> x
+ | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
+
+type ltac_type =
+ | LtacFun of ltac_type
+ | LtacBasic
+ | LtacTactic
+
+(* Values for interpretation *)
+type value =
+ | VTactic of loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+ | VRTactic of (goal list sigma * validation) (* For Match results *)
+ (* Not a true value *)
+ | VFun of (identifier*value) list * identifier option list * glob_tactic_expr
+ | VVoid
+ | VInteger of int
+ | VIntroPattern of intro_pattern_expr (* includes idents which are not *)
+ (* bound as in "Intro H" but which may be bound *)
+ (* later, as in "tac" in "Intro H; tac" *)
+ | VConstr of constr (* includes idents known bound and references *)
+ | VConstr_context of constr
+ | VRec of value ref
+
+let locate_tactic_call loc = function
+ | VTactic (_,t) -> VTactic (loc,t)
+ | v -> v
+
+let locate_error_in_file dir = function
+ | Stdpp.Exc_located (loc,e) -> Error_in_file ("",(true,dir,loc),e)
+ | e -> Error_in_file ("",(true,dir,dummy_loc),e)
+
+let catch_error loc tac g =
+ try tac g
+ with e when loc <> dummy_loc ->
+ match e with
+ | Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e))
+ | e -> raise (Stdpp.Exc_located (loc,e))
+
+(* Signature for interpretation: val_interp and interpretation functions *)
+type interp_sign =
+ { lfun : (identifier * value) list;
+ debug : debug_info }
+
+let check_is_value = function
+ | VRTactic _ -> (* These are goals produced by Match *)
+ error "Immediate match producing tactics not allowed in local definitions"
+ | _ -> ()
+
+(* For tactic_of_value *)
+exception NotTactic
+
+(* Gives the constr corresponding to a Constr_context tactic_arg *)
+let constr_of_VConstr_context = function
+ | VConstr_context c -> c
+ | _ ->
+ errorlabstrm "constr_of_VConstr_context" (str "not a context variable")
+
+(* Displays a value *)
+let pr_value env = function
+ | VVoid -> str "()"
+ | VInteger n -> int n
+ | VIntroPattern ipat -> pr_intro_pattern ipat
+ | VConstr c -> Printer.prterm_env env c
+ | VConstr_context c -> Printer.prterm_env env c
+ | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>"
+
+(* Transforms a named_context into a (string * constr) list *)
+let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
+
+(* Transforms an id into a constr if possible, or fails *)
+let constr_of_id env id =
+ construct_reference (Environ.named_context env) id
+
+(* To embed several objects in Coqast.t *)
+let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t),
+ (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) =
+ create "tactic"
+
+let ((value_in : value -> Dyn.t),
+ (value_out : Dyn.t -> value)) = create "value"
+
+let tacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
+let tacticOut = function
+ | TacArg (TacDynamic (_,d)) ->
+ if (tag d) = "tactic" then
+ tactic_out d
+ else
+ anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
+ | ast ->
+ anomalylabstrm "tacticOut"
+ (str "Not a Dynamic ast: " (* ++ print_ast ast*) )
+
+let valueIn t = TacDynamic (dummy_loc,value_in t)
+let valueOut = function
+ | TacDynamic (_,d) ->
+ if (tag d) = "value" then
+ value_out d
+ else
+ anomalylabstrm "valueOut" (str "Dynamic tag should be value")
+ | ast ->
+ anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")
+
+(* To embed constr in Coqast.t *)
+let constrIn t = CDynamic (dummy_loc,Pretyping.constr_in t)
+let constrOut = function
+ | CDynamic (_,d) ->
+ if (Dyn.tag d) = "constr" then
+ Pretyping.constr_out d
+ else
+ anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
+ | ast ->
+ anomalylabstrm "constrOut" (str "Not a Dynamic ast")
+let loc = dummy_loc
+
+(* Table of interpretation functions *)
+let interp_tab =
+ (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t)
+
+(* Adds an interpretation function *)
+let interp_add (ast_typ,interp_fun) =
+ try
+ Hashtbl.add interp_tab ast_typ interp_fun
+ with
+ Failure _ ->
+ errorlabstrm "interp_add"
+ (str "Cannot add the interpretation function for " ++ str ast_typ ++ str " twice")
+
+(* Adds a possible existing interpretation function *)
+let overwriting_interp_add (ast_typ,interp_fun) =
+ if Hashtbl.mem interp_tab ast_typ then
+ begin
+ Hashtbl.remove interp_tab ast_typ;
+ warning ("Overwriting definition of tactic interpreter command " ^ ast_typ)
+ end;
+ Hashtbl.add interp_tab ast_typ interp_fun
+
+(* Finds the interpretation function corresponding to a given ast type *)
+let look_for_interp = Hashtbl.find interp_tab
+
+(* Globalizes the identifier *)
+
+let find_reference env qid =
+ (* We first look for a variable of the current proof *)
+ match repr_qualid qid with
+ | (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env)
+ -> VarRef id
+ | _ -> Nametab.locate qid
+
+let coerce_to_reference env = function
+ | VConstr c ->
+ (try reference_of_constr c
+ with Not_found -> invalid_arg_loc (loc, "Not a reference"))
+ | v -> errorlabstrm "coerce_to_reference"
+ (str "The value" ++ spc () ++ pr_value env v ++
+ str "cannot be coerced to a reference")
+
+(* turns a value into an evaluable reference *)
+let error_not_evaluable s =
+ errorlabstrm "evalref_of_ref"
+ (str "Cannot coerce" ++ spc () ++ s ++ spc () ++
+ str "to an evaluable reference")
+
+let coerce_to_evaluable_ref env c =
+ let ev = match c with
+ | VConstr c when isConst c -> EvalConstRef (destConst c)
+ | VConstr c when isVar c -> EvalVarRef (destVar c)
+ | VIntroPattern (IntroIdentifier id)
+ when Environ.evaluable_named id env -> EvalVarRef id
+ | _ -> error_not_evaluable (pr_value env c)
+ in
+ if not (Tacred.is_evaluable env ev) then
+ error_not_evaluable (pr_value env c);
+ ev
+
+let coerce_to_inductive = function
+ | VConstr c when isInd c -> destInd c
+ | x ->
+ try
+ let r = match x with
+ | VConstr c -> reference_of_constr c
+ | _ -> failwith "" in
+ errorlabstrm "coerce_to_inductive"
+ (Printer.pr_global r ++ str " is not an inductive type")
+ with _ ->
+ errorlabstrm "coerce_to_inductive"
+ (str "Found an argument which should be an inductive type")
+
+
+(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+let atomic_mactab = ref Idmap.empty
+let add_primitive_tactic s tac =
+ (if not !Options.v7 then
+ let id = id_of_string s in
+ atomic_mactab := Idmap.add id tac !atomic_mactab)
+
+let _ =
+ if not !Options.v7 then
+ (let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+ List.iter
+ (fun (s,t) -> add_primitive_tactic s (TacAtom(dummy_loc,t)))
+ [ "red", TacReduce(Red false,nocl);
+ "hnf", TacReduce(Hnf,nocl);
+ "simpl", TacReduce(Simpl None,nocl);
+ "compute", TacReduce(Cbv all_flags,nocl);
+ "intro", TacIntroMove(None,None);
+ "intros", TacIntroPattern [];
+ "assumption", TacAssumption;
+ "cofix", TacCofix None;
+ "trivial", TacTrivial None;
+ "auto", TacAuto(None,None);
+ "left", TacLeft NoBindings;
+ "right", TacRight NoBindings;
+ "split", TacSplit(false,NoBindings);
+ "constructor", TacAnyConstructor None;
+ "reflexivity", TacReflexivity;
+ "symmetry", TacSymmetry nocl
+ ];
+ List.iter
+ (fun (s,t) -> add_primitive_tactic s t)
+ [ "idtac",TacId "";
+ "fail", TacFail(ArgArg 0,"");
+ "fresh", TacArg(TacFreshId None)
+ ])
+
+let lookup_atomic id = Idmap.find id !atomic_mactab
+let is_atomic id = Idmap.mem id !atomic_mactab
+let is_atomic_kn kn =
+ let (_,_,l) = repr_kn kn in
+ is_atomic (id_of_label l)
+
+(* Summary and Object declaration *)
+let mactab = ref Gmap.empty
+
+let lookup r = Gmap.find r !mactab
+
+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;
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+(* 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 ->
+ closed_generic_argument) *
+ (Names.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 -> failwith ("No interpretation function found for entry "^id)
+
+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
+
+(* Unboxes VRec *)
+let unrec = function
+ | VRec v -> !v
+ | a -> a
+
+(*****************)
+(* Globalization *)
+(*****************)
+
+(* We have identifier <| global_reference <| constr *)
+
+let find_ident id sign =
+ List.mem id (fst sign.ltacvars) or
+ List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+
+let find_recvar qid sign = List.assoc qid sign.ltacrecvars
+
+(* a "var" is a ltac var or a var introduced by an intro tactic *)
+let find_var id sign = List.mem id (fst sign.ltacvars)
+
+(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
+let find_ctxvar id sign = List.mem id (snd sign.ltacvars)
+
+(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
+let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign)
+
+let find_hyp id sign =
+ List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+
+(* 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 intern_name l ist = function
+ | Anonymous -> Anonymous
+ | Name id -> Name (intern_ident l ist id)
+
+let vars_of_ist (lfun,_,_,env) =
+ List.fold_left (fun s id -> Idset.add id s)
+ (vars_of_env env) lfun
+
+let get_current_context () =
+ try Pfedit.get_current_goal_context ()
+ with e when Logic.catchable_exception e ->
+ (Evd.empty, Global.env())
+
+let strict_check = ref false
+
+let adjust_loc loc = if !strict_check then dummy_loc else loc
+
+(* Globalize a name which must be bound -- actually just check it is bound *)
+let intern_hyp ist (loc,id as locid) =
+ let (_,env) = get_current_context () in
+ if not !strict_check then
+ locid
+ else if find_ident id ist then
+ (dummy_loc,id)
+ 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_int_or_var ist = function
+ | ArgVar locid as x -> ArgVar (intern_hyp ist locid)
+ | ArgArg n as x -> x
+
+let intern_inductive ist = function
+ | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
+ | r -> ArgArg (Nametab.global_inductive r)
+
+exception NotSyntacticRef
+
+let locate_reference qid =
+ match Nametab.extended_locate qid with
+ | TrueGlobal ref -> ref
+ | SyntacticDef kn ->
+ match Syntax_def.search_syntactic_definition loc kn with
+ | Rawterm.RRef (_,ref) -> ref
+ | _ -> raise NotSyntacticRef
+
+let intern_global_reference ist = function
+ | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id)
+ | r ->
+ let loc,qid = qualid_of_reference r in
+ try ArgArg (loc,locate_reference qid)
+ with _ ->
+ error_global_not_found_loc loc qid
+
+let intern_tac_ref ist = function
+ | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
+ | Ident (loc,id) ->
+ ArgArg (loc,
+ try find_recvar id ist
+ with Not_found -> locate_tactic (make_short_qualid id))
+ | r ->
+ let (loc,qid) = qualid_of_reference r in
+ ArgArg (loc,locate_tactic qid)
+
+let intern_tactic_reference ist r =
+ try intern_tac_ref ist r
+ with Not_found ->
+ let (loc,qid) = qualid_of_reference r in
+ error_global_not_found_loc loc qid
+
+let intern_constr_reference strict ist = function
+ | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
+ RVar (loc,id), None
+ | r ->
+ let loc,qid = qualid_of_reference r in
+ RRef (loc,locate_reference qid), if strict then None else Some (CRef r)
+
+let intern_reference strict ist = function
+ | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
+ | r ->
+ (try Reference (intern_tac_ref ist r)
+ with Not_found ->
+ (try
+ ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+ with Not_found ->
+ (match r with
+ | Ident (loc,id) when not strict ->
+ IntroPattern (IntroIdentifier id)
+ | _ ->
+ let (loc,qid) = qualid_of_reference r in
+ error_global_not_found_loc loc qid)))
+
+let rec intern_intro_pattern lf ist = function
+ | IntroOrAndPattern l ->
+ IntroOrAndPattern (intern_case_intro_pattern lf ist l)
+ | IntroWildcard ->
+ IntroWildcard
+ | IntroIdentifier id ->
+ IntroIdentifier (intern_ident lf ist id)
+
+and intern_case_intro_pattern lf ist =
+ List.map (List.map (intern_intro_pattern lf ist))
+
+let intern_quantified_hypothesis ist x =
+ (* We use identifier both for variables and quantified hyps (no way to
+ statically check the existence of a quantified hyp); thus nothing to do *)
+ x
+
+let intern_constr {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.interp_rawconstr_gen false sigma env
+ false (fst lfun,[])) c in
+ begin if Options.do_translate () then try
+ (* Try to infer old case and type annotations *)
+ let _ = Pretyping.understand_gen_tcc sigma env [] None c' in
+ (* msgerrnl (str "Typage tactique OK");*)
+ ()
+ with e -> (*msgerrnl (str "Warning: can't type tactic");*) () end;
+ (c',if !strict_check then None else Some c)
+
+(* Globalize bindings *)
+let intern_binding ist (loc,b,c) =
+ (loc,intern_quantified_hypothesis 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)
+
+let intern_clause_pattern ist (l,occl) =
+ let rec check = function
+ | (hyp,l) :: rest -> (intern_hyp ist (skip_metaid hyp),l)::(check rest)
+ | [] -> []
+ in (l,check occl)
+
+ (* TODO: catch ltac vars *)
+let intern_induction_arg ist = function
+ | ElimOnConstr c -> ElimOnConstr (intern_constr ist c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent (loc,id) as x ->
+ if !strict_check then
+ (* If in a defined tactic, no intros-until *)
+ ElimOnConstr (intern_constr ist (CRef (Ident (dummy_loc,id))))
+ else
+ ElimOnIdent (loc,id)
+
+(* Globalizes a reduction expression *)
+let intern_evaluable ist = function
+ | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id)
+ | Ident (_,id) when
+ (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
+ ArgArg (EvalVarRef id, None)
+ | r ->
+ let loc,qid = qualid_of_reference r in
+ try
+ let e = match locate_reference qid with
+ | ConstRef c -> EvalConstRef c
+ | VarRef c -> EvalVarRef c
+ | _ -> error_not_evaluable (pr_reference r) in
+ let short_name = match r with
+ | Ident (loc,id) when not !strict_check -> Some (loc,id)
+ | _ -> None in
+ ArgArg (e,short_name)
+ with
+ | NotSyntacticRef -> error_not_evaluable (pr_reference r)
+ | Not_found ->
+ match r with
+ | Ident (loc,id) when not !strict_check ->
+ ArgArg (EvalVarRef id, Some (loc,id))
+ | _ -> error_global_not_found_loc loc qid
+
+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_occurrence ist (l,c) = (l,intern_constr ist c)
+
+let intern_redexp 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_occurrence ist) l)
+ | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
+ | (Red _ | Hnf as r) -> r
+ | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)
+
+let intern_inversion_strength lf ist = function
+ | NonDepInversion (k,idl,ids) ->
+ NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
+ option_app (intern_intro_pattern lf ist) ids)
+ | DepInversion (k,copt,ids) ->
+ DepInversion (k, option_app (intern_constr ist) copt,
+ option_app (intern_intro_pattern lf ist) ids)
+ | InversionUsing (c,idl) ->
+ InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
+
+(* Interprets an hypothesis name *)
+let intern_hyp_location ist (id,occs,hl) =
+ (intern_hyp ist (skip_metaid id), occs, hl)
+
+(* Reads a pattern *)
+let intern_pattern evc env lfun = function
+ | Subterm (ido,pc) ->
+ let (metas,pat) = interp_constrpattern_gen evc env lfun pc in
+ ido, metas, Subterm (ido,pat)
+ | Term pc ->
+ let (metas,pat) = interp_constrpattern_gen evc env lfun pc in
+ None, metas, Term pat
+
+let intern_constr_may_eval ist = function
+ | ConstrEval (r,c) -> ConstrEval (intern_redexp 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)
+
+(* Reads the hypotheses of a Match Context rule *)
+let rec intern_match_context_hyps evc env lfun = function
+ | (Hyp ((_,na) as locna,mp))::tl ->
+ let ido, metas1, pat = intern_pattern evc env lfun mp in
+ let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in
+ let lfun' = name_cons na (option_cons ido lfun) in
+ lfun', metas1@metas2, Hyp (locna,pat)::hyps
+ | [] -> lfun, [], []
+
+(* Utilities *)
+let rec filter_some = function
+ | None :: l -> filter_some l
+ | Some a :: l -> a :: filter_some l
+ | [] -> []
+
+let extract_names lrc =
+ List.fold_right
+ (fun ((loc,name),_) l ->
+ if List.mem name l then
+ user_err_loc
+ (loc, "intern_tactic", str "This variable is bound several times");
+ name::l)
+ lrc []
+
+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; onconcl=b;concl_occs=nl } ->
+ { onhyps=None; onconcl=b; concl_occs=nl }
+ | { onhyps=Some l; onconcl=b;concl_occs=nl } ->
+ { onhyps=Some(List.map f l); onconcl=b;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,ido') ->
+ TacIntroMove (option_app (intern_ident lf ist) ido,
+ option_app (intern_hyp ist) ido')
+ | TacAssumption -> TacAssumption
+ | TacExact c -> TacExact (intern_constr ist c)
+ | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
+ | TacElim (cb,cbo) ->
+ TacElim (intern_constr_with_bindings ist cb,
+ option_app (intern_constr_with_bindings ist) cbo)
+ | TacElimType c -> TacElimType (intern_constr ist c)
+ | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
+ | TacCaseType c -> TacCaseType (intern_constr ist c)
+ | TacFix (idopt,n) -> TacFix (option_app (intern_ident lf ist) idopt,n)
+ | TacMutualFix (id,n,l) ->
+ let f (id,n,c) = (intern_ident lf ist id,n,intern_constr ist c) in
+ TacMutualFix (intern_ident lf ist id, n, List.map f l)
+ | TacCofix idopt -> TacCofix (option_app (intern_ident lf ist) idopt)
+ | TacMutualCofix (id,l) ->
+ let f (id,c) = (intern_ident lf ist id,intern_constr ist c) in
+ TacMutualCofix (intern_ident lf ist id, List.map f l)
+ | TacCut c -> TacCut (intern_constr ist c)
+ | TacTrueCut (na,c) ->
+ TacTrueCut (intern_name lf ist na, intern_constr ist c)
+ | TacForward (b,na,c) ->
+ TacForward (b,intern_name lf ist na,intern_constr ist c)
+ | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
+ | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
+ | TacLetTac (na,c,cls) ->
+ let na = intern_name lf ist na in
+ TacLetTac (na,intern_constr ist c,
+ (clause_app (intern_hyp_location ist) cls))
+ | TacInstantiate (n,c,cls) ->
+ TacInstantiate (n,intern_constr ist c,
+ (clause_app (intern_hyp_location ist) cls))
+
+ (* Automation tactics *)
+ | TacTrivial l -> TacTrivial l
+ | TacAuto (n,l) -> TacAuto (n,l)
+ | TacAutoTDB n -> TacAutoTDB n
+ | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
+ | TacDestructConcl -> TacDestructConcl
+ | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
+ | TacDAuto (n,p) -> TacDAuto (n,p)
+
+ (* Derived basic tactics *)
+ | TacSimpleInduction (h,ids) ->
+ TacSimpleInduction (intern_quantified_hypothesis ist h,ids)
+ | TacNewInduction (c,cbo,(ids,ids')) ->
+ TacNewInduction (intern_induction_arg ist c,
+ option_app (intern_constr_with_bindings ist) cbo,
+ (option_app (intern_intro_pattern lf ist) ids,ids'))
+ | TacSimpleDestruct h ->
+ TacSimpleDestruct (intern_quantified_hypothesis ist h)
+ | TacNewDestruct (c,cbo,(ids,ids')) ->
+ TacNewDestruct (intern_induction_arg ist c,
+ option_app (intern_constr_with_bindings ist) cbo,
+ (option_app (intern_intro_pattern lf ist) ids,ids'))
+ | 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 l -> TacClear (List.map (intern_hyp_or_metaid ist) l)
+ | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
+ | TacMove (dep,id1,id2) ->
+ TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2)
+ | TacRename (id1,id2) -> TacRename (intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2)
+
+ (* Constructors *)
+ | TacLeft bl -> TacLeft (intern_bindings ist bl)
+ | TacRight bl -> TacRight (intern_bindings ist bl)
+ | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
+ | TacAnyConstructor t -> TacAnyConstructor (option_app (intern_tactic ist) t)
+ | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
+
+ (* Conversion *)
+ | TacReduce (r,cl) ->
+ TacReduce (intern_redexp ist r, clause_app (intern_hyp_location ist) cl)
+ | TacChange (occl,c,cl) ->
+ TacChange (option_app (intern_constr_occurrence ist) occl,
+ 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 (intern_constr ist c)
+
+ (* Equality and inversion *)
+ | 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 (l1,l2) = ist.ltacvars in
+ let ist' = { ist with ltacvars = ((List.map fst l)@l1,l2) } in
+ let l = List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l in
+ try TacAlias (loc,s,l,(dir,intern_tactic ist' body))
+ with e -> raise (locate_error_in_file (string_of_dirpath dir) e)
+
+and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)
+
+and intern_tactic_seq ist = function
+ (* Traducteur v7->v8 *)
+ | TacAtom (_,TacReduce (Unfold [_,Ident (_,id)],_))
+ when string_of_id id = "INZ" & !Options.translate_syntax
+ -> ist.ltacvars, (TacId "")
+ (* Fin traducteur v7->v8 *)
+
+ | 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)
+ | TacLetRecIn (lrc,u) ->
+ let names = extract_names lrc in
+ let (l1,l2) = ist.ltacvars in
+ let ist = { ist with ltacvars = (names@l1,l2) } in
+ let lrc = List.map (fun (n,b) -> (n,intern_tactic_fun ist b)) lrc in
+ ist.ltacvars, TacLetRecIn (lrc,intern_tactic ist u)
+ | TacLetIn (l,u) ->
+ let l = List.map
+ (fun (n,c,b) ->
+ (n,option_app (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
+ let (l1,l2) = ist.ltacvars in
+ let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
+ ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
+ | TacMatchContext (lr,lmr) ->
+ ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
+ | TacMatch (c,lmr) ->
+ ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
+ | TacId _ as x -> ist.ltacvars, x
+ | TacFail (n,x) -> ist.ltacvars, TacFail (intern_int_or_var ist n,x)
+ | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
+ | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
+ | TacThen (t1,t2) ->
+ let lfun', t1 = intern_tactic_seq ist t1 in
+ let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
+ lfun'', TacThen (t1,t2)
+ | TacThens (t,tl) ->
+ let lfun', t = intern_tactic_seq ist t in
+ (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+ lfun',
+ TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
+ | TacDo (n,tac) ->
+ ist.ltacvars, TacDo (intern_int_or_var ist n,intern_tactic ist tac)
+ | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
+ | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
+ | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
+ | TacOrelse (tac1,tac2) ->
+ ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2)
+ | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l)
+ | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l)
+ | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a)
+
+and intern_tactic_fun ist (var,body) =
+ let (l1,l2) = ist.ltacvars in
+ let lfun' = List.rev_append (filter_some var) l1 in
+ (var,intern_tactic { ist with ltacvars = (lfun',l2) } body)
+
+and intern_tacarg strict ist = function
+ | TacVoid -> TacVoid
+ | Reference r -> intern_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,s) ->
+ (* $id can occur in Grammar tactic... *)
+ let id = id_of_string s in
+ if find_ltacvar id ist or Options.do_translate()
+ then Reference (ArgVar (adjust_loc loc,strip_meta id))
+ else error_syntactic_metavariables_not_allowed loc
+ | TacCall (loc,f,l) ->
+ TacCall (loc,
+ intern_tactic_reference ist f,
+ List.map (intern_tacarg !strict_check ist) l)
+ | TacFreshId _ as x -> x
+ | Tacexp t -> Tacexp (intern_tactic ist t)
+ | TacDynamic(loc,t) as x ->
+ (match tag t with
+ | "tactic" | "value" | "constr" -> x
+ | s -> anomaly_loc (loc, "",
+ str "Unknown dynamic: <" ++ str s ++ str ">"))
+
+(* Reads the rules of a Match Context or a Match *)
+and intern_match_rule ist = function
+ | (All tc)::tl ->
+ All (intern_tactic ist tc) :: (intern_match_rule ist tl)
+ | (Pat (rl,mp,tc))::tl ->
+ let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
+ let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
+ let ido,metas2,pat = intern_pattern sigma env lfun mp in
+ let metas = list_uniquize (metas1@metas2) in
+ let ist' = { ist with ltacvars = (metas@(option_cons ido lfun'),l2) } in
+ Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule 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_int_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 ->
+ let lf = ref ([],[]) in
+ in_gen globwit_ident(intern_ident lf ist (out_gen rawwit_ident x))
+ | HypArgType ->
+ 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_redexp ist (out_gen rawwit_red_expr x))
+ | TacticArgType ->
+ in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x))
+ | CastedOpenConstrArgType ->
+ in_gen globwit_casted_open_constr
+ (intern_constr ist (out_gen rawwit_casted_open_constr x))
+ | ConstrWithBindingsArgType ->
+ in_gen globwit_constr_with_bindings
+ (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+ | 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 -> lookup_genarg_glob s ist x
+
+(************* End globalization ************)
+
+(***************************************************************************)
+(* Evaluation/interpretation *)
+
+(* Associates variables with values and gives the remaining variables and
+ values *)
+let head_with_value (lvar,lval) =
+ let rec head_with_value_rec lacc = function
+ | ([],[]) -> (lacc,[],[])
+ | (vr::tvr,ve::tve) ->
+ (match vr with
+ | None -> head_with_value_rec lacc (tvr,tve)
+ | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+ | (vr,[]) -> (lacc,vr,[])
+ | ([],ve) -> (lacc,[],ve)
+ in
+ head_with_value_rec [] (lvar,lval)
+
+(* Gives a context couple if there is a context identifier *)
+let give_context ctxt = function
+ | None -> []
+ | Some id -> [id,VConstr_context ctxt]
+
+(* Reads a pattern by substituing vars of lfun *)
+let eval_pattern lfun c =
+ let lvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lfun in
+ instantiate_pattern lvar c
+
+let read_pattern evc env lfun = function
+ | Subterm (ido,pc) -> Subterm (ido,eval_pattern lfun pc)
+ | Term pc -> Term (eval_pattern lfun pc)
+
+(* Reads the hypotheses of a Match Context rule *)
+let cons_and_check_name id l =
+ if List.mem id l then
+ user_err_loc (loc,"read_match_context_hyps",
+ str ("Hypothesis pattern-matching variable "^(string_of_id id)^
+ " used twice in the same pattern"))
+ else id::l
+
+let rec read_match_context_hyps evc env lfun lidh = function
+ | (Hyp ((loc,na) as locna,mp))::tl ->
+ let lidh' = name_fold cons_and_check_name na lidh in
+ Hyp (locna,read_pattern evc env lfun mp)::
+ (read_match_context_hyps evc env lfun lidh' tl)
+ | [] -> []
+
+(* Reads the rules of a Match Context or a Match *)
+let rec read_match_rule evc env lfun = function
+ | (All tc)::tl -> (All tc)::(read_match_rule evc env lfun tl)
+ | (Pat (rl,mp,tc))::tl ->
+ Pat (read_match_context_hyps evc env lfun [] rl,
+ read_pattern evc env lfun mp,tc)
+ ::(read_match_rule evc env lfun tl)
+ | [] -> []
+
+(* For Match Context and Match *)
+exception No_match
+exception Not_coherent_metas
+exception Eval_fail of string
+
+let is_failure = function
+ | FailError _ | Stdpp.Exc_located (_,FailError _) -> true
+ | _ -> false
+
+let is_match_catchable = function
+ | No_match | Eval_fail _ -> true
+ | e -> is_failure e or Logic.catchable_exception e
+
+(* Verifies if the matched list is coherent with respect to lcm *)
+let rec verify_metas_coherence gl lcm = function
+ | (num,csr)::tl ->
+ if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then
+ (num,csr)::(verify_metas_coherence gl lcm tl)
+ else
+ raise Not_coherent_metas
+ | [] -> []
+
+(* Tries to match a pattern and a constr *)
+let apply_matching pat csr =
+ try
+ (matches pat csr)
+ with
+ PatternMatchingFailure -> raise No_match
+
+(* Tries to match one hypothesis pattern with a list of hypotheses *)
+let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) =
+ let get_id_couple id = function
+(* | Name idpat -> [idpat,VIdentifier id]*)
+ | Name idpat -> [idpat,VConstr (mkVar id)]
+ | Anonymous -> [] in
+ let rec apply_one_mhyp_context_rec nocc = function
+ | (id,hyp)::tl as hyps ->
+ (match pat with
+ | Term t ->
+ (try
+ let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
+ (get_id_couple id hypname,lmeta,(id,hyp),(tl,0))
+ with
+ | PatternMatchingFailure | Not_coherent_metas ->
+ apply_one_mhyp_context_rec 0 tl)
+ | Subterm (ic,t) ->
+ (try
+ let (lm,ctxt) = sub_match nocc t hyp in
+ let lmeta = verify_metas_coherence gl lmatch lm in
+ ((get_id_couple id hypname)@(give_context ctxt ic),
+ lmeta,(id,hyp),(hyps,nocc + 1))
+ with
+ | NextOccurrence _ ->
+ apply_one_mhyp_context_rec 0 tl
+ | Not_coherent_metas ->
+ apply_one_mhyp_context_rec (nocc + 1) hyps))
+ | [] ->
+ db_hyp_pattern_failure ist.debug env (hypname,pat);
+ raise No_match
+ in
+ apply_one_mhyp_context_rec nocc lhyps
+
+let constr_to_id loc = function
+ | VConstr c when isVar c -> destVar c
+ | _ -> invalid_arg_loc (loc, "Not an identifier")
+
+let constr_to_qid loc c =
+ try shortest_qualid_of_global Idset.empty (reference_of_constr c)
+ with _ -> invalid_arg_loc (loc, "Not a global reference")
+
+(* Debug reference *)
+let debug = ref DebugOff
+
+(* Sets the debugger mode *)
+let set_debug pos = debug := pos
+
+(* Gives the state of debug *)
+let get_debug () = !debug
+
+(* Interprets an identifier which must be fresh *)
+let interp_ident ist id =
+ try match List.assoc id ist.lfun with
+ | VIntroPattern (IntroIdentifier id) -> id
+ | VConstr c as v when isVar c ->
+ (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
+ (* c is then expected not to belong to the proof context *)
+ (* would be checkable if env were known from interp_ident *)
+ destVar c
+ | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++
+ str ") should have been bound to an identifier")
+ with Not_found -> id
+
+let interp_intro_pattern_var ist id =
+ try match List.assoc id ist.lfun with
+ | VIntroPattern ipat -> ipat
+ | VConstr c as v when isVar c ->
+ (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
+ (* c is then expected not to belong to the proof context *)
+ (* would be checkable if env were known from interp_ident *)
+ IntroIdentifier (destVar c)
+ | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++
+ str ") should have been bound to an introduction pattern")
+ with Not_found -> IntroIdentifier id
+
+let interp_int lfun (loc,id) =
+ try match List.assoc id lfun with
+ | VInteger n -> n
+ | _ -> user_err_loc(loc,"interp_int",str "should be bound to an integer")
+ with Not_found -> user_err_loc (loc,"interp_int",str "Unbound variable")
+
+let interp_int_or_var ist = function
+ | ArgVar locid -> interp_int ist.lfun locid
+ | ArgArg n -> n
+
+let constr_of_value env = function
+ | VConstr csr -> csr
+ | VIntroPattern (IntroIdentifier id) -> constr_of_id env id
+ | _ -> raise Not_found
+
+let is_variable env id =
+ List.mem id (ids_of_named_context (Environ.named_context env))
+
+let variable_of_value env = function
+ | VConstr c as v when isVar c -> destVar c
+ | VIntroPattern (IntroIdentifier id) when is_variable env id -> id
+ | _ -> raise Not_found
+
+(* Extract a variable from a value, if any *)
+let id_of_Identifier = variable_of_value
+
+(* Extract a constr from a value, if any *)
+let constr_of_VConstr = constr_of_value
+
+(* Interprets an variable *)
+let interp_var ist gl (loc,id) =
+ (* Look first in lfun for a value coercible to a variable *)
+ try
+ let v = List.assoc id ist.lfun in
+ try variable_of_value (pf_env gl) v
+ with Not_found ->
+ errorlabstrm "coerce_to_variable"
+ (str "Cannot coerce" ++ spc () ++ pr_value (pf_env gl) v ++ spc () ++
+ str "to a variable")
+ with Not_found ->
+ (* Then look if bound in the proof context at calling time *)
+ if is_variable (pf_env gl) id then id
+ else
+ user_err_loc (loc,"eval_variable",pr_id id ++ str " not found")
+
+(* Interprets an existing hypothesis (i.e. a declared variable) *)
+let interp_hyp = interp_var
+
+let interp_name ist = function
+ | Anonymous -> Anonymous
+ | Name id -> Name (interp_ident ist id)
+
+let interp_clause_pattern ist gl (l,occl) =
+ let rec check acc = function
+ | (hyp,l) :: rest ->
+ let hyp = interp_hyp ist gl hyp in
+ if List.mem hyp acc then
+ error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
+ (hyp,l)::(check (hyp::acc) rest)
+ | [] -> []
+ in (l,check [] occl)
+
+(* Interprets a qualified name *)
+let interp_reference ist env = function
+ | ArgArg (_,r) -> r
+ | ArgVar (loc,id) -> coerce_to_reference env (unrec (List.assoc id ist.lfun))
+
+let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
+
+let interp_inductive ist = function
+ | ArgArg r -> r
+ | ArgVar (_,id) -> coerce_to_inductive (unrec (List.assoc id ist.lfun))
+
+let interp_evaluable ist env = 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 (pr_id id)
+ with Not_found ->
+ match r with
+ | EvalConstRef _ -> r
+ | _ -> Pretype_errors.error_var_not_found_loc loc id)
+ | ArgArg (r,None) -> r
+ | ArgVar (_,id) ->
+ coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))
+
+(* Interprets an hypothesis name *)
+let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
+
+let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
+ { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol;
+ onconcl=b;
+ concl_occs=occs }
+
+(* Interpretation of constructions *)
+
+(* Extract the constr list from lfun *)
+let rec constr_list_aux env = function
+ | (id,v)::tl ->
+ let (l1,l2) = constr_list_aux env tl in
+ (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))
+ | [] -> ([],[])
+
+let constr_list ist env = constr_list_aux env ist.lfun
+
+(*Extract the identifier list from lfun: join all branches (what to do else?)*)
+let rec intropattern_ids = function
+ | IntroIdentifier id -> [id]
+ | IntroOrAndPattern ll ->
+ List.flatten (List.map intropattern_ids (List.flatten ll))
+ | IntroWildcard -> []
+
+let rec extract_ids = function
+ | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
+ | _::tl -> extract_ids tl
+ | [] -> []
+
+let retype_list sigma env lst =
+ List.fold_right (fun (x,csr) a ->
+ try (x,Retyping.get_judgment_of env sigma csr)::a with
+ | Anomaly _ -> a) lst []
+
+let interp_casted_constr ocl ist sigma env (c,ce) =
+ let (l1,l2) = constr_list ist env in
+ let tl1 = retype_list sigma env l1 in
+ let csr =
+ match ce with
+ | None ->
+ Pretyping.understand_gen_ltac sigma env (tl1,l2) ocl 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 -> interp_constr_gen sigma env (l1,l2) c ocl
+ in
+ db_constr ist.debug env csr;
+ csr
+
+let interp_constr ist sigma env c =
+ interp_casted_constr None ist sigma env c
+
+(* Interprets an open constr expression casted by the current goal *)
+let pf_interp_casted_openconstr ist gl (c,ce) =
+ let sigma = project gl in
+ let env = pf_env gl in
+ let (ltacvars,l) = constr_list ist env in
+ let typs = retype_list sigma env ltacvars in
+ let ocl = Some (pf_concl gl) in
+ match ce with
+ | None ->
+ Pretyping.understand_gen_tcc sigma env typs ocl 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 -> interp_openconstr_gen sigma env (ltacvars,l) c ocl
+
+(* Interprets a constr expression *)
+let pf_interp_constr ist gl =
+ interp_constr ist (project gl) (pf_env gl)
+
+(* Interprets a constr expression casted by the current goal *)
+let pf_interp_casted_constr ist gl c =
+ interp_casted_constr (Some(pf_concl gl)) ist (project gl) (pf_env gl) c
+
+(* Interprets a reduction expression *)
+let interp_unfold ist env (l,qid) =
+ (l,interp_evaluable ist env qid)
+
+let interp_flag ist env red =
+ { red with rConst = List.map (interp_evaluable ist env) red.rConst }
+
+let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c)
+
+let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)
+
+let redexp_interp ist sigma env = function
+ | Unfold l -> Unfold (List.map (interp_unfold ist env) l)
+ | Fold l -> Fold (List.map (interp_constr ist sigma env) l)
+ | Cbv f -> Cbv (interp_flag ist env f)
+ | Lazy f -> Lazy (interp_flag ist env f)
+ | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
+ | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
+ | (Red _ | Hnf as r) -> r
+ | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c)
+
+let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
+
+let interp_may_eval f ist gl = function
+ | ConstrEval (r,c) ->
+ let redexp = pf_redexp_interp ist gl r in
+ pf_reduction_of_redexp gl redexp (f ist gl c)
+ | ConstrContext ((loc,s),c) ->
+ (try
+ let ic = f ist gl c
+ and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in
+ subst_meta [special_meta,ic] ctxt
+ with
+ | Not_found ->
+ user_err_loc (loc, "interp_may_eval",
+ str "Unbound context identifier" ++ pr_id s))
+ | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
+ | ConstrTerm c -> f ist gl c
+
+(* Interprets a constr expression possibly to first evaluate *)
+let interp_constr_may_eval ist gl c =
+ let csr = interp_may_eval pf_interp_constr ist gl c in
+ begin
+ db_constr ist.debug (pf_env gl) csr;
+ csr
+ end
+
+let rec interp_intro_pattern ist = function
+ | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
+ | IntroWildcard -> IntroWildcard
+ | IntroIdentifier id -> interp_intro_pattern_var ist id
+
+and interp_case_intro_pattern ist =
+ List.map (List.map (interp_intro_pattern ist))
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let interp_quantified_hypothesis ist = function
+ | AnonHyp n -> AnonHyp n
+ | NamedHyp id ->
+ try match List.assoc id ist.lfun with
+ | VInteger n -> AnonHyp n
+ | VIntroPattern (IntroIdentifier id) -> NamedHyp id
+ | _ -> raise Not_found
+ with Not_found -> NamedHyp id
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let interp_declared_or_quantified_hypothesis ist gl = function
+ | AnonHyp n -> AnonHyp n
+ | NamedHyp id ->
+ try match List.assoc id ist.lfun with
+ | VInteger n -> AnonHyp n
+ | v -> NamedHyp (variable_of_value (pf_env gl) v)
+ with Not_found -> NamedHyp id
+
+let interp_induction_arg ist gl = function
+ | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent (loc,id) ->
+ if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+ else ElimOnConstr
+ (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
+
+let interp_binding ist gl (loc,b,c) =
+ (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c)
+
+let interp_bindings ist gl = function
+| NoBindings -> NoBindings
+| ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr ist gl) l)
+| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)
+
+let interp_constr_with_bindings ist gl (c,bl) =
+ (pf_interp_constr ist gl c, interp_bindings ist gl bl)
+
+(* Interprets an l-tac expression into a value *)
+let rec val_interp ist gl (tac:glob_tactic_expr) =
+
+ let value_interp ist = match tac with
+ (* Immediate evaluation *)
+ | TacFun (it,body) -> VFun (ist.lfun,it,body)
+ | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u
+ | TacLetIn (l,u) ->
+ let addlfun = interp_letin ist gl l in
+ val_interp { ist with lfun=addlfun@ist.lfun } gl u
+ | TacMatchContext (lr,lmr) -> interp_match_context ist gl lr lmr
+ | TacMatch (c,lmr) -> interp_match ist gl c lmr
+ | TacArg a -> interp_tacarg ist gl a
+ (* Delayed evaluation *)
+ | t -> VTactic (dummy_loc,eval_tactic ist 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
+ | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
+ | TacFun (it,body) -> assert false
+ | TacLetRecIn (lrc,u) -> assert false
+ | TacLetIn (l,u) -> assert false
+ | TacMatchContext _ -> assert false
+ | TacMatch (c,lmr) -> assert false
+ | TacId s -> tclIDTAC_MESSAGE s
+ | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s
+ | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
+ | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
+ | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
+ | TacThens (t,tl) ->
+ tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
+ | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
+ | TacTry tac -> tclTRY (interp_tactic ist tac)
+ | TacInfo tac -> tclINFO (interp_tactic ist tac)
+ | TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
+ | 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)
+ | TacArg a -> assert false
+
+and interp_ltac_reference isapplied ist gl = function
+ | ArgVar (loc,id) -> unrec (List.assoc id ist.lfun)
+ | ArgArg (loc,r) ->
+ let v = val_interp {lfun=[];debug=ist.debug} gl (lookup r) in
+ if isapplied then v else locate_tactic_call loc v
+
+and interp_tacarg ist gl = function
+ | TacVoid -> VVoid
+ | Reference r -> interp_ltac_reference false ist gl r
+ | Integer n -> VInteger n
+ | IntroPattern ipat -> VIntroPattern ipat
+ | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
+ | MetaIdArg (loc,id) -> assert false
+ | TacCall (loc,f,l) ->
+ let fv = interp_ltac_reference true ist gl f
+ and largs = List.map (interp_tacarg ist gl) l in
+ List.iter check_is_value largs;
+ interp_app ist gl fv largs loc
+ | TacFreshId idopt ->
+ let s = match idopt with None -> "H" | Some s -> s in
+ let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in
+ VIntroPattern (IntroIdentifier id)
+ | Tacexp t -> val_interp ist gl t
+ | TacDynamic(_,t) ->
+ let tg = (tag t) in
+ if tg = "tactic" then
+ let f = (tactic_out t) in
+ val_interp ist gl
+ (intern_tactic {
+ ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = [];
+ gsigma = project gl; genv = pf_env gl }
+ (f ist))
+ else if tg = "value" then
+ value_out t
+ else if tg = "constr" then
+ VConstr (Pretyping.constr_out t)
+ else
+ anomaly_loc (loc, "Tacinterp.val_interp",
+ (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
+
+(* Interprets an application node *)
+and interp_app ist gl fv largs loc =
+ match fv with
+ | VFun(olfun,var,body) ->
+ let (newlfun,lvar,lval)=head_with_value (var,largs) in
+ if lvar=[] then
+ let v = val_interp { ist with lfun=newlfun@olfun } gl body in
+ if lval=[] then locate_tactic_call loc v
+ else interp_app ist gl v lval loc
+ else
+ VFun(newlfun@olfun,lvar,body)
+ | _ ->
+ user_err_loc (loc, "Tacinterp.interp_app",
+ (str"Illegal tactic application"))
+
+(* Gives the tactic corresponding to the tactic value *)
+and tactic_of_value vle g =
+ match vle with
+ | VRTactic res -> res
+ | VTactic (loc,tac) -> catch_error loc tac g
+ | VFun _ -> error "A fully applied tactic is expected"
+ | _ -> raise NotTactic
+
+(* Evaluation with FailError catching *)
+and eval_with_fail ist tac goal =
+ try
+ (match val_interp ist goal tac with
+ | VTactic (loc,tac) -> VRTactic (catch_error loc tac goal)
+ | a -> a)
+ with
+ | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) ->
+ raise (Eval_fail s)
+ | Stdpp.Exc_located (s',FailError (lvl,s)) ->
+ raise (Stdpp.Exc_located (s',FailError (lvl - 1, s)))
+ | FailError (lvl,s) ->
+ raise (FailError (lvl - 1, s))
+
+(* Interprets recursive expressions *)
+and letrec_interp ist gl lrc u =
+ let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
+ let lenv =
+ List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
+ lrc lref [] in
+ let lve = List.map (fun ((loc,name),(var,body)) ->
+ (name,VFun(lenv@ist.lfun,var,body))) lrc in
+ begin
+ List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
+ val_interp { ist with lfun=lve@ist.lfun } gl u
+ end
+
+(* Interprets the clauses of a LetIn *)
+and interp_letin ist gl = function
+ | [] -> []
+ | ((loc,id),None,t)::tl ->
+ let v = interp_tacarg ist gl t in
+ check_is_value v;
+ (id,v):: (interp_letin ist gl tl)
+ | ((loc,id),Some com,tce)::tl ->
+ let env = pf_env gl in
+ let typ = constr_of_value env (val_interp ist gl com)
+ and v = interp_tacarg ist gl tce in
+ let csr =
+ try
+ constr_of_value env v
+ with Not_found ->
+ try
+ let t = tactic_of_value v in
+ let ndc = Environ.named_context env in
+ start_proof id IsLocal ndc typ (fun _ _ -> ());
+ by t;
+ let (_,({const_entry_body = pft},_,_)) = cook_proof () in
+ delete_proof (dummy_loc,id);
+ pft
+ with | NotTactic ->
+ delete_proof (dummy_loc,id);
+ errorlabstrm "Tacinterp.interp_letin"
+ (str "Term or fully applied tactic expected in Let")
+ in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
+
+(* Interprets the Match Context expressions *)
+and interp_match_context ist g lr lmr =
+ let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
+ try
+ let (lgoal,ctxt) = sub_match nocc c csr in
+ let lctxt = give_context ctxt id in
+ if mhyps = [] then
+ let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
+ eval_with_fail { ist with lfun=lgoal@lctxt@ist.lfun } mt goal
+ else
+ apply_hyps_context ist env goal mt lgoal mhyps hyps
+ with
+ | e when is_failure e -> raise e
+ | NextOccurrence _ -> raise No_match
+ | e when is_match_catchable e ->
+ apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+ let rec apply_match_context ist env goal nrs lex lpt =
+ 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 t goal
+ with e when is_match_catchable e ->
+ apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+ end
+ | (Pat (mhyps,mgoal,mt))::tl ->
+ let hyps = make_hyps (pf_hyps goal) in
+ let hyps = if lr then List.rev hyps else hyps in
+ let mhyps = List.rev mhyps (* Sens naturel *) in
+ let concl = pf_concl goal in
+ (match mgoal with
+ | Term mg ->
+ (try
+ (let lgoal = apply_matching mg concl in
+ begin
+ db_matched_concl ist.debug (pf_env goal) concl;
+ if mhyps = [] then
+ begin
+ db_mc_pattern_success ist.debug;
+ let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
+ eval_with_fail {ist with lfun=lgoal@ist.lfun} mt goal
+ end
+ else
+ apply_hyps_context ist env goal mt lgoal mhyps hyps
+ end)
+ with
+ | e when is_match_catchable e ->
+ begin
+ (match e with
+ | No_match -> db_matching_failure ist.debug
+ | Eval_fail s -> db_eval_failure ist.debug s
+ | _ -> db_logic_failure ist.debug e);
+ apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+ end)
+ | Subterm (id,mg) ->
+ (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+ with e when is_match_catchable e ->
+ apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
+ | _ ->
+ errorlabstrm "Tacinterp.apply_match_context" (str
+ "No matching clauses for match goal")
+ (v 0 (str "No matching clauses for match goal" ++
+ (if ist.debug=DebugOff then
+ fnl() ++ str "(use \"Debug On\" for more info)"
+ else mt())))
+ end in
+ let env = pf_env g in
+ apply_match_context ist env g 0 lmr
+ (read_match_rule (project g) env (fst (constr_list ist env)) lmr)
+
+(* Tries to match the hypotheses in a Match Context *)
+and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
+ let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
+ | Hyp ((_,hypname),mhyp)::tl as mhyps ->
+ let (lids,lm,hyp_match,next) =
+ apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in
+ db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
+ begin
+ try
+ let nextlhyps = list_except hyp_match lhyps_rest in
+ apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps
+ (nextlhyps,0) tl
+ with
+ | e when is_failure e -> raise e
+ | e when is_match_catchable e ->
+ apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps
+ end
+ | [] ->
+ let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in
+ db_mc_pattern_success ist.debug;
+ eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} mt goal
+ in
+ apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps
+
+ (* Interprets extended tactic generic arguments *)
+and interp_genarg ist goal 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 (out_gen globwit_intro_pattern x))
+ | IdentArgType ->
+ in_gen wit_ident (interp_ident ist (out_gen globwit_ident x))
+ | HypArgType ->
+ in_gen wit_var (mkVar (interp_hyp ist goal (out_gen globwit_var x)))
+ | RefArgType ->
+ in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x))
+ | SortArgType ->
+ in_gen wit_sort
+ (destSort
+ (pf_interp_constr ist goal
+ (RSort (dummy_loc,out_gen globwit_sort x), None)))
+ | ConstrArgType ->
+ in_gen wit_constr (pf_interp_constr ist goal (out_gen globwit_constr x))
+ | ConstrMayEvalArgType ->
+ in_gen wit_constr_may_eval (interp_constr_may_eval ist goal (out_gen globwit_constr_may_eval x))
+ | QuantHypArgType ->
+ in_gen wit_quant_hyp
+ (interp_declared_or_quantified_hypothesis ist goal
+ (out_gen globwit_quant_hyp x))
+ | RedExprArgType ->
+ in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
+ | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x)
+ | CastedOpenConstrArgType ->
+ in_gen wit_casted_open_constr
+ (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x))
+ | ConstrWithBindingsArgType ->
+ in_gen wit_constr_with_bindings
+ (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
+ | BindingsArgType ->
+ in_gen wit_bindings
+ (interp_bindings ist goal (out_gen globwit_bindings x))
+ | List0ArgType _ -> app_list0 (interp_genarg ist goal) x
+ | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
+ | OptArgType _ -> app_opt (interp_genarg ist goal) x
+ | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x
+ | ExtraArgType s -> lookup_interp_genarg s ist goal x
+
+(* Interprets the Match expressions *)
+and interp_match ist g constr lmr =
+ let rec apply_sub_match ist nocc (id,c) csr mt =
+ try
+ let (lm,ctxt) = sub_match nocc c csr in
+ let lctxt = give_context ctxt id in
+ let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+ val_interp {ist with lfun=lm@lctxt@ist.lfun} g mt
+ with | NextOccurrence _ -> raise No_match
+ in
+ let rec apply_match ist csr = function
+ | (All t)::_ ->
+ (try val_interp ist g t
+ with e when is_match_catchable e -> apply_match ist csr [])
+ | (Pat ([],Term c,mt))::tl ->
+ (try
+ let lm = apply_matching c csr in
+ let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+ val_interp
+ { ist with lfun=lm@ist.lfun } g mt
+ with e when is_match_catchable e -> apply_match ist csr tl)
+ | (Pat ([],Subterm (id,c),mt))::tl ->
+ (try
+ apply_sub_match ist 0 (id,c) csr mt
+ with | No_match ->
+ apply_match ist csr tl)
+ | _ ->
+ errorlabstrm "Tacinterp.apply_match" (str
+ "No matching clauses for match") in
+ let env = pf_env g in
+ let csr =
+ try constr_of_value env (val_interp ist g constr)
+ with Not_found ->
+ errorlabstrm "Tacinterp.apply_match"
+ (str "Argument of match does not evaluate to a term") in
+ let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in
+ apply_match ist csr ilr
+
+(* Interprets tactic expressions : returns a "tactic" *)
+and interp_tactic ist tac gl =
+ try tactic_of_value (val_interp ist gl tac) gl
+ with | NotTactic ->
+ errorlabstrm "Tacinterp.interp_tactic" (str
+ "Must be a command or must give a tactic value")
+
+(* Interprets a primitive tactic *)
+and interp_atomic ist gl = function
+ (* Basic tactics *)
+ | TacIntroPattern l ->
+ h_intro_patterns (List.map (interp_intro_pattern ist) l)
+ | TacIntrosUntil hyp ->
+ h_intros_until (interp_quantified_hypothesis ist hyp)
+ | TacIntroMove (ido,ido') ->
+ h_intro_move (option_app (interp_ident ist) ido)
+ (option_app (interp_hyp ist gl) ido')
+ | TacAssumption -> h_assumption
+ | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
+ | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
+ | TacElim (cb,cbo) ->
+ h_elim (interp_constr_with_bindings ist gl cb)
+ (option_app (interp_constr_with_bindings ist gl) cbo)
+ | TacElimType c -> h_elim_type (pf_interp_constr ist gl c)
+ | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
+ | TacCaseType c -> h_case_type (pf_interp_constr ist gl c)
+ | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n
+ | TacMutualFix (id,n,l) ->
+ let f (id,n,c) = (interp_ident ist id,n,pf_interp_constr ist gl c) in
+ h_mutual_fix (interp_ident ist id) n (List.map f l)
+ | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt)
+ | TacMutualCofix (id,l) ->
+ let f (id,c) = (interp_ident ist id,pf_interp_constr ist gl c) in
+ h_mutual_cofix (interp_ident ist id) (List.map f l)
+ | TacCut c -> h_cut (pf_interp_constr ist gl c)
+ | TacTrueCut (na,c) ->
+ h_true_cut (interp_name ist na) (pf_interp_constr ist gl c)
+ | TacForward (b,na,c) ->
+ h_forward b (interp_name ist na) (pf_interp_constr ist gl c)
+ | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
+ | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
+ | TacLetTac (na,c,clp) ->
+ let clp = interp_clause ist gl clp in
+ h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
+ | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
+ (clause_app (interp_hyp_location ist gl) ido)
+
+ (* Automation tactics *)
+ | TacTrivial l -> Auto.h_trivial l
+ | TacAuto (n, l) -> Auto.h_auto n l
+ | TacAutoTDB n -> Dhyp.h_auto_tdb n
+ | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
+ | TacDestructConcl -> Dhyp.h_destructConcl
+ | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
+ | TacDAuto (n,p) -> Auto.h_dauto (n,p)
+
+ (* Derived basic tactics *)
+ | TacSimpleInduction (h,ids) ->
+ let h =
+ if !Options.v7 then interp_declared_or_quantified_hypothesis ist gl h
+ else interp_quantified_hypothesis ist h in
+ h_simple_induction (h,ids)
+ | TacNewInduction (c,cbo,(ids,ids')) ->
+ h_new_induction (interp_induction_arg ist gl c)
+ (option_app (interp_constr_with_bindings ist gl) cbo)
+ (option_app (interp_intro_pattern ist) ids,ids')
+ | TacSimpleDestruct h ->
+ h_simple_destruct (interp_quantified_hypothesis ist h)
+ | TacNewDestruct (c,cbo,(ids,ids')) ->
+ h_new_destruct (interp_induction_arg ist gl c)
+ (option_app (interp_constr_with_bindings ist gl) cbo)
+ (option_app (interp_intro_pattern ist) ids,ids')
+ | 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 -> Elim.h_decompose_and (pf_interp_constr ist gl c)
+ | TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c)
+ | TacDecompose (l,c) ->
+ let l = List.map (interp_inductive ist) l in
+ Elim.h_decompose l (pf_interp_constr ist gl c)
+ | TacSpecialize (n,l) ->
+ h_specialize n (interp_constr_with_bindings ist gl l)
+ | TacLApply c -> h_lapply (pf_interp_constr ist gl c)
+
+ (* Context management *)
+ | TacClear l -> h_clear (List.map (interp_hyp ist gl) l)
+ | TacClearBody l -> h_clear_body (List.map (interp_hyp ist gl) l)
+ | TacMove (dep,id1,id2) ->
+ h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
+ | TacRename (id1,id2) ->
+ h_rename (interp_hyp ist gl id1) (interp_ident ist (snd id2))
+
+ (* Constructors *)
+ | TacLeft bl -> h_left (interp_bindings ist gl bl)
+ | TacRight bl -> h_right (interp_bindings ist gl bl)
+ | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
+ | TacAnyConstructor t ->
+ abstract_tactic (TacAnyConstructor t)
+ (Tactics.any_constructor (option_app (interp_tactic ist) t))
+ | TacConstructor (n,bl) ->
+ h_constructor (skip_metaid n) (interp_bindings ist gl bl)
+
+ (* Conversion *)
+ | TacReduce (r,cl) ->
+ h_reduce (pf_redexp_interp ist gl r) (interp_clause ist gl cl)
+ | TacChange (occl,c,cl) ->
+ h_change (option_app (pf_interp_pattern ist gl) occl)
+ (pf_interp_constr ist gl c) (interp_clause ist gl cl)
+
+ (* Equivalence relations *)
+ | TacReflexivity -> h_reflexivity
+ | TacSymmetry c -> h_symmetry (interp_clause ist gl c)
+ | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
+
+ (* Equality and inversion *)
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ Inv.dinv k (option_app (pf_interp_constr ist gl) c)
+ (option_app (interp_intro_pattern ist) ids)
+ (interp_declared_or_quantified_hypothesis ist gl hyp)
+ | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
+ Inv.inv_clause k
+ (option_app (interp_intro_pattern ist) ids)
+ (List.map (interp_hyp ist gl) idl)
+ (interp_declared_or_quantified_hypothesis ist gl hyp)
+ | TacInversion (InversionUsing (c,idl),hyp) ->
+ Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp)
+ (pf_interp_constr ist gl c)
+ (List.map (interp_hyp ist gl) idl)
+
+ (* For extensions *)
+ | TacExtend (loc,opn,l) ->
+ fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl
+ | TacAlias (loc,_,l,(_,body)) -> fun gl ->
+ let rec f x = match genarg_tag x with
+ | IntArgType -> VInteger (out_gen globwit_int x)
+ | IntOrVarArgType ->
+ VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x))
+ | PreIdentArgType ->
+ failwith "pre-identifiers cannot be bound"
+ | IntroPatternArgType ->
+ VIntroPattern (out_gen globwit_intro_pattern x)
+ | IdentArgType ->
+ VIntroPattern (IntroIdentifier (out_gen globwit_ident x))
+ | HypArgType ->
+ VConstr (mkVar (interp_var ist gl (out_gen globwit_var x)))
+ | RefArgType ->
+ VConstr (constr_of_reference
+ (pf_interp_reference ist gl (out_gen globwit_ref x)))
+ | SortArgType ->
+ VConstr (mkSort (Pretyping.interp_sort (out_gen globwit_sort x)))
+ | ConstrArgType ->
+ VConstr (pf_interp_constr ist gl (out_gen globwit_constr x))
+ | ConstrMayEvalArgType ->
+ VConstr
+ (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
+ | TacticArgType ->
+ val_interp ist gl (out_gen globwit_tactic x)
+ | StringArgType | BoolArgType
+ | QuantHypArgType | RedExprArgType
+ | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType
+ | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _
+ -> error "This generic type is not supported in alias"
+ in
+ let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
+ let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body)
+ in tactic_of_value v gl
+
+(* Initial call for interpretation *)
+let interp_tac_gen lfun debug t gl =
+ interp_tactic { lfun=lfun; debug=debug }
+ (intern_tactic {
+ ltacvars = (List.map fst lfun, []); ltacrecvars = [];
+ gsigma = project gl; genv = pf_env gl } t) gl
+
+let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t
+
+let interp t = interp_tac_gen [] (get_debug()) t
+
+(* Hides interpretation for pretty-print *)
+let hide_interp t ot gl =
+ let ist = { ltacvars = ([],[]); ltacrecvars = [];
+ gsigma = project gl; genv = pf_env gl } in
+ let te = intern_tactic ist t in
+ let t = eval_tactic te in
+ match ot with
+ | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
+ | Some t' -> abstract_tactic_expr (TacArg (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_inductive subst (kn,i) = (subst_kn subst kn,i)
+
+let subst_rawconstr subst (c,e) =
+ assert (e=None); (* e<>None only for toplevel tactics *)
+ (subst_raw subst c,None)
+
+let subst_binding subst (loc,b,c) =
+ (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)
+
+let subst_bindings subst = function
+ | NoBindings -> NoBindings
+ | ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l)
+ | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)
+
+let subst_raw_with_bindings subst (c,bl) =
+ (subst_rawconstr subst c, subst_bindings subst bl)
+
+let subst_induction_arg subst = function
+ | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent id as x -> x
+
+let subst_evaluable_reference subst = function
+ | EvalVarRef id -> EvalVarRef id
+ | EvalConstRef kn -> EvalConstRef (subst_kn subst kn)
+
+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) = (loc,f id)
+
+let subst_reference subst =
+ subst_or_var (subst_located (subst_kn subst))
+
+let subst_global_reference subst =
+ subst_or_var (subst_located (subst_global subst))
+
+let subst_evaluable subst =
+ subst_or_var (subst_and_short_name (subst_evaluable_reference subst))
+
+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_occurrence subst (l,c) = (l,subst_rawconstr subst c)
+
+let subst_redexp subst = function
+ | Unfold l -> Unfold (List.map (subst_unfold subst) l)
+ | Fold l -> Fold (List.map (subst_rawconstr subst) l)
+ | Cbv f -> Cbv (subst_flag subst f)
+ | Lazy f -> Lazy (subst_flag subst f)
+ | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
+ | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
+ | (Red _ | Hnf as r) -> r
+ | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c)
+
+let subst_raw_may_eval subst = function
+ | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
+ | ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c)
+ | ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c)
+ | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
+
+let subst_match_pattern subst = function
+ | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc)
+ | Term pc -> Term (subst_pattern subst pc)
+
+let rec subst_match_context_hyps subst = function
+ | Hyp (locs,mp) :: tl ->
+ Hyp (locs,subst_match_pattern subst mp)
+ :: subst_match_context_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_rawconstr subst c)
+ | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
+ | TacElim (cb,cbo) ->
+ TacElim (subst_raw_with_bindings subst cb,
+ option_app (subst_raw_with_bindings subst) cbo)
+ | TacElimType c -> TacElimType (subst_rawconstr subst c)
+ | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
+ | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
+ | TacFix (idopt,n) as x -> x
+ | TacMutualFix (id,n,l) ->
+ TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+ | TacCofix idopt as x -> x
+ | TacMutualCofix (id,l) ->
+ TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
+ | TacCut c -> TacCut (subst_rawconstr subst c)
+ | TacTrueCut (ido,c) -> TacTrueCut (ido, subst_rawconstr subst c)
+ | TacForward (b,na,c) -> TacForward (b,na,subst_rawconstr subst c)
+ | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
+ | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
+ | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
+ | TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
+
+ (* Automation tactics *)
+ | TacTrivial l -> TacTrivial l
+ | TacAuto (n,l) -> TacAuto (n,l)
+ | TacAutoTDB n -> TacAutoTDB n
+ | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
+ | TacDestructConcl -> TacDestructConcl
+ | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
+ | TacDAuto (n,p) -> TacDAuto (n,p)
+
+ (* Derived basic tactics *)
+ | TacSimpleInduction h as x -> x
+ | TacNewInduction (c,cbo,ids) ->
+ TacNewInduction (subst_induction_arg subst c,
+ option_app (subst_raw_with_bindings subst) cbo, ids)
+ | TacSimpleDestruct h as x -> x
+ | TacNewDestruct (c,cbo,ids) ->
+ TacNewDestruct (subst_induction_arg subst c,
+ option_app (subst_raw_with_bindings subst) cbo, ids)
+ | TacDoubleInduction (h1,h2) as x -> x
+ | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
+ | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
+ | TacDecompose (l,c) ->
+ let l = List.map (subst_or_var (subst_inductive subst)) l in
+ TacDecompose (l,subst_rawconstr subst c)
+ | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l)
+ | TacLApply c -> TacLApply (subst_rawconstr subst c)
+
+ (* Context management *)
+ | TacClear l as x -> x
+ | TacClearBody l as x -> x
+ | TacMove (dep,id1,id2) as x -> x
+ | TacRename (id1,id2) as x -> x
+
+ (* Constructors *)
+ | TacLeft bl -> TacLeft (subst_bindings subst bl)
+ | TacRight bl -> TacRight (subst_bindings subst bl)
+ | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
+ | TacAnyConstructor t -> TacAnyConstructor (option_app (subst_tactic subst) t)
+ | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
+
+ (* Conversion *)
+ | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
+ | TacChange (occl,c,cl) ->
+ TacChange (option_app (subst_constr_occurrence subst) occl,
+ subst_rawconstr subst c, cl)
+
+ (* Equivalence relations *)
+ | TacReflexivity | TacSymmetry _ as x -> x
+ | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
+
+ (* Equality and inversion *)
+ | TacInversion (DepInversion (k,c,l),hyp) ->
+ TacInversion (DepInversion (k,option_app (subst_rawconstr subst) c,l),hyp)
+ | TacInversion (NonDepInversion _,_) as x -> x
+ | TacInversion (InversionUsing (c,cl),hyp) ->
+ TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
+
+ (* For extensions *)
+ | TacExtend (_loc,opn,l) ->
+ TacExtend (loc,opn,List.map (subst_genarg subst) l)
+ | TacAlias (_,s,l,(dir,body)) ->
+ TacAlias (loc,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 (loc, subst_atomic subst t)
+ | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
+ | TacLetRecIn (lrc,u) ->
+ let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
+ TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
+ | TacLetIn (l,u) ->
+ let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
+ TacLetIn (l,subst_tactic subst u)
+ | TacMatchContext (lr,lmr) ->
+ TacMatchContext(lr, subst_match_rule subst lmr)
+ | TacMatch (c,lmr) ->
+ TacMatch (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,t2) ->
+ TacThen (subst_tactic subst t1,subst_tactic subst t2)
+ | TacThens (t,tl) ->
+ TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
+ | TacDo (n,tac) -> TacDo (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)
+ | TacArg a -> TacArg (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)
+ | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
+ | Tacexp t -> Tacexp (subst_tactic subst t)
+ | TacDynamic(_,t) as x ->
+ (match tag t with
+ | "tactic" | "value" | "constr" -> x
+ | s -> anomaly_loc (loc, "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_context_hyps subst rl in
+ let pat = subst_match_pattern subst mp in
+ Pat (hyps,pat,subst_tactic subst tc)
+ ::(subst_match_rule subst tl)
+ | [] -> []
+
+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 -> in_gen globwit_ident (out_gen globwit_ident x)
+ | HypArgType -> 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_rawconstr 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))
+ | TacticArgType ->
+ in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x))
+ | CastedOpenConstrArgType ->
+ in_gen globwit_casted_open_constr
+ (subst_rawconstr subst (out_gen globwit_casted_open_constr x))
+ | ConstrWithBindingsArgType ->
+ in_gen globwit_constr_with_bindings
+ (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
+ | 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 -> lookup_genarg_subst s subst x
+
+(***************************************************************************)
+(* Tactic registration *)
+
+(* For bad tactic calls *)
+let bad_tactic_args s =
+ anomalylabstrm s
+ (str "Tactic " ++ str s ++ str " called with bad arguments")
+
+(* Declaration of the TAC-DEFINITION object *)
+let add (kn,td) = mactab := Gmap.add kn td !mactab
+
+let load_md i ((sp,kn),defs) =
+ let dp,_ = repr_path sp in
+ let mp,dir,_ = repr_kn kn in
+ List.iter (fun (id,t) ->
+ 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)) defs
+
+let open_md i((sp,kn),defs) =
+ let dp,_ = repr_path sp in
+ let mp,dir,_ = repr_kn kn in
+ List.iter (fun (id,t) ->
+ 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) defs
+
+let cache_md x = load_md 1 x
+
+let subst_md (_,subst,defs) =
+ List.map (fun (id,t) -> (id,subst_tactic subst t)) defs
+
+let (inMD,outMD) =
+ 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 = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x)}
+
+(* Adds a definition for tactics in the table *)
+let make_absolute_name (loc,id) =
+ let kn = Lib.make_kn id in
+ if Gmap.mem kn !mactab or is_atomic_kn kn then
+ user_err_loc (loc,"Tacinterp.add_tacdef",
+ str "There is already an Ltac named " ++ pr_id id);
+ kn
+
+let make_empty_glob_sign () =
+ { ltacvars = ([],[]); ltacrecvars = [];
+ gsigma = Evd.empty; genv = Global.env() }
+
+let add_tacdef isrec tacl =
+(* let isrec = if !Options.p1 then isrec else true in*)
+ let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
+ let ist =
+ {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
+ let gtacl =
+ List.map (fun ((_,id),def) ->
+ (id,Options.with_option strict_check (intern_tactic ist) def))
+ tacl in
+ let id0 = fst (List.hd rfun) in
+ let _ = Lib.add_leaf id0 (inMD gtacl) in
+ List.iter
+ (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
+ rfun
+
+(***************************************************************************)
+(* Other entry points *)
+
+let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+
+let glob_tactic_env l env x =
+ intern_tactic
+ { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }
+ x
+
+let interp_redexp env evc r =
+ let ist = { lfun=[]; debug=get_debug () } in
+ let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = evc } in
+ redexp_interp ist evc env (intern_redexp gist r)
+
+(***************************************************************************)
+(* 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;debug=get_debug()})
+let _ = Auto.set_extern_intern_tac
+ (fun l ->
+ Options.with_option strict_check
+ (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
+let _ = Auto.set_extern_subst_tactic subst_tactic
+let _ = Dhyp.set_extern_interp eval_tactic
+let _ = Dhyp.set_extern_intern_tac
+ (fun t -> intern_tactic (make_empty_glob_sign()) t)