attapl-deptypes.opp.exp 8.41 KB
Newer Older
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
File "attapl-deptypes.mly", line 47, characters 28-38:
Warning: the token APOSTROPHE is unused.
File "attapl-deptypes.mly", line 49, characters 28-33:
Warning: the token BARGT is unused.
File "attapl-deptypes.mly", line 50, characters 28-37:
Warning: the token BARRCURLY is unused.
File "attapl-deptypes.mly", line 51, characters 28-38:
Warning: the token BARRSQUARE is unused.
File "attapl-deptypes.mly", line 53, characters 28-38:
Warning: the token COLONCOLON is unused.
File "attapl-deptypes.mly", line 54, characters 28-35:
Warning: the token COLONEQ is unused.
File "attapl-deptypes.mly", line 55, characters 28-37:
Warning: the token COLONHASH is unused.
File "attapl-deptypes.mly", line 57, characters 28-34:
Warning: the token DARROW is unused.
File "attapl-deptypes.mly", line 59, characters 28-35:
Warning: the token DDARROW is unused.
File "attapl-deptypes.mly", line 48, characters 28-34:
Warning: the token DQUOTE is unused.
File "attapl-deptypes.mly", line 63, characters 28-32:
Warning: the token EQEQ is unused.
File "attapl-deptypes.mly", line 64, characters 28-30:
Warning: the token GT is unused.
File "attapl-deptypes.mly", line 65, characters 28-32:
Warning: the token HASH is unused.
File "attapl-deptypes.mly", line 66, characters 28-34:
Warning: the token LCURLY is unused.
File "attapl-deptypes.mly", line 67, characters 28-37:
Warning: the token LCURLYBAR is unused.
File "attapl-deptypes.mly", line 68, characters 28-37:
Warning: the token LEFTARROW is unused.
File "attapl-deptypes.mly", line 71, characters 28-35:
Warning: the token LSQUARE is unused.
File "attapl-deptypes.mly", line 72, characters 28-38:
Warning: the token LSQUAREBAR is unused.
File "attapl-deptypes.mly", line 73, characters 28-30:
Warning: the token LT is unused.
File "attapl-deptypes.mly", line 70, characters 28-34:
Warning: the token Normal is unused.
File "attapl-deptypes.mly", line 74, characters 28-34:
Warning: the token RCURLY is unused.
File "attapl-deptypes.mly", line 76, characters 28-35:
Warning: the token RSQUARE is unused.
File "attapl-deptypes.mly", line 78, characters 28-33:
Warning: the token SLASH is unused.
File "attapl-deptypes.mly", line 80, characters 28-36:
Warning: the token TRIANGLE is unused.
File "attapl-deptypes.mly", line 30, characters 28-32:
Warning: the token TYPE is unused.
File "attapl-deptypes.mly", line 82, characters 28-32:
Warning: the token VBAR is unused.
%{
open Support.Error
open Support.Pervasive
open Syntax
let rec addbinders tyT l = match l with
   [] -> tyT
 | (tyX,k)::rest -> tyT 
%}
%start toplevel
%token <Support.Error.info> ALL
63
64
65
66
67
68
69
70
71
%token <Support.Error.info> APOSTROPHE
%token <Support.Error.info> ARROW
%token <Support.Error.info> BARGT
%token <Support.Error.info> BARRCURLY
%token <Support.Error.info> BARRSQUARE
%token <Support.Error.info> COLON
%token <Support.Error.info> COLONCOLON
%token <Support.Error.info> COLONEQ
%token <Support.Error.info> COLONHASH
72
%token <Support.Error.info> COMMA
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
%token <Support.Error.info> DARROW
%token <Support.Error.info> DDARROW
%token <Support.Error.info> DOT
%token <Support.Error.info> DQUOTE
%token <Support.Error.info> EOF
%token <Support.Error.info> EQ
%token <Support.Error.info> EQEQ
%token <Support.Error.info> GT
%token <Support.Error.info> HASH
%token <Support.Error.info> IMPORT
%token <Support.Error.info> LAMBDA
%token <string Support.Error.withinfo> LCID
%token <Support.Error.info> LCURLY
%token <Support.Error.info> LCURLYBAR
%token <Support.Error.info> LEFTARROW
%token <Support.Error.info> LPAREN
%token <Support.Error.info> LSQUARE
%token <Support.Error.info> LSQUAREBAR
%token <Support.Error.info> LT
%token <Support.Error.info> NORMAL
%token <Support.Error.info> Normal
%token <Support.Error.info> ONE
%token <Support.Error.info> PI
%token <Support.Error.info> PRF
%token <Support.Error.info> PROP
%token <Support.Error.info> RCURLY
%token <Support.Error.info> RPAREN
%token <Support.Error.info> RSQUARE
%token <Support.Error.info> SEMI
%token <Support.Error.info> SIGMA
%token <Support.Error.info> SLASH
%token <Support.Error.info> STAR
%token <string Support.Error.withinfo> STRINGV
%token <Support.Error.info> TRIANGLE
%token <Support.Error.info> TWO
%token <Support.Error.info> TYPE
%token <string Support.Error.withinfo> UCID
%token <Support.Error.info> USCORE
%token <Support.Error.info> VBAR
112
%right COMMA
113
114
115
116
%type < Syntax.context -> (Syntax.command list * Syntax.context) > toplevel
%%

toplevel:
117
  _1 = EOF
118
119
120
121
122
123
    {      ( fun ctx -> [],ctx )}
| _1 = Command _2 = SEMI _3 = toplevel
    {      ( fun ctx ->
          let cmd,ctx = _1 ctx in
          let cmds,ctx = _3 ctx in
          cmd::cmds,ctx )}
124
125

Command:
126
  _1 = IMPORT _2 = STRINGV
127
128
129
130
131
132
133
134
135
    {                   ( fun ctx -> (Import(_2.v)),ctx )}
| _1 = Term
    {      ( fun ctx -> (let t = _1 ctx in Whred(tmInfo t,t)),ctx )}
| _1 = LPAREN _2 = NORMAL _3 = Term _4 = RPAREN
    {      ( fun ctx -> (let t = _3 ctx in Eval(tmInfo t,t)),ctx )}
| _1 = UCID _2 = TyBinder
    {      ( fun ctx -> ((Bind(_1.i, _1.v, _2 ctx)), addname ctx _1.v) )}
| _1 = LCID _2 = Binder
    {      ( fun ctx -> ((Bind(_1.i,_1.v,_2 ctx)), addname ctx _1.v) )}
136
137

Binder:
138
  _1 = COLON _2 = Type
139
140
141
142
143
    {      ( fun ctx -> VarBind (_2 ctx))}
| _1 = EQ _2 = Term
    {      ( fun ctx -> TmAbbBind(_2 ctx, None) )}
| _1 = EQ _2 = Term _3 = COLON _4 = Type
    {      (fun ctx -> TmAbbBind(_2 ctx, Some(_4 ctx)) )}
144
145

Kind:
146
  _1 = PI _2 = LCID _3 = COLON _4 = Type _5 = DOT _6 = Kind
147
148
149
150
    {                                  (fun ctx -> let ctx1 = addname ctx _2.v in
          KnPi(_2.v,_4 ctx,_6 ctx1))}
| _1 = ArrowKind
    {              (_1)}
151
152

ArrowKind:
153
  _1 = AppType _2 = ARROW _3 = ArrowKind
154
155
156
    {                            ( fun ctx -> KnPi("_",_1 ctx, _3 ctx) )}
| _1 = AKind
    {        (_1 )}
157
158

AKind:
159
  _1 = STAR
160
161
162
    {         ( fun ctx -> KnStar )}
| _1 = LPAREN _2 = Kind _3 = RPAREN
    {                        ( _2 )}
163
164

Type:
165
  _1 = AppType
166
167
168
    {            ( _1 )}
| _1 = AppType _2 = ARROW _3 = Type
    {                             ( fun ctx ->
169
          let ctx1 = addname ctx "_" in
170
171
172
173
174
175
176
177
178
          TyPi("_",_1 ctx,_3 ctx1) )}
| _1 = PI _2 = LCID _3 = COLON _4 = Type _5 = DOT _6 = Type
    {      ( fun ctx ->
          let ctx1 = addname ctx _2.v in
          TyPi(_2.v,_4 ctx,_6 ctx1) )}
| _1 = SIGMA _2 = LCID _3 = COLON _4 = Type _5 = DOT _6 = Type
    {      ( fun ctx ->
          let ctx1 = addname ctx _2.v in
          TySigma(_2.v,_4 ctx,_6 ctx1) )}
179
180

AppType:
181
  _1 = AppType _2 = ATerm
182
183
184
    {                  ( fun ctx -> TyApp(_1 ctx,_2 ctx) )}
| _1 = AType
    {          ( _1 )}
185
186

AType:
187
  _1 = LPAREN _2 = Type _3 = RPAREN
188
189
190
191
192
193
194
195
196
    {           ( _2 )}
| _1 = PROP
    {         (fun ctx -> TyProp)}
| _1 = PRF _2 = LPAREN _3 = Term _4 = RPAREN
    {                           (fun ctx -> TyPrf(_3 ctx))}
| _1 = UCID
    {      ( fun ctx ->
          if isnamebound ctx _1.v then
            TyVar(name2index _1.i ctx _1.v, ctxlength ctx)
197
          else 
198
            TyId(_1.v) )}
199
200

Term:
201
  _1 = AppTerm
202
203
204
205
206
207
208
209
210
211
212
    {      ( _1 )}
| _1 = LAMBDA _2 = LCID _3 = COLON _4 = Type _5 = DOT _6 = Term
    {      ( fun ctx ->
          let ctx1 = addname ctx _2.v in
          TmAbs(_1, _2.v, _4 ctx, _6 ctx1) )}
| _1 = ALL _2 = LCID _3 = COLON _4 = Type _5 = DOT _6 = Term
    {      ( fun ctx ->
          let ctx1 = addname ctx _2.v in
          TmAll(_1, _2.v, _4 ctx, _6 ctx1) )}
| _1 = LAMBDA _2 = USCORE _3 = COLON _4 = Type _5 = DOT _6 = Term
    {      ( fun ctx ->
213
          let ctx1 = addname ctx "_" in
214
          TmAbs(_1, "_", _4 ctx, _6 ctx1) )}
215
216

PathTerm:
217
  _1 = PathTerm _2 = DOT _3 = TWO
218
219
220
221
222
223
224
    {      ( fun ctx ->
          TmProj2(_2, _1 ctx) )}
| _1 = PathTerm _2 = DOT _3 = ONE
    {      ( fun ctx ->
          TmProj1(_2, _1 ctx) )}
| _1 = ATerm
    {          ( _1 )}
225
226

AppTerm:
227
  _1 = PathTerm
228
229
230
231
232
233
    {             (_1)}
| _1 = AppTerm _2 = ATerm
    {      ( fun ctx ->
          let e1 = _1 ctx in
          let e2 = _2 ctx in
          TmApp(tmInfo e1,e1,e2) )}
234
235

ATerm:
236
  _1 = LPAREN _2 = Term _3 = RPAREN
237
238
239
240
241
242
243
    {      ( _2 )}
| _1 = LPAREN _2 = Term _3 = COMMA _4 = TermList _5 = COLON _6 = Type _7 = RPAREN
    {                                                 ( fun ctx -> 
          TmList(_1,_2 ctx :: _4 ctx ,_6 ctx))}
| _1 = LCID
    {      ( fun ctx ->
          TmVar(_1.i, name2index _1.i ctx _1.v, ctxlength ctx) )}
244
245

TermList:
246
  _1 = Term
247
248
249
    {        ( fun ctx -> [_1 ctx] )}
| _1 = Term _2 = COMMA _3 = TermList
    {                       ( fun ctx -> _1 ctx :: _3 ctx)}
250
251

TyBinder:
252
  _1 = COLON _2 = Kind
253
254
255
    {      ( fun ctx -> TyVarBind(_2 ctx) )}
| _1 = EQ _2 = Type
    {      ( fun ctx -> TyAbbBind(_2 ctx, None) )}
256
257
258
259

%%


260