diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/g_ltac.ml4 | 429 | ||||
| -rw-r--r-- | tactics/g_obligations.ml4 | 14 | ||||
| -rw-r--r-- | tactics/hightactics.mllib | 6 | ||||
| -rw-r--r-- | tactics/tacentries.ml | 263 | ||||
| -rw-r--r-- | tactics/tacentries.mli | 21 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 4 |
7 files changed, 731 insertions, 8 deletions
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 new file mode 100644 index 0000000000..f46a670080 --- /dev/null +++ b/tactics/g_ltac.ml4 @@ -0,0 +1,429 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Util +open Pp +open Compat +open Constrexpr +open Tacexpr +open Misctypes +open Genarg +open Genredexpr +open Tok (* necessary for camlp4 *) + +open Pcoq +open Pcoq.Prim +open Pcoq.Tactic + +let fail_default_value = ArgArg 0 + +let arg_of_expr = function + TacArg (loc,a) -> a + | e -> Tacexp (e:raw_tactic_expr) + +let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () +let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n +let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat +let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c + +let reference_to_id = function + | Libnames.Ident (loc, id) -> (loc, id) + | Libnames.Qualid (loc,_) -> + Errors.user_err_loc (loc, "", + str "This expression should be a simple identifier.") + +let tactic_mode = Gram.entry_create "vernac:tactic_command" + +let new_entry name = + let e = Gram.entry_create name in + let entry = Entry.create name in + let () = Pcoq.set_grammar entry e in + e + +let selector = new_entry "vernac:selector" +let tacdef_body = new_entry "tactic:tacdef_body" + +(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for + proof editing and changes nothing else). Then sets it as the default proof mode. *) +let _ = + let mode = { + Proof_global.name = "Classic"; + set = (fun () -> set_command_entry tactic_mode); + reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + } in + Proof_global.register_proof_mode mode + +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + Gram.Entry.of_parser "test_bracket_ident" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "[" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> () + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + +(* Tactics grammar rules *) + +GEXTEND Gram + GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg + tactic_mode constr_may_eval constr_eval selector; + + tactic_then_last: + [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> + Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) + | -> [||] + ] ] + ; + tactic_then_gen: + [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last) + | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l)) + | ".."; l = tactic_then_last -> ([], Some (TacId [], l)) + | ta = tactic_expr -> ([ta], None) + | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last) + | -> ([TacId []], None) + ] ] + ; + tactic_then_locality: (* [true] for the local variant [TacThens] and [false] + for [TacExtend] *) + [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] + ; + tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> te ] + | "4" LEFTA + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) + | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> + match l , tail with + | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) + | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) + | false , None -> TacThen (ta0,TacDispatch first) + | true , None -> TacThens (ta0,first) ] + | "3" RIGHTA + [ IDENT "try"; ta = tactic_expr -> TacTry ta + | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) + | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) + | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta + | IDENT "progress"; ta = tactic_expr -> TacProgress ta + | IDENT "once"; ta = tactic_expr -> TacOnce ta + | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta + | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta +(*To do: put Abstract in Refiner*) + | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) + | IDENT "abstract"; tc = NEXT; "using"; s = ident -> + TacAbstract (tc,Some s) ] +(*End of To do*) + | "2" RIGHTA + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + | IDENT "tryif" ; ta = tactic_expr ; + "then" ; tat = tactic_expr ; + "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] + | "1" RIGHTA + [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> + TacMatchGoal (b,false,mrl) + | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; + mrl = match_context_list; "end" -> + TacMatchGoal (b,true,mrl) + | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + TacMatch (b,c,mrl) + | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + TacFirst l + | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + TacSolve l + | IDENT "idtac"; l = LIST0 message_token -> TacId l + | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; + l = LIST0 message_token -> TacFail (g,n,l) + | st = simple_tactic -> st + | a = tactic_arg -> TacArg(!@loc,a) + | r = reference; la = LIST0 tactic_arg_compat -> + TacArg(!@loc,TacCall (!@loc,r,la)) ] + | "0" + [ "("; a = tactic_expr; ")" -> a + | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> + begin match tail with + | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) + | None -> TacDispatch tf + end + | a = tactic_atom -> TacArg (!@loc,a) ] ] + ; + failkw: + [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] + ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + TacFun (it,body) + | "let"; isrec = [IDENT "rec" -> true | -> false]; + llc = LIST1 let_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) + | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] + ; + (* Tactic arguments to the right of an application *) + tactic_arg_compat: + [ [ a = tactic_arg -> a + | r = reference -> Reference r + | c = Constr.constr -> ConstrMayEval (ConstrTerm c) + (* Unambigous entries: tolerated w/o "ltac:" modifier *) + | "()" -> TacGeneric (genarg_of_unit ()) ] ] + ; + (* Can be used as argument and at toplevel in tactic expressions. *) + tactic_arg: + [ [ c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l + | IDENT "type_term"; c=uconstr -> TacPretype c + | IDENT "numgoals" -> TacNumgoals ] ] + ; + (* If a qualid is given, use its short name. TODO: have the shortest + non ambiguous name where dots are replaced by "_"? Probably too + verbose most of the time. *) + fresh_id: + [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ] + ; + constr_eval: + [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> + ConstrEval (rtc,c) + | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> + ConstrContext (id,c) + | IDENT "type"; IDENT "of"; c = Constr.constr -> + ConstrTypeOf c ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> c + | c = Constr.constr -> ConstrTerm c ] ] + ; + tactic_atom: + [ [ n = integer -> TacGeneric (genarg_of_int n) + | r = reference -> TacCall (!@loc,r,[]) + | "()" -> TacGeneric (genarg_of_unit ()) ] ] + ; + match_key: + [ [ "match" -> Once + | "lazymatch" -> Select + | "multimatch" -> General ] ] + ; + input_fun: + [ [ "_" -> None + | l = ident -> Some l ] ] + ; + let_clause: + [ [ id = identref; ":="; te = tactic_expr -> + (id, arg_of_expr te) + | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + (id, arg_of_expr (TacFun(args,te))) ] ] + ; + match_pattern: + [ [ IDENT "context"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + let mode = not (!Flags.tactic_context_compat) in + Subterm (mode, oid, pc) + | IDENT "appcontext"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + msg_warning (strbrk "appcontext is deprecated"); + Subterm (true,oid, pc) + | pc = Constr.lconstr_pattern -> Term pc ] ] + ; + match_hyps: + [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) + | na = name; ":="; mpv = match_pattern -> + let t, ty = + match mpv with + | Term t -> (match t with + | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) + | _ -> mpv, None) + | _ -> mpv, None + in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) + ] ] + ; + match_context_rule: + [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "=>"; te = tactic_expr -> Pat (largs, mp, te) + | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) + | "_"; "=>"; te = tactic_expr -> All te ] ] + ; + match_context_list: + [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl + | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] + ; + match_rule: + [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) + | "_"; "=>"; te = tactic_expr -> All te ] ] + ; + match_list: + [ [ mrl = LIST1 match_rule SEP "|" -> mrl + | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] + ; + message_token: + [ [ id = identref -> MsgIdent id + | s = STRING -> MsgString s + | n = integer -> MsgInt n ] ] + ; + + ltac_def_kind: + [ [ ":=" -> false + | "::=" -> true ] ] + ; + + (* Definitions for tactics *) + tacdef_body: + [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + else + let id = reference_to_id name in + Vernacexpr.TacticDefinition (id, TacFun (it, body)) + | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> + if redef then Vernacexpr.TacticRedefinition (name, body) + else + let id = reference_to_id name in + Vernacexpr.TacticDefinition (id, body) + ] ] + ; + tactic: + [ [ tac = tactic_expr -> tac ] ] + ; + selector: + [ [ n=natural; ":" -> Vernacexpr.SelectNth n + | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id + | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ] + ; + tactic_mode: + [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ] + ; + END + +open Stdarg +open Constrarg +open Vernacexpr +open Vernac_classifier +open Goptions +open Libnames + +let print_info_trace = ref None + +let _ = declare_int_option { + optsync = true; + optdepr = false; + optname = "print info trace"; + optkey = ["Info" ; "Level"]; + optread = (fun () -> !print_info_trace); + optwrite = fun n -> print_info_trace := n; +} + +let vernac_solve n info tcom b = + let status = Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let global = match n with SelectAll -> true | _ -> false in + let info = Option.append info !print_info_trace in + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) in + if not status then Pp.feedback Feedback.AddedAxiom + +let pr_ltac_selector = function +| SelectNth i -> int i ++ str ":" +| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" +| SelectAll -> str "all" ++ str ":" + +VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector +| [ selector(s) ] -> [ s ] +END + +let pr_ltac_info n = str "Info" ++ spc () ++ int n + +VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info +| [ "Info" natural(n) ] -> [ n ] +END + +let pr_ltac_use_default b = if b then str ".." else mt () + +VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default +| [ "." ] -> [ false ] +| [ "..." ] -> [ true ] +END + +VERNAC tactic_mode EXTEND VernacSolve +| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + [ classify_as_proofstep ] -> [ + let g = Option.default (Proof_global.get_default_goal_selector ()) g in + vernac_solve g n t def + ] +| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + [ VtProofStep true, VtLater ] -> [ + vernac_solve SelectAll n t def + ] +END + +let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" + +VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level +| [ "(" "at" "level" natural(n) ")" ] -> [ n ] +END + +VERNAC ARGUMENT EXTEND ltac_production_sep +| [ "," string(sep) ] -> [ sep ] +END + +let pr_ltac_production_item = function +| TacTerm s -> quote (str s) +| TacNonTerm (_, arg, (id, sep)) -> + let sep = match sep with + | "" -> mt () + | sep -> str "," ++ spc () ++ quote (str sep) + in + str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")" + +VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item +| [ string(s) ] -> [ TacTerm s ] +| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> + [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ] +END + +VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF +| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] -> + [ + let l = Locality.LocalityFixme.consume () in + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e) + ] +END + +VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY +| [ "Print" "Ltac" reference(r) ] -> + [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] +END + +VERNAC ARGUMENT EXTEND ltac_tacdef_body +| [ tacdef_body(t) ] -> [ t ] +END + +VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ + VtSideff (List.map (function + | TacticDefinition ((_,r),_) -> r + | TacticRedefinition (Ident (_,r),_) -> r + | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater + ] -> [ + let lc = Locality.LocalityFixme.consume () in + Tacentries.register_ltac (Locality.make_module_locality lc) l + ] +END diff --git a/tactics/g_obligations.ml4 b/tactics/g_obligations.ml4 index e67d701218..4cd8bf1feb 100644 --- a/tactics/g_obligations.ml4 +++ b/tactics/g_obligations.ml4 @@ -19,16 +19,22 @@ open Constrexpr_ops open Stdarg open Constrarg open Extraargs -open Pcoq.Prim -open Pcoq.Constr -open Pcoq.Tactic + +let (set_default_tactic, get_default_tactic, print_default_tactic) = + Tactic_option.declare_tactic_option "Program tactic" + +let () = + (** Delay to recover the tactic imperatively *) + let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> + snd (get_default_tactic ()) + end in + Obligations.default_tactic := tac (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac.<foo> *) module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ module Tactic = Pcoq.Tactic open Pcoq diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 5c59465429..468b938b6a 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,8 @@ +Tacintern +Tacentries +Tacinterp +Evar_tactics +Tactic_option Extraargs G_obligations Coretactics @@ -12,3 +17,4 @@ G_rewrite Tauto Eqdecide G_eqdecide +G_ltac diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml new file mode 100644 index 0000000000..711cd8d9d0 --- /dev/null +++ b/tactics/tacentries.ml @@ -0,0 +1,263 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Names +open Libobject +open Pcoq +open Egramml +open Egramcoq +open Vernacexpr +open Libnames +open Nameops + +(**********************************************************************) +(* Tactic Notation *) + +let interp_prod_item lev = function + | TacTerm s -> GramTerminal s + | TacNonTerm (loc, nt, (_, sep)) -> + let EntryName (etyp, e) = interp_entry_name lev nt sep in + GramNonTerminal (loc, etyp, e) + +let make_terminal_status = function + | GramTerminal s -> Some s + | GramNonTerminal _ -> None + +let make_fresh_key = + let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) + +type tactic_grammar_obj = { + tacobj_key : KerName.t; + tacobj_local : locality_flag; + tacobj_tacgram : tactic_grammar; + tacobj_tacpp : Pptactic.pp_tactic; + tacobj_body : Id.t list * Tacexpr.glob_tactic_expr; +} + +let check_key key = + if Tacenv.check_alias key then + error "Conflicting tactic notations keys. This can happen when including \ + twice the same module." + +let cache_tactic_notation (_, tobj) = + let key = tobj.tacobj_key in + let () = check_key key in + Tacenv.register_alias key tobj.tacobj_body; + Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; + Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp + +let open_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in + if Int.equal i 1 && not tobj.tacobj_local then + Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram + +let load_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in + let () = check_key key in + (** Only add the printing and interpretation rules. *) + Tacenv.register_alias key tobj.tacobj_body; + Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; + if Int.equal i 1 && not tobj.tacobj_local then + Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram + +let subst_tactic_notation (subst, tobj) = + let (ids, body) = tobj.tacobj_body in + { tobj with + tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; + tacobj_body = (ids, Tacsubst.subst_tactic subst body); + } + +let classify_tactic_notation tacobj = Substitute tacobj + +let inTacticGrammar : tactic_grammar_obj -> obj = + declare_object {(default_object "TacticGrammar") with + open_function = open_tactic_notation; + load_function = load_tactic_notation; + cache_function = cache_tactic_notation; + subst_function = subst_tactic_notation; + classify_function = classify_tactic_notation} + +let cons_production_parameter = function +| TacTerm _ -> None +| TacNonTerm (_, _, (id, _)) -> Some id + +let add_tactic_notation (local,n,prods,e) = + let ids = List.map_filter cons_production_parameter prods in + let prods = List.map (interp_prod_item n) prods in + let pprule = { + Pptactic.pptac_level = n; + pptac_prods = prods; + } in + let tac = Tacintern.glob_tactic_env ids (Global.env()) e in + let parule = { + tacgram_level = n; + tacgram_prods = prods; + } in + let tacobj = { + tacobj_key = make_fresh_key (); + tacobj_local = local; + tacobj_tacgram = parule; + tacobj_tacpp = pprule; + tacobj_body = (ids, tac); + } in + Lib.add_anonymous_leaf (inTacticGrammar tacobj) + +(**********************************************************************) +(* ML Tactic entries *) + +type ml_tactic_grammar_obj = { + mltacobj_name : Tacexpr.ml_tactic_name; + (** ML-side unique name *) + mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list; + (** Grammar rules generating the ML tactic. *) +} + +exception NonEmptyArgument + +(** ML tactic notations whose use can be restricted to an identifier are added + as true Ltac entries. *) +let extend_atomic_tactic name entries = + let open Tacexpr in + let map_prod prods = + let (hd, rem) = match prods with + | GramTerminal s :: rem -> (s, rem) + | _ -> assert false (** Not handled by the ML extension syntax *) + in + let empty_value = function + | GramTerminal s -> raise NonEmptyArgument + | GramNonTerminal (_, typ, e) -> + let Genarg.Rawwit wit = typ in + let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in + let default = epsilon_value inj e in + match default with + | None -> raise NonEmptyArgument + | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def + in + try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None + in + let entries = List.map map_prod entries in + let add_atomic i args = match args with + | None -> () + | Some (id, args) -> + let args = List.map (fun a -> Tacexp a) args in + let entry = { mltac_name = name; mltac_index = i } in + let body = TacML (Loc.ghost, entry, args) in + Tacenv.register_ltac false false (Names.Id.of_string id) body + in + List.iteri add_atomic entries + +let cache_ml_tactic_notation (_, obj) = + extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod + +let open_ml_tactic_notation i obj = + if Int.equal i 1 then cache_ml_tactic_notation obj + +let inMLTacticGrammar : ml_tactic_grammar_obj -> obj = + declare_object { (default_object "MLTacticGrammar") with + open_function = open_ml_tactic_notation; + cache_function = cache_ml_tactic_notation; + classify_function = (fun o -> Substitute o); + subst_function = (fun (_, o) -> o); + } + +let add_ml_tactic_notation name prods = + let obj = { + mltacobj_name = name; + mltacobj_prod = prods; + } in + Lib.add_anonymous_leaf (inMLTacticGrammar obj); + extend_atomic_tactic name prods + +(** Command *) + + +type tacdef_kind = + | NewTac of Id.t + | UpdateTac of Nametab.ltac_constant + +let is_defined_tac kn = + try ignore (Tacenv.interp_ltac kn); true with Not_found -> false + +let register_ltac local tacl = + let map tactic_body = + match tactic_body with + | TacticDefinition ((loc,id), body) -> + let kn = Lib.make_kn id in + let id_pp = pr_id id in + let () = if is_defined_tac kn then + Errors.user_err_loc (loc, "", + str "There is already an Ltac named " ++ id_pp ++ str".") + in + let is_primitive = + try + match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with + | Tacexpr.TacArg _ -> false + | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) + with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) + in + let () = if is_primitive then + msg_warning (str "The Ltac name " ++ id_pp ++ + str " may be unusable because of a conflict with a notation.") + in + NewTac id, body + | TacticRedefinition (ident, body) -> + let loc = loc_of_reference ident in + let kn = + try Nametab.locate_tactic (snd (qualid_of_reference ident)) + with Not_found -> + Errors.user_err_loc (loc, "", + str "There is no Ltac named " ++ pr_reference ident ++ str ".") + in + UpdateTac kn, body + in + let rfun = List.map map tacl in + let recvars = + let fold accu (op, _) = match op with + | UpdateTac _ -> accu + | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu + in + List.fold_left fold [] rfun + in + let ist = Tacintern.make_empty_glob_sign () in + let map (name, body) = + let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in + (name, body) + in + let defs () = + (** Register locally the tactic to handle recursivity. This function affects + the whole environment, so that we transactify it afterwards. *) + let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in + let () = List.iter iter_rec recvars in + List.map map rfun + in + let defs = Future.transactify defs () in + let iter (def, tac) = match def with + | NewTac id -> + Tacenv.register_ltac false local id tac; + Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined") + | UpdateTac kn -> + Tacenv.redefine_ltac local kn tac; + let name = Nametab.shortest_qualid_of_tactic kn in + Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined") + in + List.iter iter defs diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli new file mode 100644 index 0000000000..3cf0bc5cc9 --- /dev/null +++ b/tactics/tacentries.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Vernacexpr +open Tacexpr + +(** Adding a tactic notation in the environment *) + +val add_tactic_notation : + locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> + unit + +val add_ml_tactic_notation : ml_tactic_name -> + Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit + +val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 36faba1137..6bf0e2aa73 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2214,3 +2214,5 @@ let _ = optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } + +let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index fd7fab0c58..b495a885f8 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -19,10 +19,6 @@ Taccoerce Tacenv Hints Auto -Tacintern Tactic_matching Tactic_debug -Tacinterp -Evar_tactics Term_dnet -Tactic_option |