aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml21
-rw-r--r--interp/notation.mli6
-rw-r--r--intf/vernacexpr.mli3
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--printing/ppvernac.ml5
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--toplevel/metasyntax.ml60
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/vernacentries.ml2
9 files changed, 76 insertions, 33 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index e765701d4..93e6f31c0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -940,17 +940,28 @@ let pr_visibility prglob = function
(* Mapping notations to concrete syntax *)
type unparsing_rule = unparsing list * precedence
-
+type extra_unparsing_rules = (string * string) list
(* Concrete syntax for symbolic-extension table *)
let printing_rules =
- ref (String.Map.empty : unparsing_rule String.Map.t)
+ ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
-let declare_notation_printing_rule ntn unpl =
- printing_rules := String.Map.add ntn unpl !printing_rules
+let declare_notation_printing_rule ntn ~extra unpl =
+ printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
let find_notation_printing_rule ntn =
- try String.Map.find ntn !printing_rules
+ try fst (String.Map.find ntn !printing_rules)
with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
+let find_notation_extra_printing_rules ntn =
+ try snd (String.Map.find ntn !printing_rules)
+ with Not_found -> []
+let add_notation_extra_printing_rule ntn k v =
+ try
+ printing_rules :=
+ let p, pp = String.Map.find ntn !printing_rules in
+ String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+ with Not_found ->
+ user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
+ str "No such Notation.")
(**********************************************************************)
(* Synchronisation with reset *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 95e176064..961e1e12e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -185,8 +185,12 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
(** Declare and look for the printing rule for symbolic notations *)
type unparsing_rule = unparsing list * precedence
-val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+type extra_unparsing_rules = (string * string) list
+val declare_notation_printing_rule :
+ notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
(** Rem: printing rules for primitive token are canonical *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index e670f68c2..2c73a974b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -206,7 +206,7 @@ type syntax_modifier =
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing of Flags.compat_version
- | SetFormat of string located
+ | SetFormat of string * string located
type proof_end =
| Admitted
@@ -290,6 +290,7 @@ type vernac_expr =
| VernacNotation of
obsolete_locality * constr_expr * (lstring * syntax_modifier list) *
scope_name option
+ | VernacNotationAddFormat of string * string * string
(* Gallina *)
| VernacDefinition of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 955179ba0..cabb09dc3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1026,6 +1026,8 @@ GEXTEND Gram
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacNotation (local,c,(s,modl),sc)
+ | 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
@@ -1072,7 +1074,11 @@ GEXTEND Gram
SetOnlyParsing Flags.Current
| IDENT "compat"; s = STRING ->
SetOnlyParsing (Coqinit.get_compat_version s)
- | IDENT "format"; s = [s = STRING -> (!@loc,s)] -> SetFormat s
+ | IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
+ s2 = OPT [s = STRING -> (!@loc,s)] ->
+ begin match s1, s2 with
+ | (_,k), Some s -> SetFormat(k,s)
+ | s, None -> SetFormat ("text",s) end
| x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
| x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8ca05f2ca..b841c19cc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -344,7 +344,8 @@ let pr_syntax_modifier = function
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
| SetOnlyParsing Flags.Current -> str"only parsing"
| SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"")
- | SetFormat s -> str"format " ++ pr_located qs s
+ | SetFormat("text",s) -> str"format " ++ pr_located qs s
+ | SetFormat(k,s) -> str"format " ++ qs k ++ spc() ++ pr_located qs s
let pr_syntax_modifiers = function
| [] -> mt()
@@ -571,6 +572,8 @@ let rec pr_vernac = function
| VernacSyntaxExtension (_,(s,l)) ->
str"Reserved Notation" ++ spc() ++ pr_located qs s ++
pr_syntax_modifiers l
+ | VernacNotationAddFormat(s,k,v) ->
+ str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
(* Gallina *)
| VernacDefinition (d,id,b) -> (* A verifier... *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 794fabc91..e810e5907 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -178,7 +178,7 @@ let rec classify_vernac e =
VtSideff [id], if bl = [] then VtLater else VtNow
(* These commands alter the parser *)
| VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
- | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _
+ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _
| VernacSyntacticDefinition _
| VernacDeclareTacticDefinition _ | VernacTacticNotation _
| VernacRequire _ | VernacImport _ | VernacInclude _
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c674fddb4..905df5f2b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -790,6 +790,7 @@ type syntax_extension = {
synext_notation : notation;
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
+ synext_extra : (string * string) list;
}
type syntax_extension_obj = locality_flag * syntax_extension list
@@ -806,7 +807,8 @@ let cache_one_syntax_extension se =
(* Declare the parsing rule *)
Egramcoq.extend_constr_grammar prec se.synext_notgram;
(* Declare the printing rule *)
- Notation.declare_notation_printing_rule ntn (se.synext_unparsing, fst prec)
+ Notation.declare_notation_printing_rule ntn
+ ~extra:se.synext_extra (se.synext_unparsing, fst prec)
let cache_syntax_extension (_, (_, sy)) =
List.iter cache_one_syntax_extension sy
@@ -839,38 +841,40 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
let interp_modifiers modl =
let onlyparsing = ref false in
- let rec interp assoc level etyps format = function
+ let rec interp assoc level etyps format extra = function
| [] ->
- (assoc,level,etyps,!onlyparsing,format)
+ (assoc,level,etyps,!onlyparsing,format,extra)
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
error (s^" is already assigned to an entry or constr level.");
- interp assoc level ((id,typ)::etyps) format l
+ interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
- interp assoc level etyps format l
+ interp assoc level etyps format extra l
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
error (s^" is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
- interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
+ interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
| SetLevel n :: l ->
if not (Option.is_empty level) then error "A level is given more than once.";
- interp assoc (Some n) etyps format l
+ interp assoc (Some n) etyps format extra l
| SetAssoc a :: l ->
if not (Option.is_empty assoc) then error"An associativity is given more than once.";
- interp (Some a) level etyps format l
+ interp (Some a) level etyps format extra l
| SetOnlyParsing _ :: l ->
onlyparsing := true;
- interp assoc level etyps format l
- | SetFormat s :: l ->
+ interp assoc level etyps format extra l
+ | SetFormat ("text",s) :: l ->
if not (Option.is_empty format) then error "A format is given more than once.";
- interp assoc level etyps (Some s) l
- in interp None None [] None modl
+ interp assoc level etyps (Some s) extra l
+ | SetFormat (k,(_,s)) :: l ->
+ interp assoc level etyps format ((k,s) :: extra) l
+ in interp None None [] None [] modl
let check_infix_modifiers modifiers =
- let (assoc,level,t,b,fmt) = interp_modifiers modifiers in
+ let (assoc,level,t,b,fmt,extra) = interp_modifiers modifiers in
if not (List.is_empty t) then
error "Explicit entry level or type unexpected in infix notation."
@@ -1035,7 +1039,7 @@ let remove_curly_brackets l =
in aux true l
let compute_syntax_data df modifiers =
- let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
+ let (assoc,n,etyps,onlyparse,fmt,extra) = interp_modifiers modifiers in
let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
let toks = split_notation_string df in
let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -1062,16 +1066,16 @@ let compute_syntax_data df modifiers =
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
(* Return relevant data for interpretation and for parsing/printing *)
- (msgs,i_data,i_typs,sy_fulldata)
+ (msgs,i_data,i_typs,sy_fulldata,extra)
let compute_pure_syntax_data df mods =
- let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data df mods in
+ let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
(msg_warning,
strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
else msgs in
- msgs, sy_data
+ msgs, sy_data, extra
(**********************************************************************)
(* Registration of notations interpretation *)
@@ -1154,11 +1158,13 @@ let recover_syntax ntn =
try
let prec = Notation.level_of_notation ntn in
let pp_rule,_ = Notation.find_notation_printing_rule ntn in
+ let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
{ synext_level = prec;
synext_notation = ntn;
synext_notgram = pa_rule;
- synext_unparsing = pp_rule; }
+ synext_unparsing = pp_rule;
+ synext_extra = pp_extra_rules }
with Not_found ->
raise NoSyntaxRule
@@ -1190,7 +1196,7 @@ let make_pp_rule (n,typs,symbols,fmt) =
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
| Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
-let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
let pa_rule = make_pa_rule i_typs sy_data ntn in
let pp_rule = make_pp_rule sy_data in
let sy = {
@@ -1198,6 +1204,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
synext_notation = ntn;
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
+ synext_extra = extra;
} in
(* By construction, the rule for "{ _ }" is declared, but we need to
redeclare it because the file where it is declared needs not be open
@@ -1212,9 +1219,9 @@ let to_map l =
List.fold_left fold Id.Map.empty l
let add_notation_in_scope local df c mods scope =
- let (msgs,i_data,i_typs,sy_data) = compute_syntax_data df mods in
+ let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
(* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sy_data in
+ let sy_rules = make_syntax_rules sy_data extra in
(* Prepare the interpretation *)
let (onlyparse, recvars,mainvars, df') = i_data in
let i_vars = make_internalization_vars recvars mainvars i_typs in
@@ -1276,8 +1283,8 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension local ((loc,df),mods) =
- let msgs, sy_data = compute_pure_syntax_data df mods in
- let sy_rules = make_syntax_rules sy_data in
+ let msgs, sy_data, extra = compute_pure_syntax_data df mods in
+ let sy_rules = make_syntax_rules sy_data extra in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
@@ -1311,6 +1318,13 @@ let add_notation local c ((loc,df),modifiers) sc =
in
Dumpglob.dump_notation (loc,df') sc true
+let add_notation_extra_printing_rule df k v =
+ let notk =
+ let dfs = split_notation_string df in
+ let _,_, symbs = analyze_notation_tokens dfs in
+ make_notation_key symbs in
+ Notation.add_notation_extra_printing_rule notk k v
+
(* Infix notations *)
let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f48c4a700..07428c86f 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -34,6 +34,8 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
val add_notation : locality_flag -> constr_expr ->
(lstring * syntax_modifier list) -> scope_name option -> unit
+val add_notation_extra_printing_rule : string -> string -> string -> unit
+
(** Declaring delimiter keys and default scopes *)
val add_delimiters : scope_name -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9aa43bd42..63253d54e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1770,6 +1770,8 @@ let interp ?proof locality poly c =
| VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc
| VernacNotation (local,c,infpl,sc) ->
vernac_notation locality local c infpl sc
+ | VernacNotationAddFormat(n,k,v) ->
+ Metasyntax.add_notation_extra_printing_rule n k v
(* Gallina *)
| VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 09:21:51 +0000