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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
open Coqast
open Pcoq
open Names
open Prim
GEXTEND Gram
GLOBAL: var ident metaident number string (*path*) ast astpat
astact entry_type;
metaident:
[ [ s = METAIDENT -> Nmeta(loc,s) ] ]
;
var:
[ [ s = IDENT -> Nvar(loc, id_of_string s) ] ]
;
ident:
[ [ s = IDENT -> Id(loc,s) ] ]
;
number:
[ [ i = INT -> Num(loc, int_of_string i) ] ]
;
string:
[ [ s = STRING -> Str(loc,s) ] ]
;
astpath:
[ [ id = IDENT; (l,a) = astfields ->
let p = make_dirpath (List.rev (id_of_string id :: l)) in
Path(loc, make_path p a)
| id = IDENT -> Nvar(loc, id_of_string id)
] ]
;
astfields:
[ [ id = FIELD; (l,a) = astfields -> id_of_string id :: l, a
| id = FIELD -> [], id_of_string id
] ]
;
astident:
[ [ s = IDENT -> s ] ]
;
(* ast *)
ast:
[ [ id = metaident -> id
| p = astpath -> p
| s = INT -> Num(loc, int_of_string s)
| s = STRING -> Str(loc, s)
| "{"; s = METAIDENT; "}" -> Id(loc,s)
| "("; nname = astident; l = LIST0 ast; ")" -> Node(loc,nname,l)
| "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id])
| "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id])
| "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id])
| "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id])
| "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l)
| "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id])
| "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id])
| "["; "<>"; "]"; b = ast -> Slam(loc,None,b)
| "["; a = ast; "]"; b = ast ->
(match a with
| Nvar (_,id) -> Slam(loc,Some id,b)
| Nmeta (_,s) -> Smetalam(loc,s,b)
| _ -> failwith "Slam expects a var or a metavar")
(*
| "["; ido = astidoption; "]"; b = ast -> Slam(loc,ido,b)
| "["; id = METAIDENT; "]"; b = ast -> Smetalam(loc,id,b)
*)
| "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
;
(*
astidoption:
[ [ "<>" -> None
| id = IDENT -> Some (id_of_string id) ] ]
;
*)
(* meta-syntax entries *)
astpat:
[ [ "<<" ; a = ast; ">>" -> Node loc "ASTPAT" [a]
| a = default_action_parser -> Node loc "ASTPAT" [a] ] ]
;
astact:
[ [ a = action -> Node loc "ASTACT" [a] ] ]
;
astlist:
[ [ l = LIST0 ast -> Node loc "ASTLIST" l ] ]
;
action:
[ [ IDENT "let"; p = astlist; et = entry_type; "="; e1 = action; "in";
e = action -> Node(loc,"$CASE",[e1; et; Node(loc,"CASE",[p;e])])
| IDENT "case"; a = action; et = entry_type; "of";
cl = LIST1 case SEP "|"; IDENT "esac" ->
Node(loc,"$CASE",a::et::cl)
| "["; al = default_action_parser; "]" -> al ] ]
;
case:
[[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
;
entry_type:
[[ ":"; IDENT "ast"; IDENT "list" ->
let _ = set_default_action_parser astlist in Id(loc,"LIST")
| ":"; IDENT "ast" ->
let _ = set_default_action_parser ast in Id(loc,"AST")
| ":"; IDENT "constr" ->
let _ = set_default_action_parser Constr.constr in Id(loc,"AST")
| ":"; IDENT "tactic" ->
let _ = set_default_action_parser Tactic.tactic in Id(loc,"AST")
| ":"; IDENT "vernac" ->
let _ = set_default_action_parser Vernac_.vernac in Id(loc,"AST")
| -> Id(loc,"AST") ]]
;
END
|
