diff options
| -rw-r--r-- | .depend | 18 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | proofs/macros.ml | 87 | ||||
| -rw-r--r-- | proofs/macros.mli | 22 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 156 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 24 |
6 files changed, 309 insertions, 1 deletions
@@ -58,12 +58,16 @@ proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi +proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ + proofs/proof_trees.cmi proofs/tacmach.cmi proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/refiner.cmi kernel/sign.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ lib/util.cmi proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi +proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ + proofs/proof_trees.cmi proofs/tacmach.cmi kernel/term.cmi proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi @@ -285,6 +289,14 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx proofs/typing_ev.cmx \ lib/util.cmx proofs/logic.cmi +proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi kernel/names.cmi \ + parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \ + kernel/term.cmi lib/util.cmi proofs/macros.cmi +proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx kernel/names.cmx \ + parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \ + kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ lib/util.cmi proofs/proof_trees.cmi @@ -299,6 +311,12 @@ proofs/refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \ lib/util.cmx proofs/refiner.cmi +proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ + kernel/term.cmi lib/util.cmi proofs/tacinterp.cmi +proofs/tacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx proofs/macros.cmx \ + kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \ + kernel/term.cmx lib/util.cmx proofs/tacinterp.cmi proofs/tacmach.cmo: parsing/ast.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ @@ -50,7 +50,8 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \ proofs/proof_trees.cmo proofs/logic.cmo \ - proofs/refiner.cmo proofs/evar_refiner.cmo proofs/clenv.cmo + proofs/refiner.cmo proofs/evar_refiner.cmo \ + proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ diff --git a/proofs/macros.ml b/proofs/macros.ml new file mode 100644 index 000000000..de6132f36 --- /dev/null +++ b/proofs/macros.ml @@ -0,0 +1,87 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Term +open Proof_trees +open Libobject +open Library +open Coqast +open Pcoq +open Ast + +(* The data stored in the table *) + +type macro_data = { + mac_args : string list; + mac_body : Ast.act } + +(* Summary and Object declaration *) + +type t = macro_data Stringmap.t +type frozen_t = macro_data Stringmap.t + +let mactab = ref Stringmap.empty + +let lookup id = Stringmap.find id !mactab + +let _ = + let init () = mactab := Stringmap.empty in + let freeze () = !mactab in + let unfreeze fs = mactab := fs in + Summary.declare_summary "tactic-macro" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +let (inMD,outMD) = + let add (na,md) = mactab := Stringmap.add na md !mactab in + let cache_md (_,(na,md)) = add (na,md) in + let specification_md x = x in + declare_object ("TACTIC-MACRO-DATA", + { cache_function = cache_md; + load_function = (fun _ -> ()); + open_function = (fun _ -> ()); + specification_function = specification_md }) + +let add_macro_hint na (ids,body) = + if Stringmap.mem na !mactab then errorlabstrm "add_macro_hint" + [< 'sTR "There is already a Tactic Macro named "; 'sTR na >]; + let _ = Lib.add_leaf (id_of_string na) OBJ + (inMD(na,{mac_args = ids; mac_body = body})) in + () + +let macro_expand macro_loc macro argcoms = + let md = + try + lookup macro + with Not_found -> + user_err_loc(macro_loc,"macro_expand", + [< 'sTR"Tactic macro ";'sTR macro; 'sPC; + 'sTR"not defined" >]) + in + let transform = + List.map + (function + | Command c -> c + | _ -> user_err_loc(macro_loc,"macro_expand", + [<'sTR "The arguments of a tactic macro"; + 'sPC; 'sTR"must be terms">])) + in + let argcoms = transform argcoms in + if List.length argcoms <> List.length md.mac_args then + user_err_loc + (macro_loc,"macro_expand", + [< 'sTR "Tactic macro "; 'sTR macro; 'sPC; + 'sTR "applied to the wrong number of arguments:"; 'sPC; + 'iNT (List.length argcoms) ; 'sTR" instead of "; + 'iNT (List.length md.mac_args) >]); + let astb = + List.map2 (fun id argcom -> (id, Vast argcom)) md.mac_args argcoms in + match Ast.eval_act macro_loc astb md.mac_body with + | Vast ast -> ast + | _ -> anomaly "expand_macro : eval_act did not return a Vast" + + diff --git a/proofs/macros.mli b/proofs/macros.mli new file mode 100644 index 000000000..c62f13c76 --- /dev/null +++ b/proofs/macros.mli @@ -0,0 +1,22 @@ + +(* $Id$ *) + +(*i*) +open Names +open Tacmach +open Proof_trees +(*i*) + +(* This file contains the table of macro tactics. The body of the + defined tactics is stored as an ast with variables, which are + substituted by the real arguments at calling time. + User defined tactics are stored in a separate table so that they + are sensible to the Reset and Require commands. *) + +type macro_data = { + mac_args : string list; + mac_body : Ast.act } + +val add_macro_hint : string -> string list * Ast.act -> unit +val lookup : string -> macro_data +val macro_expand : Coqast.loc -> string -> tactic_arg list -> Coqast.t diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml new file mode 100644 index 000000000..3413b2a61 --- /dev/null +++ b/proofs/tacinterp.ml @@ -0,0 +1,156 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Term +open Proof_trees +open Tacmach +open Macros +open Coqast +open Ast + + +let tactic_tab = + (Hashtbl.create 17 : (string, tactic_arg list -> tactic) Hashtbl.t) + +let tacinterp_add (s,f) = + try + Hashtbl.add tactic_tab s f + with Failure _ -> + errorlabstrm "tacinterp_add" + [< 'sTR"Cannot add the tactic " ; 'sTR s ; 'sTR" twice" >] + +let overwriting_tacinterp_add (s,f) = + if Hashtbl.mem tactic_tab s then begin + Hashtbl.remove tactic_tab s; + warning ("Overwriting definition of tactic interpreter command "^s) + end; + Hashtbl.add tactic_tab s f + +let tacinterp_init () = Hashtbl.clear tactic_tab + +let tacinterp_map s = Hashtbl.find tactic_tab s + +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" >]) + +let cvt_bind = function + | Node(_,"BINDING", [Num(_,n); Node(_,"COMMAND",[c])]) -> (NoDep n,c) + | Node(_,"BINDING", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> + let id = id_of_string s in (Dep id,c) + | Node(_,"BINDING", [Node(_,"COMMAND",[c])]) -> (Com,c) + | x -> errorlabstrm "cvt_bind" + [< 'sTR "Not the expected form in binding!"; print_ast x >] + +let rec cvt_intro_pattern = function + | Node(_,"IDENTIFIER", [Nvar(_,s)]) -> IdPat (id_of_string s) + | Node(_,"DISJPATTERN", l) -> DisjPat (List.map cvt_intro_pattern l) + | Node(_,"CONJPATTERN", l) -> ConjPat (List.map cvt_intro_pattern l) + | Node(_,"LISTPATTERN", l) -> ListPat (List.map cvt_intro_pattern l) + | x -> errorlabstrm "cvt_intro_pattern" + [< 'sTR "Not the expected form for an introduction pattern!"; + print_ast x >] + +let cvt_letpattern (o,l) = function + | Node(_,"HYPPATTERN", Nvar(_,s)::nums) -> + (o, (id_of_string 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") + +let cvt_letpatterns astl = List.fold_left cvt_letpattern (None,[]) astl + +let cvt_arg = function + | Nvar(_,s) -> + Identifier (id_of_string s) + | Str(_,s) -> + Quoted_string s + | Num(_,n) -> + Integer n + | Node(_,"COMMAND",[c]) -> + Command c + | Node(_,"BINDINGS",astl) -> + Bindings (List.map cvt_bind astl) + | Node(_,"REDEXP",[Node(_,redname,args)]) -> + Redexp (redname,args) + | Node(_,"CLAUSE",cl) -> + Clause (List.map (compose id_of_string nvar_of_ast) cl) + | Node(_,"TACTIC",[ast]) -> + Tacexp ast + | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> + Fixexp (id_of_string s,n,c) + | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> + Cofixexp (id_of_string s,c) + | Node(_,"INTROPATTERN", [ast]) -> + Intropattern (cvt_intro_pattern ast) + | Node(_,"LETPATTERNS", astl) -> + let (o,l) = (cvt_letpatterns astl) in Letpatterns (o,l) + | x -> + anomaly_loc (Ast.loc x, "Tacinterp.cvt_bind", + [< 'sTR "Unrecognizable ast node : "; print_ast x >]) + +let rec interp = function + | Node(loc,opn,tl) -> + (match (opn, tl) with + | ("TACTICLIST",_) -> interp_semi_list tclIDTAC tl + | ("DO",[n;tac]) -> tclDO (num_of_ast n) (interp tac) + | ("TRY",[tac]) -> tclTRY (interp tac) + | ("INFO",[tac]) -> tclINFO (interp tac) + | ("REPEAT",[tac]) -> tclREPEAT (interp tac) + | ("ORELSE",[tac1;tac2]) -> tclORELSE (interp tac1) (interp tac2) + | ("FIRST",l) -> tclFIRST (List.map interp l) + | ("TCLSOLVE",l) -> tclSOLVE (List.map interp l) + | ("CALL",macro::args) -> + interp (macro_expand loc (nvar_of_ast macro) + (List.map cvt_arg args)) + | _ -> interp_atomic loc opn (List.map cvt_arg tl)) + | ast -> user_err_loc(Ast.loc ast,"Tacinterp.interp", + [< 'sTR"A non-ASTnode constructor was found" >]) + +and interp_atomic loc opn args = + try + tacinterp_map opn args + with Not_found -> + try + vernac_tactic(opn,args) + with e -> + Stdpp.raise_with_loc loc e + +and interp_semi_list acc = function + | (Node(_,"TACLIST",seq))::l -> + interp_semi_list (tclTHENS acc (List.map interp seq)) l + | t::l -> interp_semi_list (tclTHEN acc (interp t)) l + | [] -> acc + + +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) diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli new file mode 100644 index 000000000..5dbad5176 --- /dev/null +++ b/proofs/tacinterp.mli @@ -0,0 +1,24 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Names +open Proof_trees +open Tacmach +open Term +(*i*) + +(* Interpretation of tactics. *) + +val tacinterp_add : string * (tactic_arg list -> tactic) -> unit +val tacinterp_map : string -> tactic_arg list -> tactic +val tacinterp_init : unit -> unit +val interp : Coqast.t -> tactic +val interp_atomic : Coqast.loc -> string -> tactic_arg list -> tactic +val interp_semi_list : tactic -> Coqast.t list -> tactic +val vernac_interp : Coqast.t -> tactic +val vernac_interp_atomic : identifier -> tactic_arg list -> tactic +val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit +val is_just_undef_macro : Coqast.t -> string option + |