stlc-dll: add back check cases, inline and fix replace, implement well-formed

2 files changed, 110 insertions, 25 deletions

diff --git a/lib.rkt b/lib.rkt
index 6d431fd..29d3b83 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -154,8 +154,3 @@
 (check-equal? '(λ a (λ b (λ c (a (b c)))))
   (α-convert '(λ c (λ a (λ b (c (a b)))))))
 
-(define (replace expr key value)
-  (match expr
-    [x #:when (equal? x key) value]
-    [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))]
-    [v v]))
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index bdd439b..927161a 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -5,7 +5,12 @@
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
 ;; plus sums products booleans ascryption etc, to implement doubly-linked lists
 
-;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value
+;; Interprets a desugared, stripped expression.
+;; Γ: 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 [Γ #hash()] [Σ (make-hash)])
   (interpret- (strip (desugar expr)) Γ Σ))
 (define (interpret- expr Γ Σ)
@@ -75,38 +80,96 @@
 
     [e (err (format "attempting to interpret unknown expression ~a" e))]))
 
+;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error)
+;; with: a *normalized* type
+;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context:
+;;   the current bindings in scope introduced by λx.[] and μx.[] and τx.[]
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with [Γ #hash()])
   (check-core (desugar expr) with Γ))
 (define (check-core expr with Γ)
   ; (print (format "check: ~a with ~a" (fmt expr) with))
-  (let ([with (expand with Γ)])
   (match expr
+    [`(type ,t1 ,t2 ,in)
+      (check-core in with (dict-set Γ t1 t2))]
+
+    [`(inc ,e)
+      (and (equiv? with 'Nat)
+        (check-core e 'Nat Γ))]
+    [`(if ,c ,e1 ,e2)
+      (and (check-core c 'Bool Γ)
+        (check-core e1 with Γ) (check-core e2 with Γ))]
+
+    [`(pair ,e1 ,e2)
+      (match (expand with Γ)
+        [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+        [t #f])]
+    [`(car ,e)
+      (match (expand (infer-core e Γ) Γ)
+        [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
+        [t #f])]
+    [`(cdr ,e)
+      (match (expand (infer-core e Γ) Γ)
+        [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
+        [t #f])]
+
     [`(inl ,e)
-      (match with
-        [`(,t1 ⊕ ,t2) (equiv? t1 (infer-core e Γ) Γ Γ)]
+      (match (expand with Γ)
+        [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
         [t #f])]
     [`(inr ,e)
-      (match with
-        [`(,t1 ⊕ ,t2) (equiv? t2 (infer-core e Γ) Γ Γ)]
+      (match (expand with Γ)
+        [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
+        [t #f])]
+    [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+      (match (expand (infer-core e Γ) Γ)
+        [`(,a1 ⊕ ,a2)
+          (and (check-core e1 with (dict-set Γ x1 a1))
+            (check-core e2 with (dict-set Γ x2 a2)))]
+        [t #f])]
+
+    [`(new ,e)
+      (match (expand with Γ)
+        [`(Ref ,t) (check-core e t Γ)]
+        [t #f])]
+    [`(! ,e) (check-core e `(Ref ,with) Γ)]
+    [`(set ,e1 ,e2)
+      (match (expand (infer-core e1 Γ) Γ)
+        [`(Ref ,t)
+          (and (equiv? with 'Unit Γ Γ)
+            (check-core e2 t Γ))]
         [t #f])]
 
     [`(fold (μ ,x ,t) ,e)
-      (match with
+      (match (expand with Γ)
         [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])]
     [`(unfold (μ ,x ,t) ,e)
       (and (check-core e `(μ ,x ,t) Γ)
-        (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
+        (equiv? with t Γ (dict-set Γ x `(μ ,x ,t))))]
 
     [`(fold ,e)
-      (match with
+      (match (expand with Γ)
         [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])]
     [`(unfold ,e) ; FIXME: GROSS
       (match* ((infer-core e Γ) with)
         [(`(μ ,_ ,t) `(μ ,_ ,t)) #T]
         [(t u) #f])]
 
-    [_ (equiv? with (infer-core expr Γ) Γ Γ)])))
+    [`(λ (,x : ,t) ,e)
+      (match (expand 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
+        [t #f])]
+    [`(,e1 ,e2)
+      (match (infer-core e1 Γ)
+        [`(,t1 → ,_ ,t2)
+          (and (equiv? with t2 Γ Γ)
+            (check-core e2 t1 Γ))]
+        [t #f])]
+
+
+    [_ (equiv? with (infer-core expr Γ) Γ Γ)]))
 
 ;; Checks if two expressions or types are equivalent, up to α-conversion,
 ;; given their respective contexts
@@ -140,6 +203,7 @@
       (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.
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
   (infer-core (desugar expr) Γ))
@@ -153,7 +217,7 @@
       (dict-ref Γ x)]
 
     [`(type ,t1 ,t2 ,in)
-      (infer-core in (dict-set Γ t1 (expand t2 Γ)))]
+      (infer-core in (dict-set Γ t1 t2))]
     [`(,e : ,t)
       (if (check-core e t Γ) t
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
@@ -187,10 +251,11 @@
     [`(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 Γ)))])
+          (let ([b1 (infer-core e1 (dict-set Γ x1 a1))]
+                [b2 (infer-core e2 (dict-set Γ x2 a2))])
             (if (equiv? b1 b2 Γ Γ) b1
-              (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
+              (err (format "case ~a is not of consistent type!"
+                `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
         [t (err (format "calling case on incorrect type ~a" t))])]
 
     [`(new ,e)
@@ -217,17 +282,17 @@
           e `(μ ,x ,t) (infer-core e Γ))))]
 
     [`(fold ,e)
-      (match (infer-core e Γ)
+      (match (expand (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 Γ)
+      (match (expand (infer-core e Γ) Γ)
         [`(μ ,x ,t) (replace t x `(μ ,x ,t))] ; AAAA
         [t (err (format "expected ~a to be recursive, got ~a" e t))])]
 
     [`(λ (,x : ,t1) ,e)
-      (let ([t2 (infer-core e (dict-set Γ x (expand t1 Γ)))])
-        (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x (expand t1 Γ))))])  ; KNOB
+      (let ([t2 (infer-core e (dict-set Γ x t1))])
+        (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))])  ; KNOB
           `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
@@ -239,9 +304,34 @@
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
+;; Expands a type alias to a matchable outside structure, for literal matching.
 ;;      (expand Type Table[Id, Expr ⊕ Type]): Type
 (define (expand t Γ)
-  (if (dict-has-key? Γ t) (dict-ref Γ t) t))
+  (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t))
+
+(define (replace expr key value)
+  (match expr
+    ; do not accidentally replace shadowed bindings
+    [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_)
+      `(type ,x ,_ ,_)) #:when (equal? x key) expr]
+    [x #:when (equal? x key) value]
+    [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))]
+    [v v]))
+
+;; Checks if a type is well-formed in the current context.
+;;      (well-formed Type Context): Bool
+(define (well-formed t Γ)
+  (if (well-formed-friend t Γ) #t
+    (err (format "type ~a is not well-formed!" t))))
+(define (well-formed-friend t Γ)
+  (match t
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [(or 'Unit 'Nat 'Bool) #t]
+    [`(Ref ,t) (well-formed-friend t Γ)]
+    [`(μ ,x ,t) (well-formed-friend t (dict-set Γ x 'Unit))] ; HACK
+    [(or `(,t1 → ,t2) `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+      (and (well-formed-friend t1 Γ) (well-formed-friend t2 Γ))]
+    [_ #f]))
 
 ;;      (max-level Table[Sym, Type] Expr Type Type): Natural
 (define (max-level e t1 t2 Γ)
@@ -296,7 +386,7 @@
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
     [`(if ,c ,e1 ,e2) (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))]
-    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x (expand t Γ)))] ; todo: should be 0?
+    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))