; Brian Alliet
; Programming Language Theory
; 4005-710-01

; Lexical spec and grammar for the lambda calculus format used in this assignment
(define lex-spec
    '((white-sp (whitespace) skip)
      (id ((or letter digit) (arbno (or letter digit "?" "-"))) symbol)))

(define grammar
    '((parsed-prog ((arbno "$" id "=" parsed-expr) parsed-expr) parsed-prog_)
      (parsed-expr (id) parsed-var-expr)
      (parsed-expr ("(" parsed-pexpr ")") parsed-pexpr_)
      (parsed-pexpr ("lambda" "(" id ")" parsed-expr) parsed-lambda-expr)
      (parsed-pexpr (parsed-expr parsed-expr) parsed-app-expr)))
(sllgen:make-define-datatypes lex-spec grammar)
(define parse (sllgen:make-string-parser lex-spec grammar))

; inline-macors inlines all macros defined in dict in the parsed expression pe
(define (inline-macros dict pe)
    (let
        ((fix (lambda (sym) (or (lookup sym dict) (parsed-var-expr sym))))
         (inline (curry inline-macros dict)))
        (cases parsed-expr pe
            (parsed-var-expr (id) (fix id))
            (parsed-pexpr_ (ppe) (parsed-pexpr_ 
                (cases parsed-pexpr ppe
                    (parsed-lambda-expr (id body) (parsed-lambda-expr id (inline body)))
                    (parsed-app-expr (e1 e2) (parsed-app-expr (inline e1) (inline e2)))))))))

; fix-dict inlines all macros previously defined within the body of all subsequent macros
(define-match fix-dict
    ((cons x xs) (cons x (fix-dict (map (lambda-match ((cons k v) (cons k (inline-macros (list x) v)))) xs))))
    ('() '()))

; expand inlines all the macros in a parsed program and returns the resulting expressions
(define (expand p)
    (cases parsed-prog p
        (parsed-prog_ (names values body)
            (inline-macros (fix-dict (zip names values)) body))))

; We represent variable names as (name, subscript) pairs
; The subscript is used to generate unique names during alpha conversion
(define (varname n) (cons n 0))
(define-match (varname? x)
    ((cons n s) (and (symbol? n) (number? s)))
    (_ #f))

; This is our actual term data type, it is easier to work with than 
; the parsed-expr output by sllgen
(define-datatype term term?
    (var (v varname?)) ; variable
    (app (e1 term?) (e2 term?)); aplication
    (lam (id varname?) (body term?))); lambda

; convert a parsed expression to a lambda term
(define (pexpr->term pe)
    (cases parsed-expr pe
        (parsed-var-expr (id) (var (varname id)))
        (parsed-pexpr_ (ppe) (cases parsed-pexpr ppe
            (parsed-lambda-expr (id body) (lam (varname id) (pexpr->term body)))
            (parsed-app-expr (e1 e2) (app (pexpr->term e1) (pexpr->term e2)))))))

; Unparse a variable name. variables with subscripts use underscores            
(define-match unparse-var 
    ((cons n '0) n)
    ((cons n s) (string->symbol (string-append (symbol->string n) "_" (number->string s)))))

; Unparse a lambda expression (turn it back into nested lists)
(define (unparse t)
    (cases term t
        (var (v) (unparse-var v))
        (lam (v body) (list 'lambda (list (unparse-var v)) (unparse body)))
        (app (t1 t2) (list (unparse t1) (unparse t2)))))

; Main term evaluation function. This simply calls teval_ with an empty stack (see below)
(define (teval t) (teval_ t '()))

; The lambda term evaluator always evaluates one term at a time. When an
; application is encountered we evaluate the left side of the application 
; and push the right side to a stack so we can use it later

; When a lambda term is evaluated we first check the stack for a term
; If there is a term on the stack we pop it and, do a beta reduction, 
; and evaluate the resulting expression
; If the stack is empty we simply return the lambda expression after 
; evaluating its body (since we can't do beta reduction)

; If a variable term is evaluated we first check the stack for a term
; If there is a term on the stack we need to unwind the stack and 
; turn it back into a series of applicatoions. We can't do beta reduction 
; without a lambda expression. This will happen when  an expression's normal 
; form is an application. If the stack is empty then the variable is just 
; returned, it is in normal form

; I didn't come up with this technique. It is based on a lambda calculus
; evaluator by Oleg Kiselyov which I based a lambda calculus evaluator of
; my own on a while ago.

(define (teval_ t stack)
    (cases term t
        (var (name) (if (null? stack) t (unwind t stack)))
        (lam (v b)
            (if (null? stack)
                (lam v (teval b))
                (teval_ (subst b v (car stack)) (cdr stack))))
        (app (t1 t2) (teval_ t1 (cons t2 stack)))))

(define (unwind t stack)
    (if (null? stack)
        t
        (unwind (app t (teval (car stack))) (cdr stack))))

; The substitution function substitutes st for the variable v in the term t
(define (subst t v st)
    ; See if we can get off easy, if we're replacing with ourselves do nothing
    (or (cases term st (var (v_) (if (equal? v v_) t #f)) (else #f))
    (cases term t
        ; If the variable equals the one we're substituting return st, else t
        (var (x) (if (equal? x v) st t))
        ; Simply substitute both sides of the application
        (app (t1 t2) (app (subst t1 v st) (subst t2 v st)))
        ; If we're substituting for the variable bound by the lambda expression we're done
        ; (since it shadows the one we're substituting). If not things get messy...
        (lam (x body) (if (equal? x v) t
            (match
                ; Check if the bound variable occures in our substitution 
                (match (occures st x)
                    ; If not we can leave the bound variable and the body alone
                    ('#f (cons x body))
                    ; If it does we have to rename the bound variable (alpha conversion)
                    ; s is the highest subscript that appears on a variable with the same
                    ; name as x in st
                    (s (let*
                         ; The name of x, name of v, and subscript of v
                        ((xn (car x))
                         (vn (car v))
                         (vs (cdr v))
                         ; unique1 is a unique name for x within st and v
                         (unique1 (+ (if (eqv? vn xn) (max s vs) s) 1))
                         ; unique2 is a unique name for unique1 within the  body
                         (unique2 (match (occures body (cons xn unique1))
                             ('#f unique1) ; not in body, we're done
                             (s (+ (max s unique1) 1))))) ; if it is, increment the highest
                        ; Change x's subscript to unique2 and substitute for x in the body
                        (cons (cons xn unique2) (subst body x (var (cons xn unique2)))))))
                ; This is the result of the above two calls. Now we can substitute in the body
                ; and return the new lambda expression with a possibly renamed bound variable
                ((cons x_ body_) (lam x_ (subst body_ v st)))))))))

; easier to use wrapper around occures_ (below)
(define (occures t v)
    (match (occures_ t v)
        ((cons '#f _) #f)
        ((cons '#t s) s)))

; occures looks for a variable in a term. it returns if it was found, and if it was,
; the highest subscript of all variables with that name in the term
(define (occures_ t v)
    (cases term t
        (var (v_) (cond
            ; if it is a different name we didn't find it
            ((not (eqv? (car v) (car v_))) (cons #f (cdr v)))
            ; same name but different subscripts, take the highest, but still not found
            ((not (eqv? (cdr v) (cdr v_))) (cons #f (max (cdr v) (cdr v_))))
            ; same name, found, and with the same subscript
            (else (cons #t (cdr v)))))
        ; if a lambda shadows the name it wasn't found, else, look in body
        (lam (x body) (if (equal? x v) (cons #f (cdr v)) (occures_ body v)))
        ; Just get the union of the two sides of the application
        (app (t1 t2)
            (let
                ((r1 (occures_ t1 v))
                 (r2 (occures_ t2 v)))
                (cons (or (car r1) (car r2)) (max (cdr r1) (cdr r2)))))))

; To run a lambda expression parse it, expand it, make it a term, evaluate 
; it, and unparse the result
(define (run s) (unparse (teval (pexpr->term (expand (parse s))))))

; Some test data (they compute factorials in a few different ways)
(define test 
"(((lambda (true) (lambda (false) (((((lambda (and) (lambda (or) (lambda (not) (lambda (xor) ((lambda (equ) (((lambda (id) (lambda (const) ((((lambda (succ) (lambda (pred) (lambda (iszero) ((lambda (c0) ((lambda (c1) ((lambda (c2) ((lambda (c3) ((lambda (c4) ((lambda (c5) ((lambda (plus) ((lambda (mult) ((lambda (exp) ((lambda (y) ((lambda (fac) (fac c3)) (y (lambda (f) (lambda (x) (((iszero x) c1) ((mult x) (f (pred x))))))))) (lambda (g) ((lambda (x) (g (x x))) (lambda (x) (g (x x))))))) (lambda (m) (lambda (n) ((n (mult m)) c1))))) (lambda (m) (lambda (n) ((m (plus n)) c0))))) (lambda (m) (lambda (n) ((m succ) n))))) (succ c4))) (succ c3))) (succ c2))) (succ c1))) (succ c0))) (lambda (f) (lambda (x) x)))))) (lambda (n) (lambda (f) (lambda (x) (f ((n f) x)))))) (lambda (n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) (const x)) id))))) (lambda (n) ((n (lambda (x) false)) true))))) (lambda (x) x)) (lambda (x) (lambda (y) x)))) (lambda (p) (lambda (q) (not ((xor p) q))))))))) (lambda (p) (lambda (q) ((p q) false)))) (lambda (p) (lambda (q) ((p true) q)))) (lambda (p) ((p false) true))) (lambda (p) (lambda (q) ((p ((q false) true)) q)))))) (lambda (x) (lambda (y) x))) (lambda (x) (lambda (y) y)))"
)

(define test2
"(((lambda (g) ((lambda (x) (g (x x))) (lambda (x) (g (x x))))) (lambda (f) (lambda (x) ((((lambda (n) ((n (lambda (x) (lambda (x) (lambda (y) y)))) (lambda (x) (lambda (y) x)))) x) ((lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))) (lambda (f) (lambda (x) x)))) (((lambda (m) (lambda (n) ((m ((lambda (m) (lambda (n) ((m (lambda (n) (lambda (f) (lambda (x) (f ((n f) x)))))) n))) n)) (lambda (f) (lambda (x) x))))) x) (f ((lambda (n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) ((lambda (x) (lambda (y) x)) x)) (lambda (x) x))))) x))))))) ((lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))) ((lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))) (lambda (f) (lambda (x) x)))))"
)

(define test3
"$ true =  (lambda (x) (lambda (y) x)) $ false = (lambda (x) (lambda (y) y)) $ if-then-else = (lambda (cond) (lambda (then) (lambda (else) ((cond then) else)))) $ 0 = (lambda (f) (lambda (x) x)) $ 1 = (lambda (f) (lambda (x) (f x))) $ 2 = (lambda (f) (lambda (x) (f (f x)))) $ 3 = (lambda (f) (lambda (x) (f (f (f x))))) $ repeat = (lambda (n) (lambda (x) ((n (lambda (g) (g x))) (lambda (y) y)))) $ succ = (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))) $ pred = (lambda (n) (((n (lambda (p) (lambda (z) ((z (succ (p true))) (p true))))) (lambda (z) ((z 0) 0))) false)) $ sum = (lambda (m) (lambda (n) (lambda (f) (lambda (x) ((m f) ((n f) x)))))) $ product = (lambda (m) (lambda (n) (lambda (f) (m (n f))))) $ isZero = (lambda (n) ((n (lambda (x) false)) true)) $ g = (lambda (f) (lambda (n) (((if-then-else (isZero n)) 1) ((product n) (f (pred n)))))) $ ycomb = (lambda (y) ((lambda (x) (y (x x))) (lambda (x) (y (x x))))) $ factorial = (ycomb g) ((repeat (factorial 3)) hello)"
)