aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stlc-ext.rkt37
-rw-r--r--stlc-rec.rkt17
2 files changed, 26 insertions, 28 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 45cd5bc..93e2dd8 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -40,10 +40,10 @@
[`(inl ,e) `(inl ,(interpret- e Γ))]
[`(inr ,e) `(inr ,(interpret- e Γ))]
- [`(case ,e ,f1 ,f2)
+ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
(match (interpret- e Γ)
- [`(inl ,e) (interpret- `(,f1 ,e) Γ)]
- [`(inr ,e) (interpret- `(,f2 ,e) Γ)]
+ [`(inl ,e) (interpret- e1 (dict-set Γ x1 e))]
+ [`(inr ,e) (interpret- e2 (dict-set Γ x2 e))]
[e (err (format "calling case on unknown expression ~a" e))])]
['nil 'nil]
@@ -83,7 +83,7 @@
[(n 'Nat) #:when (natural? n) #t]
[(b 'Bool) #:when (boolean? b) #t]
[(e `(,t1 ⊕ ,t2))
- (or (check- e t1 Γ) (check- e t2 Γ))]
+ (or (equiv? (infer- e Γ) with) (check- e t1 Γ) (check- e t2 Γ))]
[(x _) #:when (dict-has-key? Γ x)
(equiv? (dict-ref Γ x) with Γ Γ)]
@@ -115,12 +115,8 @@
(match (infer- e Γ)
[`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
[t #f])]
- [(`(case ,e ,f1 ,f2) with)
- (match* ((infer- f1 Γ) (infer- f2 Γ))
- [(`(,a1 → ,t1) `(,a2 → ,t2))
- (and (check- e `(,a1 ⊕ ,a2))
- (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))]
- [(t1 t2) #f])]
+ [(`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) with)
+ (equiv? with (infer- `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)]
[(`(,e : ,t) with)
(and (equiv? t with Γ Γ) (check- e t Γ))]
@@ -181,20 +177,21 @@
[`(,t1 × ,t2) t2]
[t (err (format "calling cdr on incorrect type ~a" t))])]
- [`(inl ,e)
+ [`(inl ,e) ; annotations necessary
(match (infer- e Γ)
- [`(,t1 ⊕ ,t2) t1]
+ [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)]
[t (err (format "calling inl on incorrect type ~a" t))])]
- [`(inr ,e)
+ [`(inr ,e) ; annotations necessary
(match (infer- e Γ)
- [`(,t1 ⊕ ,t2) t2]
+ [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)]
[t (err (format "calling inr on incorrect type ~a" t))])]
- [`(case ,e ,f1 ,f2)
- (match* ((infer- f1 Γ) (infer- f2 Γ))
- [(`(,a1 → ,t1) `(,a2 → ,t2))
- (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1
- (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))]
- [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])]
+ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (match (infer- e Γ)
+ [`(,a1 ⊕ ,a2)
+ (let ([b1 (infer- e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer- 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
(err (format "annotated expression ~a is not of annotated type ~a" e t)))]
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index e20b3c8..3d099c2 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -21,10 +21,11 @@
[n #:when (natural? n) n]
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
- [`(fold ,e) `(fold ,(interpret- e))]
+ [`(fold ,e) `(fold ,(interpret- e Γ))]
[`(unfold ,e)
- (match (interpret- e)
- [`(fold ,e) e] [e e])]
+ (match (interpret- e Γ)
+ [`(fold ,e) e]
+ [e `(unfold e)])]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(,e1 ,e2)
@@ -77,12 +78,12 @@
[`(fold (μ ,x ,t) ,e)
(if (check- 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)))))))]
+ (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)) (α-convert t #hash((x . `(μ ,x ,t))))
- (err (format ("expected ~a to be of type ~a, got ~a"
- e `(μ ,x ,t) (infer- e Γ)))))]
+ (if (check- e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
+ (err (format "expected ~a to be of type ~a, got ~a"
+ e `(μ ,x ,t) (infer- e Γ))))]
[`(λ (,x : ,t) ,e)
`(,t → ,(infer- e (dict-set Γ x t)))]