;; encoding of booleans
(define mytrue (lambda (t) (lambda (f) t)))
(define myfalse (lambda (t) (lambda (f) f)))

(define (mynot b) ((b myfalse) mytrue))
(define (myand b1 b2) ((b1 ((b2 mytrue) myfalse)) myfalse))
(define (myif b e1 e2) ((b e1) e2))

; function for converting to built-in booleans
(define (mybool2bool b) ((b #t) #f))

; test
(define test1 (myif (myand mytrue myfalse) 1 2))

;; encoding of pairs

(define (makepair x y) (lambda (f) (f x y)))
(define (fst p) (p (lambda (x y) x)))
(define (snd p) (p (lambda (x y) y)))
; test
(define test2 (fst (makepair 1 2)))

;; encoding of natural numbers

(define zero (lambda (s) (lambda (z) z)))
(define one  (lambda (s) (lambda (z) (s z))))
(define two  (lambda (s) (lambda (z) (s (s z)))))
(define three  (lambda (s) (lambda (z) (s (s (s z))))))

(define (succ n) (lambda (s) (lambda (z) (s ((n s) z)))))
(define plus (lambda (m) (lambda (n)
 	    (lambda (s) (lambda (z) ((m s) ((n s) z)))))))
(define mult (lambda (m) (lambda (n)
			   ((n (plus m)) zero))))
(define exp (lambda (m) (lambda (n)
			  ((n (mult m)) one))))
(define exp2 (lambda (m) (lambda (n) (n m))))
(define eqzero (lambda (n) ((n (lambda (x) myfalse)) mytrue)))

(define next (lambda (p) (makepair (succ (fst p)) (fst p))))
(define pred (lambda (n) (snd ((n next) (makepair zero zero)))))
(define minus (lambda (m) (lambda (n) ((n pred) m))))


; conversion between built-in integers and nat 
(define (int2nat n)
  (if (= n 0)
      zero
      (succ (int2nat (- n 1)))))
(define (nat2int n)
  ((n (lambda (x) (+ x 1))) 0))

; test
(define test3 (nat2int ((plus three) two)))
(define test4 (nat2int ((mult three) two)))
(define test5 (nat2int ((minus three) one)))
(define test6 (myif (eqzero one) 1 2))


;; recursion
; fixedpoint combinator for call-by-value
(define Y (lambda (f)
	    ((lambda (x) (lambda (z) ((f (x x)) z)))
	     (lambda (x) (lambda (z) ((f (x x)) z))))))
; factorial
(define factgen (lambda (f) (lambda (n) (if (= n 0) 1 (* n (f (- n 1)))))))
(define fact (Y factgen))

; pure factorial, consisting of only functions
(define purefactgen
  (lambda (f) (lambda (n)
		((myif (eqzero n)
		      (lambda (x) one)
		      (lambda (x) ((mult n) (f (pred n))))) (lambda (x) x)))))
(define purefact (Y purefactgen))

; test
(define test7 (purefact three))