readbackInCtx only blaze named lambda during the lambda case

Author: xieyuheng

examples/ackermann.test.lisp.out

@@ -1 +1 @@
-(lambda (m n) (m (lambda (t f) t) (lambda (x t f) f) (lambda (base step) (step (n base step))) (if (zero? n) (ackermann (m (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (lambda (base step) (step base))) (ackermann (m (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (ackermann m (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)))))))
+(lambda (m n) (m (lambda (t f) t) (lambda (x t f) f) (lambda (base step) (step (n base step))) (n (lambda (t f) t) (lambda (x t f) f) (ackermann (m (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (lambda (base step) (step base))) (ackermann (m (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (ackermann m (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)))))))

examples/factorial.test.lisp.out

@@ -1 +1 @@
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (base step) (step base)) (n (lambda (base step) base) (lambda (n₁) (iter-Nat (factorial (iter-Nat n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) n₁ (lambda (prev base step) (step (prev base step))))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (base step) (step base)) (n (lambda (base step) base) (lambda (n₁) (factorial (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) n₁ (lambda (prev base step) (step (prev base step))))))))

examples/fibonacci.test.lisp.out

@@ -1 +1 @@
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (base step) base) (if (zero? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (base step) (step base)) (fibonacci (iter-Nat n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (fibonacci (iter-Nat (sub1 n) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (prev base step) (step (prev base step)))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (base step) base) (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (t f) t) (lambda (x t f) f) (lambda (base step) (step base)) (fibonacci (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car)) (fibonacci (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (prev base step) (step (prev base step)))))))

examples/nat-even-odd.test.lisp.out

@@ -1,4 +1,4 @@
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (if (zero? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (t f) f) (even? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (if (zero? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (t f) t) (odd? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (if (zero? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (t f) f) (direct-even? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
-(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (if (zero? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))) (lambda (t f) t) (direct-odd? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (even? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (odd? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (direct-even? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))
+(lambda (n) (n (lambda (t f) t) (lambda (x t f) f) (lambda (t f) f) (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (t f) t) (lambda (x t f) f) (lambda (t f) t) (direct-odd? (n (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car) (lambda (f) (f (lambda (base step) base) (lambda (base step) base))) (lambda (x f) (f (x (lambda (car cdr) cdr)) (lambda (base step) (step (x (lambda (car cdr) cdr) base step))))) (lambda (car cdr) car))))))

src/lang/readback/readbackInCtx.ts

@@ -52,8 +52,6 @@ export function readbackInCtx(ctx: Ctx, value: Value): Exp {
               readbackInCtx(ctx, value.target),
               readbackInCtx(ctx, value.arg),
             )
-          } else {
-            ctx = ctxBlazeTrail(ctx, head)
           }
         }
       }