blob: d9385a49fd346970e7879ce5b7110161ac600ef3 (
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
-- top-level grammar
-- Canonical GF. AR 27/4/2003
entrypoints Canon, Line ;
-- old approach: read in a whole grammar
MGr. Canon ::= "grammar" [Ident] "of" Ident ";" [Module] ;
Gr. Canon ::= [Module] ;
-- new approach: read line by line
LMulti. Line ::= "grammar" [Ident] "of" Ident ";" ;
LHeader. Line ::= ModType "=" Extend Open "{" ;
LFlag. Line ::= Flag ";" ;
LDef. Line ::= Def ";" ;
LEnd. Line ::= "}" ;
Mod. Module ::= ModType "=" Extend Open "{" [Flag] [Def] "}" ;
MTAbs. ModType ::= "abstract" Ident ;
MTCnc. ModType ::= "concrete" Ident "of" Ident ;
MTRes. ModType ::= "resource" Ident ;
MTTrans. ModType ::= "transfer" Ident ":" Ident "->" Ident ;
separator Module "" ;
Ext. Extend ::= [Ident] "**" ;
NoExt. Extend ::= ;
Opens. Open ::= "open" [Ident] "in" ;
NoOpens. Open ::= ;
-- judgements
Flg. Flag ::= "flags" Ident "=" Ident ; --- to have the same res word as in GF
AbsDCat. Def ::= "cat" Ident "[" [Decl] "]" "=" [CIdent] ;
AbsDFun. Def ::= "fun" Ident ":" Exp "=" Exp ;
AbsDTrans. Def ::= "transfer" Ident "=" Exp ;
ResDPar. Def ::= "param" Ident "=" [ParDef] ;
ResDOper. Def ::= "oper" Ident ":" CType "=" Term ;
CncDCat. Def ::= "lincat" Ident "=" CType "=" Term ";" Term ;
CncDFun. Def ::= "lin" Ident ":" CIdent "=" "\\" [ArgVar] "->" Term ";" Term ;
AnyDInd. Def ::= Ident Status "in" Ident ;
ParD. ParDef ::= Ident [CType] ;
-- the canonicity of an indirected constant
Canon. Status ::= "data" ;
NonCan. Status ::= ;
-- names originating from resource modules: prefixed by the module name
CIQ. CIdent ::= Ident "." Ident ;
-- types and terms in abstract syntax; no longer type-annotated
EApp. Exp1 ::= Exp1 Exp2 ;
EProd. Exp ::= "(" Ident ":" Exp ")" "->" Exp ;
EAbs. Exp ::= "\\" Ident "->" Exp ;
EAtom. Exp2 ::= Atom ;
EData. Exp2 ::= "data" ;
EEq. Exp ::= "{" [Equation] "}" ; -- list of pattern eqs; primitive notion: []
coercions Exp 2 ;
SType. Sort ::= "Type" ;
Equ. Equation ::= [APatt] "->" Exp ;
APC. APatt ::= "(" CIdent [APatt] ")" ;
APV. APatt ::= Ident ;
APS. APatt ::= String ;
API. APatt ::= Integer ;
APF. APatt ::= Double ;
APW. APatt ::= "_" ;
separator Decl ";" ;
terminator APatt "" ;
terminator Equation ";" ;
AC. Atom ::= CIdent ;
AD. Atom ::= "<" CIdent ">" ;
AV. Atom ::= "$" Ident ;
AM. Atom ::= "?" Integer ;
AS. Atom ::= String ;
AI. Atom ::= Integer ;
AT. Atom ::= Sort ;
Decl. Decl ::= Ident ":" Exp ;
-- types, terms, and patterns in concrete syntax
RecType. CType ::= "{" [Labelling] "}" ;
Table. CType ::= "(" CType "=>" CType ")" ;
Cn. CType ::= CIdent ;
TStr. CType ::= "Str" ;
TInts. CType ::= "Ints" Integer ;
Lbg. Labelling ::= Label ":" CType ;
Arg. Term2 ::= ArgVar ;
I. Term2 ::= CIdent ; -- from resources
Par. Term2 ::= "<" CIdent [Term2] ">" ;
LI. Term2 ::= "$" Ident ; -- from pattern variables
R. Term2 ::= "{" [Assign] "}" ;
P. Term1 ::= Term2 "." Label ;
T. Term1 ::= "table" CType "{" [Case] "}" ;
V. Term1 ::= "table" CType "[" [Term2] "]" ;
S. Term1 ::= Term1 "!" Term2 ;
C. Term ::= Term "++" Term1 ;
FV. Term1 ::= "variants" "{" [Term2] "}" ; --- no separator!
EInt. Term2 ::= Integer ;
EFloat. Term2 ::= Double ;
K. Term2 ::= Tokn ;
E. Term2 ::= "[" "]" ;
KS. Tokn ::= String ;
KP. Tokn ::= "[" "pre" [String] "{" [Variant] "}" "]" ;
internal KM. Tokn ::= String ; -- mark-up
Ass. Assign ::= Label "=" Term ;
Cas. Case ::= [Patt] "=>" Term ;
Var. Variant ::= [String] "/" [String] ;
coercions Term 2 ;
L. Label ::= Ident ;
LV. Label ::= "$" Integer ;
A. ArgVar ::= Ident "@" Integer ; -- no bindings
AB. ArgVar ::= Ident "+" Integer "@" Integer ; -- with a number of bindings
PC. Patt ::= "(" CIdent [Patt] ")" ;
PV. Patt ::= Ident ;
PW. Patt ::= "_" ;
PR. Patt ::= "{" [PattAssign] "}" ;
PI. Patt ::= Integer ;
PF. Patt ::= Double ;
PAss. PattAssign ::= Label "=" Patt ;
--- here we use the new pragmas to generate list rules
terminator Flag ";" ;
terminator Def ";" ;
separator ParDef "|" ;
separator CType "" ;
separator CIdent "" ;
separator Assign ";" ;
separator ArgVar "," ;
separator Labelling ";" ;
separator Case ";" ;
separator Term2 "" ;
separator String "" ;
separator Variant ";" ;
separator PattAssign ";" ;
separator Patt "" ;
separator Ident "," ;
|
