;; ** The Picky interpreter, verbose version

#lang pl

#|
The grammar:
  <PICKY> ::= <num>
            | <id>
            | { + <PICKY> <PICKY> }
            | { - <PICKY> <PICKY> }
            | { = <PICKY> <PICKY> }
            | { < <PICKY> <PICKY> }
            | { fun { <id> : <TYPE> } : <TYPE> <PICKY> }
            | { call <PICKY> <PICKY> }
            | { with { <id> : <TYPE> <PICKY> } <PICKY> }
            | { if <PICKY> <PICKY> <PICKY> }
  <TYPE>  ::= Num | Number
            | Bool | Boolean
            | { <TYPE> -> <TYPE> }

Evaluation rules:
  eval(N,env)                = N
  eval(x,env)                = lookup(x,env)
  eval({+ E1 E2},env)        = eval(E1,env) + eval(E2,env)
  eval({- E1 E2},env)        = eval(E1,env) - eval(E2,env)
  eval({= E1 E2},env)        = eval(E1,env) = eval(E2,env)
  eval({< E1 E2},env)        = eval(E1,env) < eval(E2,env)
  eval({fun {x} E},env)      = <{fun {x} E}, env>
  eval({call E1 E2},env1)    = eval(B,extend(x,eval(E2,env1),env2))
                              if eval(E1,env1) = <{fun {x} B}, env2>
                             = error!  otherwise <-- never happens
  eval({with {x E1} E2},env) = eval(E2,extend(x,eval(E1,env),env))
  eval({if E1 E2 E3},env)    = eval(E2,env)  if eval(E1,env) is true
                             = eval(E3,env)  otherwise

Type checking rules:

  Γ ⊢ n : Number

  Γ ⊢ x : Γ(x)

  Γ ⊢ A : Number   Γ ⊢ B : Number
  ———————————————————————————————
       Γ ⊢ {+ A B} : Number

  Γ ⊢ A : Number   Γ ⊢ B : Number
  ———————————————————————————————
       Γ ⊢ {< A B} : Boolean

            Γ[x:=τ₁] ⊢ E : τ₂
  ——————————————————————————————————————
  Γ ⊢ {fun {x : τ₁} : τ₂ E} : (τ₁ -> τ₂)

  Γ ⊢ F : (τ₁ -> τ₂)  Γ ⊢ V : τ₁
  ——————————————————————————————
       Γ ⊢ {call F V} : τ₂

  Γ ⊢ V : τ₁   Γ[x:=τ₁] ⊢ E : τ₂
  ——————————————————————————————
   Γ ⊢ {with {x : τ₁ V} E} : τ₂

  Γ ⊢ C : Boolean   Γ ⊢ T : τ   Γ ⊢ E : τ
  ———————————————————————————————————————
            Γ ⊢ {if C T E} : τ

|#

(define-type PICKY
  [Num   Number]
  [Id    Symbol]
  [Add   PICKY PICKY]
  [Sub   PICKY PICKY]
  [Equal PICKY PICKY]
  [Less  PICKY PICKY]
  [Fun   Symbol TYPE PICKY TYPE] ; name, in-type, body, out-type
  [Call  PICKY PICKY]
  [With  Symbol TYPE PICKY PICKY]
  [If    PICKY PICKY PICKY])

(define-type TYPE
  [NumT]
  [BoolT]
  [FunT TYPE TYPE])

(: parse-sexpr : Sexpr -> PICKY)
;; parses s-expressions into PICKYs
(define (parse-sexpr sexpr)
  (match sexpr
    [(number: n)    (Num n)]
    [(symbol: name) (Id name)]
    [(list '+ lhs rhs) (Add   (parse-sexpr lhs) (parse-sexpr rhs))]
    [(list '- lhs rhs) (Sub   (parse-sexpr lhs) (parse-sexpr rhs))]
    [(list '= lhs rhs) (Equal (parse-sexpr lhs) (parse-sexpr rhs))]
    [(list '< lhs rhs) (Less  (parse-sexpr lhs) (parse-sexpr rhs))]
    [(list 'call fun arg)
                       (Call  (parse-sexpr fun) (parse-sexpr arg))]
    [(list 'if c t e)
     (If (parse-sexpr c) (parse-sexpr t) (parse-sexpr e))]
    [(cons 'fun more)
     (match sexpr
       [(list 'fun (list (symbol: name) ': itype) ': otype body)
        (Fun name
             (parse-type-sexpr itype)
             (parse-sexpr body)
             (parse-type-sexpr otype))]
       [else (error 'parse-sexpr "bad `fun' syntax in ~s" sexpr)])]
    [(cons 'with more)
     (match sexpr
       [(list 'with (list (symbol: name) ': type named) body)
        (With name
              (parse-type-sexpr type)
              (parse-sexpr named)
              (parse-sexpr body))]
       [else (error 'parse-sexpr "bad `with' syntax in ~s" sexpr)])]
    [else (error 'parse-sexpr "bad expression syntax: ~s" sexpr)]))

(: parse-type-sexpr : Sexpr -> TYPE)
;; parses s-expressions into TYPEs
(define (parse-type-sexpr sexpr)
  (match sexpr
    ['Number  (NumT)]
    ['Boolean (BoolT)]
    ;; allow shorter names too
    ['Num  (NumT)]
    ['Bool (BoolT)]
    [(list itype '-> otype)
     (FunT (parse-type-sexpr itype) (parse-type-sexpr otype))]
    [else (error 'parse-type-sexpr "bad type syntax in ~s" sexpr)]))

(: parse : String -> PICKY)
;; parses a string containing a PICKY expression to a PICKY AST
(define (parse str)
  (parse-sexpr (string->sexpr str)))

;; Typechecker and related types and helpers

;; this is similar to ENV, but it holds type information for the
;; identifiers during typechecking; it is essentially "Γ"
(define-type TYPEENV
  [EmptyTypeEnv]
  [ExtendTypeEnv Symbol TYPE TYPEENV])

(: type-lookup : Symbol TYPEENV -> TYPE)
;; similar to `lookup' for type environments; note that the
;; error is phrased as a typecheck error, since this indicates
;; a failure at the type checking stage
(define (type-lookup name typeenv)
  (cases typeenv
    [(EmptyTypeEnv) (error 'typecheck "no binding for ~s" name)]
    [(ExtendTypeEnv id type rest-env)
     (if (eq? id name) type (type-lookup name rest-env))]))

(: typecheck : PICKY TYPE TYPEENV -> Void)
;; Checks that the given expression has the specified type.
;; Used only for side-effects (to throw a type error), so return
;; a void value.
(define (typecheck expr type type-env)
  (unless (equal? type (typecheck* expr type-env))
    (error 'typecheck "type error for ~s: expecting a ~s"
           expr type)))

(: typecheck* : PICKY TYPEENV -> TYPE)
;; Returns the type of the given expression (which also means that
;; it checks it). This is a helper for the real typechecker that
;; also checks a specific return type.
(define (typecheck* expr type-env)
  (: two-nums : PICKY PICKY -> Void)
  (define (two-nums e1 e2)
    (typecheck e1 (NumT) type-env)
    (typecheck e2 (NumT) type-env))
  (cases expr
    [(Num n) (NumT)]
    [(Id name) (type-lookup name type-env)]
    [(Add   l r) (two-nums l r) (NumT)]
    [(Sub   l r) (two-nums l r) (NumT)]
    [(Equal l r) (two-nums l r) (BoolT)]
    [(Less  l r) (two-nums l r) (BoolT)]
    [(Fun bound-id in-type bound-body out-type)
     (typecheck bound-body out-type
                (ExtendTypeEnv bound-id in-type type-env))
     (FunT in-type out-type)]
    [(Call fun arg)
     (cases (typecheck* fun type-env)
       [(FunT in-type out-type)
        (typecheck arg in-type type-env)
        out-type]
       [else (error 'typecheck "type error for ~s: expecting a fun"
                    expr)])]
    [(With bound-id itype named-expr bound-body)
     (typecheck named-expr itype type-env)
     (typecheck* bound-body
                 (ExtendTypeEnv bound-id itype type-env))]
    [(If cond-expr then-expr else-expr)
     (typecheck cond-expr (BoolT) type-env)
     (let ([type (typecheck* then-expr type-env)])
       (typecheck else-expr type type-env) ; enforce same type
       type)]))

;; Evaluator and related types and helpers

(define-type ENV
  [EmptyEnv]
  [Extend Symbol VAL ENV])

(define-type VAL
  [NumV  Number]
  [BoolV Boolean]
  [FunV  Symbol PICKY ENV])

(: lookup : Symbol ENV -> VAL)
;; lookup a symbol in an environment, return its value or throw an
;; error if it isn't bound
(define (lookup name env)
  (cases env
    [(EmptyEnv) (error 'lookup "no binding for ~s" name)]
    [(Extend id val rest-env)
     (if (eq? id name) val (lookup name rest-env))]))

(: strip-numv : Symbol VAL -> Number)
;; converts a VAL to a Racket number if possible, throws an error if
;; not using the given name for the error message
(define (strip-numv name val)
  (cases val
    [(NumV n) n]
    ;; this error will never be reached, see below for more
    [else (error name "expected a number, got: ~s" val)]))

(: arith-op : (Number Number -> Number) VAL VAL -> VAL)
;; gets a Racket numeric binary operator, and uses it within a NumV
;; wrapper
(define (arith-op op val1 val2)
  (NumV (op (strip-numv 'arith-op val1)
            (strip-numv 'arith-op val2))))

(: bool-op : (Number Number -> Boolean) VAL VAL -> VAL)
;; gets a Racket numeric binary predicate, and uses it
;; within a BoolV wrapper
(define (bool-op op val1 val2)
  (BoolV (op (strip-numv 'bool-op val1)
             (strip-numv 'bool-op val2))))

(: eval : PICKY ENV -> VAL)
;; evaluates PICKY expressions by reducing them to values
(define (eval expr env)
  (cases expr
    [(Num n) (NumV n)]
    [(Id name) (lookup name env)]
    [(Add   l r) (arith-op + (eval l env) (eval r env))]
    [(Sub   l r) (arith-op - (eval l env) (eval r env))]
    [(Equal l r) (bool-op  = (eval l env) (eval r env))]
    [(Less  l r) (bool-op  < (eval l env) (eval r env))]
    [(Fun bound-id in-type bound-body out-type)
     ;; note that types are not used at runtime,
     ;; so they're not stored in the closure
     (FunV bound-id bound-body env)]
    [(Call fun-expr arg-expr)
     (define fval (eval fun-expr env))
     (cases fval
       [(FunV bound-id bound-body f-env)
        (eval bound-body
              (Extend bound-id (eval arg-expr env) f-env))]
       ;; `cases' requires complete coverage of all variants, but
       ;; this `else' is never used since we typecheck programs
       [else (error 'eval "`call' expects a function, got: ~s"
                    fval)])]
    [(With bound-id type named-expr bound-body)
     (eval bound-body (Extend bound-id (eval named-expr env) env))]
    [(If cond-expr then-expr else-expr)
     (let ([bval (eval cond-expr env)])
       (if (cases bval
             [(BoolV b) b]
             ;; same as above: this case is never reached
             [else (error 'eval "`if' expects a boolean, got: ~s"
                                bval)])
         (eval then-expr env)
         (eval else-expr env)))]))

(: run : String -> Number)
;; evaluate a PICKY program contained in a string
(define (run str)
  (let ([prog (parse str)])
    (typecheck prog (NumT) (EmptyTypeEnv))
    (let ([result (eval prog (EmptyEnv))])
      (cases result
        [(NumV n) n]
        ;; this error is never reached, since we make sure
        ;; that the program always evaluates to a number above
        [else (error 'run "evaluation returned a non-number: ~s"
                          result)]))))

;; tests -- including translations of the FLANG tests
(test (run "5") => 5)
(test (run "{< 1 2}") =error> "type error")
(test (run "{fun {x : Num} : Num {+ x 1}}") =error> "type error")
(test (run "{call {fun {x : Num} : Num {+ x 1}} 4}") => 5)
(test (run "{with {x : Num 3} {+ x 1}}") => 4)
(test (run "{with {identity : {Num -> Num} {fun {x : Num} : Num x}}
              {call identity 1}}")
      => 1)
(test (run "{with {add3 : {Num -> Num}
                   {fun {x : Num} : Num {+ x 3}}}
              {call add3 1}}")
      => 4)
(test (run "{with {add3 : {Num -> Num}
                   {fun {x : Num} : Num {+ x 3}}}
              {with {add1 : {Num -> Num}
                     {fun {x : Num} : Num {+ x 1}}}
                {with {x : Num 3}
                  {call add1 {call add3 x}}}}}")
      => 7)
(test (run "{with {identity : {{Num -> Num} -> {Num -> Num}}
                   {fun {x : {Num -> Num}} : {Num -> Num} x}}
              {with {foo : {Num -> Num}
                     {fun {x : Num} : Num {+ x 1}}}
                {call {call identity foo} 123}}}")
      => 124)
(test (run "{with {x : Num 3}
              {with {f : {Num -> Num}
                     {fun {y : Num} : Num {+ x y}}}
                {with {x : Num 5}
                  {call f 4}}}}")
      => 7)
(test (run "{call {with {x : Num 3}
                    {fun {y : Num} : Num {+ x y}}}
                  4}")
      => 7)
(test (run "{with {f : {Num -> Num}
                   {with {x : Num 3} {fun {y : Num} : Num {+ x y}}}}
              {with {x : Num 100}
                {call f 4}}}")
      => 7)
(test (run "{call {call {fun {x : {Num -> {Num -> Num}}}
                             : {Num -> Num}
                          {call x 1}}
                        {fun {x : Num} : {Num -> Num}
                          {fun {y : Num} : Num {+ x y}}}}
                  123}")
      => 124)
(test (run "{call {fun {x : Num} : Num {if {< x 2} {+ x 5} {+ x 6}}}
                  1}")
      => 6)
(test (run "{call {fun {x : Num} : Num {if {< x 2} {+ x 5} {+ x 6}}}
                  2}")
      => 8)