(in-package :cl-user)

;;; Combinatory logic

(defun cleanup (expr)
  "Removes parentheses around single atoms."
  (cond ((null expr) '())
        ((atom expr) expr)
        (t (mapcar (lambda (x)
                     (if (and (consp x) (null (cdr x)))
                         (cleanup (car x))
                         (cleanup x)))
                   expr))))

(defun cl-meta-1 (expr)
  (cond ((null expr) '())
        ((atom expr) expr)
        ((eq (car expr) 'lambda)
         (let* ((var (caadr expr))
                (body (cddr expr))
                (body-flat (flatten body)))
           (cond ((cdadr expr)
                  `(lambda (,var)
                     ,(cl-meta-1 `(lambda (,@(cdadr expr))
                                    ,@body))))
                 ((member 'lambda body-flat) ; process lambdas from the inside
                  `(lambda (,var)
                     ,@(cl-meta-1 body)))
                 ((and (equal (list var) body-flat))
                  '(I))
                 ((not (member var body-flat))
                  `(K ,body))
                 ((and (equal (list var) (flatten (lastcar body)))
                       (not (member var (flatten (butlast body)))))
                  (butlast body))
                 ((cdr body)
                  `(S (lambda (,var) ,@(butlast body))
                      (lambda (,var) ,@(last body))))
                 ((consp (car body))
                  `(lambda (,var) ,@(car body)))
                 (t `(lambda (,var) ,(cl-meta-1 body))))))
        (t (cons (cl-meta-1 (car expr))
                 (cl-meta-1 (cdr expr))))))

(defun cl-meta (expr &optional trace)
  (let ((next (cl-meta-1 expr)))
    (when trace (print expr))
    (if (member 'lambda (flatten next))
        (cl-meta next trace)
        (cleanup next))))

;;; Example:
;;; (cl-meta '(lambda (u x) x (u u x)))
;;; => (S (K (S I)) (S I I))

(defun cl-eval-1 (expr &optional (head t))
  (cond ((null expr) '())
        ((atom expr) (list expr))
        (t (let ((x (car expr)))
             (cond ((and head (eq x 'I) (cdr expr))
                    (cdr expr))
                   ((and head (eq x 'K) (cddr expr))
                    (cons (cadr expr) (cdddr expr)))
                   ((and head (eq x 'S) (cdddr expr))
                    (let ((y (cadddr expr)))
                      (append (list (cadr expr) y (list (caddr expr) y))
                              (cddddr expr))))
                   ((and head (consp x))
                    (append (cl-eval-1 x) (cdr expr)))
                   ((consp x)
                    (cons (cl-eval-1 x) (cdr expr)))
                   (t (cons x (cl-eval-1 (cdr expr) nil))))))))

(defun cl-eval (expr &optional trace)
  (let ((next (cleanup (cl-eval-1 expr))))
    (when trace (print expr))
    (if (equal expr next)
        next
        (cl-eval next trace))))

;;; Example:
;;; (cl-eval '(S (K (S I)) (S I I) u x))
;;; => (x (u u x))

#+nil
(let* ((U (cl-meta '(lambda (u x) x (u u x))))
       (V (cl-meta '(lambda (y) x (y y))))
       (Y-turing `(,U ,U))
       (Y-curry (cl-meta `(lambda (x) ,V ,V))))
  (format t "Y (Turing):~%~a~%Y (Curry-Rosenbloom):~%~a~%" Y-turing Y-curry))