stlc-dll: cut back on cases and remove max-level

1 files changed, 24 insertions, 66 deletions

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 8829ead..8b447c1 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -1,19 +1,18 @@
 #lang racket
 (require "lib.rkt")
 (require (only-in "stlc-rec.rkt" replace))
-(require rackunit)
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
 ;; plus sums products booleans ascryption etc, to implement doubly-linked lists
 
-;; Interprets a desugared, stripped expression.
+;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err
+(define (interpret expr)
+  (interpret-core (strip (desugar expr)) #hash() (make-hash)))
 ;; Γ: a Table[Symbol, Expr] representing the context:
 ;;   the current bindings in scope introduced by λx.[]
 ;; Σ: a Table[Symbol, Expr] representing the heap:
 ;;   the current references on the heap generated by (gensym). mutable
-;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err
-(define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash() (make-hash)))
+;; Interprets a *desugared* expression *stripped* of type annotations.
 (define (interpret-core expr Γ Σ)
   (match expr
     ['sole 'sole]
@@ -92,9 +91,6 @@
     [`(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 Γ))]
@@ -103,14 +99,6 @@
       (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 with
@@ -131,17 +119,8 @@
       (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 (equiv? 'Unit with Γ Γ)
-            (check-core e2 t Γ))]
-        [_ #f])]
-
-    ; [`(fold (μ ,x ,t) ,e)
-    ;   (match with
-    ;     [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])]
+    [`(! ,e)
+      (check-core e `(Ref ,with) Γ)]
 
     [`(fold ,e)
       (match with
@@ -152,16 +131,10 @@
       (match with
         [`(,t1 → ,k ,t2)
           (and (equiv? 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 → ,_ ,t2)
-          (and (equiv? t2 with Γ Γ)
-            (check-core e2 t1 Γ))]
+            (> k (level-body e (dict-set Γ x t1))))] ; KNOB
+        [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
         [_ #f])]
 
-
     [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
 
 ;; Checks if two expressions or types are equivalent, up to α-conversion,
@@ -182,22 +155,23 @@
     [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
       (let ([name gensym])
       (equiv? t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+
     ; function expressions: parameter names can be arbitrary
     [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2))
       (let ([name gensym])
-      (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
-        (equiv? t1 t2 Γ1 Γ2)))]
+      (and  (equiv? t1 t2 Γ1 Γ2)
+        (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))))]
     [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
       (let ([name gensym])
       (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
 
-    ; check for syntactic equivalence on lists and values
+    ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
       (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
 ;; Infers a type from a given expression, if possible, or errors out.
-;; Should always return a type in weak-head normal form for structural matching.
+;; Returns a type in weak-head normal form for structural matching.
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
@@ -265,29 +239,16 @@
               e1 t e2 (infer-core e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
-    [`(fold (μ ,x ,t) ,e)
-      (if (check-core e (expand t Γ) (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
-        (err (format "expected ~a to be of type ~a, got ~a"
-          e t (infer e (dict-set Γ x `(μ ,x ,t))))))]
-    [`(unfold (μ ,x ,t) ,e)
-      (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
-        (err (format "expected ~a to be of type ~a, got ~a"
-          e `(μ ,x ,t) (infer-core e Γ))))]
-
-    [`(fold ,e)
-      (match (infer-core e Γ)
-        [`(μ ,x ,t) `(μ ,x ,t)]
-        [t (err (format "expected ~a to be recursive, got ~a" e t))])]
     [`(unfold ,e)
       (match (infer-core e Γ)
         [`(μ ,x ,t) (replace t x `(μ ,x ,t))]
         [t (err (format "expected ~a to be recursive, got ~a" e t))])]
 
     [`(λ (,x : ,t1) ,e)
-      (let ([t2 (infer-core e (dict-set Γ x t1))])
-      (let ([t1 (expand t1 Γ)]) ; type annotation, must expand to weak-head normal form
-      (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))])  ; KNOB
-          `(,t1 → ,k ,t2))))]
+      (let* ([t2 (infer-core e (dict-set Γ x t1))]
+        [t1 (expand t1 Γ)] ; type annotation, must expand
+        [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB
+        `(,t1 → ,k ,t2))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,k ,t2)
@@ -301,7 +262,8 @@
 ;; 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 a type is well-formed in the current context.
 ;;      (well-formed Type Context): Bool
@@ -315,12 +277,6 @@
       (and (well-formed t1 Γ) (well-formed t2 Γ))]
     [_ #f]))
 
-;;      (max-level Table[Sym, Type] Expr Type Type): Natural
-(define (max-level e t1 t2 Γ)
-  (max
-    (level-body e Γ)
-    (level-type t1 Γ)
-    (level-type t2 Γ)))
 ;; Checks if a type is well-kinded with respect to a level in the current context
 ;;      (well-kinded Type Level Context): Bool
 (define (well-kinded t l Γ)
@@ -349,14 +305,14 @@
     [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (max (level-type t1 Γ) (level-type t2 Γ))]
     [`(μ ,x ,t) ; fixme: correct, ish, but VERY WEIRD
-      (level-type t (dict-set Γ x 'Unit))]
+      (level-type t Γ)]
     [`(,t1 → ,k ,t2)
-      (if (and (> k (level-type t1 Γ)) (> k (level-type t2 Γ))) k ; KNOB
+      (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)))]
     [`(Ref ,t)
       (let ([k (level-type t Γ)])
       (if (zero? k) 0 (+ 1 k)))] ; KNOB
-    [t (err (format "attempting to infer the level of unknown type ~a" t))]))
+    [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ
 
 ;; Infers the level of a (well-formed) expression.
 ;;      (level-body Expr Table[Sym, Type]): Natural
@@ -376,6 +332,8 @@
       (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))]
     [x #:when (symbol? x) 0])) ; local variables, not in Γ
 
+(require rackunit)
+
 (check-exn
   exn:fail?
   (λ () (infer '