(* $Id$ *) open Astterm open Closure open Generic open Libobject open Pattern open Pp open Rawterm open Sign open Tacred open Util open Names open Proof_type open Tacmach open Macros open Coqast open Ast open Term let err_msg_tactic_not_found macro_loc macro = user_err_loc (macro_loc,"macro_expand", [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >]) (*Values for interpretation*) type value= VTactic of tactic |VFTactic of tactic_arg list*(tactic_arg list->tactic) |VRTactic of (goal list sigma * validation) |VArg of tactic_arg |VFun of (string*value) list*string option list*Coqast.t |VVoid |VRec of value ref (*Gives the identifier corresponding to an Identifier tactic_arg*) let id_of_Identifier=function Identifier id -> id |_ -> anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">] (*Gives the constr corresponding to a Constr tactic_arg*) let constr_of_Constr=function Constr c -> c |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">] (*Signature for interpretation: val_interp and interpretation functions*) type interp_sign= evar_declarations*Environ.env*(string*value) list*(int*constr) list* goal sigma option (*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 (Hashtbl.remove interp_tab ast_typ; warning ("Overwriting definition of tactic interpreter command "^ast_typ)); 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 glob_nvar id= try Nametab.sp_of_id CCI id with Not_found -> error ("unbound variable "^(string_of_id id)) (*Summary and Object declaration*) let mactab=ref Gmap.empty let lookup id=Gmap.find id !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 } let (inMD,outMD)= let add (na,td)=mactab:=Gmap.add na td !mactab in let cache_md (_,(na,td))=add (na,td) in declare_object ("TACTIC-DEFINITION", {cache_function=cache_md; load_function=(fun _ -> ()); open_function=(fun _ -> ()); specification_function=(fun x -> x)}) (*Adds a Tactic Definition in the table*) let add_tacdef na vbody = if Gmap.mem na !mactab then errorlabstrm "Tacdef.add_tacdef" [< 'sTR "There is already a Tactic Definition named "; 'sTR na >]; let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in if Options.is_verbose() then mSGNL [< 'sTR (na^" is defined") >] (*Unboxes the tactic_arg*) let unvarg=function VArg a -> a |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">] (*Unboxes VRec*) let unrec=function VRec v -> !v |a -> a (*Unboxes REDEXP*) let unredexp=function Redexp c -> c |_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">] (*Reads the head of Fun*) let read_fun ast= let rec read_fun_rec=function Node(_,"VOID",[])::tl -> None::(read_fun_rec tl) |Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl) |[] -> [] |_ -> anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">] in match ast with Node(_,"FUNVAR",l) -> read_fun_rec l |_ -> anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">] (*Reads the clauses of a Rec*) let rec read_rec_clauses=function [] -> [] |Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl -> (name,it,body)::(read_rec_clauses tl) |_ -> anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR "Rec not well formed">] (*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) (*Type of hypotheses for a Match Context rule*) type match_context_hyps= NoHypId of constr_pattern |Hyp of string*constr_pattern (*Type of a Match rule for Match Context and Match*) type match_rule= Pat of match_context_hyps list*constr_pattern*Coqast.t |All of Coqast.t (*Gives the ast of a COMMAND ast node*) let ast_of_command=function Node(_,"COMMAND",[c]) -> c |ast -> anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR "Not a COMMAND ast node: ";print_ast ast>]) (*Reads the hypotheses of a Match Context rule*) let rec read_match_context_hyps evc env=function Node(_,"MATCHCONTEXTHYPS",[pc])::tl -> (NoHypId (snd (interp_constrpattern evc env (ast_of_command pc))))::(read_match_context_hyps evc env tl) |Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl -> (Hyp (s,snd (interp_constrpattern evc env (ast_of_command pc))))::(read_match_context_hyps evc env tl) |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR "Not a MATCHCONTEXTHYP ast node: ";print_ast ast>]) |[] -> [] (*Reads the rules of a Match Context*) let rec read_match_context_rule evc env=function Node(_,"MATCHCONTEXTRULE",[tc])::tl -> (All tc)::(read_match_context_rule evc env tl) |Node(_,"MATCHCONTEXTRULE",l)::tl -> let rl=List.rev l in (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd (interp_constrpattern evc env (ast_of_command (List.nth rl 1))),List.hd rl))::(read_match_context_rule evc env tl) |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR "Not a MATCHCONTEXTRULE ast node: ";print_ast ast>]) |[] -> [] (*Reads the rules of a Match*) let rec read_match_rule evc env=function Node(_,"MATCHRULE",[te])::tl -> (All te)::(read_match_rule evc env tl) |Node(_,"MATCHRULE",[com;te])::tl -> (Pat ([],snd (interp_constrpattern evc env (ast_of_command com)),te))::(read_match_rule evc env tl) |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR "Not a MATCHRULE ast node: ";print_ast ast>]) |[] -> [] (*Transforms a type_judgment signature into a (string*constr) list*) let make_hyps hyps= let lid=List.map string_of_id (ids_of_sign hyps) and lhyp=List.map body_of_type (vals_of_sign hyps) in List.combine lid lhyp (*For Match Context and Match*) exception No_match exception Not_coherent_metas (*Verifies if the matched list is coherent with respect to lcm*) let rec verify_metas_coherence lcm=function (num,csr)::tl -> if (List.for_all (fun (a,b) -> if a=num then eq_constr b csr else true) lcm) then (num,csr)::(verify_metas_coherence lcm tl) else raise Not_coherent_metas |[] -> [] (*Tries to match a pattern and a constr*) let apply_matching pat csr= try (Pattern.matches pat csr) with PatternMatchingFailure -> raise No_match (*Tries to match one hypothesis with a list of hypothesis patterns*) let apply_one_hyp_context lmatch mhyps (idhyp,hyp)= let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc=function (Hyp (idpat,pat))::tl -> (try ([idpat,VArg (Identifier (id_of_string idhyp))],verify_metas_coherence lmatch (Pattern.matches pat hyp),mhyps_acc@tl) with PatternMatchingFailure|Not_coherent_metas -> apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[Hyp (idpat,pat)]) tl) |(NoHypId pat)::tl -> (try ([],verify_metas_coherence lmatch (Pattern.matches pat hyp),mhyps_acc@tl) with PatternMatchingFailure|Not_coherent_metas -> apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat]) tl) |[] -> raise No_match in apply_one_hyp_context_rec (idhyp,hyp) [] mhyps (*Prepares the lfun list for constr substitutions*) let rec make_subs_list=function (id,VArg (Identifier i))::tl -> (id_of_string id,VAR i)::(make_subs_list tl) |(id,VArg (Constr c))::tl -> (id_of_string id,c)::(make_subs_list tl) |e::tl -> make_subs_list tl |[] -> [] (*Interprets any expression*) let rec val_interp (evc,env,lfun,lmatch,goalopt) ast= (* mSGNL [];*) (*mSGNL [];*) match ast with Node(_,"APP",l) -> let fv=val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l) and largs= List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl l) in app_interp evc env lfun lmatch goalopt fv largs ast |Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) |Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l |Node(_,"LET",[Node(_,"LETDECL",l);u]) -> let addlfun=let_interp evc env lfun lmatch goalopt ast l in val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u |Node(_,"MATCHCONTEXT",lmr) -> match_context_interp evc env lfun lmatch goalopt ast lmr |Node(_,"MATCH",lmr) -> match_interp evc env lfun lmatch goalopt ast lmr |Node(_,"IDTAC",[]) -> VTactic tclIDTAC |Node(_,"FAIL",[]) -> VTactic tclFAIL |Node(_,"TACTICLIST",l) -> VTactic (interp_semi_list tclIDTAC lfun lmatch l) |Node(_,"DO",[n;tac]) -> VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac)) |Node(_,"TRY",[tac]) -> VTactic (tclTRY (tac_interp lfun lmatch tac)) |Node(_,"INFO",[tac]) -> VTactic (tclINFO (tac_interp lfun lmatch tac)) |Node(_,"REPEAT",[tac]) -> VTactic (tclREPEAT (tac_interp lfun lmatch tac)) |Node(_,"ORELSE",[tac1;tac2]) -> VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch tac2)) |Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l)) |Node(_,"TCLSOLVE",l) -> VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l)) |Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1, "PRIM-TACTIC",[Node(loc1,s,[])])]@l)) |Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> VFTactic ([],(interp_atomic loc opn)) |Node(_,"VOID",[]) -> VVoid |Nvar(_,s) -> (try (unrec (List.assoc s (List.rev lfun))) with Not_found -> (try (lookup s) with Not_found -> VArg (Identifier (id_of_string s)))) |Str(_,s) -> VArg (Quoted_string s) |Num(_,n) -> VArg (Integer n) |Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c |Node(_,"CASTEDCOMMAND",[c]) -> cast_com_interp (evc,env,lfun,lmatch,goalopt) c |Node(_,"BINDINGS",astl) -> VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt) astl)) |Node(_,"REDEXP",[Node(_,redname,args)]) -> VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt) (redname,args))) |Node(_,"CLAUSE",cl) -> VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast))) cl)) |Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast)) (*Remains to treat*) |Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> VArg ((Fixexp (id_of_string s,n,c))) |Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> VArg ((Cofixexp (id_of_string s,c))) (*End of Remains to treat*) |Node(_,"INTROPATTERN", [ast]) -> VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) ast))) |Node(_,"LETPATTERNS",astl) -> VArg (Letpatterns (List.fold_left (cvt_letpattern (evc,env,lfun,lmatch,goalopt)) (None,[]) astl)) |Node(loc,s,l) -> (try ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast) with Not_found -> val_interp (evc,env,lfun,lmatch,goalopt) (Node(dummy_loc,"APPTACTIC",[ast]))) |_ -> anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR "Unrecognizable ast: ";print_ast ast>]) (*Interprets an application node*) and app_interp evc env lfun lmatch goalopt fv largs ast= match fv with VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) |VFun(olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then if lval=[] then val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body else app_interp evc env lfun lmatch goalopt (val_interp (evc,env, (olfun@newlfun),lmatch,goalopt) body) lval ast else VFun(olfun@newlfun,lvar,body) |_ -> anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR "Illegal application: "; print_ast ast>]) (*Interprets recursive expressions*) and rec_interp evc env lfun lmatch goalopt ast=function [Node(_,"RECCLAUSE",_)] as l -> let (name,var,body)=List.hd (read_rec_clauses l) and ve=ref VVoid in let newve= VFun(lfun@[(name,VRec ve)],read_fun var,body) in ve:=newve; !ve |[Node(_,"RECDECL",l);u] -> let lrc=read_rec_clauses l in let lref=Array.to_list (Array.make (List.length lrc) (ref VVoid)) in let lenv= List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) lrc lref [] in let lve= List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun var,body))) lrc in List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; val_interp (evc,env,(lfun@lve),lmatch,goalopt) u |_ -> anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR "Rec not well formed: "; print_ast ast>]) (*Interprets the clauses of a let*) and let_interp evc env lfun lmatch goalopt ast=function [] -> [] |Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun lmatch goalopt ast tl) |_ -> anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR "Let not well formed: "; print_ast ast>]) (*Interprets the Match Context expressions*) and match_context_interp evc env lfun lmatch goalopt ast lmr= let rec apply_match_context evc env lfun lmatch goalopt=function (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t |(Pat (mhyps,mgoal,mt))::tl -> (match goalopt with None -> errorlabstrm "Tacinterp.apply_match_context" [<'sTR "No goal available">] |Some g -> let hyps=make_hyps (pf_hyps g) and concl=pf_concl g in try (let lgoal=apply_matching mgoal concl in if mhyps=[] then val_interp (evc,env,lfun,lgoal@lmatch,goalopt) mt else apply_hyps_context evc env lfun lmatch g mt lgoal mhyps hyps) with No_match -> apply_match_context evc env lfun lmatch goalopt tl) |_ -> errorlabstrm "Tacinterp.apply_match_context" [<'sTR "No matching clauses for Match Context">] in apply_match_context evc env lfun lmatch goalopt (read_match_context_rule evc env lmr) (*Tries to match the hypotheses in a Match Context*) and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps hyps= let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun lmatch mhyps hyps hyps_acc= match hyps with hd::tl -> (try (let (lid,lm,newmhyps)=apply_one_hyp_context lmatch mhyps hd in if newmhyps=[] then match (val_interp (evc,env,(lfun@lid@lfun_glob), (lmatch@lm@lmatch_glob),Some goal) mt) with VTactic tac -> VRTactic (tac goal) |VFTactic (largs,f) -> VRTactic (f largs goal) |a -> a else apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt (lfun@lid) (lmatch@lm) newmhyps (hyps_acc@tl) []) with No_match | _ -> apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun lmatch mhyps tl (hyps_acc@[hd])) |[] -> raise No_match in apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps hyps [] (*Interprets the Match expressions*) and match_interp evc env lfun lmatch goalopt ast lmr= let rec apply_match evc env lfun lmatch goalopt csr=function (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t |(Pat ([],mc,mt))::tl -> (try (let lcsr=apply_matching mc csr in val_interp (evc,env,lfun,(apply_matching mc csr)@lmatch,goalopt) mt) with No_match -> apply_match evc env lfun lmatch goalopt csr tl) |_ -> errorlabstrm "Tacinterp.apply_match" [<'sTR "No matching clauses for Match">] in let csr= constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (List.hd lmr))) and ilr=read_match_rule evc env (List.tl lmr) in apply_match evc env lfun lmatch goalopt csr ilr (*Interprets tactic expressions*) and tac_interp lfun lmatch ast g= let evc=project g and env=pf_env g in match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with VTactic tac -> (tac g) |VFTactic (largs,f) -> (f largs g) |VRTactic res -> res |_ -> errorlabstrm "Tacinterp.interp_rec" [<'sTR "Interpretation gives a non-tactic value">] (*Interprets a primitive tactic*) and interp_atomic loc opn args=vernac_tactic(opn,args) (*Interprets sequences of tactics*) and interp_semi_list acc lfun lmatch=function (Node(_,"TACLIST",seq))::l -> interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq)) lfun lmatch l |t::l -> interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l |[] -> acc (*Interprets bindings for tactics*) and bind_interp evc env lfun lmatch goalopt=function Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> (NoDep n,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[c]))))) |Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c]))))) |Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[c]))))) |x -> errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; print_ast x>] (*Interprets a COMMAND expression*) and com_interp (evc,env,lfun,lmatch,goalopt)=function Node(_,"EVAL",[c;rtc]) -> let redexp= unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc env (make_subs_list lfun) lmatch c))) |c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) (*Interprets a CASTEDCOMMAND expression*) and cast_com_interp (evc,env,lfun,lmatch,goalopt) com= match goalopt with Some gl -> (match com with Node(_,"EVAL",[c;rtc]) -> let redexp= unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c (pf_concl gl)))) |c -> VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c (pf_concl gl)))) |None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] and cvt_pattern (evc,env,lfun,lmatch,goalopt)=function Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> let occs=List.map num_of_ast nums and csr= constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[com])))) in let jdt=Typing.unsafe_machine env evc csr in (occs, jdt.Environ.uj_val, jdt.Environ.uj_type) |arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) com)))) |arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") (*Interprets the arguments of Fold*) and cvt_fold (evc,env,lfun,lmatch,goalopt)=function Node(_,"COMMAND",[c]) as ast -> constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast)) |arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") (*Interprets the reduction flags*) and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= let beta = ref false in let delta = ref false in let iota = ref false in let idents = ref (None: (sorts oper -> bool) option) in let set_flag = function Node(_,"Beta",[]) -> beta := true | Node(_,"Delta",[]) -> delta := true | Node(_,"Iota",[]) -> iota := true | Node(loc,"Unf",l) -> if !delta then if !idents = None then let idl= List.map (fun v -> glob_nvar (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l in idents := Some (function Const sp -> List.mem sp idl | Abst sp -> List.mem sp idl | _ -> false) else user_err_loc(loc,"flag_of_ast", [< 'sTR"Cannot specify identifiers to unfold twice" >]) else user_err_loc(loc,"flag_of_ast", [< 'sTR"Delta must be specified before" >]) | Node(loc,"UnfBut",l) -> if !delta then if !idents = None then let idl= List.map (fun v -> glob_nvar (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l in idents := Some (function Const sp -> not (List.mem sp idl) | Abst sp -> not (List.mem sp idl) | _ -> false) else user_err_loc(loc,"flag_of_ast", [< 'sTR"Cannot specify identifiers to unfold twice" >]) else user_err_loc(loc,"flag_of_ast", [< 'sTR"Delta must be specified before" >]) | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") in List.iter set_flag lf; { r_beta = !beta; r_iota = !iota; r_delta = match (!delta,!idents) with (false,_) -> (fun _ -> false) | (true,None) -> (fun _ -> true) | (true,Some p) -> p } (*Interprets a reduction expression*) and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function |("Red", []) -> Red |("Hnf", []) -> Hnf |("Simpl", []) -> Simpl |("Unfold", ul) -> Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul) |("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl) |("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) |("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) |("Pattern",lp) -> Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp) |(s,_) -> invalid_arg ("malformed reduction-expression: "^s) (*Interprets the patterns of Intro*) and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Nvar (loc,s))))) |Node(_,"DISJPATTERN", l) -> DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) |Node(_,"CONJPATTERN", l) -> ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) |Node(_,"LISTPATTERN", l) -> ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) |x -> errorlabstrm "cvt_intro_pattern" [<'sTR "Not the expected form for an introduction pattern!";print_ast x>] (*Interprets a pattern of Let*) and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Nvar (loc,s)))),List.map num_of_ast nums)::l) |Node(_,"CCLPATTERN", nums) -> if o<>None then error "\"Goal\" occurs twice" else (Some (List.map num_of_ast nums), l) |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") (*Interprets tactic arguments*) let interp_tacarg sign ast=unvarg (val_interp sign ast) (*Initial call for interpretation*) let interp=tac_interp [] [] let is_just_undef_macro ast = match ast with | Node(_,"TACTICLIST",[Node(loc,"CALL",macro::_)]) -> let id = nvar_of_ast macro in (try let _ = Macros.lookup id in None with Not_found -> Some id) | _ -> None let vernac_interp = let gentac = hide_tactic "Interpret" (fun vargs gl -> match vargs with | [Tacexp com] -> interp com gl | _ -> assert false) in fun com -> gentac [Tacexp com] let vernac_interp_atomic = let gentac = hide_tactic "InterpretAtomic" (fun argl gl -> match argl with | (Identifier id)::args -> interp_atomic dummy_loc (string_of_id id) args gl | _ -> assert false) in fun opn args -> gentac ((Identifier opn)::args) let bad_tactic_args s = anomalylabstrm s [< 'sTR"Tactic "; 'sTR s; 'sTR" called with bad arguments" >]