#lang racket

;; Project 3: A church-compiler for Scheme, to Lambda-calculus

(provide church-compile
         ; provided conversions:
         church->nat
         church->bool
         church->listof)


;; Input language:
;
; e ::= (letrec ([x (lambda (x ...) e)]) e)    
;     | (let ([x e] ...) e)  
;     | (let* ([x e] ...) e)
;     | (lambda (x ...) e)
;     | (e e ...)    
;     | x  
;     | (and e ...) | (or e ...)
;     | (if e e e)
;     | (prim e) | (prim e e)
;     | datum
; datum ::= nat | (quote ()) | #t | #f 
; nat ::= 0 | 1 | 2 | ... 
; x is a symbol
; prim is a primitive operation in list prims
; The following are *extra credit*: -, =, sub1  
(define prims '(+ * - = add1 sub1 cons car cdr null? not zero?))

; This input language has semantics identical to Scheme / Racket, except:
;   + You will not be provided code that yields any kind of error in Racket
;   + You do not need to treat non-boolean values as #t at if, and, or forms
;   + primitive operations are either strictly unary (add1 sub1 null? zero? not car cdr), 
;                                           or binary (+ - * = cons)
;   + There will be no variadic functions or applications---but any fixed arity is allowed

;; Output language:

; e ::= (lambda (x) e)
;     | (e e)
;     | x
;
; also as interpreted by Racket


;; Using the following decoding functions:

; A church-encoded nat is a function taking an f, and x, returning (f^n x)
(define (church->nat c-nat)
  ((c-nat add1) 0))

; A church-encoded bool is a function taking a true-thunk and false-thunk,
;   returning (true-thunk) when true, and (false-thunk) when false
(define (church->bool c-bool)
  ((c-bool #t) #f))

; A church-encoded cons-cell is a function taking a when-cons callback, and a when-null callback (thunk),
;   returning when-cons applied on the car and cdr elements
; A church-encoded cons-cell is a function taking a when-cons callback, and a when-null callback (thunk),
;   returning the when-null thunk, applied on a dummy value (arbitrary value that will be thrown away)
(define ((church->listof T) c-lst)
  ; when it's a pair, convert the element with T, and the tail with (church->listof T)
  ((c-lst (lambda (a) (lambda (b) (cons (T a) ((church->listof T) b)))))
   ; when it's null, return Racket's null
   (lambda (_) '())))





;; Write your church-compiling code below:


(define (churchify e)
  (match e
        ; Let
        ; This isn't what was in the p3 intro video (and it's super wacky)
        ;   BUT it's the only way i've found that handles the k-ary let scheme 
        [`(let ([,xs ,e0s] ...) ,e1) 
        (churchify `((lambda ,xs ,e1) .,e0s))]
        [`(let () ,e1)
         (churchify e1)] 

        ; Let*
        [`(let* (,x0 ,e0 ...) ,e1)
         (churchify `(let (,x0) (let* (,@e0) ,e1)))]
        [`(let* () ,e1)
         (churchify e1)]

        ;letrec
        [`(letrec ([,f ,y] ...) ,e1) 
        (churchify `())]

        ; Curry Lambdas
        [`(lambda () ,e1) `(lambda (_) ,
        (churchify e1))]
        [`(lambda (,x) ,e1) `(lambda (,x) ,
        (churchify e1))]
        [`(lambda (,x ,ys ...) ,e1) `(lambda (,x) ,
        (churchify `(lambda ,ys ,e1)))]

        ; Logic stuff
        [`(if ,ge ,te ,fe) (churchify `(,ge (lambda (_) ,te) (lambda (_) ,fe)))]

        

        
        

        ; Literals
        [(? natural? nat)
          (define (wrap nat)


            (cond
            [(= 0 nat )'x]
            [else
              `(f ,(wrap (- nat 1)))]))
          (churchify `(lambda (f ) (lambda (x) ,(wrap nat))))]
        [''() (churchify '(lambda (cons null) (null)))]
        ; Why does this (x x) work and x alone does not???
        [#t `(lambda (x) (lambda (y) (x x)))]
        [#f `(lambda (x) (lambda (y) (y y)))]

        ; Curry Applications
        ; moved to bottom because we want to match every possible thing before currying
        [`(,fun) 
        `(,(churchify fun) (lambda (x) x))]
        [`(,fun ,arg) 
        `(,(churchify fun) ,(churchify arg))]
        [`(,fun ,arg1 ,arg2 ...) 
        (churchify `((,fun ,arg1) ,@arg2))]

        [_ e]
  ))

; Takes a whole program in the input language, and converts it into an equivalent program in lambda-calc
(define (church-compile program)
  ; Define primitive operations and needed helpers using a top-level let form?
  (define todo `(lambda (x) x))
  (define myplus `(lambda (m n) (lambda (f x) (n f (m f x)))))
  (define mymultiplication `(lambda (m n) (lambda (f x) ((m (n f)) x))))
  (define myadd1 `(lambda (n) (lambda (f x) (f ((n f) x)))))
  (define mynull? `(lambda (n) (n (lambda (x y) #f) (lambda () #t))))
  (define mynot `(lambda (n) (if n #f #t)))
  (define mycons `(lambda (n m) (lambda (cons null) (cons n m))))
  (define mycar `(lambda (n) (n (lambda (x y) x) (lambda () (lambda (n) n)))))
  (define mycdr `(lambda (n) (n (lambda (x y) y) (lambda () (lambda (m) m)))))
  (define mysub1 `(lambda (n) (lambda (x) (lambda (y) (((n (lambda (g) (lambda (h) (h (g f)))))(lambda (_) y)) (lambda (x) x))))))
  (define myminus `(lambda (m n) ((n ,mysub1) m)))
  (churchify
   `(let 
      (
        [+ ,myplus]
        [* ,mymultiplication]
        [- ,myminus]
        [add1 ,myadd1]
        [null? ,mynull?]
        [not ,mynot]
        [cons ,mycons]
        [car ,mycar]
        [cdr ,mycdr]
      )
      ,program)))




; Tests

;add (working)
; (define prog '(+ 1 (+ 2 (+ 3 3))))
; (print prog)
; (define unchurch church->nat)
; (print "Value of compiled program:")
; (print prog)
; (define v (eval prog (make-base-namespace)))
; (with-output-to-file "answer"
;   (lambda ()
;     (print v))
;   #:exists 'replace)

; (define compiled (church-compile prog))
; (define cv-comp (eval compiled (make-base-namespace)))
; (define v-comp (unchurch cv-comp))
; (with-output-to-file "output"
;   (lambda ()
;     (print v-comp))
;   #:exists 'replace)

  ;add1 working
;   (define prog '(add1 (add1 2)))
; (define unchurch church->nat)
; (define v (eval prog (make-base-namespace)))
; (with-output-to-file "answer"
;   (lambda ()
;     (print v))
;   #:exists 'replace)

; (define compiled (church-compile prog))
; (define cv-comp (eval compiled (make-base-namespace)))
; (define v-comp (unchurch cv-comp))
; (with-output-to-file "output"
;   (lambda ()
;     (print v-comp))
;   #:exists 'replace)
; (print v-comp)  

; arith 0
;working

; (define prog '(+ 1 (add1 (* 3 3))))

; (define unchurch church->nat)

; (define v (eval prog (make-base-namespace)))
; (with-output-to-file "answer"
;   (lambda ()
;     (print v))
;   #:exists 'replace)

; (define compiled (church-compile prog))
; (define cv-comp (eval compiled (make-base-namespace)))
; (define v-comp (unchurch cv-comp))
; (with-output-to-file "output"
;   (lambda ()
;     (print v-comp))
;   #:exists 'replace)

; (print v-comp)


;arith1 working
; (define prog '(* (+ (add1 0) (* 1 (* 2 2))) 3))

; (define unchurch church->nat)

; (define v (eval prog (make-base-namespace)))
; (with-output-to-file "answer"
;   (lambda ()
;     (print v))
;   #:exists 'replace)

; (define compiled (church-compile prog))
; (define cv-comp (eval compiled (make-base-namespace)))
; (define v-comp (unchurch cv-comp))
; (with-output-to-file "output"
;   (lambda ()
;     (print v-comp))
;   #:exists 'replace)

; (print v-comp)
;bool0
(define prog '#f)

(define unchurch church->bool)

; (print "Value of prog before compilation:")
; (print prog)

(define compiled (church-compile prog))

; (print "Value of compiled program:")
; (print compiled)

(define cv-comp (eval compiled (make-base-namespace)))
(define v-comp (unchurch cv-comp))
(with-output-to-file "output"
  (lambda ()
    (print v-comp))
  #:exists 'replace)
(print v-comp)