blob: dfb788907ea773df585876696d2fd2eaa9467b8b (
plain)
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
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
{
open Names
open Libnames
open Pcoq
open Pcoq.Prim
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
let _ = List.iter CLexer.add_keyword prim_kw
let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
let my_int_of_string loc s =
try
int_of_string s
with Failure _ ->
CErrors.user_err ~loc (Pp.str "This number is too large.")
}
GRAMMAR EXTEND Gram
GLOBAL:
bigint natural integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
preident:
[ [ s = IDENT -> { s } ] ]
;
ident:
[ [ s = IDENT -> { Id.of_string s } ] ]
;
pattern_ident:
[ [ LEFTQMARK; id = ident -> { id } ] ]
;
pattern_identref:
[ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
;
var: (* as identref, but interpret as a term identifier in ltac *)
[ [ id = ident -> { CAst.make ~loc id } ] ]
;
identref:
[ [ id = ident -> { CAst.make ~loc id } ] ]
;
field:
[ [ s = FIELD -> { Id.of_string s } ] ]
;
fields:
[ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') }
| id = field -> { ([],id) }
] ]
;
fullyqualid:
[ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) }
| id = ident -> { CAst.make ~loc [id] }
] ]
;
basequalid:
[ [ id = ident; f=fields -> { let (l,id') = f in local_make_qualid loc (l@[id]) id' }
| id = ident -> { qualid_of_ident ~loc id }
] ]
;
name:
[ [ IDENT "_" -> { CAst.make ~loc Anonymous }
| id = ident -> { CAst.make ~loc @@ Name id } ] ]
;
reference:
[ [ id = ident; f = fields -> {
let (l,id') = f in
local_make_qualid loc (l@[id]) id' }
| id = ident -> { local_make_qualid loc [] id }
] ]
;
by_notation:
[ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ]
;
smart_global:
[ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c }
| ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ]
;
qualid:
[ [ qid = basequalid -> { qid } ] ]
;
ne_string:
[ [ s = STRING ->
{ if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s }
] ]
;
ne_lstring:
[ [ s = ne_string -> { CAst.make ~loc s } ] ]
;
dirpath:
[ [ id = ident; l = LIST0 field ->
{ DirPath.make (List.rev (id::l)) } ] ]
;
string:
[ [ s = STRING -> { s } ] ]
;
lstring:
[ [ s = string -> { CAst.make ~loc s } ] ]
;
integer:
[ [ i = INT -> { my_int_of_string loc i }
| "-"; i = INT -> { - my_int_of_string loc i } ] ]
;
natural:
[ [ i = INT -> { my_int_of_string loc i } ] ]
;
bigint: (* Negative numbers are dealt with elsewhere *)
[ [ i = INT -> { i } ] ]
;
END
|
