;; 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?)]
  [amb (e1 FAE?) (e2 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?)])

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

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

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

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

(define (bindList f g)
  (foldl append empty (map g f)))

(define (returnList x) (list x))

(define (bind f g) 
  (bindList f (lambda (a) 
                (type-case Maybe a 
                           [Success (v) (g v)]
                           [Error (msg) (returnList (Error msg))]))))

(define (return x) (returnList (returnMaybe x)))

(define (liftMaybe x) (returnList 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 '())
      (liftMaybe (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))))]
    [amb (e1 e2)
         (append (interp e1 env) (interp e2 env))]))
   
; 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 
  (add (amb (num 2) (num 3)) (amb (num 5) (num 6))))

(define test4 
  (add (amb (num 2) (id 'x)) (amb (num 5) (num 6))))

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