1
1
//! Type and kind-checking for our DDL
2
2
3
+ use std:: rc:: Rc ;
4
+
3
5
use syntax:: { binary, host} ;
4
6
use syntax:: { Name , Named , Program , Var } ;
5
7
use syntax:: context:: { Binding , Context } ;
@@ -19,28 +21,28 @@ pub enum ExpectedType<N> {
19
21
#[ derive( Debug , Clone , PartialEq , Eq ) ]
20
22
pub enum TypeError < N > {
21
23
/// A variable of the requested name was not bound in this scope
22
- UnboundVariable { expr : host:: BoxExpr < N > , name : N } ,
24
+ UnboundVariable { expr : host:: RcExpr < N > , name : N } ,
23
25
/// Variable bound in the context was not at the value level
24
26
ExprBindingExpected {
25
- expr : host:: BoxExpr < N > ,
27
+ expr : host:: RcExpr < N > ,
26
28
found : Named < N , Binding < N > > ,
27
29
} ,
28
30
/// One type was expected, but another was found
29
31
Mismatch {
30
- expr : host:: BoxExpr < N > ,
31
- found : host:: BoxType < N > ,
32
+ expr : host:: RcExpr < N > ,
33
+ found : host:: RcType < N > ,
32
34
expected : ExpectedType < N > ,
33
35
} ,
34
36
/// Unexpected operand types in a equality comparison
35
37
EqualityOperands {
36
- expr : host:: BoxExpr < N > ,
37
- lhs_ty : host:: BoxType < N > ,
38
- rhs_ty : host:: BoxType < N > ,
38
+ expr : host:: RcExpr < N > ,
39
+ lhs_ty : host:: RcType < N > ,
40
+ rhs_ty : host:: RcType < N > ,
39
41
} ,
40
42
/// A field was missing when projecting on a record
41
43
MissingField {
42
- struct_expr : host:: BoxExpr < N > ,
43
- struct_ty : host:: BoxType < N > ,
44
+ struct_expr : host:: RcExpr < N > ,
45
+ struct_ty : host:: RcType < N > ,
44
46
field_name : N ,
45
47
} ,
46
48
}
@@ -49,13 +51,13 @@ pub enum TypeError<N> {
49
51
/// in the environment
50
52
pub fn ty_of < N : Name > (
51
53
ctx : & Context < N > ,
52
- expr : & host:: BoxExpr < N > ,
53
- ) -> Result < host:: BoxType < N > , TypeError < N > > {
54
+ expr : & host:: RcExpr < N > ,
55
+ ) -> Result < host:: RcType < N > , TypeError < N > > {
54
56
use syntax:: host:: { Binop , Expr , Type , TypeConst , Unop } ;
55
57
56
58
match * * expr {
57
59
// Constants are easy!
58
- Expr :: Const ( _, c) => Ok ( Box :: new ( Type :: Const ( c. ty_const_of ( ) ) ) ) ,
60
+ Expr :: Const ( _, c) => Ok ( Rc :: new ( Type :: Const ( c. ty_const_of ( ) ) ) ) ,
59
61
60
62
// Variables
61
63
Expr :: Var ( _, Var :: Free ( ref name) ) => Err ( TypeError :: UnboundVariable {
@@ -77,11 +79,11 @@ pub fn ty_of<N: Name>(
77
79
Expr :: Unop ( _, op, ref expr) => match op {
78
80
Unop :: Neg => {
79
81
expect_ty ( ctx, expr, Type :: int ( ) ) ?;
80
- Ok ( Box :: new ( Type :: int ( ) ) )
82
+ Ok ( Rc :: new ( Type :: int ( ) ) )
81
83
}
82
84
Unop :: Not => {
83
85
expect_ty ( ctx, expr, Type :: bool ( ) ) ?;
84
- Ok ( Box :: new ( Type :: bool ( ) ) )
86
+ Ok ( Rc :: new ( Type :: bool ( ) ) )
85
87
}
86
88
} ,
87
89
@@ -93,24 +95,24 @@ pub fn ty_of<N: Name>(
93
95
expect_ty ( ctx, lhs_expr, Type :: bool ( ) ) ?;
94
96
expect_ty ( ctx, rhs_expr, Type :: bool ( ) ) ?;
95
97
96
- Ok ( Box :: new ( Type :: bool ( ) ) )
98
+ Ok ( Rc :: new ( Type :: bool ( ) ) )
97
99
}
98
100
99
101
// Equality operators
100
102
Binop :: Eq | Binop :: Ne => {
101
103
let lhs_ty = ty_of ( ctx, lhs_expr) ?;
102
104
let rhs_ty = ty_of ( ctx, rhs_expr) ?;
103
105
104
- match ( * lhs_ty, * rhs_ty) {
105
- ( Type :: Const ( TypeConst :: Bit ) , Type :: Const ( TypeConst :: Bit ) ) |
106
- ( Type :: Const ( TypeConst :: Bool ) , Type :: Const ( TypeConst :: Bool ) ) |
107
- ( Type :: Const ( TypeConst :: Int ) , Type :: Const ( TypeConst :: Int ) ) => {
108
- Ok ( Box :: new ( Type :: bool ( ) ) )
106
+ match ( & * lhs_ty, & * rhs_ty) {
107
+ ( & Type :: Const ( TypeConst :: Bit ) , & Type :: Const ( TypeConst :: Bit ) ) |
108
+ ( & Type :: Const ( TypeConst :: Bool ) , & Type :: Const ( TypeConst :: Bool ) ) |
109
+ ( & Type :: Const ( TypeConst :: Int ) , & Type :: Const ( TypeConst :: Int ) ) => {
110
+ Ok ( Rc :: new ( Type :: bool ( ) ) )
109
111
}
110
112
( lhs_ty, rhs_ty) => Err ( TypeError :: EqualityOperands {
111
113
expr : expr. clone ( ) ,
112
- lhs_ty : Box :: new ( lhs_ty) ,
113
- rhs_ty : Box :: new ( rhs_ty) ,
114
+ lhs_ty : Rc :: new ( lhs_ty. clone ( ) ) ,
115
+ rhs_ty : Rc :: new ( rhs_ty. clone ( ) ) ,
114
116
} ) ,
115
117
}
116
118
}
@@ -120,15 +122,15 @@ pub fn ty_of<N: Name>(
120
122
expect_ty ( ctx, lhs_expr, Type :: int ( ) ) ?;
121
123
expect_ty ( ctx, rhs_expr, Type :: int ( ) ) ?;
122
124
123
- Ok ( Box :: new ( Type :: bool ( ) ) )
125
+ Ok ( Rc :: new ( Type :: bool ( ) ) )
124
126
}
125
127
126
128
// Arithmetic operators
127
129
Binop :: Add | Binop :: Sub | Binop :: Mul | Binop :: Div => {
128
130
expect_ty ( ctx, lhs_expr, Type :: int ( ) ) ?;
129
131
expect_ty ( ctx, rhs_expr, Type :: int ( ) ) ?;
130
132
131
- Ok ( Box :: new ( Type :: int ( ) ) )
133
+ Ok ( Rc :: new ( Type :: int ( ) ) )
132
134
}
133
135
}
134
136
}
@@ -153,11 +155,11 @@ pub fn ty_of<N: Name>(
153
155
154
156
match * ty_of ( ctx, array_expr) ? {
155
157
// Check if index is in bounds?
156
- Type :: Array ( elem_ty, _) => Ok ( elem_ty) ,
157
- found => Err ( TypeError :: Mismatch {
158
+ Type :: Array ( ref elem_ty, _) => Ok ( elem_ty. clone ( ) ) ,
159
+ ref found => Err ( TypeError :: Mismatch {
158
160
expr : array_expr. clone ( ) ,
159
161
expected : ExpectedType :: Array ,
160
- found : Box :: new ( found) ,
162
+ found : Rc :: new ( found. clone ( ) ) ,
161
163
} ) ,
162
164
}
163
165
}
@@ -167,7 +169,7 @@ pub fn ty_of<N: Name>(
167
169
// FIXME: avoid cloning the environment
168
170
let mut ctx = ctx. clone ( ) ;
169
171
ctx. extend ( param_name. clone ( ) , Binding :: Expr ( param_ty. clone ( ) ) ) ;
170
- Ok ( Box :: new (
172
+ Ok ( Rc :: new (
171
173
Type :: arrow ( param_ty. clone ( ) , ty_of ( & ctx, body_expr) ?) ,
172
174
) )
173
175
}
@@ -176,13 +178,10 @@ pub fn ty_of<N: Name>(
176
178
177
179
// Kinding
178
180
179
- pub fn simplify_ty < N : Name > ( ctx : & Context < N > , ty : & binary:: BoxType < N > ) -> binary:: BoxType < N > {
181
+ pub fn simplify_ty < N : Name > ( ctx : & Context < N > , ty : & binary:: RcType < N > ) -> binary:: RcType < N > {
180
182
use syntax:: binary:: Type ;
181
183
182
- fn compute_ty < N : Name > (
183
- ctx : & Context < N > ,
184
- ty : & binary:: BoxType < N > ,
185
- ) -> Option < binary:: BoxType < N > > {
184
+ fn compute_ty < N : Name > ( ctx : & Context < N > , ty : & binary:: RcType < N > ) -> Option < binary:: RcType < N > > {
186
185
match * * ty {
187
186
Type :: Var ( _, Var :: Bound ( Named ( _, i) ) ) => match ctx. lookup_ty_def ( i) {
188
187
Ok ( Named ( _, def_ty) ) => Some ( def_ty. clone ( ) ) ,
@@ -192,7 +191,7 @@ pub fn simplify_ty<N: Name>(ctx: &Context<N>, ty: &binary::BoxType<N>) -> binary
192
191
Type :: Abs ( _, _, ref body_ty) => {
193
192
// FIXME: Avoid clone
194
193
let mut body = body_ty. clone ( ) ;
195
- body. instantiate ( arg_ty) ;
194
+ Rc :: make_mut ( & mut body) . instantiate ( arg_ty) ;
196
195
Some ( body)
197
196
}
198
197
_ => None ,
@@ -216,24 +215,24 @@ pub fn simplify_ty<N: Name>(ctx: &Context<N>, ty: &binary::BoxType<N>) -> binary
216
215
#[ derive( Debug , Clone , PartialEq , Eq ) ]
217
216
pub enum ExpectedKind {
218
217
Arrow ,
219
- Actual ( binary:: BoxKind ) ,
218
+ Actual ( binary:: RcKind ) ,
220
219
}
221
220
222
221
/// An error that was encountered during kind checking
223
222
#[ derive( Debug , Clone , PartialEq , Eq ) ]
224
223
pub enum KindError < N > {
225
224
/// A variable of the requested name was not bound in this scope
226
- UnboundVariable { ty : binary:: BoxType < N > , name : N } ,
225
+ UnboundVariable { ty : binary:: RcType < N > , name : N } ,
227
226
/// Variable bound in the context was not at the type level
228
227
TypeBindingExpected {
229
- ty : binary:: BoxType < N > ,
228
+ ty : binary:: RcType < N > ,
230
229
found : Named < N , Binding < N > > ,
231
230
} ,
232
231
/// One kind was expected, but another was found
233
232
Mismatch {
234
- ty : binary:: BoxType < N > ,
233
+ ty : binary:: RcType < N > ,
235
234
expected : ExpectedKind ,
236
- found : binary:: BoxKind ,
235
+ found : binary:: RcKind ,
237
236
} ,
238
237
/// A repr error
239
238
Repr ( binary:: ReprError < N > ) ,
@@ -257,8 +256,8 @@ impl<N> From<TypeError<N>> for KindError<N> {
257
256
/// the environment
258
257
pub fn kind_of < N : Name > (
259
258
ctx : & Context < N > ,
260
- ty : & binary:: BoxType < N > ,
261
- ) -> Result < binary:: BoxKind , KindError < N > > {
259
+ ty : & binary:: RcType < N > ,
260
+ ) -> Result < binary:: RcKind , KindError < N > > {
262
261
use syntax:: binary:: { Kind , Type , TypeConst } ;
263
262
264
263
match * * ty {
@@ -276,14 +275,14 @@ pub fn kind_of<N: Name>(
276
275
} ,
277
276
278
277
// Bit type
279
- Type :: Const ( TypeConst :: Bit ) => Ok ( Box :: new ( Kind :: Type ) ) ,
278
+ Type :: Const ( TypeConst :: Bit ) => Ok ( Rc :: new ( Kind :: Type ) ) ,
280
279
281
280
// Array types
282
281
Type :: Array ( _, ref elem_ty, ref size_expr) => {
283
282
expect_ty_kind ( ctx, elem_ty) ?;
284
283
expect_ty ( ctx, size_expr, host:: Type :: int ( ) ) ?;
285
284
286
- Ok ( Box :: new ( Kind :: Type ) )
285
+ Ok ( Rc :: new ( Kind :: Type ) )
287
286
}
288
287
289
288
// Conditional types
@@ -292,7 +291,7 @@ pub fn kind_of<N: Name>(
292
291
let pred_ty = host:: Type :: arrow ( ty. repr ( ) ?, host:: Type :: bool ( ) ) ;
293
292
expect_ty ( ctx, pred_expr, pred_ty) ?;
294
293
295
- Ok ( Box :: new ( Kind :: Type ) )
294
+ Ok ( Rc :: new ( Kind :: Type ) )
296
295
}
297
296
298
297
// Interpreted types
@@ -301,15 +300,15 @@ pub fn kind_of<N: Name>(
301
300
let conv_ty = host:: Type :: arrow ( ty. repr ( ) ?, host_ty. clone ( ) ) ;
302
301
expect_ty ( ctx, conv_expr, conv_ty) ?;
303
302
304
- Ok ( Box :: new ( Kind :: Type ) )
303
+ Ok ( Rc :: new ( Kind :: Type ) )
305
304
}
306
305
307
306
// Type abstraction
308
307
Type :: Abs ( _, Named ( ref name, ref param_kind) , ref body_ty) => {
309
308
// FIXME: avoid cloning the environment
310
309
let mut ctx = ctx. clone ( ) ;
311
310
ctx. extend ( name. clone ( ) , Binding :: Type ( param_kind. clone ( ) ) ) ;
312
- Ok ( Box :: new (
311
+ Ok ( Rc :: new (
313
312
Kind :: arrow ( param_kind. clone ( ) , kind_of ( & ctx, body_ty) ?) ,
314
313
) )
315
314
}
@@ -320,7 +319,7 @@ pub fn kind_of<N: Name>(
320
319
expect_ty_kind ( ctx, ty) ?;
321
320
}
322
321
323
- Ok ( Box :: new ( Kind :: Type ) )
322
+ Ok ( Rc :: new ( Kind :: Type ) )
324
323
}
325
324
326
325
// Struct type
@@ -335,19 +334,19 @@ pub fn kind_of<N: Name>(
335
334
ctx. extend ( field. name . clone ( ) , Binding :: Expr ( field_ty. repr ( ) ?) ) ;
336
335
}
337
336
338
- Ok ( Box :: new ( Kind :: Type ) )
337
+ Ok ( Rc :: new ( Kind :: Type ) )
339
338
}
340
339
341
340
// Type application
342
341
Type :: App ( _, ref fn_ty, ref arg_ty) => match * kind_of ( ctx, fn_ty) ? {
343
342
Kind :: Type => Err ( KindError :: Mismatch {
344
343
ty : fn_ty. clone ( ) ,
345
- found : Box :: new ( Kind :: Type ) ,
344
+ found : Rc :: new ( Kind :: Type ) ,
346
345
expected : ExpectedKind :: Arrow ,
347
346
} ) ,
348
- Kind :: Arrow ( param_kind, ret_kind) => {
349
- expect_kind ( ctx, arg_ty, param_kind) ?;
350
- Ok ( ret_kind)
347
+ Kind :: Arrow ( ref param_kind, ref ret_kind) => {
348
+ expect_kind ( ctx, arg_ty, param_kind. clone ( ) ) ?;
349
+ Ok ( ret_kind. clone ( ) )
351
350
}
352
351
} ,
353
352
}
@@ -368,9 +367,9 @@ pub fn check_program<N: Name>(program: &Program<N>) -> Result<(), KindError<N>>
368
367
369
368
fn expect_ty < N : Name > (
370
369
ctx : & Context < N > ,
371
- expr : & host:: BoxExpr < N > ,
370
+ expr : & host:: RcExpr < N > ,
372
371
expected : host:: Type < N > ,
373
- ) -> Result < host:: BoxType < N > , TypeError < N > > {
372
+ ) -> Result < host:: RcType < N > , TypeError < N > > {
374
373
let found = ty_of ( ctx, expr) ?;
375
374
376
375
if * found == expected {
@@ -386,9 +385,9 @@ fn expect_ty<N: Name>(
386
385
387
386
fn expect_kind < N : Name > (
388
387
ctx : & Context < N > ,
389
- ty : & binary:: BoxType < N > ,
390
- expected : binary:: BoxKind ,
391
- ) -> Result < binary:: BoxKind , KindError < N > > {
388
+ ty : & binary:: RcType < N > ,
389
+ expected : binary:: RcKind ,
390
+ ) -> Result < binary:: RcKind , KindError < N > > {
392
391
let found = kind_of ( ctx, ty) ?;
393
392
394
393
if found == expected {
@@ -402,6 +401,8 @@ fn expect_kind<N: Name>(
402
401
}
403
402
}
404
403
405
- fn expect_ty_kind < N : Name > ( ctx : & Context < N > , ty : & binary:: BoxType < N > ) -> Result < ( ) , KindError < N > > {
406
- expect_kind ( ctx, ty, Box :: new ( binary:: Kind :: Type ) ) . map ( |_| ( ) )
404
+ fn expect_ty_kind < N : Name > ( ctx : & Context < N > , ty : & binary:: RcType < N > ) -> Result < ( ) , KindError < N > > {
405
+ use syntax:: binary:: Kind ;
406
+
407
+ expect_kind ( ctx, ty, Rc :: new ( Kind :: Type ) ) . map ( |_| ( ) )
407
408
}
0 commit comments