backport check refactorings

1 files changed, 14 insertions, 11 deletions

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)