aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/dune20
-rw-r--r--parsing/extend.ml11
-rw-r--r--parsing/g_constr.mlg10
-rw-r--r--parsing/notation_gram.ml3
-rw-r--r--parsing/notgram_ops.ml46
-rw-r--r--parsing/pcoq.ml127
-rw-r--r--parsing/pcoq.mli28
-rw-r--r--parsing/ppextend.ml21
-rw-r--r--parsing/ppextend.mli1
9 files changed, 190 insertions, 77 deletions
diff --git a/parsing/dune b/parsing/dune
new file mode 100644
index 0000000000..b70612a52b
--- /dev/null
+++ b/parsing/dune
@@ -0,0 +1,20 @@
+(library
+ (name parsing)
+ (public_name coq.parsing)
+ (wrapped false)
+ (libraries proofs))
+
+(rule
+ (targets cLexer.ml)
+ (deps (:ml4-file cLexer.ml4))
+ (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets})))
+
+(rule
+ (targets g_prim.ml)
+ (deps (:mlg-file g_prim.mlg))
+ (action (run coqpp %{mlg-file})))
+
+(rule
+ (targets g_constr.ml)
+ (deps (:mlg-file g_constr.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/parsing/extend.ml b/parsing/extend.ml
index f57e32c884..6fe2956643 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -34,14 +34,12 @@ type production_level =
(** User-level types used to tell how to parse or interpret of the non-terminal *)
type 'a constr_entry_key_gen =
- | ETName
- | ETReference
+ | ETIdent
+ | ETGlobal
| ETBigint
| ETBinder of bool (* open list of binders if true, closed list of binders otherwise *)
- | ETConstr of 'a
- | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
+ | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
| ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
- | ETOther of string * string
(** Entries level (left-hand side of grammar rules) *)
@@ -63,9 +61,8 @@ type constr_prod_entry_key =
| ETProdName (* Parsed as a name (ident or _) *)
| ETProdReference (* Parsed as a global reference *)
| ETProdBigint (* Parsed as an (unbounded) integer *)
- | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+ | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
| ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *)
- | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
| ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
| ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index b2913d5d4f..7cb5af787b 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -225,11 +225,11 @@ GRAMMAR EXTEND Gram
| "("; c = operconstr LEVEL "200"; ")" ->
{ (match c.CAst.v with
| CPrim (Numeral (n,true)) ->
- CAst.make ~loc @@ CNotation("( _ )",([c],[],[],[]))
+ CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
| _ -> c) }
| "{|"; c = record_declaration; "|}" -> { c }
| "{"; c = binder_constr ; "}" ->
- { CAst.make ~loc @@ CNotation(("{ _ }"),([c],[],[],[])) }
+ { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
| "`{"; c = operconstr LEVEL "200"; "}" ->
{ CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
| "`("; c = operconstr LEVEL "200"; ")" ->
@@ -249,7 +249,7 @@ GRAMMAR EXTEND Gram
record_field_declaration:
[ [ id = global; bl = binders; ":="; c = lconstr ->
- { (id, mkCLambdaN ~loc bl c) } ] ]
+ { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ]
;
binder_constr:
[ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
@@ -411,13 +411,13 @@ GRAMMAR EXTEND Gram
| "("; p = pattern LEVEL "200"; ")" ->
{ (match p.CAst.v with
| CPatPrim (Numeral (n,true)) ->
- CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+ CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
| _ -> p) }
| "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
{ let p =
match p with
| { CAst.v = CPatPrim (Numeral (n,true)) } ->
- CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+ CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
| _ -> p
in
CAst.make ~loc @@ CPatCast (p, ty) }
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 346350641f..d8c08803b6 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -17,7 +17,8 @@ type precedence = int
type parenRelation = L | E | Any | Prec of precedence
type tolerability = precedence * parenRelation
-type level = precedence * tolerability list * constr_entry_key list
+type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+ (* first argument is InCustomEntry s for custom entries *)
type grammar_constr_prod_item =
| GramConstrTerminal of Tok.t
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 071e6db205..5cc1292c92 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -11,55 +11,61 @@
open Pp
open CErrors
open Util
-open Extend
+open Notation
open Notation_gram
(* Uninterpreted notation levels *)
-let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
let declare_notation_level ?(onlyprint=false) ntn level =
- if String.Map.mem ntn !notation_level_map then
- anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
- notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
+ try
+ let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
+ if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+ with Not_found ->
+ notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
let level_of_notation ?(onlyprint=false) ntn =
- let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+ let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
if onlyprint' && not onlyprint then raise Not_found;
level
(**********************************************************************)
-(* Operations on scopes *)
+(* Equality *)
+
+open Extend
let parenRelation_eq t1 t2 = match t1, t2 with
| L, L | E, E | Any, Any -> true
| Prec l1, Prec l2 -> Int.equal l1 l2
| _ -> false
-let production_level_eq l1 l2 = true (* (l1 = l2) *)
+let production_position_eq pp1 pp2 = match (pp1,pp2) with
+| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
+| InternalProd, InternalProd -> true
+| (BorderProd _ | InternalProd), _ -> false
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+let production_level_eq l1 l2 = match (l1,l2) with
| NextLevel, NextLevel -> true
| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
+| (NextLevel | NumLevel _), _ -> false
let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETName, ETName -> true
-| ETReference, ETReference -> true
+| ETIdent, ETIdent -> true
+| ETGlobal, ETGlobal -> true
| ETBigint, ETBigint -> true
| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
+ notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
let prod_eq (l1,pp1) (l2,pp2) =
- if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
- else production_level_eq l1 l2 in
- Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+ not strict ||
+ (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
+ notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
&& List.equal (constr_entry_key_eq prod_eq) u1 u2
let level_eq = level_eq_gen false
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6726603e60..eb3e633892 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -271,14 +271,21 @@ type gram_reinit = gram_assoc * gram_position
type extend_rule =
| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
+module EntryCommand = Dyn.Make ()
+module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end
+module EntryDataMap = EntryCommand.Map(EntryData)
+
type ext_kind =
| ByGrammar of extend_rule
| ByEXTEND of (unit -> unit) * (unit -> unit)
+ | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind
(** The list of extensions *)
let camlp5_state = ref []
+let camlp5_entries = ref EntryDataMap.empty
+
(** Deletion *)
let grammar_delete e reinit (pos,rls) =
@@ -344,7 +351,7 @@ module Gram =
let rec remove_grammars n =
if n>0 then
- (match !camlp5_state with
+ match !camlp5_state with
| [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
| ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
grammar_delete g reinit (of_coq_extend_statement ext);
@@ -355,7 +362,17 @@ let rec remove_grammars n =
camlp5_state := t;
remove_grammars n;
redo();
- camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state)
+ camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state
+ | ByEntry (tag, name, e) :: t ->
+ G.Unsafe.clear_entry e;
+ camlp5_state := t;
+ let EntryData.Ex entries =
+ try EntryDataMap.find tag !camlp5_entries
+ with Not_found -> EntryData.Ex String.Map.empty
+ in
+ let entries = String.Map.remove name entries in
+ camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries;
+ remove_grammars (n - 1)
let make_rule r = [None, None, r]
@@ -517,59 +534,119 @@ module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
let grammar_interp = ref GrammarInterpMap.empty
-let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref []
+type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t
+
+module EntryInterp = struct type _ t = Ex : ('a, 'b) entry_extension -> ('a * 'b) t end
+module EntryInterpMap = EntryCommand.Map(EntryInterp)
+
+let entry_interp = ref EntryInterpMap.empty
+
+type grammar_entry =
+| GramExt of int * GrammarCommand.t
+| EntryExt : int * ('a * 'b) EntryCommand.tag * 'a -> grammar_entry
+
+let (grammar_stack : (grammar_entry * GramState.t) list ref) = ref []
type 'a grammar_command = 'a GrammarCommand.tag
+type ('a, 'b) entry_command = ('a * 'b) EntryCommand.tag
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 create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) entry_command =
+ let obj = EntryCommand.create name in
+ let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in
+ obj
+
let extend_grammar_command tag g =
let modify = GrammarInterpMap.find tag !grammar_interp in
let grammar_state = match !grammar_stack with
| [] -> GramState.empty
- | (_, _, st) :: _ -> st
+ | (_, st) :: _ -> st
in
let (rules, st) = modify g grammar_state in
let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
let () = List.iter iter rules in
let nb = List.length rules in
- grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack
+ grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
-let recover_grammar_command (type a) (tag : a grammar_command) : a list =
- let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) ->
- match GrammarCommand.eq tag tag' with
- | None -> None
- | Some Refl -> Some v
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list =
+ let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
+ let grammar_state = match !grammar_stack with
+ | [] -> GramState.empty
+ | (_, st) :: _ -> st
in
- List.map_filter filter !grammar_stack
+ let (names, st) = modify g grammar_state in
+ let entries = List.map (fun name -> Gram.entry_create name) names in
+ let iter name e =
+ camlp5_state := ByEntry (tag, name, e) :: !camlp5_state;
+ let EntryData.Ex old =
+ try EntryDataMap.find tag !camlp5_entries
+ with Not_found -> EntryData.Ex String.Map.empty
+ in
+ let entries = String.Map.add name e old in
+ camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries
+ in
+ let () = List.iter2 iter names entries in
+ let nb = List.length entries in
+ let () = grammar_stack := (EntryExt (nb, tag, g), st) :: !grammar_stack in
+ entries
+
+let find_custom_entry tag name =
+ let EntryData.Ex map = EntryDataMap.find tag !camlp5_entries in
+ String.Map.find name map
-let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g
+let extend_dyn_grammar (e, _) = match e with
+| GramExt (_, (GrammarCommand.Dyn (tag, g))) -> extend_grammar_command tag g
+| EntryExt (_, tag, g) -> ignore (extend_entry_command tag g)
-(* Summary functions: the state of the lexer is included in that of the parser.
+(** Registering extra grammar *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammars_by_name name grams =
+ grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+ try String.Map.find name !grammar_names
+ with Not_found ->
+ let fold (EntryDataMap.Any (tag, EntryData.Ex map)) accu =
+ try AnyEntry (String.Map.find name map) :: accu
+ with Not_found -> accu
+ in
+ EntryDataMap.fold fold !camlp5_entries []
+
+(** 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 * GrammarCommand.t * GramState.t) list * CLexer.keyword_state
+type frozen_t =
+ (grammar_entry * GramState.t) list *
+ CLexer.keyword_state
-let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ())
+let freeze _ : frozen_t =
+ (!grammar_stack, CLexer.get_keyword_state ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
let factorize_grams l1 l2 =
if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
-let number_of_entries gcl =
- List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
+let rec number_of_entries accu = function
+| [] -> accu
+| ((GramExt (p, _) | EntryExt (p, _, _)), _) :: rem ->
+ number_of_entries (p + accu) rem
let unfreeze (grams, lex) =
let (undo, redo, common) = factorize_grams !grammar_stack grams in
- let n = number_of_entries undo in
+ let n = number_of_entries 0 undo in
remove_grammars n;
grammar_stack := common;
CLexer.set_keyword_state lex;
- List.iter extend_dyn_grammar (List.rev_map pi2 redo)
+ List.iter extend_dyn_grammar (List.rev redo)
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
@@ -603,15 +680,3 @@ let () =
Grammar.register0 wit_sort_family (Constr.sort_family);
Grammar.register0 wit_constr (Constr.constr);
()
-
-(** Registering extra grammar *)
-
-type any_entry = AnyEntry : 'a Entry.t -> any_entry
-
-let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
-
-let register_grammars_by_name name grams =
- grammar_names := String.Map.add name grams !grammar_names
-
-let find_grammars_by_name name =
- String.Map.find name !grammar_names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 029c437136..e12ccaa636 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -233,6 +233,8 @@ val grammar_extend : 'a Entry.t -> gram_reinit option ->
module GramState : Store.S
(** Auxiliary state of the grammar. Any added data must be marshallable. *)
+(** {6 Extension with parsing rules} *)
+
type 'a grammar_command
(** Type of synchronized parsing extensions. The ['a] type should be
marshallable. *)
@@ -253,8 +255,30 @@ val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_comman
val extend_grammar_command : 'a grammar_command -> 'a -> unit
(** Extend the grammar of Coq with the given data. *)
-val recover_grammar_command : 'a grammar_command -> 'a list
-(** Recover the current stack of grammar extensions. *)
+(** {6 Extension with parsing entries} *)
+
+type ('a, 'b) entry_command
+(** Type of synchronized entry creation. The ['a] type should be
+ marshallable. *)
+
+type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t
+(** Entry extension entry point. Given some ['a] and a current grammar state,
+ such a function must produce the list of entry extensions that will be
+ created and kept synchronized w.r.t. the summary, together
+ with a new state. It should be pure. *)
+
+val create_entry_command : string -> ('a, 'b) entry_extension -> ('a, 'b) entry_command
+(** Create a new entry-creating command with the given name. The extension
+ function is called to generate the new entries for a given data. *)
+
+val extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list
+(** Create new synchronized entries using the provided data. *)
+
+val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t
+(** Find an entry generated by the synchronized system in the current state.
+ @raise Not_found if non-existent. *)
+
+(** {6 Protection w.r.t. backtrack} *)
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index d2b50fa83d..e1f5e20117 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -11,6 +11,7 @@
open Util
open Pp
open CErrors
+open Notation
open Notation_gram
(*s Pretty-print. *)
@@ -48,29 +49,29 @@ type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
(* Concrete syntax for symbolic-extension table *)
let notation_rules =
- Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+ Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
let declare_notation_rule ntn ~extra unpl gram =
- notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+ notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
let find_notation_printing_rule ntn =
- try pi1 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+ try pi1 (NotationMap.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
let find_notation_extra_printing_rules ntn =
- try pi2 (String.Map.find ntn !notation_rules)
+ try pi2 (NotationMap.find ntn !notation_rules)
with Not_found -> []
let find_notation_parsing_rules ntn =
- try pi3 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+ try pi3 (NotationMap.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
let get_defined_notations () =
- String.Set.elements @@ String.Map.domain !notation_rules
+ NotationSet.elements @@ NotationMap.domain !notation_rules
let add_notation_extra_printing_rule ntn k v =
try
notation_rules :=
- let p, pp, gr = String.Map.find ntn !notation_rules in
- String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+ let p, pp, gr = NotationMap.find ntn !notation_rules in
+ NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
with Not_found ->
user_err ~hdr:"add_notation_extra_printing_rule"
(str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 9f61e121a4..7eb5967a3e 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,7 +41,6 @@ type unparsing =
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
-
val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
val find_notation_printing_rule : notation -> unparsing_rule
val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 12:33:00 +0000