backport check case reduction

1 files changed, 12 insertions, 44 deletions

diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index ee64fcb..9f3fc9c 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -29,37 +29,19 @@
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
   (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)
       (match with
         [`(Ref ,t) (check-core e t Γ)]
         [_ #f])]
-    [`(! ,e) (check-core e `(Ref ,with) Γ)]
-    [`(set ,e1 ,e2)
-      (match (infer-core e1 Γ)
-        [`(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 with) (equal? t1 (infer-core e2 Γ)))]
+          (and (equal? t t1) (check-core e t2 (dict-set Γ x t1))
+            (>= k (level-body e (dict-set Γ x t1))))] ; KNOB
         [_ #f])]
 
-    [_ #f]))
+    [_ (equal? (infer-core expr Γ) with)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -85,9 +67,9 @@
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
     [`(λ (,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* ([t2 (infer-core e (dict-set Γ x t1))]
+        [k (level-body e (dict-set Γ x t1))]) ; KNOB
+      `(,t1 → ,k ,t2))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
@@ -97,23 +79,14 @@
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
-;;      (max-level Table[Sym, Type] Expr Type Type): Natural
-(define (max-level e Γ t1 t2)
-  (max
-    (level-type t1)
-    (level-type t2)
-    (level-body e Γ)))
-
 ;;      (level-type Type): Natural
 (define (level-type t)
   (match t
-    ['Unit 0]
-    ['Nat 0]
+    [(or 'Unit 'Nat) 0]
     [`(,t1 → ,k ,t2)
-      (if (or (< k (level-type t1)) (< k (level-type t2)))
+      (if (and (>= k (level-type t1)) (>= k (level-type t2))) k
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
-          k t1 t2))
-        k)]
+          k t1 t2)))]
     [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB)
     [t (err (format "attempting to infer the level of unknown type ~a" t))]))
 
@@ -124,14 +97,9 @@
     [n #:when (natural? n) 0]
     [x #:when (dict-has-key? Γ x)
       (level-type (dict-ref Γ x))]
-
-    [`(new ,e) (level-body e Γ)]
-    [`(! ,e) (level-body e Γ)]
-    [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
-
-    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
-    [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
-    [e (err (format "attempting to infer the level of unknown expression ~a" e))]))
+    [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)]
+    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))]
+    [x #:when (symbol? x) 0]))
 
 ; simple diverging program in STLC-ref
 ; https://www.youtube.com/watch?v=XNgE8kBfSz8