diff options
author | JJ | 2024-07-29 19:47:19 +0000 |
---|---|---|
committer | JJ | 2024-07-29 19:47:19 +0000 |
commit | 83a1400957da57bf6930bab4b81af87f1851be5b (patch) | |
tree | ace9579033a9967893656e681ad938e8ac82f351 /stlc-let.rkt | |
parent | 17c9a9a1eb4b211b5b4260d7cdca598d14316ac3 (diff) |
split lib into lib and base; move tests to separate files & directory
Diffstat (limited to 'stlc-let.rkt')
-rw-r--r-- | stlc-let.rkt | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/stlc-let.rkt b/stlc-let.rkt deleted file mode 100644 index 089f9d0..0000000 --- a/stlc-let.rkt +++ /dev/null @@ -1,57 +0,0 @@ -#lang racket -(require "lib.rkt") - -;; The Simply-Typed Lambda Calculus, with let sugar and some base types - -;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr) - (interpret-core (strip (desugar expr)) #hash())) -(define (interpret-core expr Γ) - (match expr - ['sole 'sole] - [n #:when (natural? n) n] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret-core e1 Γ) - [`(λ ,x ,e1 ,env) (interpret-core e1 (dict-set env x (interpret-core e2 Γ)))] - [e1 `(,e1 ,(interpret-core e2 Γ))])] - [e e])) - -;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) - (match with - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] - [_ #f])] - [_ (equal? (infer-core expr Γ) with)])) - -;; (infer Expr Table[Sym, Type]): Type -(define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(λ (,x : ,t) ,e) - `(,t → ,(infer-core e (dict-set Γ x t)))] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (if (check-core e2 t1 Γ) t2 - (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) - -(require rackunit) -(check-equal? (interpret '(λ x x)) '(λ x x #hash())) -(check-equal? (interpret '((λ a a) (x y))) '(x y)) -(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y)) -(check-equal? (interpret '((λ a (a y)) x)) '(x y)) |