;;;; Helper functions

;; variables

(defun make-var (sym) 
       (list 'VAR sym))

(defun variable? (term) 
       (eq (car term) 'VAR))

(defun var-symbol (term) 
       (cadr term))

;; abstractions

(defun make-abs (sym term) 
       (list 'LAMBDA sym term)
)

(defun abstraction? (term)
       (eq (car term) 'LAMBDA))

(defun abs-var (term)
       (cadr term))

(defun abs-body (term)
       (caddr term))


;; applications

(defun make-app (fn arg)
       (list 'APP fn arg))

(defun application? (term)	
       (eq (car term) 'APP))

(defun app-fn (term)
       (cadr term))

(defun app-arg (term)
       (caddr term))


;;;; Renaming free variables

(defun alphaconvert (term x y)
       (cond 
       ;; deal with variables: if the variable is x, return y
       ;; if not, return the term unchanged
       ;; x[y/x] = x
       ;; z[y/z] = z
          ((variable? term) (if (eq x (var-symbol term)) (make-var y)
       term))

       ;; deal with applications: recursively perform the renaming 
       ;; in the function part and argument part, and reassemble the 
       ;; two parts into an application
       ;; MN[y/x] = M[y/x]N[y/x]
	  ((application? term) (make-app (alphaconvert (app-fn term) x
       y)  (alphaconvert (app-arg term) x y)))

       ;; deal with abstractions: if the bound variable is x, return 
       ;; the term unchanged. Otherwise, recursively perform renaming
       ;; inside the body.    
       ;; (lambda x.M)[y/x] = lambda x.M
       ;; (lambda z.M)[y/x] = lambda z.(M[y/x])
	  ((abstraction? term) (if (eq x (abs-var term)) term
       (make-abs (abs-var term) (alphaconvert (abs-body term) x y))))
	  )
)

;;;; Substitution

(defun subs (term1 var term2)	
       (cond 
       ;; deal with variables
       ;; x[N/x] = M
       ;; y[N/x] = y 
       	  ((variable? term1) (if (eq var (var-symbol term1)) term2
       term1))
       ;; deal with applications
       ;; M1M2[N/x] = M1[N/x]M2[N/x]
         ((application? term1) (make-app (subs (app-fn term1) var
       term2) (subs (app-arg term1) var term2)))
       ;; deal with abstractions
       ;; (lambda x.M)[N/x] = lambda x.M
       ;; (lambda y.M)[N/x] = lambda z.((M[z/y])[N/x])
       ;; In the last case, use alphaconvert to rename the abstracted
       variable, to a fresh variable generated by (gensym)
       ;; and then use a recursive call to substitute N into the body
        ((abstraction? term1) 
	   (let ((newvar (gensym))) (make-abs newvar (subs (alphaconvert
       (abs-body term1) (abs-var term1) newvar) var term2))))
       )
)

;;;; Reduction

(defun redex? (term)
       ;; a redex is an application whose function part is an abstraction
       (and (application? term) (abstraction? (app-fn term))))

(defun contains-redex? (term)
       (cond 
       ;; variables contain no redexes
            ( (variable? term) #f)
       ;; an abstraction contains a redex if its body does
	    ( (abstraction? term) (contains-redex? (abs-body term)))
       ;; an application contains a redex if either the function part
       ;; or the argument part does
	    ( (application? term) (or (redex? term) (contains-redex?
       (app-fn term)) (contains-redex? (app-arg term))))
       )
)

(defun normalbeta (term)
  ;; does the term contain any redexes?
     (if (contains-redex? term)
	 ;; if the term is a redex, beta reduce it
       (if (redex? term)
	   ;; (lambda x.M)N --> M[N/x]
          (subs (abs-body (app-fn term)) (abs-var (app-fn term))
       (app-arg term))
	 ;; term is not a redex but contains one. Let's find the leftmost
	 ;; outermost redex and reduce it
           (cond 
	    ;; if the term is an abstraction, reduce the body
            ((abstraction? term)
	      (make-abs (abs-var term) (normalbeta (abs-body term))))
	    ;; if the term is an application, first try to find a redex in the function part (leftmost first!)
	    ((application? term) 
	      (if (contains-redex? (app-fn term))
	            (make-app (normalbeta (app-fn term)) (app-arg
     term))
		;; no redex in the function part so find and reduce the redex in the argument part
                    (make-app (app-fn term) (normalbeta (app-arg
     term)))
     )
     )   )
       )
   term)
)


(defun normal-reduce (term)
       (if (contains-redex? term)	
	   ;; if there's a redex, reduce it and carry on
	   ;; NB can replace (print term) with just term
	   ;; if you don't want to see all the intermediate steps
	(normal-reduce (normalbeta (print term)))
	;; if not, stop
	term)
)

;;;; weak head normal form


(defun whnf? (term)
       (cond
	;; a variable is in WHNF
         ((variable? term) #t)
	 ;; an abstraction is in WHNF
         ((abstraction? term) #t)
	 ;; an application is in WHNF if the function part is a WHNF and is not an abstraction
	 ((application? term) (and (whnf? (app-fn term)) (not
       (abstraction? (app-fn term)))))
       )
)

;; compare with normal-reduce
(defun whnf-reduce (term)
       (if (whnf? term)
         term
	 (whnf-reduce (normalbeta (print term)))))

       

;;;; some programming

;; pairs

(setq pair (make-abs 'x (make-abs 'y (make-abs 's (make-app (make-app
(make-var 's) (make-var 'x)) (make-var 'y))))))

(setq left (make-abs 'p (make-app (make-var 'p) (make-abs 'x (make-abs
'y (make-var 'x))))))

(setq right (make-abs 'p (make-app (make-var 'p) (make-abs 'x (make-abs
'y (make-var 'y))))))

(setq xy (make-app (make-app pair (make-var 'x)) (make-var 'y)))

;; conditional

(setq true (make-abs 'x (make-abs 'y (make-var 'x))))
(setq false (make-abs 'x (make-abs 'y (make-var 'y))))
(setq c (make-abs 'x (make-var 'x)))

;; lists

(setq lnil (make-abs 'x true))
(setq lnull (make-abs 'p (make-app (make-var 'p) (make-abs 'x
(make-abs 'y false)))))

;; fixed points

(setq curry-y (make-abs 'f (make-app (make-abs 'x (make-app (make-var
'f) (make-app (make-var 'x) (make-var 'x)))) (make-abs 'x (make-app (make-var
'f) (make-app (make-var 'x) (make-var 'x)))) )))

(setq turing-y (make-app (make-abs 'x (make-abs 'y (make-app (make-var
'y) (make-app (make-app (make-var 'x) (make-var 'x)) (make-var 'y)))))
(make-abs 'x (make-abs 'y (make-app (make-var
'y) (make-app (make-app (make-var 'x) (make-var 'x)) (make-var
'y)))))))

;; numerals

(setq zero (make-abs 'x (make-var 'x)))
(setq succ (make-abs 'n (make-app (make-app pair false) (make-var
'n))))

(setq pred right)
(setq iszero (make-abs 'n (make-app (make-var 'n) true)))

(setq add (make-app curry-y (make-abs 'a (make-abs 'n (make-abs 'm
(make-app (make-app (make-app c (make-app iszero (make-var 'm)))
(make-var 'n)) (make-app succ (make-app (make-app (make-var 'a)
(make-var 'n)) (make-app pred (make-var 'm))))))))))

(setq three (make-app succ (make-app succ (make-app succ zero))))
(setq one (make-app succ zero))

(setq answer (make-app iszero (make-app pred (make-app pred (make-app
pred (make-app pred (make-app (make-app add three) one)))))))