;; Using DrScheme **299.400** or later, run this program
;; in the "MzScheme" language, which is the first
;; choice in the "PLT" group.

;; To see a term with definitions expanded, type it
;; in DrScheme's interaction window (after clicking "Run"):
;;
;;  > {iszero one}
;;  ((fun (n) ((n (fun (x) (fun (x) (fun (y) y))))
;;             (fun (x) (fun (y) x)))) (fun (f) (fun (x) (f x))))

;; To see the result of a single reduction, use `reduce':
;;
;;  > (reduce {iszero one})
;;  (((fun (f) (fun (x) (f x))) (fun (x) (fun (x) (fun (y) y))))
;;   (fun (x) (fun (y) x)))
;;  > (reduce (reduce (reduce {iszero one})))
;;  ((fun (x) (fun (x) (fun (y) y))) (fun (x) (fun (y) x)))

;; To see the simplest form, use `simplify':
;;
;;  > (simplify {iszero one})
;;  (fun (x) (fun (y) y))
;;  > (simplify {fac {add1 two}})
;;  (fun (g) (fun (y) (g (g (g (g (g (g y))))))))

;; ----------------------------------------
;; Macros:

;; Change the syntax of function application
;; so that {} constructs an LC expression
;; insrtead of applying a function:
(require (rename mzscheme mz-app #%app))
(define-syntax (#%app stx)
  (if (eq? #\{ (syntax-property stx 'paren-shape))
      (syntax-case stx ()
        [(_ a b) 
         #'`(,a ,b)])
      (syntax-case stx ()
        [(_ arg ...)
         #'(mz-app arg ...)])))

;; Change `fun' to build an LC-expression, too.
;; It binds the fun argument as syntax to expand to
;; the quoted argument name, then treats the fun
;; body as an expression.
(define-syntax (fun stx)
  (syntax-case stx ()
    [{_ {id} body}
     #'(let-syntax ([id
                     (syntax-id-rules ()
                       [(_ y) `(id ,y)]
                       [_ 'id])])
         `{fun {,id} ,body})]))


;; ----------------------------------------
;; Reduction functions

(require (lib "plt-match.ss"))

;; Perform the left-most outermost reduction.
(define (reduce x)
  (match x
    [`{{fun {,x} ,body} ,arg}
      (subst body x arg)]
    [`{fun {,x} ,body}
      `{fun {,x} ,(reduce body)}]
    [`{,x ,y}
      (let ([sx (reduce x)])
        (if (equal? x sx)
            `{,x ,(reduce y)}
            `{,sx ,y}))]
    [else x]))

;; Beta substitution
(define (subst expr id val)
  (match expr
    [`{fun {,x} ,body}
      (if (eq? x id)
          expr
          (let ([y (if (not-free? x val)
                       x
                       (gensym))])
            `{fun {,y} ,(subst (if (eq? x y)
                                   body
                                   (subst body x y))
                               id val)}))]
    [`{,a ,b} `{,(subst a id val) ,(subst b id val)}]
    [x (if (eq? x id)
           val
           x)]))

;; Used to avoid generating ids substituting into a
;;  function, when we can:
(define (not-free? id expr)
  (match expr
    [`{fun {,x} ,body}
      (or (eq? x id)
          (not-free? id body))]
    [`{,a , b} (and (not-free? id a)
                    (not-free? id b))]
    [x (not (eq? x id))]))

;; Loop until reduction doesn't change the
;;  expression:
(define (simplify x)
  (let ([s (reduce x)])
    (if (equal? s x)
        x
        (simplify s))))

;; ----------------------------------------
;; Term definitions:

(define zero {fun {f} {fun {x} x}})
(define one {fun {f} {fun {x} {f x}}})
(define two {fun {f} {fun {x} {f {f x}}}})

(define true {fun {x} {fun {y} x}})
(define false {fun {x} {fun {y} y}})

(define cons {fun {x} {fun {y} 
			   {fun {b} {{b x} y}}}})

(define first {fun {p} {p true}})
(define rest {fun {p} {p false}})

(define add1 {fun {n} 
		  {fun {g} {fun {y} 
				{g {{n g} y}}}}})
(define add2 {fun {n} {add1 {add1 n}}})
(define add3 {fun {n} {add1 {add1 {add1 n}}}})

(define add {fun {n} {fun {m} {{n add1} m}}})

(define mult {fun {n} {fun {m} {{n {add m}} zero}}})

(define iszero {fun {n} {{n {fun {x} false}} true}})

(define wrap {fun {f} {fun {p}
			   {{cons false}
			    {{{first p}
			      {rest p}}
			     {f {rest p}}}}}})
(define sub1 {fun {n}
		  {fun {g} {fun {y}
				{rest
				 {{n {wrap g}}
				  {{cons true} y}}}}}})

(define mk-rec {fun {body}
		    {{fun {fX} {fX fX}}
		     {fun {fX}
			  {{fun {f} {body f}}
			   {fun {x} {{fX fX} x}}}}}})

(define fac {mk-rec 
	     {fun {fac}
		  {fun {n}
		       {{{iszero n}
			 one}
			{{mult n} {fac {sub1 n}}}}}}})