From a8fa6eeb42fd0d119d3ce55f53c332da3df46db7 Mon Sep 17 00:00:00 2001
From: JJ
Date: Mon, 15 Jul 2024 18:17:18 -0700
Subject: backport check refactorings

---
 stlc-dll.rkt  |  45 +++++++++--------------
 stlc-ext.rkt  | 115 ++++++++++++++++++++++++++++++++--------------------------
 stlc-fix.rkt  |  25 +++++++------
 stlc-imp.rkt  |  45 +++++++++++++----------
 stlc-let.rkt  |  24 +++++++-----
 stlc-pred.rkt |  51 ++++++++++++++------------
 stlc-rec.rkt  |  47 ++++++++++++++----------
 stlc-ref.rkt  |  43 +++++++++++++---------
 stlc.rkt      |  20 ++++++----
 9 files changed, 227 insertions(+), 188 deletions(-)

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 83cc2c9..1bd82e9 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -1,5 +1,6 @@
 #lang racket
 (require "lib.rkt")
+(require (only-in "stlc-rec.rkt" replace))
 (require rackunit)
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
@@ -14,7 +15,6 @@
 (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]
     [n #:when (natural? n) n]
@@ -88,13 +88,12 @@
 (define (check expr with)
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
-  ; (print (format "check: ~a with ~a" (fmt expr) with))
   (match expr
     [`(type ,t1 ,t2 ,in)
       (check-core in with (dict-set Γ t1 t2))]
 
     [`(inc ,e)
-      (and (equiv? with 'Nat)
+      (and (equiv? 'Nat with)
         (check-core e 'Nat Γ))]
     [`(if ,c ,e1 ,e2)
       (and (check-core c 'Bool Γ)
@@ -103,42 +102,42 @@
     [`(pair ,e1 ,e2)
       (match with
         [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
-        [t #f])]
+        [_ #f])]
     [`(car ,e)
       (match (infer-core e Γ)
         [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
-        [t #f])]
+        [_ #f])]
     [`(cdr ,e)
       (match (infer-core e Γ)
         [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
-        [t #f])]
+        [_ #f])]
 
     [`(inl ,e)
       (match with
         [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
-        [t #f])]
+        [_ #f])]
     [`(inr ,e)
       (match with
         [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
-        [t #f])]
+        [_ #f])]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (match (infer-core e Γ)
         [`(,a1 ⊕ ,a2)
           (and (check-core e1 with (dict-set Γ x1 a1))
             (check-core e2 with (dict-set Γ x2 a2)))]
-        [t #f])]
+        [_ #f])]
 
     [`(new ,e)
       (match with
         [`(Ref ,t) (check-core e t Γ)]
-        [t #f])]
+        [_ #f])]
     [`(! ,e) (check-core e `(Ref ,with) Γ)]
     [`(set ,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(Ref ,t)
-          (and (equiv? with 'Unit Γ Γ)
+          (and (equiv? 'Unit with Γ Γ)
             (check-core e2 t Γ))]
-        [t #f])]
+        [_ #f])]
 
     ; [`(fold (μ ,x ,t) ,e)
     ;   (match with
@@ -147,23 +146,23 @@
     [`(fold ,e)
       (match with
         [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))]
-        [t #f])]
+        [_ #f])]
 
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,k ,t2)
           (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t))
             (> k (max-level e t1 t2 (dict-set Γ x t1))))] ; KNOB
-        [t #f])]
+        [_ #f])]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,_ ,t2)
-          (and (equiv? with t2 Γ Γ)
+          (and (equiv? t2 with Γ Γ)
             (check-core e2 t1 Γ))]
-        [t #f])]
+        [_ #f])]
 
 
-    [_ (equiv? with (infer-core expr Γ) Γ Γ)]))
+    [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
 
 ;; Checks if two expressions or types are equivalent, up to α-conversion,
 ;; given their respective contexts
@@ -203,7 +202,6 @@
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
-  ; (print (format "infer: ~a" (fmt expr)))
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
@@ -305,15 +303,6 @@
 (define (expand t Γ)
   (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t))
 
-(define (replace expr key value)
-  (match expr
-    ; do not accidentally replace shadowed bindings
-    [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_)
-      `(type ,x ,_ ,_)) #:when (equal? x key) expr]
-    [x #:when (equal? x key) value]
-    [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))]
-    [v v]))
-
 ;; Checks if a type is well-formed in the current context.
 ;;      (well-formed Type Context): Bool
 (define (well-formed t Γ)
@@ -322,7 +311,7 @@
     [(or 'Unit 'Nat 'Bool) #t]
     [`(Ref ,t) (well-formed t Γ)]
     [`(μ ,x ,t) (well-formed t (dict-set Γ x 'Unit))] ; todo: HACK
-    [(or `(,t1 → ,t2) `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+    [(or `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (and (well-formed t1 Γ) (well-formed t2 Γ))]
     [_ #f]))
 
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 72490a2..b11cb58 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -76,69 +76,82 @@
 (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]
-    [(s 'Str) #:when (string? s) #t]
-    [(n 'Nat) #:when (natural? n) #t]
-    [(b 'Bool) #:when (boolean? b) #t]
-    [(e `(,t1 ⊕ ,t2))
-      (or (equiv? (infer-core e Γ) with) (check-core e t1 Γ) (check-core e t2 Γ))]
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    ['sole (equal? 'Unit with)]
+    [s #:when (string? s) (equal? 'Str with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [b #:when (boolean? b) (equal? 'Bool with)]
+
+    [x #:when (dict-has-key? Γ x)
       (equiv? (dict-ref Γ x) with Γ Γ)]
 
-    [(`(type ,t1 ,t2 ,in) with)
+    [`(type ,t1 ,t2 ,in)
       (check-core in with (dict-set Γ t1 t2))]
 
-    [(`(inc ,e) 'Nat)
-      (check-core e 'Nat Γ)]
-    [(`(if ,c ,e1 ,e2) with)
+    [`(inc ,e)
+      (and (equiv? 'Nat with)
+        (check-core e 'Nat Γ))]
+    [`(if ,c ,e1 ,e2)
       (and (check-core c 'Bool Γ)
-        (check-core e1 with Γ) (check e2 with Γ))]
+        (check-core e1 with Γ) (check-core e2 with Γ))]
 
-    [(`(pair ,e1 ,e2) `(,t1 × ,t2))
-      (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
-    [(`(car ,e) with)
+    [`(pair ,e1 ,e2)
+      (match with
+        [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+        [_ #f])]
+    [`(car ,e)
       (match (infer-core e Γ)
         [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
-        [t #f])]
-    [(`(cdr ,e) with)
+        [_ #f])]
+    [`(cdr ,e)
       (match (infer-core e Γ)
         [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
-        [t #f])]
+        [_ #f])]
 
-    [(`(inl ,e) with)
+    [`(inl ,e)
       (match (infer-core e Γ)
         [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
-        [t #f])]
-    [(`(inr ,e) with)
+        [_ #f])]
+    [`(inr ,e)
       (match (infer-core e Γ)
         [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
-        [t #f])]
-    [(`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) with)
-      (equiv? with (infer-core `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)]
-    [(`(,e : ,t) with)
+        [_ #f])]
+    [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+      (match (infer-core e Γ)
+        [`(,a1 ⊕ ,a2)
+          (and (check-core e1 with (dict-set Γ x1 a1))
+            (check-core e2 with (dict-set Γ x2 a2)))]
+        [_ #f])]
+    [`(,e : ,t)
       (and (equiv? t with Γ Γ) (check-core e t Γ))]
 
-    [('nil `(List ,t)) #t]
-    [(`(cons ,f1 ,f2) `(List ,t))
-      (and (check-core f1 t Γ) (check-core f2 `(List ,t) Γ))]
-    [(`(head ,e) with)
+    ['nil
+      (match with
+        [`(List ,t) #t]
+        [_ #f])]
+    [`(cons ,f1 ,f2)
+      (match with
+        [`(List ,t) (and (check-core f1 t Γ) (check-core f2 `(List ,t) Γ))]
+        [_ #f])]
+    [`(head ,e)
       (match (infer-core e)
         [`(List ,t) (equiv? t with Γ Γ)]
-        [t #f])]
-    [(`(tail ,e) with)
+        [_ #f])]
+    [`(tail ,e)
       (equiv? (infer-core e Γ) with Γ Γ)]
 
-    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
-      (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equiv? t1 t Γ Γ) (check-core e t2 (dict-set Γ x t1)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
-          (and (equiv? t2 t Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))]
-        [t #f])]
+          (and (equiv? t2 with Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))]
+        [_ #f])]
 
-    [(e t) #f])))
+    [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -150,10 +163,13 @@
     [n #:when (natural? n) 'Nat]
     [b #:when (boolean? b) 'Bool]
     [x #:when (dict-has-key? Γ x)
-      (dict-ref Γ x)]
+      (expand (dict-ref Γ x) Γ)]
 
     [`(type ,t1 ,t2 ,in)
-      (infer in (dict-set Γ t1 t2))]
+      (infer-core in (dict-set Γ t1 t2))]
+    [`(,e : ,t)
+      (if (check-core e (expand t Γ) Γ) (expand t Γ)
+        (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
     [`(inc ,e)
       (if (check-core e 'Nat Γ) 'Nat
@@ -192,9 +208,6 @@
             (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-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)
@@ -211,7 +224,7 @@
         [t (err (format "calling tail on incorrect type ~a" t))])]
 
     [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer-core e (dict-set Γ x t)))]
+      `(,(expand t Γ) → ,(infer-core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
@@ -222,16 +235,16 @@
     [e (err (format "inferring an unknown expression ~a" e))]))
 
 (define (expand t Γ)
-  (if (dict-has-key? Γ t) (dict-ref Γ t) t))
+  (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t))
 
 ;; checks if two expressions are equivalent up to α-renaming and ascryption
-(define (equiv? e1 e2 [Γ1 #hash()] [Γ2 #hash()])
+(define (equiv? e1 e2 Γ1 Γ2)
   (match* (e1 e2)
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
       (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
       (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)]
-    [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) ; todo: merge these into one
+    [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2))
       (let ([name gensym])
       (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
         (equiv? t1 t2 Γ1 Γ2)))]
@@ -241,10 +254,10 @@
     [(`(,l1 ...) `(,l2 ...))
       (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
-(check-true (equiv? '(λ a a) '(λ b b)))
-(check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b))))
-(check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b)))))))
 
+(check-true (equiv? '(λ a a) '(λ b b) #hash() #hash()))
+(check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b)) #hash() #hash()))
+(check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash() #hash()))
 (check-eq? (interpret '(if #t 1 0)) 1)
 (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
 (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index e8f15e6..8fa96f9 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -34,24 +34,27 @@
   (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]
-    [(n 'Nat) #:when (natural? n) #t]
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    ['sole (equal? 'Unit with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(fix ,e) with)
+    [`(fix ,e)
       (check-core (infer-core e) `(,with → ,with) Γ)]
 
-    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
-      (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
-          (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
+          (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))]
+        [_ #f])]
 
-    [(e t) #f])))
+    [_ #f])))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index 541de2c..fc34115 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -31,38 +31,43 @@
 (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)
+  (match with
+    ['sole (equal? 'Unit with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
-    [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
-    [(`(set ,e1 ,e2) 'Unit)
+    [`(new ,e)
+      (match with
+        [`(Ref ,t) (check-core e t Γ)]
+        [_ #f])]
+    [`(! ,e) (check-core e `(Ref ,with) Γ)]
+    [`(set ,e1 ,e2)
       (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-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+        [`(Ref ,t)
+          (and (equal? 'Unit with)
+            (check-core e2 t Γ))]
+        [_ #f])]
+
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,k ,t2)
+          (and (equal? t t1) (check-core e t2 (dict-set Γ x t))
+            (> k (max-level e t1 t2 (dict-set Γ x t1))))] ; KNOB
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
-          (and (equal? t2 t)
+          (and (equal? t2 with)
                (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
+        [_ #f])]
 
-    [(e t) #f]))
+    [_ #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
-  ; (print (format "infer: ~a" (fmt expr)))
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
diff --git a/stlc-let.rkt b/stlc-let.rkt
index 3c4fef0..f906e48 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -22,18 +22,22 @@
 (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)
+  (match with
+    ['sole (equal? 'Unit with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
-    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
-      (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
-        [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
-    [(e t) #f]))
+        [`(,t1 → ,t2)
+          (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))]
+        [_ #f])]
+    [_ #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index c9c77b6..ee64fcb 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -28,38 +28,43 @@
 (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]
-    [(n 'Nat) #:when (natural? n) #t]
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    ['sole (equal? 'Unit with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
-    [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
-    [(`(set ,e1 ,e2) 'Unit)
+    [`(new ,e)
+      (match with
+        [`(Ref ,t) (check-core e t Γ)]
+        [_ #f])]
+    [`(! ,e) (check-core e `(Ref ,with) Γ)]
+    [`(set ,e1 ,e2)
       (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-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+        [`(Ref ,t)
+          (and (equal? 'Unit with)
+            (check-core e2 t Γ))]
+        [_ #f])]
+
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,k ,t2)
+          (and
+            (equal? t t1)
+            (>= k (max-level e (dict-set Γ x t1) t1 t2))  ; (KNOB)
+            (check-core e t2 (dict-set Γ x t1)))])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
-          (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
+          (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))]
+        [_ #f])]
 
-    [(e t) #f]))
+    [_ #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
-  ; (print (format "infer: ~a" (fmt expr)))
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
@@ -81,8 +86,8 @@
 
     [`(λ (,x : ,t1) ,e)
       (let ([t2 (infer-core e (dict-set Γ x t1))])
-        (let ([k (max-level e (dict-set Γ x t1) t1 t2)])  ; (KNOB)
-          `(,t1 → ,k ,t2)))]
+      (let ([k (max-level e (dict-set Γ x t1) t1 t2)])  ; (KNOB)
+        `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 8819116..c90fdae 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -1,6 +1,6 @@
 #lang racket
 (require "lib.rkt")
-(require (only-in "stlc-ext.rkt" equiv?))
+(provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with iso-recursive types
 
@@ -40,35 +40,34 @@
 (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]
-    [(n 'Nat) #:when (natural? n) #t]
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    ['sole (equal? 'Unit with)]
+    [n #:when (natural? n) (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(fold (μ ,x ,t) ,e) `(μ ,x ,t))
-      (check-core e t (dict-set Γ x `(μ ,x ,t)))]
-    [(`(unfold (μ ,x ,t) ,e) with)
-      (and (check-core e `(μ ,x ,t) Γ)
-        (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
-
-    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
-      (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
+    [`(fold (μ ,x ,t) ,e)
+      (match with
+        [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))]
+        [_ #f])]
 
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
-          (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
+          (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))]
+        [_ #f])]
 
-    [(e t) #f]))
+    [_ (equal? (infer-core expr Γ) with)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
-  ; (print (format "infer: ~a" (fmt expr)))
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
@@ -96,3 +95,13 @@
         [t (err (format "expected → type on application body, got ~a" t))])]
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
+
+;; Replace all references to an expression with a value.
+(define (replace expr key value)
+  (match expr
+    ; do not accidentally replace shadowed bindings
+    [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_)
+      `(type ,x ,_ ,_)) #:when (equal? x key) expr]
+    [x #:when (equal? x key) value]
+    [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))]
+    [v v]))
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index f054d4e..d911557 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -7,7 +7,6 @@
 (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]
     [n #:when (natural? n) n]
@@ -42,35 +41,43 @@
 (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]
-    [(n 'Nat) #:when (natural? n) #t]
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    ['sole
+      (equal? 'Unit with)]
+    [n #:when (natural? n)
+      (equal? 'Nat with)]
+    [x #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
-    [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
-    [(`(set ,e1 ,e2) 'Unit)
+    [`(new ,e)
+      (match with
+        [`(Ref ,t) (check-core e t Γ)]
+        [_ #f])]
+    [`(! ,e) (check-core e `(Ref ,with) Γ)]
+    [`(set ,e1 ,e2)
       (match (infer-core e1 Γ)
-        [`(Ref ,t) (check-core e2 t Γ)]
-        [t #f])]
+        [`(Ref ,t)
+          (and (equal? 'Unit with)
+            (check-core e2 t Γ))]
+        [_ #f])]
 
-    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
-      (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
-          (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
-        [t #f])]
+          (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))]
+        [_ #f])]
 
-    [(e t) #f]))
+    [_ #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
-  ; (print (format "infer: ~a" (fmt expr)))
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
diff --git a/stlc.rkt b/stlc.rkt
index 803cc8c..706557d 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -18,16 +18,20 @@
 
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with [Γ #hash()])
-  (match* (expr with)
-    [(x _) #:when (dict-has-key? Γ x)
+  (match expr
+    [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)))]
-    [(`(,e1 ,e2) t)
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,t2)
+          (and (equal? t t1) (check e t2 (dict-set Γ x)))]
+        [_ #f])]
+    [`(,e1 ,e2)
       (match (infer e1 Γ)
-        [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer e2 Γ)))]
-        [t #f])]
-    [(e t) #f]))
+        [`(,t1 → ,t2)
+          (and (equal? t2 with) (equal? t1 (infer e2 Γ)))]
+        [_ #f])]
+    [_ #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
-- 
cgit v1.2.3-70-g09d2