aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml8
-rw-r--r--interp/notation.ml28
-rw-r--r--interp/notation.mli3
-rw-r--r--parsing/extend.ml2
-rw-r--r--parsing/notgram_ops.ml3
-rw-r--r--test-suite/output/Notations4.out2
-rw-r--r--test-suite/output/Notations4.v3
-rw-r--r--vernac/egramcoq.ml8
-rw-r--r--vernac/g_vernac.mlg1
-rw-r--r--vernac/metasyntax.ml17
-rw-r--r--vernac/ppvernac.ml1
11 files changed, 67 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c198c4eb9b..06232b8e1a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -792,9 +792,11 @@ let rec flatten_application c = match DAst.get c with
let extern_possible_prim_token (custom,scopes) r =
let (sc,n) = uninterp_prim_token r in
- match availability_of_entry_coercion custom InConstrEntrySomeLevel with
- | None -> raise No_match
- | Some coercion ->
+ let coercion =
+ if entry_has_prim_token n custom then [] else
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion -> coercion in
match availability_of_prim_token n sc scopes with
| None -> raise No_match
| Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
diff --git a/interp/notation.ml b/interp/notation.ml
index 93969f3718..9d6cab550d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1349,6 +1349,34 @@ let entry_has_ident = function
| InCustomEntryLevel (s,n) ->
try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
+let entry_has_numeral_map = ref String.Map.empty
+let entry_has_string_map = ref String.Map.empty
+
+let declare_custom_entry_has_numeral s n =
+ try
+ let p = String.Map.find s !entry_has_numeral_map in
+ user_err (str "Custom entry " ++ str s ++
+ str " has already a rule for numerals at level " ++ int p ++ str ".")
+ with Not_found ->
+ entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map
+
+let declare_custom_entry_has_string s n =
+ try
+ let p = String.Map.find s !entry_has_string_map in
+ user_err (str "Custom entry " ++ str s ++
+ str " has already a rule for strings at level " ++ int p ++ str ".")
+ with Not_found ->
+ entry_has_string_map := String.Map.add s n !entry_has_string_map
+
+let entry_has_prim_token prim = function
+ | InConstrEntrySomeLevel -> true
+ | InCustomEntryLevel (s,n) ->
+ match prim with
+ | Numeral _ ->
+ (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false)
+ | String _ ->
+ (try String.Map.find s !entry_has_string_map <= n with Not_found -> false)
+
let uninterp_prim_token c =
match glob_prim_constr_key c with
| None -> raise Notation_ops.No_match
diff --git a/interp/notation.mli b/interp/notation.mli
index ea5125f7ec..707be6cb87 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -305,9 +305,12 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve
val declare_custom_entry_has_global : string -> int -> unit
val declare_custom_entry_has_ident : string -> int -> unit
+val declare_custom_entry_has_numeral : string -> int -> unit
+val declare_custom_entry_has_string : string -> int -> unit
val entry_has_global : notation_entry_level -> bool
val entry_has_ident : notation_entry_level -> bool
+val entry_has_prim_token : prim_token -> notation_entry_level -> bool
(** Rem: printing rules for primitive token are canonical *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 848861238a..178f7354f2 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -29,6 +29,7 @@ type 'a constr_entry_key_gen =
| ETIdent
| ETGlobal
| ETBigint
+ | ETString
| ETBinder of bool (* open list of binders if true, closed list of binders otherwise *)
| 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 *)
@@ -53,6 +54,7 @@ type constr_prod_entry_key =
| ETProdName (* Parsed as a name (ident or _) *)
| ETProdReference (* Parsed as a global reference *)
| ETProdBigint (* Parsed as an (unbounded) integer *)
+ | ETProdString (* Parsed as a string *)
| 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) *)
| ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a5ade43295..5c220abeda 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -55,11 +55,12 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
| ETIdent, ETIdent -> true
| ETGlobal, ETGlobal -> true
| ETBigint, ETBigint -> true
+| ETString, ETString -> true
| ETBinder b1, ETBinder b2 -> b1 == b2
| 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
-| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
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
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 807914a671..1c8f237bb8 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,6 +14,8 @@ Entry constr:myconstr is
: nat
[<< # 0 >>]
: option nat
+[2 + 3]
+ : nat
[1 {f 1}]
: Expr
fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 2906698386..4ab800c9ba 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,6 +22,9 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
Check [ << # 0 >> ].
+Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
+Check [ 2 + 3 ].
+
End A.
Module B.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 3181bcc4bc..5e98f5ddc0 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,6 +249,7 @@ type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
| TTBigint : ('self, string) entry
+| TTString : ('self, string) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -369,12 +370,14 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
| TTName -> MayRecNo (Aentry Prim.name)
| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTString -> MayRecNo (Aentry Prim.string)
| TTReference -> MayRecNo (Aentry Constr.global)
let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
| ETProdReference -> TTAny TTReference
| ETProdBigint -> TTAny TTBigint
+| ETProdString -> TTAny TTString
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -414,6 +417,11 @@ match e with
| ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v)))
| ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v)))
end
+| TTString ->
+ begin match forpat with
+ | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v))
+ | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v))
+ end
| TTReference ->
begin match forpat with
| ForConstr -> push_constr subst (CAst.make @@ CRef (v, None))
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 28b9fa7449..97c9d23c68 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1234,6 +1234,7 @@ GRAMMAR EXTEND Gram
syntax_extension_type:
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
+ | IDENT "string" -> { ETString }
| IDENT "binder" -> { ETBinder true }
| IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
| IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 7794b0a37a..d39ee60c25 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -396,7 +396,7 @@ let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
let prec = unparsing_precedence_of_entry_type from x in
match x with
- | ETConstr _ | ETGlobal | ETBigint ->
+ | ETConstr _ | ETGlobal | ETBigint | ETString ->
UnpMetaVar (i,prec)
| ETPattern _ ->
UnpBinderMetaVar (i,prec)
@@ -686,6 +686,7 @@ let prod_entry_type = function
| ETIdent -> ETProdName
| ETGlobal -> ETProdReference
| ETBigint -> ETProdBigint
+ | ETString -> ETProdString
| ETBinder _ -> assert false (* See check_binder_type *)
| ETConstr (s,_,p) -> ETProdConstr (s,p)
| ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
@@ -989,7 +990,7 @@ let set_entry_type from n etyps (x,typ) =
| ETConstr (s,bko,n), InternalProd ->
ETConstr (s,bko,(n,InternalProd))
| ETPattern (b,n), _ -> ETPattern (b,n)
- | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
+ | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x
with Not_found ->
ETConstr (from,None,(make_lev n from,typ))
in (x,typ)
@@ -1011,7 +1012,7 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
- | ETConstr _ | ETBigint | ETGlobal
+ | ETConstr _ | ETBigint | ETString | ETGlobal
| ETIdent | ETPattern _ -> NtnInternTypeAny
let set_internalization_type typs =
@@ -1033,7 +1034,7 @@ let make_interpretation_type isrec isonlybinding = function
(* Others *)
| ETIdent -> NtnTypeBinder NtnParsedAsIdent
| ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
- | ETBigint | ETGlobal -> NtnTypeConstr
+ | ETBigint | ETString | ETGlobal -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
@@ -1097,6 +1098,8 @@ type entry_coercion_kind =
| IsEntryCoercion of notation_entry_level
| IsEntryGlobal of string * int
| IsEntryIdent of string * int
+ | IsEntryNumeral of string * int
+ | IsEntryString of string * int
let is_coercion = function
| Some (custom,n,_,[e]) ->
@@ -1108,6 +1111,8 @@ let is_coercion = function
else Some (IsEntryCoercion subentry)
| ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
| ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
+ | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n))
+ | ETString, InCustomEntry s -> Some (IsEntryString (s,n))
| _ -> None)
| Some _ -> assert false
| None -> None
@@ -1149,7 +1154,7 @@ let find_precedence custom lev etyps symbols onlyprint =
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps, custom with
| ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
- | (ETIdent | ETBigint | ETGlobal), _ ->
+ | (ETIdent | ETBigint | ETString | ETGlobal), _ ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1375,6 +1380,8 @@ let open_notation i (_, nobj) =
| Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
| Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
| Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+ | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
+ | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
| None -> ())
end
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f4918caeff..0cf407619b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -126,6 +126,7 @@ open Pputils
| ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
| ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
+ | ETString -> str "string"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:15:20 +0000