aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/metasyntax.ml90
-rw-r--r--vernac/metasyntax.mli2
-rw-r--r--vernac/ppvernac.ml9
-rw-r--r--vernac/ppvernac.mli2
-rw-r--r--vernac/vernacexpr.ml8
6 files changed, 83 insertions, 48 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f8a28332b1..2343ffc7e7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -52,7 +52,6 @@ let of_type = Entry.create "of_type"
let section_subset_expr = Entry.create "section_subset_expr"
let scope_delimiter = Entry.create "scope_delimiter"
let syntax_modifiers = Entry.create "syntax_modifiers"
-let only_parsing = Entry.create "only_parsing"
let make_bullet s =
let open Proof_bullet in
@@ -1160,7 +1159,7 @@ GRAMMAR EXTEND Gram
(* Grammar extensions *)
GRAMMAR EXTEND Gram
- GLOBAL: syntax only_parsing syntax_modifiers;
+ GLOBAL: syntax syntax_modifiers;
syntax:
[ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
@@ -1181,10 +1180,9 @@ GRAMMAR EXTEND Gram
modl = syntax_modifiers;
sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
{ VernacInfix ((op,modl),p,sc) }
- | IDENT "Notation"; id = identref;
- idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
- { VernacSyntacticDefinition
- (id,(idl,c),{ onlyparsing = b }) }
+ | IDENT "Notation"; id = identref; idl = LIST0 ident;
+ ":="; c = constr; modl = syntax_modifiers ->
+ { VernacSyntacticDefinition (id,(idl,c), modl) }
| IDENT "Notation"; s = lstring; ":=";
c = constr;
modl = syntax_modifiers;
@@ -1207,10 +1205,6 @@ GRAMMAR EXTEND Gram
to factorize with other "Print"-based or "Declare"-based vernac entries *)
] ]
;
- only_parsing:
- [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true }
- | -> { false } ] ]
- ;
level:
[ [ IDENT "level"; n = natural -> { NumLevel n }
| IDENT "next"; IDENT "level" -> { NextLevel } ] ]
@@ -1230,10 +1224,12 @@ GRAMMAR EXTEND Gram
{ begin match s1, s2 with
| { CAst.v = 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,None,lev) }
+ | x = IDENT; ","; l = LIST1 IDENT SEP ","; v =
+ [ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) }
+ | "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l }
| x = IDENT; "at"; lev = level; b = OPT binder_interp ->
{ SetItemLevel ([x],b,lev) }
+ | x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) }
| x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
| x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
] ]
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f9f65a8c30..c5bfba900c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -862,6 +862,41 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
(* Interpreting user-provided modifiers *)
(* XXX: We could move this to the parser itself *)
+
+module SyndefMods = struct
+
+type t = {
+ only_parsing : bool;
+ scopes : (Id.t * scope_name) list;
+}
+
+let default = {
+ only_parsing = false;
+ scopes = [];
+}
+
+end
+
+let interp_syndef_modifiers modl = let open SyndefMods in
+ let rec interp skipped acc = function
+ | [] -> List.rev skipped, acc
+ | SetOnlyParsing :: l ->
+ interp skipped { acc with only_parsing = true; } l
+ | SetItemScope([],_) :: l ->
+ interp skipped acc l
+ | SetItemScope(s::ids,k) :: l ->
+ let scopes = acc.scopes in
+ let id = Id.of_string s in
+ if List.mem_assoc id scopes then
+ user_err (str "Notation scope for argument " ++ str s ++
+ str " can be specified only once.");
+ interp skipped { acc with scopes = (id,k) :: scopes }
+ (SetItemScope(ids,s) :: l)
+ | x :: l ->
+ interp (x :: skipped) acc l
+ in
+ interp [] default modl
+
module NotationMods = struct
type notation_modifier = {
@@ -872,7 +907,6 @@ type notation_modifier = {
subtyps : (Id.t * production_level) list;
(* common to syn_data below *)
- only_parsing : bool;
only_printing : bool;
format : lstring option;
extra : (string * string) list;
@@ -884,7 +918,6 @@ let default = {
custom = InConstrEntry;
etyps = [];
subtyps = [];
- only_parsing = false;
only_printing = false;
format = None;
extra = [];
@@ -945,8 +978,6 @@ let interp_modifiers modl = let open NotationMods in
| SetAssoc a :: l ->
if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
interp subtyps { acc with assoc = Some a; } l
- | SetOnlyParsing :: l ->
- interp subtyps { acc with only_parsing = true; } l
| SetOnlyPrinting :: l ->
interp subtyps { acc with only_printing = true; } l
| SetFormat ("text",s) :: l ->
@@ -954,8 +985,10 @@ let interp_modifiers modl = let open NotationMods in
interp subtyps { acc with format = Some s; } l
| SetFormat (k,s) :: l ->
interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
+ | (SetOnlyParsing | SetItemScope _) :: _ -> assert false
in
- let subtyps,mods = interp [] default modl in
+ let modl, syndef_mods = interp_syndef_modifiers modl in
+ let subtyps, mods = interp [] default modl in
(* interpret item levels wrt to main entry *)
let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in
(* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *)
@@ -965,10 +998,10 @@ let interp_modifiers modl = let open NotationMods in
if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true))
else (id,ETIdent)
| x -> x) mods.etyps } in
- { mods with etyps = extra_etyps@mods.etyps }
+ syndef_mods, { mods with etyps = extra_etyps@mods.etyps }
let check_infix_modifiers modifiers =
- let mods = interp_modifiers modifiers in
+ let _, mods = interp_modifiers modifiers in
let t = mods.NotationMods.etyps in
let u = mods.NotationMods.subtyps in
if not (List.is_empty t) || not (List.is_empty u) then
@@ -1036,7 +1069,7 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
| ETConstr _ | ETBigint | ETGlobal
- | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny
+ | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny None
let set_internalization_type typs =
List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -1292,23 +1325,25 @@ let check_locality_compatibility local custom i_typs =
let compute_syntax_data ~local deprecation df modifiers =
let open SynData in
+ let open SyndefMods in
let open NotationMods in
- let mods = interp_modifiers modifiers in
- let onlyprint = mods.only_printing in
- let onlyparse = mods.only_parsing in
- if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
+ let syndef_mods, mods = interp_modifiers modifiers in
+ let only_printing = mods.only_printing in
+ let only_parsing = syndef_mods.only_parsing in
+ if only_printing && only_parsing then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
+ if syndef_mods.scopes <> [] then user_err (str "General notations don't support 'in scope'.");
let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
- let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
+ let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint:only_printing df in
let _ = check_useless_entry_types recvars mainvars mods.etyps in
(* Notations for interp and grammar *)
- let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
+ let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols only_printing in
let ntn_for_interp = make_notation_key mods.custom symbols in
let symbols_for_grammar =
if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in
let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in
- if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
+ if mods.custom = InConstrEntry && not only_printing then check_rule_productivity symbols_for_grammar;
(* To globalize... *)
let etyps = join_auxiliary_recursive_types recvars mods.etyps in
let sy_typs, prec =
@@ -1329,8 +1364,8 @@ let compute_syntax_data ~local deprecation df modifiers =
(* Return relevant data for interpretation and for parsing/printing *)
{ info = i_data;
- only_parsing = mods.only_parsing;
- only_printing = mods.only_printing;
+ only_parsing;
+ only_printing;
deprecation;
format = mods.format;
extra = mods.extra;
@@ -1793,11 +1828,18 @@ let remove_delimiters local scope =
let add_class_scope local scope cl =
Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
-let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
+let add_syntactic_definition ~local deprecation env ident (vars,c) modl =
+ let open SyndefMods in
+ let skipped, { only_parsing; scopes } = interp_syndef_modifiers modl in
+ if skipped <> [] then
+ user_err (str "Simple notations don't support " ++ Ppvernac.pr_syntax_modifier (List.hd skipped));
+ let vars = List.map (fun v -> v, List.assoc_opt v scopes) vars in
let acvars,pat,reversibility =
- try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
- with Not_found ->
- let fold accu id = Id.Map.add id NtnInternTypeAny accu in
+ match vars, intern_name_alias c with
+ | [], Some(r,u) ->
+ Id.Map.empty, NRef(r, u), APrioriReversible
+ | _ ->
+ let fold accu (id,scope) = Id.Map.add id (NtnInternTypeAny scope) accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
let nenv = {
ninterp_var_type = i_vars;
@@ -1805,11 +1847,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
} in
interp_notation_constr env nenv c
in
- let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
+ let in_pat (id,_) = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in
- let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
+ let vars = List.map (fun (x,_) -> (x, Id.Map.find x interp)) vars in
let also_in_cases_pattern = has_no_binders_type vars in
- let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
+ let onlyparsing = only_parsing || fst (printability None [] false reversibility pat) in
Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat)
(**********************************************************************)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index dd71817083..3ece04f5f9 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
(** Add a syntactic definition (as in "Notation f := ...") *)
val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
- Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit
+ Id.t -> Id.t list * constr_expr -> syntax_modifier list -> unit
(** Print the Camlp5 state of a grammar *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 8e5942440b..be34c563c8 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -468,6 +468,8 @@ let pr_syntax_modifier = let open Gramlib.Gramext in function
| SetItemLevel (l,bko,n) ->
prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
pr_opt pr_constr_as_binder_kind bko
+ | SetItemScope (l,s) ->
+ prlist_with_sep sep_v2 str l ++ spc () ++ str"in scope" ++ str s
| SetLevel n -> pr_at_level (NumLevel n)
| SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
| SetAssoc LeftA -> keyword "left associativity"
@@ -484,9 +486,6 @@ let pr_syntax_modifiers = function
| l -> spc() ++
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
-let pr_only_parsing_clause onlyparsing =
- pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
-
let pr_decl_notation prc decl_ntn =
let open Vernacexpr in
let
@@ -1098,12 +1097,12 @@ let pr_vernac_expr v =
)
| VernacHints (dbnames,h) ->
return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
+ | VernacSyntacticDefinition (id,(ids,c),l) ->
return (
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
- pr_only_parsing_clause onlyparsing)
+ pr_syntax_modifiers l)
)
| VernacArguments (q, args, more_implicits, mods) ->
return (
diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli
index 9339803948..d36e61864d 100644
--- a/vernac/ppvernac.mli
+++ b/vernac/ppvernac.mli
@@ -13,6 +13,8 @@
val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
+val pr_syntax_modifier : Vernacexpr.syntax_modifier -> Pp.t
+
(** Prints a fixpoint body *)
val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 46acaf7264..9757783d09 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -114,10 +114,6 @@ type import_filter_expr =
| ImportAll
| ImportNames of one_import_filter_name list
-type onlyparsing_flag = { onlyparsing : bool }
- (* Some v = Parse only; None = Print also.
- If v<>Current, it contains the name of the coq version
- which this notation is trying to be compatible with *)
type locality_flag = bool (* true = Local *)
type option_setting =
@@ -135,6 +131,7 @@ type definition_expr =
type syntax_modifier =
| SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
+ | SetItemScope of string list * scope_name
| SetLevel of int
| SetCustomEntry of string * int option
| SetAssoc of Gramlib.Gramext.g_assoc
@@ -411,8 +408,7 @@ type nonrec vernac_expr =
| VernacRemoveHints of string list * qualid list
| VernacHints of string list * hints_expr
| VernacSyntacticDefinition of
- lident * (Id.t list * constr_expr) *
- onlyparsing_flag
+ lident * (Id.t list * constr_expr) * syntax_modifier list
| VernacArguments of
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:28:40 +0000