Finish adding natural numbers

nbe-test.rkt

@@ -39,6 +39,14 @@
   (tm-abs (tm-abs
            (tm-app b (tm-var 1) (tm-app a (tm-var 1) (tm-var 0))))))
 
+(: tm-ind (-> Term Term Term Term))
+(define (tm-ind a b c)
+  `(ind ,a ,b ,c))
+
+(: tm-padd (-> Term Term Term))
+(define (tm-padd a b)
+  (tm-app (tm-ind a tm-id (tm-abs (tm-psuc (tm-app (tm-var 1) (tm-var 0))))) b))
+
 (: tm-compose (-> Term Term Term))
 (define (tm-compose a b)
   (tm-abs (tm-app a (tm-app b (tm-var 0)))))
@@ -70,19 +78,9 @@
       `(succ ,(tm-pnat (- n 1)))
       'zero))
 
-;; (define (tm-ifz a b c)
-;;   `(if-zero ,a ,b ,c))
-
-;; (define (tm-psuc a)
-;;   `(succ ,a))
-
-;; (define (tm-double m)
-;;   (tm-app tm-fix
-;;           (tm-abs (tm-abs (tm-ifz (tm-var 0) 'zero 'zero))) m ))
-
-;; (define (tm-padd m n)
-;;   (tm-app tm-fix
-;;           (tm-abs (tm-abs (tm-abs (tm-ifz (tm-var 1) (tm-var 0) (tm-psuc (tm-app (tm-var 3) (tm-var 0) (tm-var 1))))))) m n))
+(: tm-psuc (-> Term Term))
+(define (tm-psuc a)
+  `(succ ,a))
 
 (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst)
@@ -91,10 +89,7 @@
 (check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
 (check-equal? (normalize (tm-app tm-const (tm-nat 0) tm-loop)) (normalize (tm-nat 0)))
 (check-equal? (normalize (tm-app tm-nat-to-pnat (tm-nat 10))) (tm-pnat 10))
-;; (check-equal? (normalize (tm-mult (tm-nat 3) (tm-nat 2))) (normalize (tm-nat 6)))
-;; (check-equal? (normalize (tm-mult (tm-nat 11) (tm-nat 116))) (normalize (tm-nat 1276)))
-;; (check η-eq? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
-;; (check βη-eq? (tm-mult (tm-nat 6) (tm-nat 7)) (tm-nat 42))
-;; (check βη-eq? '(if-zero (succ (succ zero)) zero (succ (succ (var 0)))) (tm-pnat 3))
-;; (check βη-eq? (tm-padd (tm-pnat 8) (tm-pnat 11)) (tm-pnat 19))
-;; (check βη-eq? (tm-padd (tm-pnat 2) (tm-psuc (tm-var 0))) '(succ (succ (succ (var 0)))))
+(check-equal? (normalize `(ind ,(tm-pnat 3) ,(tm-pnat 0) (var 1))) (tm-pnat 2))
+(check-equal? (normalize `(ind ,(tm-pnat 3) ,tm-loop (var 1))) (tm-pnat 2))
+(check-equal? (normalize (tm-padd (tm-pnat 10000) (tm-pnat 2000)))
+              (tm-pnat 12000))

nbe.rkt

@@ -14,12 +14,11 @@
 (define-type D (∪ 'zero
                   (List 'succ (Promise D))
                   (List 'fun (-> (Promise D) D))
-                  (List 'fun2 (-> (Promise D) (Promise D) D))
-                  (List 'neu D-ne)
-                  ;; (List 'ind (-> (Promise D) (Promise D) D))
-                  ))
+                  (List 'neu D-ne)))
 
-(define-type D-ne (∪ (List 'app D-ne D) (List 'idx V)))
+(define-type D-ne (∪ (List 'app D-ne D)
+                     (List 'idx V)
+                     (List 'ind D-ne D (-> (Promise D) (Promise D) D))))
 
 (: ext (-> denv (Promise D) denv))
 (define (ext ρ a)
@@ -28,19 +27,30 @@
         a
         (ρ (- i 1)))))
 
-(define-syntax-rule (ap a b)
-  (match a
-    [`(fun ,f) (f (delay b))]
-    [`(neu ,u) `(neu (app ,u ,b))]))
+
 
 (: interp-fun (-> Term denv D))
 (define (interp-fun a ρ)
   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
-(: interp-ind (-> D (Promise D) (Promise D) denv D))
-(define (interp-ind a b c ρ)
+(: interp-fun2 (-> Term denv (-> (Promise D) (Promise D) D)))
+(define (interp-fun2 a ρ)
+  (λ (x y) (interp a (ext (ext ρ x) y))))
+
+(: interp-ind (-> D (Promise D) (-> (Promise D) (Promise D) D) D))
+(define (interp-ind a b c)
   (match a
-    [_ (error "unimplemented")]))
+    [`(neu ,u) `(neu (ind ,u ,(force b) ,c))]
+    ['zero (force b)]
+    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]))
+
+(: ap (-> D Term denv D))
+(define (ap a b ρ)
+  (match a
+    ['zero (error "type-error: ap zero")]
+    [`(succ ,_) (error "type-error: ap succ")]
+    [`(fun ,f) (f (delay (interp b ρ)))]
+    [`(neu ,u) `(neu (app ,u ,(interp b ρ)))]))
 
 (: interp (-> Term denv D))
 (define (interp a ρ)
@@ -51,25 +61,9 @@
     [`(ind ,a ,b ,c) (interp-ind
                       (interp a ρ)
                       (delay (interp b ρ))
-                      (delay (interp c ρ)) ρ)]
+                      (interp-fun2 c ρ))]
     [`(λ ,a) (interp-fun a ρ)]
-    [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
-
-;; Domain
-;; D := neu D_ne | fun [(var -> var) -> D → D]
-;; D_ne := var i | app D_ne D
-
-
-;; (: interp (-> Term (-> Term)))
-
-;; (define (interp a ρ)
-;;   (delay (match a
-;;     [`(var ,i) (force (ρ i))]
-;;     ['zero 'zero]
-;;     [`(succ ,a) `(succ ,(interp a ρ))]
-;;     [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
-;;     [`(λ ,a) (interp-fun a ρ)]
-;;     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])))
+    [`(app ,a ,b) (ap (interp a ρ) b ρ)]))
 
 (: reify (-> V D Term))
 (define (reify n a)
@@ -79,15 +73,15 @@
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
     [`(neu ,a) (reify-neu n a)]))
 
-;; (define (extract-body a)
-;;   (match a
-;;     [`(λ ,a) a]
-;;     [_ (error "reify-neu: not reifiable")]))
-
 (: reify-neu (-> V D-ne Term))
 (define (reify-neu n a)
   (match a
-    ;; [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+    [`(ind ,a ,b ,c) (list 'ind
+                           (reify-neu n a)
+                           (reify n b)
+                           (reify (+ n 2)
+                                  (c (delay `(neu (idx ,n)))
+                                     (delay `(neu (idx ,(+ 1 n)))))))]
     [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
     [`(idx ,i) (list 'var (max 0 (- n (+ i 1))))]))
 
@@ -99,7 +93,7 @@
   (match a
     ['zero 0]
     [`(succ ,a) (scope a)]
-    (`(ind ,a ,b ,c) (max (scope a) (scope b) (scope c)))
+    (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
     [`(λ ,a) (max 0 (- (scope a) 1))]
     [`(app ,a ,b) (max (scope a) (scope b))]