;; ---< An alternative "Church" encoding: use lists to encode numbers >---

#lang pl schlac

(define identity (lambda (x) x))

;; Booleans (same as before)

(define #t (lambda (x y) x))
(define #f (lambda (x y) y))

(define if (lambda (c t e) (c t e))) ; not really needed

(test (->bool (if #t #f #t))
      => '#f)
(test (->bool (if #f ((lambda (x) (x x)) (lambda (x) (x x))) #t))
      => '#t)

(define and (lambda (a b) (a b a)))
(define or  (lambda (a b) (a a b)))
(define not (lambda (a x y) (a y x)))

(test (->bool (and #f #f)) => '#f)
(test (->bool (and #t #f)) => '#f)
(test (->bool (and #f #t)) => '#f)
(test (->bool (and #t #t)) => '#t)
(test (->bool (or  #f #f)) => '#f)
(test (->bool (or  #t #f)) => '#t)
(test (->bool (or  #f #t)) => '#t)
(test (->bool (or  #t #t)) => '#t)
(test (->bool (not #f)) => '#t)
(test (->bool (not #t)) => '#f)

;; Lists (same as before)

(define cons (lambda (x y s) (s x y)))
(define car (lambda (x) (x #t)))
(define cdr (lambda (x) (x #f)))

(define 1st car)
(define 2nd (lambda (l) (car (cdr l))))
(define 3rd (lambda (l) (car (cdr (cdr l)))))
(define 4th (lambda (l) (car (cdr (cdr (cdr l))))))
(define 5th (lambda (l) (car (cdr (cdr (cdr (cdr l)))))))

(define null (lambda (s) #t))
(define null? (lambda (x) (x (lambda (x y) #f))))

;; Natural numbers (alternate encoding)

(define 0 identity)

(define add1 (lambda (n) (cons #f n)))

(define zero? car) ; tricky

(define sub1 cdr) ; this becomes very simple

(define 1 (add1 0))
(define 2 (add1 1))
(define 3 (add1 2))
(define 4 (add1 3))
(define 5 (add1 4))

(test (->nat* (add1 (add1 5))) => '7)
(test (->nat* (sub1 (sub1 (add1 (add1 5))))) => '5)
(test (->bool (and (zero? 0) (not (zero? 3)))) => '#t)
(test (->bool (zero? (sub1 (sub1 (sub1 3))))) => '#t)

;; list-of-numbers tests
(define l123 (cons 1 (cons 2 (cons 3 null))))
(test (->listof ->nat* l123) => '(1 2 3))
(test (->listof (->listof ->nat*) (cons l123 (cons l123 null)))
      => '((1 2 3) (1 2 3)))

;; Recursive functions

(define Y
  (lambda (f)
    ((lambda (x) (x x)) (lambda (x) (f (x x))))))
(rewrite (define/rec f E) => (define f (Y (lambda (f) E))))

;; note that this example is doing something silly now
(define/rec length
  (lambda (l)
    (if (null? l)
      0
      (add1 (length (cdr l))))))
(test (->nat* (length l123)) => '3)

;; addition becomes hard since it requires a recursive definition
;; (define/rec +
;;   (lambda (m n) (if (zero? n) m (+ (add1 m) (sub1 n)))))
;; (test (->nat* (+ 4 5)) => '9)

;; faster alternative:
(define/rec +
  (lambda (m n)
    (if (zero? m) n
        (if (zero? n) m
            (add1 (add1 (+ (sub1 m) (sub1 n))))))))
(test (->nat* (+ 4 5)) => '9)

;; subtraction is similar to addition
;; (define/rec -
;;   (lambda (m n) (if (zero? n) m (- (sub1 m) (sub1 n)))))
;; (test (->nat* (- (+ 4 5) 4)) => '5)
;; but this is not "natural subtraction": doesn't work when n>m,
;; because (sub1 0) does not return 0.

;; a solution is like alternative form of +:
(define/rec -
  (lambda (m n)
    (if (zero? m) 0
        (if (zero? n) m
            (- (sub1 m) (sub1 n))))))
(test (->nat* (- (+ 4 5) 4)) => '5)
(test (->nat* (- 2 5)) => '0)
;; alternatively, could change sub1 above:
;; (define sub1 (lambda (n) (if (zero? n) n (cdr n))))

;; we can do multiplication in a similar way
(define/rec *
  (lambda (m n)
    (if (zero? m) 0
        (+ n (* (sub1 m) n)))))
(test (->nat* (* 4 5)) => '20)
(test (->nat* (+ 4 (* (+ 2 5) 5))) => '39)

;; and the rest of the examples

(define/rec fact
  (lambda (x)
    (if (zero? x) 1 (* x (fact (sub1 x))))))
(test (->nat* (fact 5)) => '120)

(define/rec fib
  (lambda (x)
    (if (or (zero? x) (zero? (sub1 x)))
      1
      (+ (fib (sub1 x)) (fib (sub1 (sub1 x)))))))
(test (->nat* (fib (* 5 2))) => '89)

#|
;; Fully-expanded Fibonacci (note: shorter than the previous encoding)
(define fib((lambda(f)((lambda(x)(x x))(lambda(x)(f(x x)))))(lambda(f)
(lambda(x)(((((x (lambda(x y) x))(x(lambda(x y)x)))((x(lambda(x y)y))(
lambda(x y)x)))(lambda(s)(s(lambda(x y)y)(lambda(x)x))))((((lambda(f)(
(lambda(x)(x x))(lambda(x)(f(x x)))))(lambda(f)(lambda(m n)((m(lambda(
x y)x))n(((n(lambda(x y)x))m)(lambda(s)((s(lambda(x y)y))(lambda(s)((s
(lambda(x y)y)) ((f(m(lambda(x y)y)))(n (lambda(x y)y))))))))))))(f(x(
lambda(x y)y))))(f((x(lambda(x y)y))(lambda(x y)y)))))))))
|#