aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/g_number_string.mlg32
-rw-r--r--plugins/syntax/number.mli5
-rw-r--r--plugins/syntax/string_notation.ml27
-rw-r--r--plugins/syntax/string_notation.mli4
4 files changed, 39 insertions, 29 deletions
diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg
index b584505530..c8badd238d 100644
--- a/plugins/syntax/g_number_string.mlg
+++ b/plugins/syntax/g_number_string.mlg
@@ -32,7 +32,7 @@ let warn_deprecated_numeral_notation =
(fun () ->
strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
-let pr_number_mapping (b, n, n') =
+let pr_number_string_mapping (b, n, n') =
if b then
str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc ()
++ Libnames.pr_qualid n'
@@ -40,17 +40,20 @@ let pr_number_mapping (b, n, n') =
Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc ()
++ Libnames.pr_qualid n'
-let pr_number_via (n, l) =
+let pr_number_string_via (n, l) =
str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
- ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]"
+ ++ prlist_with_sep pr_comma pr_number_string_mapping l ++ str "]"
let pr_number_modifier = function
| After a -> pr_number_after a
- | Via nl -> pr_number_via nl
+ | Via nl -> pr_number_string_via nl
let pr_number_options l =
str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")"
+let pr_string_option l =
+ str "(" ++ pr_number_string_via l ++ str ")"
+
}
VERNAC ARGUMENT EXTEND deprecated_number_modifier
@@ -60,22 +63,22 @@ VERNAC ARGUMENT EXTEND deprecated_number_modifier
| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
END
-VERNAC ARGUMENT EXTEND number_mapping
- PRINTED BY { pr_number_mapping }
+VERNAC ARGUMENT EXTEND number_string_mapping
+ PRINTED BY { pr_number_string_mapping }
| [ reference(n) "=>" reference(n') ] -> { false, n, n' }
| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' }
END
-VERNAC ARGUMENT EXTEND number_via
- PRINTED BY { pr_number_via }
-| [ "via" reference(n) "mapping" "[" ne_number_mapping_list_sep(l, ",") "]" ] -> { n, l }
+VERNAC ARGUMENT EXTEND number_string_via
+ PRINTED BY { pr_number_string_via }
+| [ "via" reference(n) "mapping" "[" ne_number_string_mapping_list_sep(l, ",") "]" ] -> { n, l }
END
VERNAC ARGUMENT EXTEND number_modifier
PRINTED BY { pr_number_modifier }
| [ "warning" "after" bignat(waft) ] -> { After (Warning (NumTok.UnsignedNat.of_string waft)) }
| [ "abstract" "after" bignat(n) ] -> { After (Abstract (NumTok.UnsignedNat.of_string n)) }
-| [ number_via(v) ] -> { Via v }
+| [ number_string_via(v) ] -> { Via v }
END
VERNAC ARGUMENT EXTEND number_options
@@ -83,6 +86,11 @@ VERNAC ARGUMENT EXTEND number_options
| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l }
END
+VERNAC ARGUMENT EXTEND string_option
+ PRINTED BY { pr_string_option }
+| [ "(" number_string_via(v) ")" ] -> { v }
+END
+
VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
| #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":"
ident(sc) ] ->
@@ -96,7 +104,7 @@ VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
- | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+ | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) string_option_opt(o) ":"
ident(sc) ] ->
- { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+ { vernac_string_notation (Locality.make_module_locality locality) ty f g o (Id.to_string sc) }
END
diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli
index 5a13d1068b..d7d28b29ed 100644
--- a/plugins/syntax/number.mli
+++ b/plugins/syntax/number.mli
@@ -24,3 +24,8 @@ val vernac_number_notation : locality_flag ->
qualid -> qualid ->
number_option list ->
Notation_term.scope_name -> unit
+
+(** These are also used in string notations *)
+val locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list
+val elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
+val elaborate_to_post_via : Environ.env -> Evd.evar_map -> Libnames.qualid -> Names.inductive -> (bool * Libnames.qualid * Libnames.qualid) list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 98ea318c92..774d59dda3 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -14,15 +14,10 @@ open Libnames
open Constrexpr
open Constrexpr_ops
open Notation
+open Number
(** * String notation *)
-let get_constructors ind =
- let mib,oib = Global.lookup_inductive ind in
- let mc = oib.Declarations.mind_consnames in
- Array.to_list
- (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
-
let qualid_of_ref n =
n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -45,7 +40,7 @@ let type_error_of g ty =
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
-let vernac_string_notation local ty f g scope =
+let vernac_string_notation local ty f g via scope =
let env = Global.env () in
let sigma = Evd.from_env env in
let app x y = mkAppC (x,[y]) in
@@ -55,14 +50,16 @@ let vernac_string_notation local ty f g scope =
let coption = cref (q_option ()) in
let opt r = app coption r in
let clist_byte = app clist cbyte in
- let tyc = Smartlocate.global_inductive_with_alias ty in
+ let ty_name = ty in
+ let ty, via =
+ match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
+ let tyc, params = locate_global_inductive (via = None) ty in
let to_ty = Smartlocate.global_with_alias f in
let of_ty = Smartlocate.global_with_alias g in
let cty = cref ty in
let arrow x y =
mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
- let constructors = get_constructors tyc in
(* Check the type of f *)
let to_kind =
if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
@@ -79,12 +76,10 @@ let vernac_string_notation local ty f g scope =
else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
else type_error_of g ty
in
- let o = { to_kind = to_kind;
- to_ty = to_ty;
- to_post = [||];
- of_kind = of_kind;
- of_ty = of_ty;
- ty_name = ty;
+ let to_post, pt_refs = match via with
+ | None -> elaborate_to_post_params env sigma tyc params
+ | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
+ let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
warning = () }
in
let i =
@@ -92,7 +87,7 @@ let vernac_string_notation local ty f g scope =
pt_scope = scope;
pt_interp_info = StringNotation o;
pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
- pt_refs = constructors;
+ pt_refs;
pt_in_match = true }
in
enable_prim_token_interpretation i
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index 0d99f98d26..f3c7c969c6 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -14,5 +14,7 @@ open Vernacexpr
(** * String notation *)
val vernac_string_notation : locality_flag ->
- qualid -> qualid -> qualid ->
+ qualid ->
+ qualid -> qualid ->
+ Number.number_string_via option ->
Notation_term.scope_name -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:06:15 +0000