aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml153
-rw-r--r--parsing/egramcoq.mli33
-rw-r--r--parsing/pcoq.ml110
-rw-r--r--parsing/pcoq.mli8
4 files changed, 43 insertions, 261 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 8c4930806e..f0c12ab8ef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -217,115 +217,48 @@ let extend_constr_pat_notation ng =
let ext = ETConstr (level, ()), ng.notgram_assoc in
extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
-let extend_constr_notation ng =
+let extend_constr_notation (_, ng) =
(* Add the notation in constr *)
let nb = extend_constr_constr_notation ng in
(* Add the notation in cases_pattern *)
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)^".")
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
-(**********************************************************************)
-(** State of the grammar extensions *)
+let grammar_interp = ref GrammarInterpMap.empty
-type tactic_grammar = {
- tacgram_level : int;
- tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
-type all_grammar_command =
- | Notation of Notation.level * notation_grammar
- | TacticGrammar of KerName.t * tactic_grammar
- | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
+type 'a grammar_command = 'a GrammarCommand.tag
-(** ML Tactic grammar extensions *)
+let create_grammar_command name interp : _ grammar_command =
+ let obj = GrammarCommand.create name in
+ let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+ obj
-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 (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
- let nb = match gram with
- | Notation (_,a) -> extend_constr_notation a
- | TacticGrammar (kn, g) -> add_tactic_entry kn g
- | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
- in
- grammar_state := (nb,gram) :: !grammar_state
+let extend_grammar tag g =
+ let nb = GrammarInterpMap.find tag !grammar_interp g in
+ grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
-let extend_constr_grammar pr ntn =
- extend_grammar (Notation (pr, ntn))
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
-let extend_tactic_grammar kn ntn =
- extend_grammar (TacticGrammar (kn, ntn))
+let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+ create_grammar_command "Notation" extend_constr_notation
-let extend_ml_tactic_grammar name ntn =
- extend_grammar (MLTacticGrammar (name, ntn))
+let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
let recover_constr_grammar ntn prec =
- let filter = function
- | _, Notation (prec', ng) when
- Notation.level_eq prec prec' &&
- String.equal ntn ng.notgram_notation -> Some ng
- | _ -> None
+ let filter (_, gram) : notation_grammar option = match gram with
+ | GrammarCommand.Dyn (tag, obj) ->
+ match GrammarCommand.eq tag constr_grammar with
+ | None -> None
+ | Some Refl ->
+ let (prec', ng) = obj in
+ if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+ else None
in
match List.map_filter filter !grammar_state with
| [x] -> x
@@ -334,7 +267,7 @@ let recover_constr_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
@@ -353,7 +286,7 @@ let unfreeze (grams, lex) =
remove_levels n;
grammar_state := common;
Lexer.unfreeze lex;
- List.iter extend_grammar (List.rev_map snd redo)
+ List.iter extend_dyn_grammar (List.rev_map snd redo)
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
@@ -373,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 23eaa64eec..6ec1066260 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,34 +36,27 @@ 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
+(** Type of synchronized parsing extensions. The ['a] type should be
+ marshallable. *)
+
+val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The function
+ should modify the parser state and return the number of grammar extensions
+ performed. *)
+
+val extend_grammar : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
(** {5 Adding notations} *)
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]. *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 207b43064c..75144addb2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -57,16 +57,6 @@ type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> ty
let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
let weaken_entry x = Gramobj.weaken_entry x
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
-
(** Grammar extensions *)
(** NB: [extend_statment =
@@ -740,108 +730,8 @@ let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
unsafe_grammar_extend e reinit ext
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-let atactic n =
- if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
- else Aentryl (name_of_entry Tactic.tactic_expr, n)
-
-let try_get_entry u s =
- (** Order the effects: get_entry can raise Not_found *)
- let TypedEntry (typ, e) = get_entry u s in
- EntryName (typ, Aentry (name_of_entry e))
-
-(** Quite ad-hoc *)
-let get_tacentry n m =
- let check_lvl n =
- Int.equal m n
- && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
- && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
- in
- if check_lvl n then EntryName (rawwit wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
- else EntryName (rawwit wit_tactic, atactic n)
-
-let rec parse_user_entry s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
- Ulist1 entry
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
- Ulist1sep (entry, sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
- Ulist0 entry
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
- Ulist0sep (entry, sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
- Uopt entry
- else if l > 5 && coincide s "_mods" (l-5) then
- let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
- Umodifiers entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
- let n = Char.code s.[6] - 48 in
- Uentryl ("tactic", n)
- else
- let s = match s with "hyp" -> "var" | _ -> s in
- Uentry s
-
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
-let rec interp_entry_name up_level s sep =
- let rec eval = function
- | Ulist1 e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist1 g)
- | Ulist1sep (e, sep) ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist1sep (g, sep))
- | Ulist0 e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist0 g)
- | Ulist0sep (e, sep) ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist0sep (g, sep))
- | Uopt e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_opt t, Aopt g)
- | Umodifiers e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Amodifiers g)
- | Uentry s ->
- begin
- try try_get_entry uprim s with Not_found ->
- try try_get_entry uconstr s with Not_found ->
- try try_get_entry utactic s with Not_found ->
- error ("Unknown entry "^s^".")
- end
- | Uentryl (s, n) ->
- (** FIXME: do better someday *)
- assert (String.equal s "tactic");
- get_tacentry n up_level
- in
- eval (parse_user_entry s sep)
-
let list_entry_names () =
let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 35973a4d72..afe8889096 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,13 +268,9 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** Binding general entry keys to symbols *)
-type entry_name = EntryName :
- 'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-(** [interp_entry_name lev n sep] returns the entry corresponding to the name
- [n] of the form "ne_constr_list" in a tactic entry of level [lev] with
- separator [sep]. *)
-val interp_entry_name : int -> string -> string -> entry_name
+val get_entry : gram_universe -> string -> typed_entry
(** Recover the list of all known tactic notation entries. *)
val list_entry_names : unit -> (string * argument_type) list
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 01:17:20 +0000