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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4use: "pa_extend.cmo" i*)
(*i $Id$ i*)
open Pcoq
open Names
open Libnames
open Topconstr
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw
open Prim
open Nametab
let local_make_qualid l id = make_qualid (make_dirpath l) id
let my_int_of_string loc s =
try
let n = int_of_string s in
(* To avoid Array.make errors (that e.g. Undo uses), we set a *)
(* more restricted limit than int_of_string does *)
if n > 1024 * 2048 then raise Exit;
n
with Failure _ | Exit ->
Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
GEXTEND Gram
GLOBAL:
bigint natural integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
ne_string string pattern_ident pattern_identref by_notation smart_global;
preident:
[ [ s = IDENT -> s ] ]
;
ident:
[ [ s = IDENT -> id_of_string s ] ]
;
pattern_ident:
[ [ s = LEFTQMARK; id = ident -> id ] ]
;
pattern_identref:
[ [ id = pattern_ident -> (loc, id) ] ]
;
var: (* as identref, but interpret as a term identifier in ltac *)
[ [ id = ident -> (loc,id) ] ]
;
identref:
[ [ id = ident -> (loc,id) ] ]
;
field:
[ [ s = FIELD -> id_of_string s ] ]
;
fields:
[ [ id = field; (l,id') = fields -> (l@[id],id')
| id = field -> ([],id)
] ]
;
fullyqualid:
[ [ id = ident; (l,id')=fields -> loc,id::List.rev (id'::l)
| id = ident -> loc,[id]
] ]
;
basequalid:
[ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id'
| id = ident -> qualid_of_ident id
] ]
;
name:
[ [ IDENT "_" -> (loc, Anonymous)
| id = ident -> (loc, Name id) ] ]
;
reference:
[ [ id = ident; (l,id') = fields ->
Qualid (loc, local_make_qualid (l@[id]) id')
| id = ident -> Ident (loc,id)
] ]
;
by_notation:
[ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ]
;
smart_global:
[ [ c = reference -> Genarg.AN c
| ntn = by_notation -> Genarg.ByNotation ntn ] ]
;
qualid:
[ [ qid = basequalid -> loc, qid ] ]
;
ne_string:
[ [ s = STRING ->
if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
] ]
;
ne_lstring:
[ [ s = ne_string -> (loc,s) ] ]
;
dirpath:
[ [ id = ident; l = LIST0 field ->
make_dirpath (l@[id]) ] ]
;
string:
[ [ s = STRING -> 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 specially *)
[ [ i = INT -> (Bigint.of_string i) ] ]
;
END
|
