From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:26:00 +0200 Subject: Merge numeral and string notation plugins --- plugins/syntax/g_number_string.mlg | 102 +++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 plugins/syntax/g_number_string.mlg (limited to 'plugins/syntax/g_number_string.mlg') diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg new file mode 100644 index 0000000000..b584505530 --- /dev/null +++ b/plugins/syntax/g_number_string.mlg @@ -0,0 +1,102 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* mt () + | Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n + | Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n + +let pr_deprecated_number_modifier m = str "(" ++ pr_number_after m ++ str ")" + +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + +let pr_number_mapping (b, n, n') = + if b then + str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + else + Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + +let pr_number_via (n, l) = + str "via " ++ Libnames.pr_qualid n ++ str " mapping [" + ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]" + +let pr_number_modifier = function + | After a -> pr_number_after a + | Via nl -> pr_number_via nl + +let pr_number_options l = + str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" + +} + +VERNAC ARGUMENT EXTEND deprecated_number_modifier + PRINTED BY { pr_deprecated_number_modifier } +| [ ] -> { Nop } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } +END + +VERNAC ARGUMENT EXTEND number_mapping + PRINTED BY { pr_number_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 } +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 } +END + +VERNAC ARGUMENT EXTEND number_options + PRINTED BY { pr_number_options } +| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } +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) ] -> + + { vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) (Id.to_string sc) } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) deprecated_number_modifier(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) } +END + +VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) ] -> + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } +END -- cgit v1.2.3 From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- plugins/syntax/g_number_string.mlg | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) (limited to 'plugins/syntax/g_number_string.mlg') 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 -- cgit v1.2.3