diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 4 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 20 | ||||
| -rw-r--r-- | parsing/highparsing.mllib | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 3 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 38 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 | ||||
| -rw-r--r-- | tactics/g_ltac.ml4 (renamed from parsing/g_ltac.ml4) | 57 | ||||
| -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 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 170 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 9 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 7 | ||||
| -rw-r--r-- | toplevel/obligations.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 95 | ||||
| -rw-r--r-- | toplevel/vernacentries.mli | 3 |
22 files changed, 376 insertions, 362 deletions
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/intf/vernacexpr.mli b/intf/vernacexpr.mli index 36b855ec3b..bd5890e296 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 @@ -291,8 +290,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) @@ -382,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 c89238d296..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; ":"; @@ -890,7 +886,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) @@ -1048,10 +1043,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 +1068,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 +1099,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/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/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 887a14d2bf..c1f5e122bd 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 () @@ -466,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) -> @@ -644,8 +631,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 ") ++ @@ -1010,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 a459cd65f8..2d2ea1f8b0 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 @@ -697,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 97d6e1fb71..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 *) @@ -195,7 +188,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) diff --git a/parsing/g_ltac.ml4 b/tactics/g_ltac.ml4 index d1992c57bb..f46a670080 100644 --- a/parsing/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 @@ -370,3 +372,58 @@ 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 + 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 diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e5edc74222..6277a8146a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -43,176 +43,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 *) let entry_buf = Buffer.create 64 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) -> 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ba5eb3f7d..bdd52d5be0 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 = @@ -912,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 @@ -1500,8 +1427,7 @@ 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) = 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 +1438,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 = @@ -1580,7 +1506,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)) @@ -1820,8 +1745,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 @@ -1899,8 +1822,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) -> @@ -1976,15 +1897,13 @@ let check_vernac_supports_locality c l = match l, c with | None, _ -> () | Some _, ( - VernacTacticNotation _ - | VernacOpenCloseScope _ + VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacDeclareMLModule _ - | VernacDeclareTacticDefinition _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ 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 |