File tree 1 file changed +8
-0
lines changed 1 file changed +8
-0
lines changed Original file line number Diff line number Diff line change @@ -366,6 +366,7 @@ if (typeof LambdaJS == 'undefined') var LambdaJS = {};
366
366
var self = new Strategy . Base ( ) ;
367
367
self . name = 'manual' ;
368
368
self . markAbs = function ( abs , allowEta ) {
369
+ abs . redex = false ;
369
370
abs . body = self . _mark ( abs . body , allowEta ) ;
370
371
if ( allowEta && abs . isEtaRedex ( ) ) {
371
372
self . marked = true ;
@@ -375,6 +376,7 @@ if (typeof LambdaJS == 'undefined') var LambdaJS = {};
375
376
return abs ;
376
377
} ;
377
378
self . markApp = function ( app , allowEta ) {
379
+ app . redex = false ;
378
380
if ( app . fun . type == 'Abs' ) {
379
381
self . marked = true ;
380
382
app . redex = true ;
@@ -383,6 +385,12 @@ if (typeof LambdaJS == 'undefined') var LambdaJS = {};
383
385
app . arg = self . _mark ( app . arg , allowEta ) ;
384
386
return app ;
385
387
} ;
388
+ var reduceMarked = self . reduceMarked ;
389
+ self . reduceMarked = function ( exp ) {
390
+ var r = reduceMarked . call ( self , exp ) ;
391
+ self . mark ( exp ) ;
392
+ return r ;
393
+ } ;
386
394
return self ;
387
395
}
388
396
} ;
You can’t perform that action at this time.
0 commit comments