From 728d19a40871692ed4143852538997d596e86411 Mon Sep 17 00:00:00 2001
From: JJ
Date: Sun, 23 Jun 2024 21:15:05 -0700
Subject: stlc-ext, stlc-rec: backport bug fixes

---
 stlc-ext.rkt | 37 +++++++++++++++++--------------------
 stlc-rec.rkt | 17 +++++++++--------
 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)))]
-- 
cgit v1.2.3-70-g09d2