diff options
| -rw-r--r-- | stlc-ext.rkt | 138 | ||||
| -rw-r--r-- | stlc-fix.rkt | 42 | ||||
| -rw-r--r-- | stlc-imp.rkt | 45 | ||||
| -rw-r--r-- | stlc-let.rkt | 36 | ||||
| -rw-r--r-- | stlc-pred.rkt | 44 | ||||
| -rw-r--r-- | stlc-rec.rkt | 48 | ||||
| -rw-r--r-- | stlc-ref.rkt | 60 | ||||
| -rw-r--r-- | stlc.rkt | 12 |
8 files changed, 212 insertions, 213 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 93e2dd8..72490a2 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -7,9 +7,9 @@ ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption ;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()]) - (interpret- (strip (desugar expr)) Γ)) -(define (interpret- expr Γ) +(define (interpret expr) + (interpret-core (strip (desugar expr)) #hash())) +(define (interpret-core expr Γ) (match expr ['sole 'sole] [s #:when (string? s) s] @@ -18,64 +18,64 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(inc ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) [n #:when (natural? n) (+ n 1)] [e (format "incrementing an unknown value ~a" e)])] [`(if ,c ,e1 ,e2) - (match (interpret- c Γ) - ['#t (interpret- e1 Γ)] - ['#f (interpret- e2 Γ)] + (match (interpret-core c Γ) + ['#t (interpret-core e1 Γ)] + ['#f (interpret-core e2 Γ)] [e (err (format "calling if on unknown expression ~a" e))])] [`(pair ,e1 ,e2) - `(pair ,(interpret- e1 Γ) ,(interpret- e2 Γ))] + `(pair ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))] [`(car ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) [`(pair ,e1 ,e2) e1] [e (err (format "calling car on unknown expression ~a" e))])] [`(cdr ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) [`(pair ,e1 ,e2) e2] [e (err (format "calling cdr on unknown expression ~a" e))])] - [`(inl ,e) `(inl ,(interpret- e Γ))] - [`(inr ,e) `(inr ,(interpret- e Γ))] + [`(inl ,e) `(inl ,(interpret-core e Γ))] + [`(inr ,e) `(inr ,(interpret-core e Γ))] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (interpret- e Γ) - [`(inl ,e) (interpret- e1 (dict-set Γ x1 e))] - [`(inr ,e) (interpret- e2 (dict-set Γ x2 e))] + (match (interpret-core e Γ) + [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e))] + [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e))] [e (err (format "calling case on unknown expression ~a" e))])] ['nil 'nil] [`(nil? ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) ['nil '#t] [`(cons ,e1 ,e2) '#f] [e (err (format "calling isnil on unknown expression ~a" e))])] [`(cons ,e1 ,e2) - `(cons ,(interpret- e1 Γ) ,(interpret- e2 Γ))] + `(cons ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))] [`(head ,e) - (match (interpret- e Γ) - [`(cons ,e1 ,e2) (interpret- e1 Γ)] + (match (interpret-core e Γ) + [`(cons ,e1 ,e2) (interpret-core e1 Γ)] [e (err (format "calling head on unknown expression ~a" e))])] [`(tail ,e) - (match (interpret- e Γ) - [`(cons ,e1 ,e2) (interpret- e2 Γ)] + (match (interpret-core e Γ) + [`(cons ,e1 ,e2) (interpret-core e2 Γ)] [e (err (format "calling tail on unknown expression ~a" e))])] [`(λ ,x ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret- e1 Γ) + (match (interpret-core e1 Γ) [`(λ ,x ,e ,env) - (interpret- e (dict-set env x (interpret- e2 Γ)))] + (interpret-core e (dict-set env x (interpret-core e2 Γ)))] [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])] [e (err (format "interpreting an unknown expression ~a" e))])) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) (let ([with (expand with Γ)]) (match* (expr with) [('sole 'Unit) #t] @@ -83,67 +83,67 @@ [(n 'Nat) #:when (natural? n) #t] [(b 'Bool) #:when (boolean? b) #t] [(e `(,t1 ⊕ ,t2)) - (or (equiv? (infer- e Γ) with) (check- e t1 Γ) (check- e t2 Γ))] + (or (equiv? (infer-core e Γ) with) (check-core e t1 Γ) (check-core e t2 Γ))] [(x _) #:when (dict-has-key? Γ x) (equiv? (dict-ref Γ x) with Γ Γ)] [(`(type ,t1 ,t2 ,in) with) - (check- in with (dict-set Γ t1 t2))] + (check-core in with (dict-set Γ t1 t2))] [(`(inc ,e) 'Nat) - (check- e 'Nat Γ)] + (check-core e 'Nat Γ)] [(`(if ,c ,e1 ,e2) with) - (and (check- c 'Bool Γ) - (check- e1 with Γ) (check e2 with Γ))] + (and (check-core c 'Bool Γ) + (check-core e1 with Γ) (check e2 with Γ))] [(`(pair ,e1 ,e2) `(,t1 × ,t2)) - (and (check- e1 t1 Γ) (check- e2 t2 Γ))] + (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] [(`(car ,e) with) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(cdr ,e) with) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(inl ,e) with) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(inr ,e) with) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) with) - (equiv? with (infer- `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)] + (equiv? with (infer-core `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)] [(`(,e : ,t) with) - (and (equiv? t with Γ Γ) (check- e t Γ))] + (and (equiv? t with Γ Γ) (check-core e t Γ))] [('nil `(List ,t)) #t] [(`(cons ,f1 ,f2) `(List ,t)) - (and (check- f1 t Γ) (check- f2 `(List ,t) Γ))] + (and (check-core f1 t Γ) (check-core f2 `(List ,t) Γ))] [(`(head ,e) with) - (match (infer- e) + (match (infer-core e) [`(List ,t) (equiv? t with Γ Γ)] [t #f])] [(`(tail ,e) with) - (equiv? (infer- e Γ) with Γ Γ)] + (equiv? (infer-core e Γ) with Γ Γ)] [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) - (and (equiv? t t1 Γ Γ) (check- e t2 (dict-set Γ x t1)))] + (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))] + (and (equiv? t2 t Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))] [t #f])] [(e t) #f]))) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) (match expr ['sole 'Unit] [s #:when (string? s) 'Str] @@ -156,66 +156,66 @@ (infer in (dict-set Γ t1 t2))] [`(inc ,e) - (if (check- e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a" (infer- e Γ))))] + (if (check-core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))] [`(if ,c ,e1 ,e2) - (if (check- c 'Bool Γ) - (let ([t (infer- e1 Γ)]) - (if (check- e2 t Γ) t + (if (check-core c 'Bool Γ) + (let ([t (infer-core e1 Γ)]) + (if (check-core e2 t Γ) t (err (format "condition has branches of differing types ~a and ~a" - t (infer- e2 Γ))))) - (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))] + t (infer-core e2 Γ))))) + (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))] [`(pair ,e1 ,e2) - `(,(infer- e1 Γ) × ,(infer- e2 Γ))] + `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))] [`(car ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a" t))])] [`(cdr ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a" t))])] [`(inl ,e) ; annotations necessary - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] [t (err (format "calling inl on incorrect type ~a" t))])] [`(inr ,e) ; annotations necessary - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] [t (err (format "calling inr on incorrect type ~a" t))])] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer- e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer- e2 (dict-set Γ x2 (expand a2 Γ)))]) + (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))]) (if (equiv? b1 b2 Γ Γ) b1 (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] [t (err (format "calling case on incorrect type ~a" t))])] [`(,e : ,t) - (if (check- e t Γ) t + (if (check-core e t Γ) t (err (format "annotated expression ~a is not of annotated type ~a" e t)))] ['nil (err (format "unable to infer type of empty list!"))] [`(cons ,e1 ,e2) - (let ([t (infer- e1 Γ)]) - (if (check- e2 `(List ,t) Γ) `(List ,t) + (let ([t (infer-core e1 Γ)]) + (if (check-core e2 `(List ,t) Γ) `(List ,t) (err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))] [`(head ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(List ,t) t] [t (err (format "calling head on incorrect type ~a" t))])] [`(tail ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(List ,t) `(List ,t)] [t (err (format "calling tail on incorrect type ~a" t))])] [`(λ (,x : ,t) ,e) - `(,t → ,(infer- e (dict-set Γ x t)))] + `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check- e2 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))])] diff --git a/stlc-fix.rkt b/stlc-fix.rkt index cb6a592..e8f15e6 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -4,35 +4,35 @@ ;; The Simply-Typed Lambda Calculus, with general recursion ;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()]) - (interpret- (strip (desugar expr)) Γ)) -(define (interpret- expr Γ) +(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)] [`(fix ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) [`(λ ,x ,e ,env) ; FIXME: unsure what should be Γ and what should be env - (interpret- e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))] + (interpret-core e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))] [e (err (format "applying fix to unknown expression ~a" e))])] [`(λ ,id ,body) `(λ ,id ,body ,Γ)] [`(λ ,id ,body ,env) `(λ ,id ,body ,env)] [`(,body ,arg) - (match (interpret- body Γ) + (match (interpret-core body Γ) [`(λ ,id ,body ,env) - (interpret- body (dict-set env id (interpret- arg Γ)))] + (interpret-core body (dict-set env id (interpret-core arg Γ)))] [e (err (format "applying arg ~a to unknown expression ~a" arg e))])] [e (err (format "interpreting an unknown expression ~a" e))])) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) (match* (expr with) [('sole 'Unit) #t] @@ -41,22 +41,22 @@ (equal? (dict-ref Γ x) with)] [(`(fix ,e) with) - (check- (infer- e) `(,with → ,with) Γ)] + (check-core (infer-core e) `(,with → ,with) Γ)] [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) - (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f]))) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] @@ -64,16 +64,16 @@ (dict-ref Γ x)] [`(fix ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(,t → ,t) t] [t (err (format "fix expects a term of type t → t, got ~a" t))])] [`(λ (,x : ,t) ,e) - `(,t → ,(infer- e (dict-set Γ x t)))] + `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check- e2 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))])] diff --git a/stlc-imp.rkt b/stlc-imp.rkt index e10b09c..541de2c 100644 --- a/stlc-imp.rkt +++ b/stlc-imp.rkt @@ -28,41 +28,40 @@ (require (only-in "stlc-ref.rkt" interpret)) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) - ; (check- expr (dict-ref Γ with) Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) (match* (expr with) [('sole 'Unit) #t] [(n 'Nat) #:when (natural? n) #t] [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check- e t Γ)] - [(`(! ,e) t) (check- e `(Ref ,t) Γ)] + [(`(new ,e) `(Ref ,t)) (check-core e t Γ)] + [(`(! ,e) t) (check-core e `(Ref ,t) Γ)] [(`(set ,e1 ,e2) 'Unit) - (match (infer- e1 Γ) - [`(Ref ,t) (check- e2 t Γ)] + (match (infer-core e1 Γ) + [`(Ref ,t) (check-core e2 t Γ)] [t #f])] [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equal? t t1) (> k (max-level e (dict-set Γ x t1) t1 t2)) ; KNOB - (check- e t2 (dict-set Γ x t1)))] + (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) (and (equal? t2 t) - (equal? t1 (infer- e2 Γ)))] + (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] @@ -70,28 +69,28 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(new ,e) `(Ref ,(infer- e Γ))] + [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(Ref ,t) - (if (check- e2 t Γ) 'Unit + (if (check-core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer- e2 Γ))))] + e1 t e2 (infer-core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer- e (dict-set Γ x t1))]) + (let ([t2 (infer-core e (dict-set Γ x t1))]) (let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))]) ; KNOB `(,t1 → ,k ,t2)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (if (check- e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))] + (if (check-core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) diff --git a/stlc-let.rkt b/stlc-let.rkt index edf39a7..3c4fef0 100644 --- a/stlc-let.rkt +++ b/stlc-let.rkt @@ -4,50 +4,50 @@ ;; The Simply-Typed Lambda Calculus, with let sugar and some base types ;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()]) - (interpret- (strip (desugar expr)) Γ)) -(define (interpret- expr Γ) +(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- e1 Γ) - [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 Γ)))] - [e1 `(,e1 ,(interpret- 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 [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) (match* (expr with) [('sole 'Unit) #t] [(n 'Nat) #:when (natural? n) #t] [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) - (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) - [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (match (infer-core e1 Γ) + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] [`(λ (,x : ,t) ,e) - `(,t → ,(infer- e (dict-set Γ x t)))] + `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check- e2 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))])) diff --git a/stlc-pred.rkt b/stlc-pred.rkt index d13e60d..c9c77b6 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -25,9 +25,9 @@ (require (only-in "stlc-ref.rkt" interpret)) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) [('sole 'Unit) #t] @@ -35,30 +35,30 @@ [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check- e t Γ)] - [(`(! ,e) t) (check- e `(Ref ,t) Γ)] + [(`(new ,e) `(Ref ,t)) (check-core e t Γ)] + [(`(! ,e) t) (check-core e `(Ref ,t) Γ)] [(`(set ,e1 ,e2) 'Unit) - (match (infer- e1 Γ) - [`(Ref ,t) (check- e2 t Γ)] + (match (infer-core e1 Γ) + [`(Ref ,t) (check-core e2 t Γ)] [t #f])] [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equal? t t1) (>= k (max-level e (dict-set Γ x t1) t1 t2)) ; (KNOB) - (check- e t2 (dict-set Γ x t1)))] + (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] @@ -66,28 +66,28 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(new ,e) `(Ref ,(infer- e Γ))] + [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(Ref ,t) - (if (check- e2 t Γ) 'Unit + (if (check-core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer- e2 Γ))))] + e1 t e2 (infer-core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer- e (dict-set Γ x t1))]) + (let ([t2 (infer-core e (dict-set Γ x t1))]) (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB) `(,t1 → ,k ,t2)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (if (check- e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))] + (if (check-core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) diff --git a/stlc-rec.rkt b/stlc-rec.rkt index 3d099c2..8819116 100644 --- a/stlc-rec.rkt +++ b/stlc-rec.rkt @@ -13,33 +13,33 @@ ; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t ;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()]) - (interpret- (strip (desugar expr)) Γ)) -(define (interpret- expr Γ) +(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)] - [`(fold ,e) `(fold ,(interpret- e Γ))] + [`(fold ,e) `(fold ,(interpret-core e Γ))] [`(unfold ,e) - (match (interpret- e Γ) + (match (interpret-core e Γ) [`(fold ,e) e] [e `(unfold e)])] [`(λ ,x ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret- e1 Γ) + (match (interpret-core e1 Γ) [`(λ ,x ,e ,env) - (interpret- e (dict-set env x (interpret- e2 Γ)))] + (interpret-core e (dict-set env x (interpret-core e2 Γ)))] [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])] [e (err (format "interpreting an unknown expression ~a" e))])) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) [('sole 'Unit) #t] @@ -48,26 +48,26 @@ (equal? (dict-ref Γ x) with)] [(`(fold (μ ,x ,t) ,e) `(μ ,x ,t)) - (check- e t (dict-set Γ x `(μ ,x ,t)))] + (check-core e t (dict-set Γ x `(μ ,x ,t)))] [(`(unfold (μ ,x ,t) ,e) with) - (and (check- e `(μ ,x ,t) Γ) + (and (check-core e `(μ ,x ,t) Γ) (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))] [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) - (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] @@ -77,21 +77,21 @@ (dict-ref Γ x)] [`(fold (μ ,x ,t) ,e) - (if (check- e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t) + (if (check-core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t) (err (format "expected ~a to be of type ~a, got ~a" e t (infer e (dict-set Γ x `(μ ,x ,t))))))] [`(unfold (μ ,x ,t) ,e) - (if (check- e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) + (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) (err (format "expected ~a to be of type ~a, got ~a" - e `(μ ,x ,t) (infer- e Γ))))] + e `(μ ,x ,t) (infer-core e Γ))))] [`(λ (,x : ,t) ,e) - `(,t → ,(infer- e (dict-set Γ x t)))] + `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check- e2 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))])] diff --git a/stlc-ref.rkt b/stlc-ref.rkt index b025309..f054d4e 100644 --- a/stlc-ref.rkt +++ b/stlc-ref.rkt @@ -4,9 +4,9 @@ ;; The Simply-Typed Lambda Calculus with references ;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()] [Σ (make-hash)]) - (interpret- (strip (desugar expr)) Γ Σ)) -(define (interpret- expr Γ Σ) +(define (interpret expr) + (interpret-core (strip (desugar expr)) #hash() (make-hash))) +(define (interpret-core expr Γ Σ) ; (print (format "interpret: ~a" (fmt expr))) (match expr ['sole 'sole] @@ -18,30 +18,30 @@ (let ([r (gensym)]) (dict-set! Σ r e) r)] [`(! ,e) - (let ([r (interpret- e Γ Σ)]) + (let ([r (interpret-core e Γ Σ)]) (if (dict-has-key? Σ r) - (interpret- (dict-ref Σ r) Γ Σ) + (interpret-core (dict-ref Σ r) Γ Σ) (err (format "attempting to deref unknown reference ~a" r))))] [`(set ,e1 ,e2) - (let ([r (interpret- e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret- e2 Γ Σ)) + (let ([r (interpret-core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ)) (err (format "attempting to update unknown reference ~a" r)))) 'sole] [`(λ ,x ,e) `(λ ,x ,e ,Γ)] [`(λ ,x ,e ,env) `(λ ,x ,e ,env)] ; ??? [`(,e1 ,e2) - (match (interpret- e1 Γ Σ) + (match (interpret-core e1 Γ Σ) [`(λ ,x ,e1 ,env) - (interpret- e1 (dict-set env x (interpret- e2 Γ Σ)) Σ)] + (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)] [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])] [e (err (format "attempting to interpret unknown expression ~a" e))])) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) [('sole 'Unit) #t] @@ -49,27 +49,27 @@ [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check- e t Γ)] - [(`(! ,e) t) (check- e `(Ref ,t) Γ)] + [(`(new ,e) `(Ref ,t)) (check-core e t Γ)] + [(`(! ,e) t) (check-core e `(Ref ,t) Γ)] [(`(set ,e1 ,e2) 'Unit) - (match (infer- e1 Γ) - [`(Ref ,t) (check- e2 t Γ)] + (match (infer-core e1 Γ) + [`(Ref ,t) (check-core e2 t Γ)] [t #f])] [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) - (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] @@ -77,25 +77,25 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(new ,e) `(Ref ,(infer- e Γ))] + [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(Ref ,t) - (if (check- e2 t Γ) 'Unit + (if (check-core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer- e2 Γ))))] + e1 t e2 (infer-core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t) ,e) - `(,t → ,(infer- e (dict-set Γ x t)))] + `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check- e2 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))])] @@ -4,16 +4,16 @@ ;; The Simply-Typed Lambda Calculus ;; (interpret Expr Table[Sym, Expr]): Value -(define (interpret expr [Γ #hash()]) - (interpret- (strip expr) Γ)) -(define (interpret- expr Γ) +(define (interpret expr) + (interpret-core (strip expr) #hash())) +(define (interpret-core expr Γ) (match expr [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(λ ,x ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret- e1 Γ) - [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 Γ)))] - [e `(,e ,(interpret- e2 Γ))])] + (match (interpret-core e1 Γ) + [`(λ ,x ,e ,env) (interpret-core e (dict-set env x (interpret-core e2 Γ)))] + [e `(,e ,(interpret-core e2 Γ))])] [e e])) ;; (check Expr Type Table[Sym, Type]): Bool |