backport check refactorings

1 files changed, 28 insertions, 23 deletions

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)