debruijnize converts functions to curry form

5 files changed, 79 insertions, 206 deletions

diff --git a/multisyntax/examples/untyped-lambda-calculus-prelude.scm b/multisyntax/examples/untyped-lambda-calculus-prelude.scm
index 95952f4..db67896 100644
--- a/multisyntax/examples/untyped-lambda-calculus-prelude.scm
+++ b/multisyntax/examples/untyped-lambda-calculus-prelude.scm
@@ -22,25 +22,13 @@
     ((∘ f g ...)
      (f (∘ g ...)))))
 
-(splicing-let-syntax ((define-syntax* define-syntax))
-  (define-syntax* define-syntax
-    (syntax-rules (let-syntax letrec-syntax)
-      ((_ name (let-syntax bindings body))
-       (splicing-let-syntax bindings
-         (define-syntax name body)))
-      ((_ name (letrec-syntax bindings body))
-       (splicing-letrec-syntax bindings
-         (define-syntax name body)))
-      ((_ name body)
-       (define-syntax* name body)))))
-
 (define-syntax ∘←
   ;; postfix function composition
-  (let-syntax ((R (syntax-rules ()
-                    ((R () (acc ...))
-                     (∘ acc ...))
-                    ((R (head rest ...) (acc ...))
-                     (R (rest ...) (acc ...))))))
+  (letrec-syntax ((R (syntax-rules ()
+                       ((R () (acc ...))
+                        (∘ acc ...))
+                       ((R (head rest ...) (acc ...))
+                        (R (rest ...) (acc ...))))))
     (syntax-rules ()
       ((∘← f ...) (R (f ...) ())))))
 
@@ -77,10 +65,11 @@
 
 (define-syntax let* let)
 
-(define (Y f)
+(define Y
   ;; Y combinator.
-  (let ((recursor (λ (x) (f (x x)))))
-    (recursor recursor)))
+  (lambda (f)
+    (let ((recursor (λ (x) (f (x x)))))
+      (recursor recursor))))
 
 (define-syntax rec
   ;; Define a recursive function.
@@ -100,13 +89,6 @@
        ((υ (name param ...) body ...)
         first-binding ...)))))
 
-(define-syntax letrec
-  (syntax-rules ()
-    ((letrec ((name value) ...) body ...)
-     (let ((name (λ (name ...) value)) ...)
-       (let ((name (name name ...)) ...)
-         body ...)))))
-
 (splicing-let-syntax ((%define define))
   (define-syntax define
     (syntax-rules ()
@@ -132,180 +114,58 @@
       (define d-name (let ((name value) ...) d-value ...))
       ...))))
 
-;;; Boolean logic. `#t` maps to this definition of true, and `#f` maps to
-;;; this definition of false.
-(define (true x y) x)
-(define (false x y) y)
-(define (not x) (x false true))
+;;; ;;;;;;;;;;;;
+;;; untyped operations
 
-(define (binary-and x y) (x y false))
-(binary-to-arbitrary and binary-and)
+(define (%cons car cdr)
+  (λ selector (selector car cdr)))
 
-(define (binary-or x y) (x true y))
-(binary-to-arbitrary or binary-or)
+(define (%car pair)
+  (pair (λ (x y) x)))
+(define (%cdr pair)
+  (pair (λ (x y) y)))
 
-(define (if predicate truthy falsy)
-  (predicate truthy falsy))
+(define %true (λ (x y) x))
+(define %false (λ (x y) y))
+(define (%and x y) (x y x))
 
-(define-syntax cond
-  ;; Simplified cond.
-  (syntax-rules (else)
-    ((_ (predicate expression ...)
-        rest ...)
-     (if predicate
-         (begin expression ...)
-         (case rest ...)))
-    ((_ (else expression ...))
-     (begin expression ...))))
+(define %null (λ (f x) x))
+(define (%null? value)
+  (church-numeral (λ x %false) %true))
 
-;;; Church numeral operations
+(define (%succ n) (λ (f x) (f (n f x))))
 
-(define (S n)
-  (λ (f x) (f (n f x))))
+(define (%pred n)
+  (%car (n (λ p (%cons (%cdr p) (%succ (%car p))))
+           (%cons %null %null))))
 
-(define (binary+ x y) (x S n))
-(binary-to-arbitrary + binary+)
+(define (%- x y) (y pred) x)
+(define (%<= x y) (%null? (%- x y)))
+(define (%= x y) (%and (%<= x y) (%<= y x)))
 
-(define (binary* x y) (λ (f) (m (n f))))
-(binary-to-arbitary * binary*)
+;;; ;;;;;;;;;;;;;;;
+;;; Typed pairs
 
-(define (expt b n) (n b))
+(define (type-constructor tag)
+  (λ value (%cons tag value)))
+(define (type-predicate tag)
+  (λ value (%= (%car value) tag)))
+(define type-value %cdr)
 
-;;; Pairs and lists
+(let-lowered ((tag %null)))
 
-(define (cons car cdr)
-  (lambda (f) (f car cdr)))
-(define null false)
+(let-lowered ((tag %null))
+  (define null ((type-constructor tag) null))
+  (define null? (type-predicate tag)))
 
-(define-syntax list
-  (syntax-rules ()
-    ((list) null)
-    ((list x y ...)
-     (cons x (list y ...)))))
+(let-lowered ((tag (%succ %null)))
+  (define (cons car cdr)
+    ((type-constructor tag) (%cons car cdr)))
+  (define pair? (type-predicate tag)))
 
-(define-syntax cons*
-  (syntax-rules ()
-    ((cons* x y) (cons x y))
-    ((cons* x y z ...)
-     (cons x (cons* y z ...)))))
-
-(define (car pair) (pair true))
-(define (cdr pair) (pair false))
-
-(define (null? x) (x (λ (h t d) false) true))
-
-(define (fold kons nil list)
-  ;; This is a left-fold: i.e.
-  ;; (kons (kons (... (kons (car list) nil))))
-  ;; 
-  ;; This is the fundamental list iterator that all other list functions
-  ;; are defined with.
-  (if (null? list)
-      nil
-      (fold kons (kons (car list) nil) (cdr list))))
-
-(define (reverse-append list1 list2)
-  (fold cons list2 list1))
-(define (reverse list) (reverse-append list1 null))
-
-(define (fold-right kons nil list)
-  (fold kons nil (reverse list)))
-
-(define (append list1 list2) (fold-right cons list2 list1))
-
-(define (append-n list-of-lists)
-  (fold-right (λ (list acc) (append list acc))
-              null
-              list-of-lists))
-
-(let-lowered ((mapper (λ (car cdr) (cons (f car) cdr))))
-  (define (map-reverse f list) (fold mapper null list))
-  (define (map f list) (fold-right mapper null list)))
-
-(define (any f list)
-  (fold (λ (value previous) (or previous (f value))) false list))
-(define (all f list)
-  (fold (λ (value previous) (and previous (f value))) true list))
-
-(define (length list) (fold (lambda (_ n) (+ n 1)) 0 list))
-
-(define (iota-fold kons nil count start step)
-  ;; `iota` cannot be defined in terms of `fold`s.
-  (if (<= count 0)
-      nil
-      (iota-fold kons
-                 (kons start nil)
-                 (- count 1)
-                 (+ start step)
-                 step)))
-
-(define (reverse-iota count start step)
-  (iota-fold cons null count start step))
-(define (iota count start step)
-  (reverse (reverse-iota count start step)))
-
-(define (make-list n fill)
-  (iota-fold (λ (_ cdr) (cons fill cdr)) null n 0 1))
-
-(define (list-tabulate n init-proc)
-  (iota-fold (λ (i cdr) (cons (init-proc i) cdr)) null n 0 1))
-
-(define (list-tail n list failure)
-  (let ((length (length list)))
-    (if (>= n length)
-        (failure n)
-        (iota-fold (lambda (_ list) list) n 0 1))))
-
-(define (list-ref n list failure)
-  (car (list-tail n list (lambda (n)
-                           (cons (failure n) nil)))))
-
-(define (list-drop list i)
-  (iota-fold (λ (_ cdr) cdr) list i 0 1))
-
-(define (list-take list i)
-  (reverse (list-drop (reverse list) (- (length list) i))))
-
-(define (list-take-right list i)
-  (list-drop list (- (length list) i)))
-
-(define (list-drop-right list i)
-  (list-take list (- (length list) i)))
-
-(define (last list default)
-  (fold (λ (kar knil) kar) default list))
-
-(define (transverse list-of-lists)
-  (let ((init-list (list-tabluate (length (car list-of-lists)) null))
-        (add-element
-         (λ (el state)
-           (let ((n (list-ref state 0))
-                 (acc (list-ref state 1)))
-             (list (+ n 1)
-                   (append (list-take acc n)
-                           (cons el (list-ref acc n))
-                           (list-drop acc (+ n 1))))))))
-    (fold-right (λ (l state)
-                  (fold-right add-element l (list 0 state)))
-                init-list
-                list-of-lists)))
-
-(define (foldn f init list-of-lists)
-  (fold (λ (elements init)
-          (letrec ((loop
-                    (λ (f elements init)
-                      (if (null? elements)
-                          (f init)
-                          (loop (f (car elements)) (cdr elements) init)))))
-            (loop f elements init)))
-        init
-        (transverse list-of-lists)))
-
-(define (list= = l1 l2)
-  (fold-n (λ (e1 e2 result)
-            (cond
-              ((not result) result)
-              ((= e1 e2) true)
-              (else false)))
-          (list l1 l2)))
+(define (car cell)
+  ((∘← type-value primitive-car) cell))
+
+(define (cdr cell)
+  ((∘← type-value primitive-cdr) cell))
 
diff --git a/multisyntax/examples/untyped-lambda-calculus.scm b/multisyntax/examples/untyped-lambda-calculus.scm
index 11aa17e..ab00a85 100644
--- a/multisyntax/examples/untyped-lambda-calculus.scm
+++ b/multisyntax/examples/untyped-lambda-calculus.scm
@@ -413,6 +413,14 @@
        => cdr)
       ((identifier? stx) (syntax->datum stx))
       ((pair? stx)
-       (cons (debruijnize env (car stx) free-variables)
-             (debruijnize env (cdr stx) free-variables)))
+       (let ((function (debruijnize env (car stx) free-variables))
+             (argument (debruijnize env
+                                    (syntax-cxr '(d a) stx)
+                                    free-variables))
+             (rest (syntax-cxr '(d d) stx)))
+         (if (null? rest)
+             (list function argument)
+             (debruijnize env
+                          (cons (list function argument) rest)
+                          free-variables))))
       (else stx))))
diff --git a/multisyntax/examples/untyped-lambda-calculus.sld b/multisyntax/examples/untyped-lambda-calculus.sld
index e4e33db..cb9f8e8 100644
--- a/multisyntax/examples/untyped-lambda-calculus.sld
+++ b/multisyntax/examples/untyped-lambda-calculus.sld
@@ -14,10 +14,11 @@
  |#
 
 (define-library (multisyntax examples untyped-lambda-calculus)
-  (import (scheme base) (scheme write)
+  (import (scheme base) (scheme write) (scheme cxr)
           (srfi 1) (srfi 26) (srfi 146 hash)
           (multisyntax syntax-object)
           (multisyntax pattern matcher)
           (multisyntax pattern producer))
-  (export expand transformer? initial-environment alpha debruijnize)
+  (export expand transformer? initial-environment alpha
+          debruijnize)
   (include "untyped-lambda-calculus.scm"))
\ No newline at end of file
diff --git a/test/examples/untyped-lambda-calculus.scm b/test/examples/untyped-lambda-calculus.scm
index a2f308e..c7baedf 100644
--- a/test/examples/untyped-lambda-calculus.scm
+++ b/test/examples/untyped-lambda-calculus.scm
@@ -13,6 +13,21 @@
  | limitations under the License.
  |#
 
+(define (curry-form form)
+  (cond
+    ((and (pair? form)
+          (eq? (car form) 'lambda))
+     (list 'lambda (curry-form (cadr form))))
+    ((and (pair? form)
+          (> (length form) 2))
+     (curry-form (cons (list (list-ref form 0)
+                             (list-ref form 1))
+                       (list-tail form 2))))
+    ((pair? form)
+     (list (curry-form (list-ref form 0))
+           (curry-form (list-ref form 1))))
+    (else form)))
+
 (define-syntax test-alpha
   (syntax-rules ()
     ((test-alpha name (inputs ...) output)
@@ -21,7 +36,7 @@
                    (expand initial-environment
                            (list (empty-wrap (quote inputs)) ...))))
        (test-equal name
-                   (quote output)
+                   (map curry-form (quote output))
                    (map (lambda (term)
                           (debruijnize global-map term '()))
                         expanded-list))))))
diff --git a/test/run.scm b/test/run.scm
index e6055c0..ff3f2ce 100644
--- a/test/run.scm
+++ b/test/run.scm
@@ -31,14 +31,3 @@
 (load "examples/untyped-lambda-calculus.sld")
 (import (multisyntax examples untyped-lambda-calculus test))
 (test-untyped-lambda-calculus)
-
-#;(let-values (((global-map expanded-list)
-              (expand initial-environment
-                      (list (empty-wrap '(define I (lambda x x)))
-                            (empty-wrap '(I (lambda I I)))))))
-  (display (alpha expanded-list)) (newline))
-
-#;(begin
-  (load "examples/untyped-lambda-calculus.sld")
-  (import (multisyntax examples untyped-lambda-calculus test))
-  (test-untyped-lambda-calculus))