From 1d04feebec1abfc9daa0e7b42e56ebce0854035c Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Tue, 13 May 2025 15:44:17 -0400
Subject: [PATCH] Add missing case for lambdas

---
 nbe-test.rkt | 5 +++++
 nbe.rkt      | 8 +++++---
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/nbe-test.rkt b/nbe-test.rkt
index 300a90b..25c5b04 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -98,4 +98,9 @@
 (check βη-eq? (tm-padd (tm-pnat 10000) (tm-pnat 2000)) (tm-pnat 12000))
 (check βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 0)))
 (check βη-eq? `(Π (U 0) (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π (U 0) (Π (var 0) (var 1))))
+(check-false (βη-eq? '(succ zero) '(var 0)))
+(check βη-eq? (tm-app (tm-var 0) (tm-var 1)) (tm-app (tm-var 0) (tm-var 1)))
+(check βη-eq? (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)) (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)))
+(check-false (βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 1))))
+(check-false (βη-eq? (tm-app (tm-var 0) (tm-var 0)) (tm-ind (tm-var 0) 'zero 'zero)))
 (check-false (βη-eq? '(U 0) '(var 0)))
diff --git a/nbe.rkt b/nbe.rkt
index 85f0adc..b083ddb 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -91,7 +91,7 @@
     [`((fun ,f) (neu ,u)) (compare (add1 n) (open-dom n f) `(neu (app ,u (neu (idx ,n)))))]
     [`((neu ,_) (fun ,_)) (compare n a1 a0)]
     [`((neu ,a) (neu ,b)) (compare-neu n a b)]
-    [(list _ _) #f]))
+    [_ #f]))
 
 (: compare-neu (-> V D-ne D-ne Boolean))
 (define (compare-neu n a0 a1)
@@ -100,7 +100,8 @@
     [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (compare-neu n u0 u1) (compare n v0 v1))]
     [`((ind ,a0 ,b0 ,c0) (ind ,a1 ,b1 ,c1)) (and (compare-neu n a0 a1)
                                                  (compare n b0 b1)
-                                                 (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))]))
+                                                 (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))]
+    [_ #f]))
 
 (: reify (-> V D Term))
 (define (reify n a)
@@ -195,7 +196,8 @@
 
 (: βη-eq? (-> Term Term Boolean))
 (define (βη-eq? a b)
-  (η-eq? (normalize a) (normalize b)))
+  (let ([n (max (scope a) (scope b))])
+    (compare n (interp a (λ (x) (delay (idsub n x)))) (interp b (λ (x) (delay (idsub n x)))))))
 
 (: β-eq? (-> Term Term Boolean))
 (define (β-eq? a b)