;; The first three lines of this file were inserted by DrScheme. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(planet plai/plai:1:6/lang/reader)
; Lecture Notes 
; Programming Languages and Types
; 
; Introduction to Monads

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-type FAE
  [num (n number?)]
  [add (lhs FAE?) (rhs FAE?)]
  [with (name symbol?) (named-expr FAE?) (body FAE?)]
  [id (name symbol?)]
  [fun (param symbol?) (body FAE?)]
  [app (fun-expr FAE?) (arg-expr FAE?)])

(define-type FAE-Value
  [numV (n number?)]
  [closureV (param symbol?) (body FAE?) (env Env?)])

(define-type Env
  [emptyEnv]
  [anEnv (name symbol?) (value FAE-Value?) (rest Env?)])

; we lift the lookup function into the Monad, too, such that
; we can signal an error by returning an Error value.

; lookup: symbol Env -> M FAE-Value
(define (lookup name env)
  (type-case Env env
    [emptyEnv () (Error (format "name not found:~s" name))]
    [anEnv (n value rest)
           (if (symbol=? n name)
               (return value)
               (lookup name rest))]))


; Let's define the interpreter

(define-type Maybe
  [Success (v any/c)]
  [Error (msg string?)])

; bind: M a -> (a -> M b) -> M b
(define (bind f g)
  (type-case Maybe f
     [Success (v) (g v)]
     [Error (m) f]))

; return : a -> M a
(define (return x) (Success x))

(define-syntax do
  (syntax-rules (<-)
    ((do expr              ) expr)
    ((do (v <- expr) . rest) (bind expr (lambda (v) (do . rest))))
    ((do expr        . rest) (bind expr (lambda (v) (do . rest)))))) 

(define (check b msg)
   (if b
      (return '())
      (Error msg)))

; interp: Expr Env -> M Value
(define (interp expr env)
  (type-case FAE expr
    [num (n) (return (numV n))]
    [add (l r) 
         (do 
           (lv <- (interp l env))
           (check (numV? lv) "lh operator must be a number")                 
           (rv <- (interp r env))
           (check (numV? rv) "rh operator must be a number")                 
           (return (numV (+ (numV-n lv) (numV-n rv)))))]    
    [id (v)  (lookup v env)]
    [fun (bound-id bound-body) (return (closureV bound-id bound-body env))]
    [with (n e body) (interp (app (fun n body) e) env)]
    [app (the-fun the-arg) 
         (do
           (f <- (interp the-fun env))
           (check (closureV? f) "operator must be a function")
           (a <- (interp the-arg env))
           (interp (closureV-body f)
                   (anEnv
                    (closureV-param f)
                    a
                    (closureV-env f))))]))

    ; Tests

(define test1 
  (with 'x (num 3)
         (with 'f (fun 'y (add (id 'x) (id 'y)))
               (with 'x (num 5)
                     (app (id 'f) (num 4))))))


(define test2 
  (with 'y (num 3)
         (with 'f (fun 'y (add (id 'x) (id 'y)))
               (with 'x (num 5)
                     (app (id 'f) (num 4))))))


(test (interp test1 (emptyEnv)) (Success (numV 7)))