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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: g_primnew.ml4,v 1.4.2.2 2004/07/16 19:30:39 herbelin Exp $ i*)
open Coqast
open Pcoq
open Names
open Libnames
open Topconstr
let _ =
if not !Options.v7 then
Pcoq.reset_all_grammars()
let _ =
if not !Options.v7 then
let f = Gram.Unsafe.clear_entry in
f Prim.bigint;
f Prim.qualid;
f Prim.ast;
f Prim.reference
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"]
let _ =
if not !Options.v7 then
List.iter (fun s -> Lexer.add_token("",s)) prim_kw
open Prim
open Nametab
let local_id_of_string = id_of_string
let local_make_dirpath = make_dirpath
let local_make_qualid l id' = make_qualid (local_make_dirpath l) id'
let local_make_short_qualid id = make_short_qualid id
let local_make_posint = int_of_string
let local_make_negint n = - int_of_string n
let local_make_path l a = encode_kn (local_make_dirpath l) a
let local_make_binding loc a b =
match a with
| Nvar (_,id) -> Slam(loc,Some id,b)
| Nmeta (_,s) -> Smetalam(loc,s,b)
| _ -> failwith "Slam expects a var or a metavar"
let local_append l id = l@[id]
if not !Options.v7 then
GEXTEND Gram
GLOBAL: bigint qualid reference ne_string;
field:
[ [ s = FIELD -> local_id_of_string s ] ]
;
fields:
[ [ id = field; (l,id') = fields -> (local_append l id,id')
| id = field -> ([],id)
] ]
;
basequalid:
[ [ id = base_ident; (l,id')=fields ->
local_make_qualid (local_append l id) id'
| id = base_ident -> local_make_short_qualid id
] ]
;
reference:
[ [ id = base_ident; (l,id') = fields ->
Qualid (loc, local_make_qualid (local_append l id) id')
| id = base_ident -> Ident (loc,id)
] ]
;
qualid:
[ [ qid = basequalid -> loc, qid ] ]
;
ne_string:
[ [ s = STRING ->
if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
] ]
;
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
;
END
|
