backport check case reduction

9 files changed, 52 insertions, 191 deletions

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 8b447c1..81bab7b 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -1,6 +1,7 @@
 #lang racket
 (require "lib.rkt")
 (require (only-in "stlc-rec.rkt" replace))
+(require (only-in "stlc-ext.rkt" expand))
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
 ;; plus sums products booleans ascryption etc, to implement doubly-linked lists
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index b11cb58..9727068 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -77,20 +77,9 @@
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
   (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)
       (check-core in with (dict-set Γ t1 t2))]
 
-    [`(inc ,e)
-      (and (equiv? 'Nat with)
-        (check-core e 'Nat Γ))]
     [`(if ,c ,e1 ,e2)
       (and (check-core c 'Bool Γ)
         (check-core e1 with Γ) (check-core e2 with Γ))]
@@ -99,22 +88,14 @@
       (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 Γ Γ)]
-        [_ #f])]
-    [`(cdr ,e)
-      (match (infer-core e Γ)
-        [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
-        [_ #f])]
 
     [`(inl ,e)
-      (match (infer-core e Γ)
-        [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
+      (match with
+        [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
         [_ #f])]
     [`(inr ,e)
-      (match (infer-core e Γ)
-        [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
+      (match with
+        [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
         [_ #f])]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (match (infer-core e Γ)
@@ -122,8 +103,6 @@
           (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
       (match with
@@ -131,25 +110,16 @@
         [_ #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 Γ Γ)]
+        [`(List ,t)
+          (and (check-core f1 t Γ)
+            (check-core f2 `(List ,t) Γ))]
         [_ #f])]
-    [`(tail ,e)
-      (equiv? (infer-core e Γ) with Γ Γ)]
 
     [`(λ (,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 with Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))]
-        [_ #f])]
 
     [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
 
@@ -204,9 +174,10 @@
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (match (infer-core e Γ)
         [`(,a1 ⊕ ,a2)
-          (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))])
-            (if (equiv? b1 b2 Γ Γ) b1
-              (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))]
+          (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))]
+            [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))])
+          (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))])]
 
     ['nil (err (format "unable to infer type of empty list!"))]
@@ -234,8 +205,11 @@
 
     [e (err (format "inferring an unknown expression ~a" e))]))
 
+;; Expands a type alias into weak-head normal form, for literal matching.
+;;      (expand Type Table[Id, Expr ⊕ Type]): Type
 (define (expand t Γ)
-  (if (dict-has-key? Γ t) (expand (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 Γ2)
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index 8fa96f9..ad45b90 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -35,26 +35,17 @@
 (define (check-core expr with Γ)
   (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) 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)]
-
     [`(fix ,e)
       (check-core (infer-core e) `(,with → ,with) Γ)]
 
     [`(λ (,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 with) (equal? t1 (infer-core e2 Γ)))]
+          (and (equal? t1 t)
+            (check-core e t2 (dict-set Γ x t1)))]
         [_ #f])]
 
-    [_ #f])))
+    [_ (equal? (infer-core expr Γ) with)])))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -63,8 +54,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)]
 
     [`(fix ,e)
       (match (infer-core e Γ)
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 Γ
diff --git a/stlc-let.rkt b/stlc-let.rkt
index f906e48..089f9d0 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -23,21 +23,12 @@
   (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)]
     [`(λ (,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 with) (equal? t1 (infer-core e2 Γ)))]
-        [_ #f])]
-    [_ #f]))
+    [_ (equal? (infer-core expr Γ) with)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -46,6 +37,7 @@
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
     [`(λ (,x : ,t) ,e)
       `(,t → ,(infer-core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
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
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index c90fdae..342f265 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -41,11 +41,6 @@
   (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)]
-
     [`(fold (μ ,x ,t) ,e)
       (match with
         [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))]
@@ -56,11 +51,6 @@
         [`(,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 with) (equal? t1 (infer-core e2 Γ)))]
-        [_ #f])]
 
     [_ (equal? (infer-core expr Γ) with)]))
 
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index d911557..41aec59 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -42,37 +42,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 → ,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 with) (equal? t1 (infer-core e2 Γ)))]
-        [_ #f])]
 
-    [_ #f]))
+    [_ (equal? (infer-core expr Γ) with)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -81,8 +63,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)
diff --git a/stlc.rkt b/stlc.rkt
index 706557d..820197b 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -19,23 +19,17 @@
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with [Γ #hash()])
   (match expr
-    [x #:when (dict-has-key? Γ x)
-      (equal? (dict-ref Γ x) with)]
     [`(λ (,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 with) (equal? t1 (infer e2 Γ)))]
-        [_ #f])]
-    [_ #f]))
+    [_ (equal? (infer with Γ) with)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
   (match expr
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
     [`(λ (,x : ,t) ,e)
       `(,t → ,(infer e (dict-set Γ x t)))]
     [`(,e1 ,e2)