diff options
Diffstat (limited to 'stlc.rkt')
| -rw-r--r-- | stlc.rkt | 26 |
1 files changed, 12 insertions, 14 deletions
@@ -1,32 +1,32 @@ #lang racket (require "lib.rkt") +(require "base.rkt") +(provide interpret check infer) ;; The Simply-Typed Lambda Calculus -;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr) - (interpret-core (strip expr) #hash())) -(define (interpret-core expr Γ) - (match expr +;; (interpret Expr Context): Value +(define (interpret expr [Γ #hash()]) + (match (strip expr) [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(λ ,x ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret-core e1 Γ) - [`(λ ,x ,e ,env) (interpret-core e (dict-set env x (interpret-core e2 Γ)))] - [e `(,e ,(interpret-core e2 Γ))])] + (match (interpret e1 Γ) + [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))] + [e `(,e ,(interpret e2 Γ))])] [e e])) -;; (check Expr Type Table[Sym, Type]): Bool +;; (check Expr Type Context): Bool (define (check expr with [Γ #hash()]) (match expr [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equal? t t1) (check e t2 (dict-set Γ x)))] + (and (equal? t t1) (check e t2 (dict-set Γ x t)))] [_ #f])] - [_ (equal? (infer with Γ) with)])) + [_ (equal? with (infer with Γ))])) -;; (infer Expr Table[Sym, Type]): Type +;; (infer Expr Context): Type (define (infer expr [Γ #hash()]) (match expr [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] @@ -39,5 +39,3 @@ (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) - -(provide interpret check infer) |