;; ---< The Picky interpreter, verbose version >--- #lang pl #| The grammar: ::= | | { + } | { - } | { = } | { < } | { fun { : } : } | { call } | { with { : } } | { if } ::= Num | Number | Bool | Boolean | { -> } 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(Ef,extend(x,eval(E2,env1),env2)) if eval(E1,env1) = <{fun {x} Ef}, env2> = error! otherwise -- but this doesn't happen 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) ;; to convert 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 in ~s" sexpr)])) (: parse-type-sexpr : Sexpr -> TYPE) ;; to convert 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 (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 function" 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) (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] [else (error name "expects 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) (let ([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 is another error that 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 "{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 "{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 10} {+ x 20}}} 1}") => 11) (test (run "{call {fun {x : Num} : Num {if {< x 2} {+ x 10} {+ x 20}}} 2}") => 22)