From c9651d9c20c94e2fb45b5ac4ec3bb350dc2dfd4b Mon Sep 17 00:00:00 2001
From: JJ
Date: Fri, 26 Jul 2024 17:14:26 -0700
Subject: backport check case reduction

---
 stlc-imp.rkt | 57 ++++++++++++++-------------------------------------------
 1 file changed, 14 insertions(+), 43 deletions(-)

(limited to 'stlc-imp.rkt')

diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index fc34115..0c3c3c7 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -32,37 +32,19 @@
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
   (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)
       (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) (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 with)
-               (equal? t1 (infer-core e2 Γ)))]
+            (> 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)
@@ -71,8 +53,7 @@
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
-    [x #:when (dict-has-key? Γ x)
-      (dict-ref Γ x)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(new ,e) `(Ref ,(infer-core e Γ))]
     [`(! ,e)
@@ -88,35 +69,28 @@
         [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 (+ 1 (max-level e (dict-set Γ x t1) t1 t2))])  ; KNOB
-          `(,t1 → ,k ,t2)))]
+      (let* ([t2 (infer-core e (dict-set Γ x t1))]
+        [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB
+      `(,t1 → ,k ,t2))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
           (if (check-core e2 t1 Γ) t2
-            (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))]
+            (err (format "inferred argument type ~a does not match arg ~a of type ~a"
+              t1 e2 (infer-core e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
 
     [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]
     [`(,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)
       (let ([k (level-type t)])
       (if (zero? k) 0 (+ 1 k)))] ; KNOB
@@ -127,10 +101,7 @@
   (match e
     ['sole 0]
     [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 Γ))]))
+    [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))]
+    [(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])) ; local variables, not in Γ
-- 
cgit v1.2.3-70-g09d2