diff options
| -rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
| -rw-r--r-- | ltac/extraargs.ml4 | 4 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 119 | ||||
| -rw-r--r-- | ltac/tacentries.mli | 8 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 110 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 21 |
6 files changed, 127 insertions, 137 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index f9f3ee988..adfbd8cfd 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -140,7 +140,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< do { Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; - Egramcoq.create_ltac_quotation $se$ + Tacentries.create_ltac_quotation $se$ (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) ($lid:s$, None) } >> ] diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index d33ec91f9..4d3507cbc 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -25,7 +25,7 @@ open Locus let create_generic_quotation name e wit = let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in - Egramcoq.create_ltac_quotation name inject (e, None) + Tacentries.create_ltac_quotation name inject (e, None) let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string @@ -38,7 +38,7 @@ let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Con let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) (* Rewriting orientation *) diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index e247a138d..99c2213e1 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -128,6 +128,88 @@ let interp_entry_name up_level s sep = eval (parse_user_entry s sep) (**********************************************************************) +(** Grammar declaration for Tactic Notation (Coq level) *) + +let get_tactic_entry n = + if Int.equal n 0 then + Tactic.simple_tactic, None + else if Int.equal n 5 then + Tactic.binder_tactic, None + else if 1<=n && n<5 then + Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) + else + error ("Invalid Tactic Notation level: "^(string_of_int n)^".") + +(**********************************************************************) +(** State of the grammar extensions *) + +type tactic_grammar = { + tacgram_level : int; + tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; +} + +(** ML Tactic grammar extensions *) + +let add_ml_tactic_entry (name, prods) = + let entry = Tactic.simple_tactic in + let mkact i loc l : Tacexpr.raw_tactic_expr = + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + let map arg = TacGeneric arg in + TacML (loc, entry, List.map map l) + in + let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in + synchronize_level_positions (); + grammar_extend entry None (None, [(None, None, List.rev rules)]); + 1 + +(* Declaration of the tactic grammar rule *) + +let head_is_ident tg = match tg.tacgram_prods with +| GramTerminal _::_ -> true +| _ -> false + +(** Tactic grammar extensions *) + +let add_tactic_entry (kn, tg) = + let open Tacexpr in + let entry, pos = get_tactic_entry tg.tacgram_level in + let mkact loc l = + let filter = function + | GramTerminal _ -> None + | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t) + in + let types = List.map_filter filter tg.tacgram_prods in + let map arg t = + (** HACK to handle especially the tactic(...) entry *) + let wit = Genarg.rawwit Constrarg.wit_tactic in + if Genarg.argument_type_eq t (Genarg.unquote wit) then + Tacexp (Genarg.out_gen wit arg) + else + TacGeneric arg + in + let l = List.map2 map l types in + (TacAlias (loc,kn,l):raw_tactic_expr) + in + let () = + if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then + error "Notation for simple tactic must start with an identifier." + in + let rules = make_rule mkact tg.tacgram_prods in + synchronize_level_positions (); + grammar_extend entry None (pos, [(None, None, List.rev [rules])]); + 1 + +let tactic_grammar = + create_grammar_command "TacticGrammar" add_tactic_entry + +let ml_tactic_grammar = + create_grammar_command "MLTacticGrammar" add_ml_tactic_entry + +let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn) +let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn) + +(**********************************************************************) (* Tactic Notation *) let interp_prod_item lev = function @@ -172,13 +254,13 @@ 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; + 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 + extend_tactic_grammar key tobj.tacobj_tacgram let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in @@ -187,7 +269,7 @@ let load_tactic_notation i (_, tobj) = 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 + extend_tactic_grammar key tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = let (ids, body) = tobj.tacobj_body in @@ -297,6 +379,37 @@ let add_ml_tactic_notation name prods = Lib.add_anonymous_leaf (inMLTacticGrammar obj); extend_atomic_tactic name prods +(**********************************************************************) +(** Ltac quotations *) + +let ltac_quotations = ref String.Set.empty + +let create_ltac_quotation name cast (e, l) = + let open Extend in + let () = + if String.Set.mem name !ltac_quotations then + failwith ("Ltac quotation " ^ name ^ " already registered") + in + let () = ltac_quotations := String.Set.add name !ltac_quotations in + let entry = match l with + | None -> Aentry (name_of_entry e) + | Some l -> Aentryl (name_of_entry e, l) + in +(* let level = Some "1" in *) + let level = None in + let assoc = None in + let rule = + Next (Next (Next (Next (Next (Stop, + Atoken (Lexer.terminal name)), + Atoken (Lexer.terminal ":")), + Atoken (Lexer.terminal "(")), + entry), + Atoken (Lexer.terminal ")")) + in + let action _ v _ _ _ loc = cast (loc, v) in + let gram = (level, assoc, [Rule (rule, action)]) in + Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) + (** Command *) diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 3cf0bc5cc..b60d8f478 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -19,3 +19,11 @@ 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 + +(** {5 Adding tactic quotations} *) + +val create_ltac_quotation : string -> + ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit +(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, + Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and + generates an argument using [f] on the entry parsed by [e]. *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 5e89567cc..f0c12ab8e 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -224,27 +224,6 @@ let extend_constr_notation (_, ng) = let nb' = extend_constr_pat_notation ng in nb + nb' -(**********************************************************************) -(** Grammar declaration for Tactic Notation (Coq level) *) - -let get_tactic_entry n = - if Int.equal n 0 then - Tactic.simple_tactic, None - else if Int.equal n 5 then - Tactic.binder_tactic, None - else if 1<=n && n<5 then - Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) - else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") - -(**********************************************************************) -(** State of the grammar extensions *) - -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; -} - module GrammarCommand = Dyn.Make(struct end) module GrammarInterp = struct type 'a t = 'a -> int end module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) @@ -260,57 +239,6 @@ let create_grammar_command name interp : _ grammar_command = let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in obj -(** ML Tactic grammar extensions *) - -let add_ml_tactic_entry (name, prods) = - let entry = Tactic.simple_tactic in - let mkact i loc l : raw_tactic_expr = - let open Tacexpr in - let entry = { mltac_name = name; mltac_index = i } in - let map arg = TacGeneric arg in - TacML (loc, entry, List.map map l) - in - let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in - synchronize_level_positions (); - grammar_extend entry None (None, [(None, None, List.rev rules)]); - 1 - -(* Declaration of the tactic grammar rule *) - -let head_is_ident tg = match tg.tacgram_prods with -| GramTerminal _::_ -> true -| _ -> false - -(** Tactic grammar extensions *) - -let add_tactic_entry (kn, tg) = - let entry, pos = get_tactic_entry tg.tacgram_level in - let mkact loc l = - let filter = function - | GramTerminal _ -> None - | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t) - in - let types = List.map_filter filter tg.tacgram_prods in - let map arg t = - (** HACK to handle especially the tactic(...) entry *) - let wit = Genarg.rawwit Constrarg.wit_tactic in - if Genarg.argument_type_eq t (Genarg.unquote wit) then - Tacexp (Genarg.out_gen wit arg) - else - TacGeneric arg - in - let l = List.map2 map l types in - (TacAlias (loc,kn,l):raw_tactic_expr) - in - let () = - if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then - error "Notation for simple tactic must start with an identifier." - in - let rules = make_rule mkact tg.tacgram_prods in - synchronize_level_positions (); - grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - 1 - let extend_grammar tag g = let nb = GrammarInterpMap.find tag !grammar_interp g in grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state @@ -320,15 +248,7 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag = create_grammar_command "Notation" extend_constr_notation -let tactic_grammar = - create_grammar_command "TacticGrammar" add_tactic_entry - -let ml_tactic_grammar = - create_grammar_command "MLTacticGrammar" add_ml_tactic_entry - let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn) -let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn) -let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn) let recover_constr_grammar ntn prec = let filter (_, gram) : notation_grammar option = match gram with @@ -386,33 +306,3 @@ let with_grammar_rule_protection f x = let reraise = Errors.push reraise in let () = unfreeze fs in iraise reraise - -(**********************************************************************) -(** Ltac quotations *) - -let ltac_quotations = ref String.Set.empty - -let create_ltac_quotation name cast (e, l) = - let () = - if String.Set.mem name !ltac_quotations then - failwith ("Ltac quotation " ^ name ^ " already registered") - in - let () = ltac_quotations := String.Set.add name !ltac_quotations in - let entry = match l with - | None -> Aentry (name_of_entry e) - | Some l -> Aentryl (name_of_entry e, l) - in -(* let level = Some "1" in *) - let level = None in - let assoc = None in - let rule = - Next (Next (Next (Next (Next (Stop, - Atoken (Lexer.terminal name)), - Atoken (Lexer.terminal ":")), - Atoken (Lexer.terminal "(")), - entry), - Atoken (Lexer.terminal ")")) - in - let action _ v _ _ _ loc = cast (loc, v) in - let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 153f7528f..6ec106626 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,11 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; -} - (** {5 Extending the parser with Summary-synchronized commands} *) type 'a grammar_command @@ -60,24 +55,8 @@ val extend_grammar : 'a grammar_command -> 'a -> unit val extend_constr_grammar : Notation.level -> notation_grammar -> unit (** Add a term notation rule to the parsing system. *) -val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit -(** Add a tactic notation rule to the parsing system. This produces a TacAlias - tactic with the provided kernel name. *) - -val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit -(** Add a ML tactic notation rule to the parsing system. This produces a - TacML tactic with the provided string as name. *) - val recover_constr_grammar : notation -> Notation.level -> notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b - -(** {5 Adding tactic quotations} *) - -val create_ltac_quotation : string -> - ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit -(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, - Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and - generates an argument using [f] on the entry parsed by [e]. *) |