1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
DECLARE PLUGIN "number_string_notation_plugin"
{
open Notation
open Number
open String_notation
open Pp
open Names
open Stdarg
open Pcoq.Prim
let pr_number_after = function
| Nop -> 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_string_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_string_via (n, l) =
str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
++ 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_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
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_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_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_string_via(v) ] -> { Via v }
END
VERNAC ARGUMENT EXTEND number_options
PRINTED BY { pr_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) ] ->
{ 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) string_option_opt(o) ":"
ident(sc) ] ->
{ vernac_string_notation (Locality.make_module_locality locality) ty f g o (Id.to_string sc) }
END
|
