;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;        ARITHMETICAL LANGUAGE WITH             ;;
;;        FIRST CLASS FUNCTIONS                  ;;
;;        (call-by-name)                        ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#lang play

#|
<expr> ::= (num <num>)
         | (add <expr> <expr>)
         | (sub <expr> <expr>)
         | (if0 <expr> <expr> <expr>)
         | (id <id>)
         | (fun <sym> <expr>)
         | (app <expr> <expr>)
|#
;; Inductive type for representing (the abstract syntax
;; of) an aritmetical language with first-class functions
(deftype Expr
  (num n)
  (add l r)
  (sub l r)
  (if0 c t f)
  (id x)
  (fun arg body)
  (app f-name f-arg))



;; s-expressions used as concrete syntax for our programs
#|
<s-expr> ::= <num>
           | <sym>
           | (list '+  <s-expr> <s-expr>)
           | (list '-  <s-expr> <s-expr>)
           | (list 'if0  <s-expr> <s-expr> <s-expr>)
           | (list 'fun (list <sym>) <s-expr>)
           | (list <s-expr> <s-expr>)
           | (list 'with (list <sym> <s-expr>) <s-expr>)   <- syntactical sugar
|#

;; parse :: s-expr -> Expr
;; converts s-expressions into Exprs
(define (parse s-expr)
  (match s-expr
    [ n #:when (number? n) (num n) ]
    [ x #:when (symbol? x) (id x) ]
    [(list '+ l r) (add (parse l) (parse r))]
    [(list '- l r) (sub (parse l) (parse r))]
    [(list 'if0 c t f) (if0 (parse c) (parse t) (parse f))]
    [(list 'fun (list x) b) (fun x (parse b))]
    [(list f a) (app (parse f) (parse a))]    
    [(list 'with (list x e) b) #:when (symbol? x)
         (app (fun x (parse b)) (parse e))]))



;; Interface of the Abstract Dada Type (ADT) for  
;; representing idenfifier environments

;; empty-env  :: Env
;; extend-env :: Symbol Value Env -> Env
;; env-lookup :: Symbol Env -> Value

;; Implementation of the ADT

;; <env> ::= mtEnv
;;         | (aEnv <id> <value> <env>)
(deftype Env
  (mtEnv)
  (aEnv id val env))

(define empty-env (mtEnv))
 
(define extend-env aEnv)
 
(define (env-lookup x env)
  (match env
    [(mtEnv) (error 'env-lookup "free identifier: ~a" x)]
    [(aEnv id val rest) (if (symbol=? id x)
                            val
                            (env-lookup x rest))]))



;; <value> ::= (numV <number>)
;;          |  (closureV <sym> <Expr> <env>)
;;          |  (exprV <Expr> <env>

;; values of expressions
(deftype Value
  (numV n)
  (closureV id body env)
  (exprV expr env))

;; Auxiliary functions handling numeric values
(define (num+ n1 n2)
  (def (numV v1) n1) (def (numV v2) n2) (numV (+ v1 v2)))

(define (num- n1 n2)
  (def (numV v1) n1) (def (numV v2) n2) (numV (- v1 v2)))

(define (num-zero? n)
  (def (numV v) n) (zero? v))


;; Further reduces a Value to a numV or closureV
;; strict :: Value -> Value [without exprV]
(define (strict v)
  (match v
    [(exprV expr env) (strict (eval expr env))]
    [ _ v]))


;;; Further reduces a Value to a numV or closureV
;;; signaling the reduction
;;; strict :: Value -> Value [without exprV]
;(define (strict v)
;  (match v
;    [(exprV expr env)
;     (let ([val (strict (eval expr env))])
;       (printf "Forcing exprV to ~v~n" val)
;       val)]
;    [ _ v]))

;; eval :: Expr Env -> Value
;; evaluates an expression in a given
;; environment using static scoping 
(define (eval expr env)
  (match expr
    [(num n) (numV n)]
    [(fun id body) (closureV id body env)]
    [(id x) (env-lookup x env)]
    [(add l r) (num+ (strict (eval l env)) (strict (eval r env)))]
    [(sub l r) (num- (strict (eval l env)) (strict (eval r env)))]
    [(if0 c t f) (if  (num-zero? (strict (eval c env)))
                      (eval t env)
                      (eval f env))]
    [(app f e) (def (closureV the-arg the-body the-clos-env) (strict (eval f env)))
               (def the-ext-env (extend-env the-arg (exprV e env) the-clos-env))
               (eval the-body the-ext-env)]))


;; run :: s-expr -> value
;; evaluates an expression using static scoping 
(define (run prog)
  (strict (eval (parse prog) empty-env)))



;; some testing
(print-only-errors #t)
(define expr1 '(with (f (fun (y) y)) (f 4)))
(test (run expr1) (numV 4))
(define expr2 '(with (x 3)
                       (with (f (fun (y) (+ x y)))
                             (f 4))))
(test (run expr2) (numV 7))
(define expr3 '(with (x 3)
                       (with (f (fun (y) (+ x y)))
                             (with (x 5) (+ x (f 4))))))
(test (run expr3) (numV 12))
(define expr4 '(with (f (undef x)) 4))
(test (run expr4) (numV 4))