From 64d9e1d1b9875c64613c7c5a95c696ab3e6f04cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 21:26:58 +0100 Subject: Moving the use of Tactic_option from Obligations to G_obligations. --- tactics/g_obligations.ml4 | 14 ++++++++++---- toplevel/obligations.ml | 7 +++---- toplevel/obligations.mli | 6 ++---- 3 files changed, 15 insertions(+), 12 deletions(-) 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. *) module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ module Tactic = Pcoq.Tactic open Pcoq diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 44c83be46c..b2fc456d07 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -323,8 +323,7 @@ let get_info x = let assumption_message = Declare.assumption_message -let (set_default_tactic, get_default_tactic, print_default_tactic) = - Tactic_option.declare_tactic_option "Program tactic" +let default_tactic = ref (Proofview.tclUNIT ()) (* true = All transparent, false = Opaque if possible *) let proofs_transparency = ref true @@ -895,7 +894,7 @@ let rec solve_obligation prg num tac = let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in - let _ = Pfedit.by (snd (get_default_tactic ())) in + let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac and obligation (user_num, name, typ) tac = @@ -924,7 +923,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> match obl.obl_tac with | Some t -> t - | None -> snd (get_default_tactic ()) + | None -> !default_tactic in let evd = Evd.from_ctx !prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index e257da0161..3e99f5760b 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -54,10 +54,8 @@ type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) | Defined of global_reference (* Defined as id *) - -val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit -val get_default_tactic : unit -> locality_flag * unit Proofview.tactic -val print_default_tactic : unit -> Pp.std_ppcmds + +val default_tactic : unit Proofview.tactic ref val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) val get_proofs_transparency : unit -> bool -- cgit v1.2.3 From 8cb2040e4af40594826df97a735c38c8882934ca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 00:30:24 +0100 Subject: Moving Tacinterp to Hightactics. --- parsing/g_ltac.ml4 | 372 --------------------------------------------- parsing/highparsing.mllib | 1 - tactics/g_ltac.ml4 | 372 +++++++++++++++++++++++++++++++++++++++++++++ tactics/hightactics.mllib | 4 + tactics/tacinterp.ml | 2 + tactics/tactics.mllib | 3 - toplevel/vernacentries.ml | 10 +- toplevel/vernacentries.mli | 3 + 8 files changed, 387 insertions(+), 380 deletions(-) delete mode 100644 parsing/g_ltac.ml4 create mode 100644 tactics/g_ltac.ml4 diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 deleted file mode 100644 index d1992c57bb..0000000000 --- a/parsing/g_ltac.ml4 +++ /dev/null @@ -1,372 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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" - -(* 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 - -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 diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index eed6caea30..8df519b567 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -3,4 +3,3 @@ G_vernac G_prim G_proofs G_tactic -G_ltac diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 new file mode 100644 index 0000000000..d1992c57bb --- /dev/null +++ b/tactics/g_ltac.ml4 @@ -0,0 +1,372 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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" + +(* 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 + +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 diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 5c59465429..0649f2f72e 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,6 @@ +Tacinterp +Evar_tactics +Tactic_option Extraargs G_obligations Coretactics @@ -12,3 +15,4 @@ G_rewrite Tauto Eqdecide G_eqdecide +G_ltac 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..584cc0b730 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -22,7 +22,4 @@ Auto Tacintern Tactic_matching Tactic_debug -Tacinterp -Evar_tactics Term_dnet -Tactic_option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ba5eb3f7d..64f9cd9caa 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -20,7 +20,6 @@ open Tacmach open Constrintern open Prettyp open Printer -open Tacinterp open Command open Goptions open Libnames @@ -34,6 +33,9 @@ open Misctypes open Locality open Sigma.Notations +(** TODO: make this function independent of Ltac *) +let (f_interp_redexp, interp_redexp_hook) = Hook.make () + let debug = false let prerr_endline = if debug then prerr_endline else fun _ -> () @@ -471,7 +473,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = | None -> None | Some r -> let (evc,env)= get_current_context () in - Some (snd (interp_redexp env evc r)) in + Some (snd (Hook.get f_interp_redexp env evc r)) in do_definition id (local,p,k) pl bl red_option c typ_opt hook) let vernac_start_proof locality p kind l lettop = @@ -1501,7 +1503,7 @@ let vernac_check_may_eval redexp glopt rc = Printer.pr_universe_ctx sigma uctx) | Some r -> Tacintern.dump_glob_red_expr r; - let (sigma',r_interp) = interp_redexp env sigma' r in + let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in let evm = Sigma.Unsafe.of_evar_map evm in @@ -1512,7 +1514,7 @@ let vernac_check_may_eval redexp glopt rc = let vernac_declare_reduction locality s r = let local = make_locality locality in - declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r)) + declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 4a59b1299b..4e7fa4a087 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -61,3 +61,6 @@ val vernac_end_proof : val with_fail : bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind + +val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr -> + Evd.evar_map * Redexpr.red_expr) Hook.t -- cgit v1.2.3 From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:31:43 +0100 Subject: Moving Tactic Notation to an EXTEND based command. --- intf/vernacexpr.mli | 2 -- parsing/g_vernac.ml4 | 13 ------------- printing/ppvernac.ml | 13 ------------- stm/texmacspp.ml | 3 --- stm/vernac_classifier.ml | 1 - tactics/g_ltac.ml4 | 34 ++++++++++++++++++++++++++++++++++ toplevel/vernacentries.ml | 5 +---- 7 files changed, 35 insertions(+), 36 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 36b855ec3b..123b3ec1b7 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -291,8 +291,6 @@ type vernac_expr = | VernacError of exn (* always fails *) (* Syntax *) - | VernacTacticNotation of - int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c89238d296..3b5d276dd2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1048,10 +1048,6 @@ GEXTEND Gram | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) - | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; - pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticNotation (n,pil,t) - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; @@ -1077,9 +1073,6 @@ GEXTEND Gram obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; - tactic_level: - [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] @@ -1111,10 +1104,4 @@ GEXTEND Gram | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; - production_item: - [ [ s = ne_string -> TacTerm s - | nt = IDENT; - po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] - ; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 887a14d2bf..88bb805a72 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -378,17 +378,6 @@ module Make | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let print_level n = - if not (Int.equal n 0) then - spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")") - else - mt () - - let pr_grammar_tactic_rule n (_,pil,t) = - hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++ - hov 0 (prlist_with_sep sep pr_production_item pil ++ - spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) - let pr_univs pl = match pl with | None -> mt () @@ -644,8 +633,6 @@ module Make return (keyword "No-parsing-rule for VernacError") (* Syntax *) - | VernacTacticNotation (n,r,e) -> - return (pr_grammar_tactic_rule n ("",r,e)) | VernacOpenCloseScope (_,(opening,sc)) -> return ( keyword (if opening then "Open " else "Close ") ++ diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index a459cd65f8..e83313aa8e 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -503,9 +503,6 @@ let rec tmpp v loc = | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) - | VernacTacticNotation _ as x -> - xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - | VernacSyntaxExtension (_, ((_, name), sml)) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in xmlReservedNotation attrs name loc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 97d6e1fb71..41b753fb8b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -195,7 +195,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index d1992c57bb..3573ca7177 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -370,3 +370,37 @@ VERNAC tactic_mode EXTEND VernacSolve 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 + Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e) + ] +END diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 64f9cd9caa..bdf0ada2cd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1822,8 +1822,6 @@ let interp ?proof ~loc locality poly c = | VernacError e -> raise e (* Syntax *) - | VernacTacticNotation (n,r,e) -> - Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e) | VernacSyntaxExtension (local,sl) -> vernac_syntax_extension locality local sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr @@ -1978,8 +1976,7 @@ let check_vernac_supports_locality c l = match l, c with | None, _ -> () | Some _, ( - VernacTacticNotation _ - | VernacOpenCloseScope _ + VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ -- cgit v1.2.3 From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:09:54 +0100 Subject: Moving Print Ltac to an EXTEND based command. --- intf/vernacexpr.mli | 1 - parsing/g_vernac.ml4 | 1 - printing/ppvernac.ml | 2 -- tactics/g_ltac.ml4 | 5 +++++ toplevel/vernacentries.ml | 1 - 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 123b3ec1b7..1a67a37d7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -60,7 +60,6 @@ type printable = | PrintClasses | PrintTypeClasses | PrintInstances of reference or_by_notation - | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3b5d276dd2..0ad39d8047 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -890,7 +890,6 @@ GEXTEND Gram | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses | IDENT "Instances"; qid = smart_global -> PrintInstances qid - | IDENT "Ltac"; qid = global -> PrintLtac qid | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 88bb805a72..edd32e8337 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -455,8 +455,6 @@ module Make keyword "Print TypeClasses" | PrintInstances qid -> keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintLtac qid -> - keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid | PrintCoercions -> keyword "Print Coercions" | PrintCoercionPaths (s,t) -> diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index 3573ca7177..5c0ae215d8 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -404,3 +404,8 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF Metasyntax.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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bdf0ada2cd..d0af1b951b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1582,7 +1582,6 @@ let vernac_print = function | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> msg_notice (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) -- cgit v1.2.3 From 9f5d9cd2622f3890e70dad01898868fe29df6048 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:23:02 +0100 Subject: Moving the tactic related code from Metasyntax to a new file. --- grammar/tacextend.ml4 | 2 +- tactics/g_ltac.ml4 | 2 +- tactics/hightactics.mllib | 1 + tactics/tacentries.ml | 186 ++++++++++++++++++++++++++++++++++++++++++++++ tactics/tacentries.mli | 19 +++++ toplevel/metasyntax.ml | 170 ------------------------------------------ toplevel/metasyntax.mli | 9 --- 7 files changed, 208 insertions(+), 181 deletions(-) create mode 100644 tactics/tacentries.ml create mode 100644 tactics/tacentries.mli diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index bbd3d8a62f..2ef30f299b 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -120,7 +120,7 @@ let declare_tactic loc s c cl = match cl with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in - let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { try do { diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index 5c0ae215d8..d75073877e 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -401,7 +401,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in - Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e) + Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e) ] END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0649f2f72e..b18d148ec6 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,4 @@ +Tacentries Tacinterp Evar_tactics Tactic_option diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml new file mode 100644 index 0000000000..e40f5f46a0 --- /dev/null +++ b/tactics/tacentries.ml @@ -0,0 +1,186 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli new file mode 100644 index 0000000000..635415b9d2 --- /dev/null +++ b/tactics/tacentries.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + unit + +val add_ml_tactic_notation : ml_tactic_name -> + Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e5edc74222..6277a8146a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -42,176 +42,6 @@ let inToken : string -> obj = let add_token_obj s = Lib.add_anonymous_leaf (inToken s) -(**********************************************************************) -(* 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 - (**********************************************************************) (* Printing grammar entries *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 5d01405b27..085cc87c8b 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -15,15 +15,6 @@ open Notation_term val add_token_obj : string -> unit -(** 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 - (** Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (lstring * syntax_modifier list) -> -- cgit v1.2.3 From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:23:21 +0100 Subject: Moving the Ltac definition command to an EXTEND based command. --- intf/vernacexpr.mli | 1 - parsing/g_vernac.ml4 | 6 +--- parsing/pcoq.ml | 3 -- parsing/pcoq.mli | 1 - printing/ppvernac.ml | 23 -------------- stm/texmacspp.ml | 1 - stm/vernac_classifier.ml | 7 ----- tactics/g_ltac.ml4 | 18 +++++++++++ tactics/tacentries.ml | 77 ++++++++++++++++++++++++++++++++++++++++++++++ tactics/tacentries.mli | 2 ++ toplevel/vernacentries.ml | 78 ----------------------------------------------- 11 files changed, 98 insertions(+), 119 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 1a67a37d7f..bd5890e296 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -379,7 +379,6 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0ad39d8047..8d7b6a2b48 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -751,11 +751,7 @@ GEXTEND Gram GLOBAL: command query_command class_rawexpr; command: - [ [ IDENT "Ltac"; - l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition l - - | IDENT "Comments"; l = LIST0 comment -> VernacComments l + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9c2f09db84..c7cb62d592 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -364,9 +364,6 @@ module Tactic = (* Main entry for quotations *) let tactic_eoi = eoi_entry tactic - (* For Ltac definition *) - let tacdef_body = Gram.entry_create "tactic:tacdef_body" - end module Vernac_ = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7410d4e44c..35973a4d72 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -229,7 +229,6 @@ module Tactic : val binder_tactic : raw_tactic_expr Gram.entry val tactic : raw_tactic_expr Gram.entry val tactic_eoi : raw_tactic_expr Gram.entry - val tacdef_body : Vernacexpr.tacdef_body Gram.entry end module Vernac_ : diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index edd32e8337..c1f5e122bd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -995,29 +995,6 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition l -> - let pr_tac_body tacdef_body = - let id, redef, body = - match tacdef_body with - | TacticDefinition ((_,id), body) -> pr_id id, false, body - | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body - in - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ - pr_raw_tactic body - in - return ( - hov 1 - (keyword "Ltac" ++ spc () ++ - prlist_with_sep (fun () -> - fnl() ++ keyword "with" ++ spc ()) pr_tac_body l) - ) | VernacCreateHintDb (dbname,b) -> return ( hov 1 (keyword "Create HintDb" ++ spc () ++ diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index e83313aa8e..2d2ea1f8b0 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -694,7 +694,6 @@ let rec tmpp v loc = | VernacBackTo _ -> PCData "VernacBackTo" (* Commands *) - | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x | VernacCreateHintDb _ as x -> xmlTODO loc x | VernacRemoveHints _ as x -> xmlTODO loc x | VernacHints _ as x -> xmlTODO loc x diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 41b753fb8b..ecaf0fb7c5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -173,13 +173,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition l -> - let open Libnames in - let open Vernacexpr in - VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r - | TacticRedefinition (Ident (_,r),_) -> r - | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index d75073877e..f46a670080 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -48,6 +48,7 @@ let new_entry name = 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. *) @@ -311,6 +312,7 @@ open Constrarg open Vernacexpr open Vernac_classifier open Goptions +open Libnames let print_info_trace = ref None @@ -409,3 +411,19 @@ 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/tacentries.ml b/tactics/tacentries.ml index e40f5f46a0..711cd8d9d0 100644 --- a/tactics/tacentries.ml +++ b/tactics/tacentries.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Util open Names @@ -14,6 +15,8 @@ open Pcoq open Egramml open Egramcoq open Vernacexpr +open Libnames +open Nameops (**********************************************************************) (* Tactic Notation *) @@ -184,3 +187,77 @@ let add_ml_tactic_notation name 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 index 635415b9d2..3cf0bc5cc9 100644 --- a/tactics/tacentries.mli +++ b/tactics/tacentries.mli @@ -17,3 +17,5 @@ val add_tactic_notation : 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/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d0af1b951b..bbfa8818b0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -914,81 +914,6 @@ let vernac_restore_state file = (************) (* Commands *) -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 - -let vernac_declare_tactic_definition locality def = - let local = make_module_locality locality in - register_ltac local def - let vernac_create_hintdb locality id b = let local = make_module_locality locality in Hints.create_hint_db local id full_transparent_state b @@ -1898,8 +1823,6 @@ let interp ?proof ~loc locality poly c = | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") (* Commands *) - | VernacDeclareTacticDefinition def -> - vernac_declare_tactic_definition locality def | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids | VernacHints (local,dbnames,hints) -> @@ -1982,7 +1905,6 @@ let check_vernac_supports_locality c l = | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacDeclareMLModule _ - | VernacDeclareTacticDefinition _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ -- cgit v1.2.3 From 5f703bbb8b4f439af9d76b1f6ef24162b67049c2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:43:45 +0100 Subject: Moving Tacintern to Hightactics. --- tactics/hightactics.mllib | 1 + tactics/tactics.mllib | 1 - toplevel/vernacentries.ml | 1 - 3 files changed, 1 insertion(+), 2 deletions(-) diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index b18d148ec6..468b938b6a 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,4 @@ +Tacintern Tacentries Tacinterp Evar_tactics diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 584cc0b730..b495a885f8 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -19,7 +19,6 @@ Taccoerce Tacenv Hints Auto -Tacintern Tactic_matching Tactic_debug Term_dnet diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bbfa8818b0..bdd52d5be0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1427,7 +1427,6 @@ let vernac_check_may_eval redexp glopt rc = pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ Printer.pr_universe_ctx sigma uctx) | Some r -> - Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in -- cgit v1.2.3