1
1
use failure:: Error ;
2
+ use symbol:: Symbol ;
2
3
3
4
use ast:: { Decl , Expr , Literal , Op , PrintStyle } ;
4
- use eval:: util:: { apply, beta_number, reducible} ;
5
+ use eval:: util:: { apply, arg_normal_enough , beta_number, reducible} ;
5
6
use eval:: Evaluator ;
6
7
7
8
/// Call-by-name evaluation.
@@ -60,15 +61,24 @@ fn step<Aux: Clone>(expr: Expr<Aux>, decls: &[Decl<Aux>]) -> Result<Expr<Aux>, E
60
61
Expr :: Op ( Op :: App , l, r, aux) => match beta {
61
62
Some ( n) if n > 0 => Expr :: Op ( Op :: App , l, r, aux) ,
62
63
Some ( 0 ) => {
63
- debug ! ( "rip strictness analysis" ) ;
64
64
let mut args = vec ! [ * r] ;
65
65
let mut func = * l;
66
- while let Expr :: Op ( Op :: App , f, a, _) = func {
66
+ let mut r_types = vec ! [ aux] ;
67
+ while let Expr :: Op ( Op :: App , f, a, ty) = func {
67
68
args. push ( * a) ;
68
69
func = * f;
70
+ r_types. push ( ty) ;
69
71
}
70
72
args. reverse ( ) ;
71
- apply ( func, args, decls) ?
73
+ let func_name = match func {
74
+ Expr :: Variable ( var, _) => var,
75
+ func => panic ! ( "Invalid callable expression: {}" , func) ,
76
+ } ;
77
+ if let Some ( n) = check_arg_normalization ( func_name, & args, decls) {
78
+ normalize_arg ( n, func, args, r_types, decls) ?
79
+ } else {
80
+ apply ( func_name, args, decls) ?
81
+ }
72
82
}
73
83
_ => Expr :: Op ( Op :: App , Box :: new ( step ( * l, decls) ?) , r, aux) ,
74
84
} ,
@@ -97,6 +107,19 @@ fn step<Aux: Clone>(expr: Expr<Aux>, decls: &[Decl<Aux>]) -> Result<Expr<Aux>, E
97
107
Ok ( expr)
98
108
}
99
109
110
+ fn check_arg_normalization < Aux : Clone > (
111
+ func : Symbol ,
112
+ args : & [ Expr < Aux > ] ,
113
+ decls : & [ Decl < Aux > ] ,
114
+ ) -> Option < usize > {
115
+ for ( i, a) in args. iter ( ) . enumerate ( ) {
116
+ if !arg_normal_enough ( a, i, func, decls) {
117
+ return Some ( i) ;
118
+ }
119
+ }
120
+ None
121
+ }
122
+
100
123
fn math_op < Aux : Clone , F : Fn ( usize , usize ) -> Result < usize , Error > > (
101
124
op : Op ,
102
125
l : Box < Expr < Aux > > ,
@@ -116,30 +139,52 @@ fn math_op<Aux: Clone, F: Fn(usize, usize) -> Result<usize, Error>>(
116
139
}
117
140
}
118
141
142
+ fn normalize_arg < Aux : Clone > (
143
+ n : usize ,
144
+ func : Expr < Aux > ,
145
+ mut args : Vec < Expr < Aux > > ,
146
+ mut r_types : Vec < Aux > ,
147
+ decls : & [ Decl < Aux > ] ,
148
+ ) -> Result < Expr < Aux > , Error > {
149
+ assert_eq ! ( args. len( ) , r_types. len( ) ) ;
150
+ args. reverse ( ) ;
151
+ let mut out = func;
152
+ let mut i = 0 ;
153
+ while let Some ( arg) = args. pop ( ) {
154
+ let arg = if i == n { step ( arg, decls) ? } else { arg } ;
155
+ i += 1 ;
156
+ out = Expr :: Op (
157
+ Op :: App ,
158
+ Box :: new ( out) ,
159
+ Box :: new ( arg) ,
160
+ r_types. pop ( ) . unwrap ( ) ,
161
+ ) ;
162
+ }
163
+ assert_eq ! ( n, 0 ) ;
164
+ Ok ( out)
165
+ }
166
+
119
167
#[ cfg( test) ]
120
168
mod tests {
121
169
use super :: * ;
122
- use ast:: { Pattern , Type } ;
170
+ use ast:: Pattern ;
123
171
124
172
#[ test]
125
173
fn app ( ) {
126
174
let mut evaluator = CallByName :: new ( vec ! [
127
175
Decl {
128
176
name: "f" . into( ) ,
129
177
args: vec![
130
- Pattern :: Binding ( "x" . into( ) , Type :: Int ) ,
131
- Pattern :: Binding ( "y" . into( ) , Type :: Int ) ,
178
+ Pattern :: Binding ( "x" . into( ) , ( ) ) ,
179
+ Pattern :: Binding ( "y" . into( ) , ( ) ) ,
132
180
] ,
133
181
body: Expr :: Op (
134
182
Op :: Add ,
135
- Box :: new( Expr :: Variable ( "x" . into( ) , Type :: Int ) ) ,
136
- Box :: new( Expr :: Variable ( "y" . into( ) , Type :: Int ) ) ,
137
- Type :: Int ,
138
- ) ,
139
- aux: Type :: Func (
140
- Box :: new( Type :: Int ) ,
141
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
183
+ Box :: new( Expr :: Variable ( "x" . into( ) , ( ) ) ) ,
184
+ Box :: new( Expr :: Variable ( "y" . into( ) , ( ) ) ) ,
185
+ ( ) ,
142
186
) ,
187
+ aux: ( ) ,
143
188
} ,
144
189
Decl {
145
190
name: "" . into( ) ,
@@ -148,30 +193,24 @@ mod tests {
148
193
Op :: App ,
149
194
Box :: new( Expr :: Op (
150
195
Op :: App ,
151
- Box :: new( Expr :: Variable (
152
- "f" . into( ) ,
153
- Type :: Func (
154
- Box :: new( Type :: Int ) ,
155
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
156
- ) ,
157
- ) ) ,
196
+ Box :: new( Expr :: Variable ( "f" . into( ) , ( ) ) ) ,
158
197
Box :: new( Expr :: Op (
159
198
Op :: Add ,
160
- Box :: new( Expr :: Literal ( Literal :: Int ( 1 ) , Type :: Int ) ) ,
161
- Box :: new( Expr :: Literal ( Literal :: Int ( 2 ) , Type :: Int ) ) ,
162
- Type :: Int ,
199
+ Box :: new( Expr :: Literal ( Literal :: Int ( 1 ) , ( ) ) ) ,
200
+ Box :: new( Expr :: Literal ( Literal :: Int ( 2 ) , ( ) ) ) ,
201
+ ( ) ,
163
202
) ) ,
164
- Type :: Int ,
203
+ ( ) ,
165
204
) ) ,
166
205
Box :: new( Expr :: Op (
167
206
Op :: Add ,
168
- Box :: new( Expr :: Literal ( Literal :: Int ( 3 ) , Type :: Int ) ) ,
169
- Box :: new( Expr :: Literal ( Literal :: Int ( 4 ) , Type :: Int ) ) ,
170
- Type :: Int ,
207
+ Box :: new( Expr :: Literal ( Literal :: Int ( 3 ) , ( ) ) ) ,
208
+ Box :: new( Expr :: Literal ( Literal :: Int ( 4 ) , ( ) ) ) ,
209
+ ( ) ,
171
210
) ) ,
172
- Type :: Int ,
211
+ ( ) ,
173
212
) ,
174
- aux: Type :: Int ,
213
+ aux: ( ) ,
175
214
} ,
176
215
] ) ;
177
216
@@ -205,68 +244,50 @@ mod tests {
205
244
Decl {
206
245
name: "f" . into( ) ,
207
246
args: vec![
208
- Pattern :: Literal ( Literal :: Nil , Type :: List ( Box :: new ( Type :: Int ) ) ) ,
209
- Pattern :: Binding ( "y" . into( ) , Type :: Int ) ,
247
+ Pattern :: Literal ( Literal :: Nil , ( ) ) ,
248
+ Pattern :: Binding ( "y" . into( ) , ( ) ) ,
210
249
] ,
211
- body: Expr :: Variable ( "y" . into( ) , Type :: Int ) ,
212
- aux: Type :: Func (
213
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
214
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
215
- ) ,
250
+ body: Expr :: Variable ( "y" . into( ) , ( ) ) ,
251
+ aux: ( ) ,
216
252
} ,
217
253
Decl {
218
254
name: "f" . into( ) ,
219
255
args: vec![
220
256
Pattern :: Cons (
221
- Box :: new( Pattern :: Binding ( "h" . into( ) , Type :: Int ) ) ,
222
- Box :: new( Pattern :: Binding ( "t" . into( ) , Type :: Int ) ) ,
223
- Type :: List ( Box :: new ( Type :: Int ) ) ,
257
+ Box :: new( Pattern :: Binding ( "h" . into( ) , ( ) ) ) ,
258
+ Box :: new( Pattern :: Binding ( "t" . into( ) , ( ) ) ) ,
259
+ ( ) ,
224
260
) ,
225
- Pattern :: Binding ( "y" . into( ) , Type :: Int ) ,
261
+ Pattern :: Binding ( "y" . into( ) , ( ) ) ,
226
262
] ,
227
263
body: Expr :: Op (
228
264
Op :: Add ,
229
- Box :: new( Expr :: Variable ( "h" . into( ) , Type :: Int ) ) ,
265
+ Box :: new( Expr :: Variable ( "h" . into( ) , ( ) ) ) ,
230
266
Box :: new( Expr :: Op (
231
267
Op :: App ,
232
268
Box :: new( Expr :: Op (
233
269
Op :: App ,
234
- Box :: new( Expr :: Variable (
235
- "f" . into( ) ,
236
- Type :: Func (
237
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
238
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
239
- ) ,
240
- ) ) ,
241
- Box :: new( Expr :: Variable ( "t" . into( ) , Type :: Int ) ) ,
242
- Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ,
270
+ Box :: new( Expr :: Variable ( "f" . into( ) , ( ) ) ) ,
271
+ Box :: new( Expr :: Variable ( "t" . into( ) , ( ) ) ) ,
272
+ ( ) ,
243
273
) ) ,
244
- Box :: new( Expr :: Variable ( "y" . into( ) , Type :: Int ) ) ,
245
- Type :: Int ,
274
+ Box :: new( Expr :: Variable ( "y" . into( ) , ( ) ) ) ,
275
+ ( ) ,
246
276
) ) ,
247
- Type :: Func (
248
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
249
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
250
- ) ,
251
- ) ,
252
- aux: Type :: Func (
253
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
254
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
277
+ ( ) ,
255
278
) ,
279
+ aux: ( ) ,
256
280
} ,
257
281
Decl {
258
282
name: "g" . into( ) ,
259
- args: vec![ Pattern :: Binding ( "x" . into( ) , Type :: Int ) ] ,
283
+ args: vec![ Pattern :: Binding ( "x" . into( ) , ( ) ) ] ,
260
284
body: Expr :: Op (
261
285
Op :: Cons ,
262
- Box :: new( Expr :: Variable ( "x" . into( ) , Type :: Int ) ) ,
263
- Box :: new( Expr :: Literal ( Literal :: Nil , Type :: List ( Box :: new( Type :: Int ) ) ) ) ,
264
- Type :: List ( Box :: new( Type :: Int ) ) ,
265
- ) ,
266
- aux: Type :: Func (
267
- Box :: new( Type :: Int ) ,
268
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
286
+ Box :: new( Expr :: Variable ( "x" . into( ) , ( ) ) ) ,
287
+ Box :: new( Expr :: Literal ( Literal :: Nil , ( ) ) ) ,
288
+ ( ) ,
269
289
) ,
290
+ aux: ( ) ,
270
291
} ,
271
292
Decl {
272
293
name: "" . into( ) ,
@@ -275,41 +296,29 @@ mod tests {
275
296
Op :: App ,
276
297
Box :: new( Expr :: Op (
277
298
Op :: App ,
278
- Box :: new( Expr :: Variable (
279
- "f" . into( ) ,
280
- Type :: Func (
281
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
282
- Box :: new( Type :: Func ( Box :: new( Type :: Int ) , Box :: new( Type :: Int ) ) ) ,
283
- ) ,
284
- ) ) ,
299
+ Box :: new( Expr :: Variable ( "f" . into( ) , ( ) ) ) ,
285
300
Box :: new( Expr :: Op (
286
301
Op :: App ,
287
- Box :: new( Expr :: Variable (
288
- "g" . into( ) ,
289
- Type :: Func (
290
- Box :: new( Type :: Int ) ,
291
- Box :: new( Type :: List ( Box :: new( Type :: Int ) ) ) ,
292
- ) ,
293
- ) ) ,
302
+ Box :: new( Expr :: Variable ( "g" . into( ) , ( ) ) ) ,
294
303
Box :: new( Expr :: Op (
295
304
Op :: Add ,
296
- Box :: new( Expr :: Literal ( Literal :: Int ( 1 ) , Type :: Int ) ) ,
297
- Box :: new( Expr :: Literal ( Literal :: Int ( 2 ) , Type :: Int ) ) ,
298
- Type :: Int ,
305
+ Box :: new( Expr :: Literal ( Literal :: Int ( 1 ) , ( ) ) ) ,
306
+ Box :: new( Expr :: Literal ( Literal :: Int ( 2 ) , ( ) ) ) ,
307
+ ( ) ,
299
308
) ) ,
300
- Type :: List ( Box :: new ( Type :: Int ) ) ,
309
+ ( ) ,
301
310
) ) ,
302
- Type :: Func ( Box :: new ( Type :: Int ) , Box :: new ( Type :: Int ) ) ,
311
+ ( ) ,
303
312
) ) ,
304
313
Box :: new( Expr :: Op (
305
314
Op :: Add ,
306
- Box :: new( Expr :: Literal ( Literal :: Int ( 3 ) , Type :: Int ) ) ,
307
- Box :: new( Expr :: Literal ( Literal :: Int ( 4 ) , Type :: Int ) ) ,
308
- Type :: Int ,
315
+ Box :: new( Expr :: Literal ( Literal :: Int ( 3 ) , ( ) ) ) ,
316
+ Box :: new( Expr :: Literal ( Literal :: Int ( 4 ) , ( ) ) ) ,
317
+ ( ) ,
309
318
) ) ,
310
- Type :: Int ,
319
+ ( ) ,
311
320
) ,
312
- aux: Type :: Int ,
321
+ aux: ( ) ,
313
322
} ,
314
323
] ) ;
315
324
@@ -335,7 +344,10 @@ mod tests {
335
344
assert ! ( !evaluator. normal_form( ) ) ;
336
345
337
346
assert ! ( evaluator. step( ) . is_ok( ) ) ;
338
- assert_eq ! ( format!( "{}" , evaluator) , "Add(Add(1, 2), Add(3, 4))" ) ;
347
+ assert_eq ! (
348
+ format!( "{}" , evaluator) ,
349
+ "Add(3, App(App(f, []), Add(3, 4)))"
350
+ ) ;
339
351
assert ! ( !evaluator. normal_form( ) ) ;
340
352
341
353
assert ! ( evaluator. step( ) . is_ok( ) ) ;
0 commit comments