; Pure lambda calculus (see http://en.wikipedia.org/wiki/Lambda_calculus)

(require :globals)
(require :combination-hook)
(defun combination-hook::combination-hook (form) (cons 'funcall form))

; A Quine
((LAMBDA (X) (LIST X (LIST 'QUOTE X))) '(LAMBDA (X) (LIST X (LIST 'QUOTE X))))

; Another Quine.  Doesn't need combination-hook but it's cute
(let ((let '`(let ((let ',let)) ,let))) `(let ((let ',let)) ,let))

; Non-currying lambda (this will break stuff downstream)
(defmacro λ (args body)
  `(lambda ,args (declare (ignorable ,@args))
     (flet (,@(loop for arg in args collect `(,arg (&rest args) (apply ,arg args))))
       ,body)))

; Currying lambda
(defmacro λ (args body)
  (if args
    `(lambda (&rest args1)
       (let ((,(first args) (first args1)))
         (declare (ignorable ,(first args)))
         (flet ((,(first args) (&rest args2) (apply ,(first args) args2)))
           (let ((f (λ ,(rest args) ,body)))
             (if (rest args1) (apply f (rest args1)) f)))))
    body))

(defmacro define (name value)
  `(progn
     (defv ,name ,value)
     (defun ,name (&rest args) (apply ,name args))))

; Logic
(define \true (λ (x y) x))
(define \false (λ (x y) y))
(define \if (λ (p a b) (p a b)))

(define \and (λ (p q) (p q p)))
(define \or (λ (p q) (p p q)))
(define \not (λ (p) (λ (a b) (p b a))))

; Cons cells
(define \cons (λ (a b) (λ (f) (f a b))))
(define \car (λ (pair) (pair \true)))
(define \cdr (λ (pair) (pair \false)))
(define \nil (λ (x) \true))
(define \null (λ (pair) (pair (λ (x y) \false))))

; Church numerals
(define \zero (λ (f x) x))
(define \succ (λ (n) (λ (f x) (f (n f x)))))
(define \plus (λ (m n) (λ (f x) (m f (n f x)))))
(define \mult (λ (m n) (λ (f) (m (n f)))))
(define \expt (λ (b e) (e b)))

(define \pred (λ (n) (λ (f x) (n (λ (g h) (h (g f))) (λ (u) x) (λ (u) u)))))
(define \sub (λ (m n) (n \pred m)))

(define \zero? (λ (n) (n (λ (x) \false) \true)))
(define \leq? (λ (n m) (\zero? (\sub m n))))
(define \eql? (λ (m n) (\and (\leq? m n) (\leq? n m))))

; Alternate (much faster) definitions
(define \plus (λ (m n) (m \succ n)))
(define \mult (λ (m n) (m (\plus n) \zero)))
(define \expt (λ (b e) (e (\mult b) (\succ \zero))))

(define \phi (λ (pair) (\cons (\cdr pair) (\succ (\cdr pair)))))
(define \pred (λ (n) (\car (n \phi (\cons \zero \zero)))))

; The Y combinator

(define y (λ (f) ((λ (h) (λ (x) ((f (h h)) x))) (λ (h) (λ (x) ((f (h h)) x))))))

(define y (λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x))))))

(define fact* (λ (f) (λ (n) (if (zerop n) 1 (* n (f (1- n)))))))

((y fact*) 15)

((y (λ (f) (λ (n) (if (zerop n) 1 (* n (f (1- n))))))) 15)

(((λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x)))))
  (λ (f) (λ (n) (if (zerop n) 1 (* n (f (1- n)))))))
 15)

; Factorial with Church numerals (Holy shit!  It works!)

(define \fact (y (λ (f)
                    (λ (n)
                       (if (\if (\zero? n) t nil)
                         (\succ \zero)
                         (\mult n (f (\pred n))))))))

(defun cn (n) (if (zerop n) \zero (\succ (cn (1- n)))))
(defun pcn (cn) (funcall cn '1+ 0)) ; For Church numerals only
(defun pcn (cn) (if (\if (\zero? cn) t nil) 0 (1+ (pcn (\pred cn)))))

(pcn (\expt (cn 3) (cn 4)))
(pcn (\fact (cn 6)))

; Expanded Church numeral factorial
(pcn
 (((λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x)))))
   (λ (f)
      (λ (n)
         (if ((λ (p a b) (p a b)) ((λ (n) (n (λ (x) (λ (x y) y)) (λ (x y) x))) n) t nil)
           ((λ (n) (λ (f x) (f (n f x)))) (λ (f x) x))
           ((λ (m n) (m ((λ (m n) (λ (f x) (m f (n f x)))) n) (λ (f x) x)))
            n (f ((λ (n) (λ (f x) (n (λ (g h) (h (g f))) (λ (u) x) (λ (u) u)))) n)))))))
  ((λ (n) (λ (f x) (f (n f x))))
   ((λ (n) (λ (f x) (f (n f x))))
    ((λ (n) (λ (f x) (f (n f x))))
     ((λ (n) (λ (f x) (f (n f x))))
      ((λ (n) (λ (f x) (f (n f x))))
       ((λ (n) (λ (f x) (f (n f x))))
        (λ (f x) x)))))))))

((((λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x)))))
   (λ (f)
      (λ (n)
         (if ((λ (p a b) (p a b)) ((λ (n) (n (λ (x) (λ (x y) y)) (λ (x y) x))) n) t nil)
           ((λ (n) (λ (f x) (f (n f x)))) (λ (f x) x))
           ((λ (m n) (m ((λ (m n) (λ (f x) (m f (n f x)))) n) (λ (f x) x)))
            n (f ((λ (n) (λ (f x) (n (λ (g h) (h (g f))) (λ (u) x) (λ (u) u)))) n)))))))
  ((λ (n) (λ (f x) (f (n f x))))
   ((λ (n) (λ (f x) (f (n f x))))
    ((λ (n) (λ (f x) (f (n f x))))
     ((λ (n) (λ (f x) (f (n f x))))
      ((λ (n) (λ (f x) (f (n f x))))
       ((λ (n) (λ (f x) (f (n f x))))
        (λ (f x) x))))))))
 '1+ 0)

; (fact (fact 3))
((((λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x)))))
   (λ (f)
      (λ (n)
         (if ((λ (p a b) (p a b)) ((λ (n) (n (λ (x) (λ (x y) y)) (λ (x y) x))) n) t nil)
           ((λ (n) (λ (f x) (f (n f x)))) (λ (f x) x))
           ((λ (m n) (m ((λ (m n) (λ (f x) (m f (n f x)))) n) (λ (f x) x)))
            n (f ((λ (n) (λ (f x) (n (λ (g h) (h (g f))) (λ (u) x) (λ (u) u)))) n)))))))
  (((λ (f) ((λ (g) (g g)) (λ (h) (λ (x) ((f (h h)) x)))))
    (λ (f)
       (λ (n)
          (if ((λ (p a b) (p a b)) ((λ (n) (n (λ (x) (λ (x y) y)) (λ (x y) x))) n) t nil)
            ((λ (n) (λ (f x) (f (n f x)))) (λ (f x) x))
            ((λ (m n) (m ((λ (m n) (λ (f x) (m f (n f x)))) n) (λ (f x) x)))
             n (f ((λ (n) (λ (f x) (n (λ (g h) (h (g f))) (λ (u) x) (λ (u) u)))) n)))))))
  ((λ (n) (λ (f x) (f (n f x))))
   ((λ (n) (λ (f x) (f (n f x))))
    ((λ (n) (λ (f x) (f (n f x))))
     (λ (f x) x))))))
 '1+ 0)


#|
; CONS numerals

(define \zero \nil)
(define \zero? \null)
(define \succ (λ (n) (\cons \nil n)))
(define \pred (λ (n) (\if (\zero? n) n (\cdr n))))

(define \plus (y (λ (f)
                    (λ (n1 n2)
                       (if (\if (\zero? n2) t nil)
                         n1
                         (f (\succ n1) (\pred n2)))))))

(define \mult (λ (n1 n2)
                 ((y (λ (f)
                    (λ (n1 n2 n3)
                       (if (\if (\zero? n1) t nil)
                         n3
                         (f (\pred n1) n2 (\plus n2 n3))))))
                  n1 n2 \zero)))

(define \expt (λ (n1 n2)
                 ((y (λ (f)
                        (λ (n1 n2 n3)
                           (if (\if (\zero? n1) t nil)
                             n3
                             (f (\pred n1) n2 (\mult n2 n3))))))
                  n2 n1 (\succ \zero))))

(pcn (\expt (cn 7) (cn 5)))
|#