From 83a1400957da57bf6930bab4b81af87f1851be5b Mon Sep 17 00:00:00 2001
From: JJ
Date: Mon, 29 Jul 2024 12:47:19 -0700
Subject: split lib into lib and base; move tests to separate files & directory

---
 base.rkt            |  78 ++++++++++++++++++
 lib.rkt             |  77 ++----------------
 stlc-dll.rkt        | 228 +---------------------------------------------------
 stlc-ext.rkt        |  11 +--
 stlc-fix.rkt        |   7 +-
 stlc-imp.rkt        |   7 +-
 stlc-let.rkt        |  57 -------------
 stlc-pred.rkt       |  68 +---------------
 stlc-rec.rkt        |   3 +-
 stlc-ref.rkt        |  14 +---
 stlc.rkt            |  26 +++---
 tests/stlc-dll.rkt  | 225 +++++++++++++++++++++++++++++++++++++++++++++++++++
 tests/stlc-ext.rkt  |  11 +++
 tests/stlc-imp.rkt  |  29 +++++++
 tests/stlc-pred.rkt |  29 +++++++
 tests/stlc.rkt      |   8 ++
 16 files changed, 418 insertions(+), 460 deletions(-)
 create mode 100644 base.rkt
 delete mode 100644 stlc-let.rkt
 create mode 100644 tests/stlc-dll.rkt
 create mode 100644 tests/stlc-ext.rkt
 create mode 100644 tests/stlc-imp.rkt
 create mode 100644 tests/stlc-pred.rkt
 create mode 100644 tests/stlc.rkt

diff --git a/base.rkt b/base.rkt
new file mode 100644
index 0000000..c88a8ee
--- /dev/null
+++ b/base.rkt
@@ -0,0 +1,78 @@
+#lang racket
+(require "lib.rkt")
+(provide (all-defined-out))
+
+;; Base utility functions for working with the simply-typed lambda calculus
+
+;; Provides a pretty-print utility for terms in the simply-typed lambda calculus
+;;      (fmt Expr): String
+(define (fmt expr)
+  (match expr
+    ['sole "⟨⟩"]
+    [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))]
+    [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))]
+    [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))]
+    [`((λ (,x : ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
+    [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))]
+    [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
+    [`(let (,x : ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
+    [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))]
+    [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))]
+    [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
+    [`(,a → ,k ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
+    [`(Ref ,a) (format "Ref ~a" (fmt a))]
+    [`(new ,a) (format "new ~a" (fmt a))]
+    [`(! ,a) (format "!~a" (fmt a))]
+    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
+    [(hash-table (keys values) ...)
+      (format "{~a}" (foldl (λ (k v acc) (format "~a: ~a;" (fmt k) (fmt v))) "" keys values))]
+    [expr (format "~a" expr)]))
+
+;; Removes typing annotations and similar constructs, for interpretation
+(define (strip expr)
+  (match expr
+    [`(,e : ,_) (strip e)]
+    [`(type ,_ ,_ ,e) (strip e)]
+    [`(fold ,_ ,e) `(fold ,(strip e))]
+    [`(unfold ,_ ,e) `(unfold ,(strip e))]
+    [`(,e ...) `(,@(map strip e))]
+    [e e]))
+
+;; Define aliases from higher-level constructs to their core forms
+(define (desugar expr)
+  (match expr
+    ['⟨⟩ 'sole]
+    [`(ref ,e) (desugar `(new ,e))]
+    [`(deref ,e) (desugar `(! ,e))]
+
+    ; set-with-continuation
+    [`(set ,e1 ,e2 ,in)
+      (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))]
+
+    ; many forms of let. this lets us elide many typing annotations
+    [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in)
+      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in)
+      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let ,x (,e : ,t) ,in)
+      (desugar `((λ (,x : ,t) ,in) (,e : ,t)))]
+    [`(let ,x ,e ,in)
+      (desugar `((λ ,x ,in) ,e))]
+    [`(let ,x ,e)
+      (desugar `(let ,x ,e sole))]
+
+    ; letrec as let + fix
+    [`(letrec (,x : ,t) ,e ,in)
+      (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))]
+
+    [`(,e ...) `(,@(map desugar e))]
+    [e e]))
+
+    ; [`(list ,exprs ...)
+      ; (foldr (λ (expr res) `(cons ,expr ,res)) 'nil)]
+    ; [`(type ,x ,type ,in) ; fails b/c types are not inferrable
+    ;   (desugar `(let (,x : Type) ,type ,in))]
diff --git a/lib.rkt b/lib.rkt
index e44eb6a..2149620 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -1,8 +1,9 @@
 #lang racket
 (require rackunit)
+(require racket/trace)
 (require syntax/location)
 (require (for-syntax syntax/location))
-(provide (all-defined-out))
+(provide (all-defined-out) trace)
 
 (define-syntax-rule (dbg body)
   (let ([res body])
@@ -30,10 +31,6 @@
   (with-syntax ([src (syntax-source-file-name stx)] [line (syntax-line stx)])
     #'(error 'todo (format "[~a:~a] unimplemented" src line))))
 
-; todo: write a trace macro
-; todo: write a fmt alias to format
-; todo: write a namer
-
 (define (any? proc lst)
   (foldl (λ (x acc) (if (proc x) #t acc)) #f lst))
 
@@ -43,77 +40,14 @@
 (define (inc i) (+ i 1))
 (define (dec i) (- i 1))
 
-;; removes typing annotations
-(define (strip expr)
-  (match expr
-    [`(,x : ,t) (strip x)]
-    [`(type ,t1 ,t2 ,in) (strip in)]
-    [`(fold ,t ,e) `(fold ,(strip e))]
-    [`(unfold ,t ,e) `(unfold ,(strip e))]
-    [`(,e ...) `(,@(map strip e))]
-    [e e]))
-
-;;      (fmt Expr): String
-(define (fmt expr)
-  (match expr
-    ['sole "⟨⟩"]
-    [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))]
-    [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))]
-    [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))]
-    [`((λ (,x : ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
-    [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))]
-    [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
-    [`(let (,x : ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
-    [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))]
-    [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))]
-    [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
-    [`(,a → ,k ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
-    [`(Ref ,a) (format "Ref ~a" (fmt a))]
-    [`(new ,a) (format "new ~a" (fmt a))]
-    [`(! ,a) (format "!~a" (fmt a))]
-    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
-    [(hash-table (keys values) ...)
-      (format "{~a}" (foldl (λ (k v acc) (format "~a: ~a;" (fmt k) (fmt v))) "" keys values))]
-    [expr (format "~a" expr)]))
-
-;; transforms higher-level constructs into the core calculus
-(define (desugar expr)
-  (match expr
-    ['⟨⟩ 'sole]
-    [`(ref ,e) (desugar `(new ,e))]
-    [`(deref ,e) (desugar `(! ,e))]
-
-    [`(set ,e1 ,e2 ,in)
-      (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))]
-
-    [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in)
-      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in)
-      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let ,x (,e : ,t) ,in)
-      (desugar `((λ (,x : ,t) ,in) (,e : ,t)))]
-    [`(let ,x ,e ,in)
-      (desugar `((λ ,x ,in) ,e))]
-    [`(let ,x ,e)
-      (desugar `(let ,x ,e sole))]
-
-    [`(letrec (,x : ,t) ,e ,in)
-      (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))]
-
-    [`(,e ...) `(,@(map desugar e))]
-    [e e]))
-
 (define (char-inc c) (integer->char (inc (char->integer c))))
 (define (char->string c) (list->string (list c)))
 (define (symbol->list s) (string->list (symbol->string s)))
 (define (list->symbol l) (string->symbol (list->string l)))
 (define (symbol-append a b) (string->symbol (string-append (symbol->string a) (symbol->string b))))
 
-;; provides a "pretty" gensym: 'a -> 'b, 'z -> 'aa, 'az -> 'ba etc. quite inefficient.
+;; Provides a "pretty" gensym: 'a -> 'b, 'z -> 'aa, 'az -> 'ba etc.
+;; quite inefficient.
 (define (fresh used)
   (cond
     [(list? used) (fresh-helper '|| (list->set used))]
@@ -133,7 +67,7 @@
 (check-equal? (fresh-next 'zaa) 'zab)
 (check-equal? (fresh-next 'azz) 'baa)
 
-;; normalizes an expression into binding variables descending
+;; Normalizes an expression into binding variables descending
 ;;      (α-convert Expr Table[Old New] Set[New])
 (define (α-convert expr [used #hash()])
   (match expr
@@ -153,4 +87,3 @@
   (α-convert '(λ a (λ b (λ c (a (b c)))))))
 (check-equal? '(λ a (λ b (λ c (a (b c)))))
   (α-convert '(λ c (λ a (λ b (c (a b)))))))
-
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 42ed82e..296648e 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -1,7 +1,8 @@
 #lang racket
-(require "lib.rkt")
+(require "lib.rkt" "base.rkt")
 (require (only-in "stlc-rec.rkt" replace))
 (require (only-in "stlc-ext.rkt" expand))
+(provide interpret check infer level-type level-body equiv-type)
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
 ;; plus sums products booleans ascryption etc, to implement doubly-linked lists
@@ -307,7 +308,7 @@
   (match e
     ['sole 0]
     [n #:when (natural? n) 0]
-    [x #:when (dict-has-key? Γ x) ; free variables
+    [x #:when (dict-has-key? Γ x) ; free variables, get their level
       (level-type (expand (dict-ref Γ x) Γ) Γ)]
     [(or `(,e : ,_) `(λ (,_ : ,_) ,e)
       `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e)
@@ -318,226 +319,3 @@
     [(or `(if ,c ,e1 ,e2) `(case ,c (,_ ⇒ ,e1) (,_ ⇒ ,e2)))
       (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))]
     [x #:when (symbol? x) 0])) ; local variables, not in Γ
-
-(require rackunit)
-(define-test-suite let-set-inc-case
-  (check-exn
-    exn:fail?
-    (λ () (infer '
-      (let (id : (Nat → 1 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 1 Nat))) (new id)
-      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
-      (set r f
-      (f 0))))))))
-
-  (check-eq?
-    (infer '
-      (let (id : (Nat → 1 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 1 Nat))) (new id)
-      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
-      (f 0)))))
-    'Nat)
-
-  (check-eq?
-    (check '
-      (let (id : (Nat → 1 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 1 Nat))) (new id)
-      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
-      (f 0))))
-      'Nat)
-    #t)
-
-  (check-eq? (interpret '(if #t 1 0)) 1)
-  (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
-  (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
-  (check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
-
-  (check-equal?
-    (infer
-      '(case ((inr sole) : (Nat ⊕ Unit))
-        (x ⇒ 0) (x ⇒ 1))) 'Nat)
-
-  (check-true
-    (check
-      '(case ((inr sole) : (Nat ⊕ Unit))
-        (x ⇒ x)
-        (x ⇒ 1)) 'Nat))
-
-  (check-equal?
-    (interpret
-      '((λ p1 (car (unfold p1)))
-        (fold
-          (pair 413
-          (pair (inl sole)
-                (inl sole))))))
-    413))
-
-;; initial implementation of doubly linked lists:
-;; (type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))
-(define-test-suite dll-no-empty-lists
-  (check-equal?
-    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-     (let get
-      (λ x (car (unfold x)))
-     (let my_list
-      (fold
-        (pair 413
-        (pair (inl sole)
-              (inl sole))))
-     (get my_list)))))
-    413)
-
-  (check-equal?
-    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-     (let prev
-      (λ x
-        (case (car (cdr (unfold x)))
-          (x ⇒ (inl (! x)))
-          (x ⇒ (inr sole))))
-     (let my_list
-      (fold
-        (pair 413
-        (pair (inl (new sole))
-              (inl (new sole)))))
-     (prev my_list)))))
-    '(inl sole))
-
-  (check-equal?
-    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-     (let next
-      (λ x
-        (case (cdr (cdr (unfold x)))
-          (x ⇒ (inl (! x)))
-          (x ⇒ (inr sole))))
-     (let my_list
-      (fold
-        (pair 413
-        (pair (inr (new sole))
-              (inr (new sole)))))
-     (next my_list)))))
-    '(inr sole))
-
-  (check-true
-    (equiv-type
-      (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-        (λ (self : DoublyLinkedList)
-           (case (cdr (cdr (unfold self)))
-            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))))
-      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))
-      #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))))))
-
-  (check-true
-    (check
-      '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-        (λ (self : DoublyLinkedList)
-           (case (cdr (cdr (unfold self)))
-            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))
-      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))))
-
-  (check-equal?
-    (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-      (let (get : (DoublyLinkedList → 1 Nat))
-        (λ self (car (unfold self)))
-      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-        (λ self
-          (case (car (cdr (unfold self)))
-            (x ⇒ (inl (! x)))
-            (x ⇒ (inr sole))))
-      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-        (λ self
-          (case (cdr (cdr (unfold self)))
-            (x ⇒ (inl (! x)))
-            (x ⇒ (inr sole))))
-      (let (my_list : DoublyLinkedList)
-        (fold
-          (pair 413
-          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
-                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
-      (prev my_list)))))))
-    '(DoublyLinkedList ⊕ Unit))
-
-  (check-true
-    (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-      (let (get : (DoublyLinkedList → 1 Nat))
-        (λ self (car (unfold self)))
-      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-        (λ self
-          (case (car (cdr (unfold self)))
-            (x ⇒ (inl (! x)))
-            (x ⇒ (inr sole))))
-      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-        (λ self
-          (case (cdr (cdr (unfold self)))
-            (x ⇒ (inl (! x)))
-            (x ⇒ (inr sole))))
-      (let (my_list : DoublyLinkedList)
-        (fold
-          (pair 413
-          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
-                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
-      (prev my_list))))))
-      '(DoublyLinkedList ⊕ Unit))))
-
-;; new implementation of doubly linked lists:
-;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))
-(define-test-suite dll-with-empty-lists
-  (check-equal?
-    (interpret
-     '(let next
-      (λ self
-        (case (unfold self)
-          (some ⇒ (! (cdr (cdr some))))
-          (none ⇒ (fold (inr sole)))))
-     (let my_list
-      (fold
-        (inl
-          (pair 413
-          (pair (new (inr sole))
-                (new (inr sole))))))
-     (next my_list))))
-    '(inr sole))
-
-  (check-equal?
-    (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
-      (λ (self : DoublyLinkedList)
-         (case (unfold self)
-          (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList))
-          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
-    '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
-
-  (check-true
-    (equiv-type
-      (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
-        (λ (self : DoublyLinkedList)
-           (case (unfold self)
-            (some ⇒ (! (cdr (cdr some))))
-            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
-    '(DoublyLinkedList → 1 DoublyLinkedList)
-      #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
-
-  (check-true
-    (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
-      (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
-        (λ self
-          (case (unfold self)
-            (some ⇒ (inl (car some)))
-            (none ⇒ (inr sole))))
-      (let (prev : (DoublyLinkedList → 1 DoublyLinkedList))
-        (λ self
-          (case (unfold self)
-            (some ⇒ (! (car (cdr some))))
-            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
-      (let (next : (DoublyLinkedList → 1 DoublyLinkedList))
-        (λ self
-          (case (unfold self)
-            (some ⇒ (! (cdr (cdr some))))
-            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
-      (let (my_list : DoublyLinkedList)
-        (fold (inl
-          (pair 413
-          (pair (new ((fold (inr sole)) : DoublyLinkedList))
-                (new ((fold (inr sole)) : DoublyLinkedList))))))
-      (prev my_list))))))
-      'DoublyLinkedList)))
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 300a473..84c476c 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -1,5 +1,6 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
 (provide interpret check infer expand equiv-type equiv-term)
 
 ;; The Simply-Typed Lambda Calculus, with simple extensions
@@ -252,13 +253,3 @@
     [(`(,l1 ...) `(,l2 ...))
       (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
-
-(require rackunit)
-(define-test-suite ext
-  (check-true (equiv-term '(λ a a) '(λ b b) #hash()))
-  (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash()))
-  (check-true (equiv-term '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash()))
-  (check-eq? (interpret '(if #t 1 0)) 1)
-  (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
-  (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
-  (check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat)))
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index ad45b90..2c68696 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -1,9 +1,10 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
 
 ;; The Simply-Typed Lambda Calculus, with general recursion
 
-;;      (interpret Expr Table[Sym, Expr]): Value
+;;      (interpret Expr Context): Value
 (define (interpret expr)
   (interpret-core (strip (desugar expr)) #hash()))
 (define (interpret-core expr Γ)
@@ -29,7 +30,7 @@
 
     [e (err (format "interpreting an unknown expression ~a" e))]))
 
-;;      (check Expr Type Table[Sym, Type]): Bool
+;;      (check Expr Type Context): Bool
 (define (check expr with)
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
@@ -47,7 +48,7 @@
 
     [_ (equal? (infer-core expr Γ) with)])))
 
-;;      (infer Expr Table[Sym, Type]): Type
+;;      (infer Expr Context): Type
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index 0c3c3c7..c550359 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -1,5 +1,8 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
+(require (only-in "stlc-ref.rkt" interpret))
+(provide check infer level-type level-body)
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references
 
@@ -31,11 +34,13 @@
 (define (check expr with)
   (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
-  (match with
+  (match expr
     [`(new ,e)
       (match with
         [`(Ref ,t) (check-core e t Γ)]
         [_ #f])]
+    [`(! ,e)
+      (check-core e `(Ref ,with) Γ)]
 
     [`(λ (,x : ,t) ,e)
       (match with
diff --git a/stlc-let.rkt b/stlc-let.rkt
deleted file mode 100644
index 089f9d0..0000000
--- a/stlc-let.rkt
+++ /dev/null
@@ -1,57 +0,0 @@
-#lang racket
-(require "lib.rkt")
-
-;; The Simply-Typed Lambda Calculus, with let sugar and some base types
-
-;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash()))
-(define (interpret-core expr Γ)
-  (match expr
-    ['sole 'sole]
-    [n #:when (natural? n) n]
-    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
-    [`(,e1 ,e2)
-      (match (interpret-core e1 Γ)
-        [`(λ ,x ,e1 ,env) (interpret-core e1 (dict-set env x (interpret-core e2 Γ)))]
-        [e1 `(,e1 ,(interpret-core e2 Γ))])]
-    [e e]))
-
-;;      (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
-  (match with
-    [`(λ (,x : ,t) ,e)
-      (match with
-        [`(,t1 → ,t2)
-          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
-        [_ #f])]
-    [_ (equal? (infer-core expr Γ) with)]))
-
-;;      (infer Expr Table[Sym, Type]): Type
-(define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
-  (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)
-      (match (infer-core e1 Γ)
-        [`(,t1 → ,t2)
-          (if (check-core e2 t1 Γ) t2
-            (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
-
-(provide interpret check infer)
-
-(require rackunit)
-(check-equal? (interpret '(λ x x)) '(λ x x #hash()))
-(check-equal? (interpret '((λ a a) (x y))) '(x y))
-(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y))
-(check-equal? (interpret '((λ a (a y)) x)) '(x y))
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index 9f3fc9c..197ad74 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -1,29 +1,11 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
+(require (only-in "stlc-ref.rkt" interpret))
+(provide check infer level-type level-body)
 
 ;; The Simply-Typed Lambda Calculus with higher-order *predicative* references
 
-; Γ, x: τ₁ ⊢ e: τ₂    k ≥ max-level(Γ, τ₁, τ₂)
-; ---------------------------------------------
-; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂
-
-; Γ ⊢ e₁: τ₁ →ᵏ τ₂    Γ ⊢ e₂: τ₁
-; --------------------------------
-; Γ ⊢ (e₁ e₂): τ₂
-
-; --------------------------
-; Nat::Type₀, Unit::Type₀
-
-; τ::Typeᵢ
-; -------------
-; Ref τ :: Typeᵢ₊₁
-
-; τ₁::Typeᵢ, τ₂::Typeⱼ, k ≥ max-level(τ₁, τ₂)
-; -----------------------------------------
-; τ₁ →ᵏ τ₂ :: Typeₖ
-
-(require (only-in "stlc-ref.rkt" interpret))
-
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with)
   (check-core (desugar expr) with #hash()))
@@ -100,47 +82,3 @@
     [(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
-#;
-(interpret '
-  (let (id : (Nat → 0 Nat)) (λ x x)
-    (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-        (set r f
-          (f 0))))))
-#;
-(print (fmt '
-  (let (id : (Nat → 0 Nat)) (λ x x)
-    (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-        (set r f
-          (f 0)))))))
-
-(require rackunit)
-(check-exn
-  exn:fail?
-  (λ () (infer '
-    (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-          (set r f
-            (f 0))))))))
-
-(check-eq?
-  (infer '
-    (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-          (f 0)))))
-  'Nat)
-
-(check-eq?
-  (check '
-    (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-          (f 0))))
-    'Nat)
-  #t)
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 342f265..84103bb 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -1,5 +1,6 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with iso-recursive types
@@ -92,6 +93,6 @@
     ; 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))]
+    [x #:when (equal? x key) value]
     [v v]))
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index 41aec59..d0afec0 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -1,5 +1,7 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
+(provide interpret check infer)
 
 ;; The Simply-Typed Lambda Calculus with references
 
@@ -88,15 +90,3 @@
         [t (err (format "expected → type on application body, got ~a" t))])]
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
-
-(provide interpret check infer)
-
-; simple diverging program in STLC-ref
-; https://www.youtube.com/watch?v=XNgE8kBfSz8
-#;
-(interpret '
-  (let (id : (Nat → Nat)) (λ x x)
-    (let (r : (Ref (Nat → Nat))) (new id)
-      (let (f : (Nat → Nat)) (λ x ((! r) x))
-        (set r f
-          (f 0))))))
diff --git a/stlc.rkt b/stlc.rkt
index 820197b..2ed7d90 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -1,32 +1,32 @@
 #lang racket
 (require "lib.rkt")
+(require "base.rkt")
+(provide interpret check infer)
 
 ;; The Simply-Typed Lambda Calculus
 
-;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr)
-  (interpret-core (strip expr) #hash()))
-(define (interpret-core expr Γ)
-  (match expr
+;;      (interpret Expr Context): Value
+(define (interpret expr [Γ #hash()])
+  (match (strip expr)
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
     [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret-core e1 Γ)
-        [`(λ ,x ,e ,env) (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
-        [e `(,e ,(interpret-core e2 Γ))])]
+      (match (interpret e1 Γ)
+        [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))]
+        [e `(,e ,(interpret e2 Γ))])]
     [e e]))
 
-;;      (check Expr Type Table[Sym, Type]): Bool
+;;      (check Expr Type Context): Bool
 (define (check expr with [Γ #hash()])
   (match expr
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
-          (and (equal? t t1) (check e t2 (dict-set Γ x)))]
+          (and (equal? t t1) (check e t2 (dict-set Γ x t)))]
         [_ #f])]
-    [_ (equal? (infer with Γ) with)]))
+    [_ (equal? with (infer with Γ))]))
 
-;;      (infer Expr Table[Sym, Type]): Type
+;;      (infer Expr Context): Type
 (define (infer expr [Γ #hash()])
   (match expr
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
@@ -39,5 +39,3 @@
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
         [t (err (format "expected → type on application body, got ~a" t))])]
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
-
-(provide interpret check infer)
diff --git a/tests/stlc-dll.rkt b/tests/stlc-dll.rkt
new file mode 100644
index 0000000..87034ab
--- /dev/null
+++ b/tests/stlc-dll.rkt
@@ -0,0 +1,225 @@
+#lang racket
+(require (except-in rackunit check))
+(require "../stlc-dll.rkt")
+
+(define-test-suite let-set-inc-case
+  (check-exn
+    exn:fail?
+    (λ () (infer '
+      (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
+      (set r f
+      (f 0))))))))
+
+  (check-eq?
+    (infer '
+      (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
+      (f 0)))))
+    'Nat)
+
+  (check-eq?
+    (check '
+      (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
+      (f 0))))
+      'Nat)
+    #t)
+
+  (check-eq? (interpret '(if #t 1 0)) 1)
+  (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
+  (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
+  (check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
+
+  (check-equal?
+    (infer
+      '(case ((inr sole) : (Nat ⊕ Unit))
+        (x ⇒ 0) (x ⇒ 1))) 'Nat)
+
+  (check-true
+    (check
+      '(case ((inr sole) : (Nat ⊕ Unit))
+        (x ⇒ x)
+        (x ⇒ 1)) 'Nat))
+
+  (check-equal?
+    (interpret
+      '((λ p1 (car (unfold p1)))
+        (fold
+          (pair 413
+          (pair (inl sole)
+                (inl sole))))))
+    413))
+
+;; initial implementation of doubly linked lists:
+;; (type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))
+(define-test-suite dll-no-empty-lists
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let get
+      (λ x (car (unfold x)))
+     (let my_list
+      (fold
+        (pair 413
+        (pair (inl sole)
+              (inl sole))))
+     (get my_list)))))
+    413)
+
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let prev
+      (λ x
+        (case (car (cdr (unfold x)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
+     (let my_list
+      (fold
+        (pair 413
+        (pair (inl (new sole))
+              (inl (new sole)))))
+     (prev my_list)))))
+    '(inl sole))
+
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let next
+      (λ x
+        (case (cdr (cdr (unfold x)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
+     (let my_list
+      (fold
+        (pair 413
+        (pair (inr (new sole))
+              (inr (new sole)))))
+     (next my_list)))))
+    '(inr sole))
+
+  (check-true
+    (equiv-type
+      (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+        (λ (self : DoublyLinkedList)
+           (case (cdr (cdr (unfold self)))
+            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
+            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))))
+      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))
+      #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))))))
+
+  (check-true
+    (check
+      '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+        (λ (self : DoublyLinkedList)
+           (case (cdr (cdr (unfold self)))
+            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
+            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))
+      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))))
+
+  (check-equal?
+    (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+      (let (get : (DoublyLinkedList → 1 Nat))
+        (λ self (car (unfold self)))
+      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (car (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (cdr (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (my_list : DoublyLinkedList)
+        (fold
+          (pair 413
+          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
+                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
+      (prev my_list)))))))
+    '(DoublyLinkedList ⊕ Unit))
+
+  (check-true
+    (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+      (let (get : (DoublyLinkedList → 1 Nat))
+        (λ self (car (unfold self)))
+      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (car (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (cdr (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (my_list : DoublyLinkedList)
+        (fold
+          (pair 413
+          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
+                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
+      (prev my_list))))))
+      '(DoublyLinkedList ⊕ Unit))))
+
+;; new implementation of doubly linked lists:
+;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))
+(define-test-suite dll-with-empty-lists
+  (check-equal?
+    (interpret
+     '(let next
+      (λ self
+        (case (unfold self)
+          (some ⇒ (! (cdr (cdr some))))
+          (none ⇒ (fold (inr sole)))))
+     (let my_list
+      (fold
+        (inl
+          (pair 413
+          (pair (new (inr sole))
+                (new (inr sole))))))
+     (next my_list))))
+    '(inr sole))
+
+  (check-equal?
+    (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+      (λ (self : DoublyLinkedList)
+         (case (unfold self)
+          (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList))
+          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
+    '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
+
+  (check-true
+    (equiv-type
+      (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+        (λ (self : DoublyLinkedList)
+           (case (unfold self)
+            (some ⇒ (! (cdr (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
+    '(DoublyLinkedList → 1 DoublyLinkedList)
+      #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
+
+  (check-true
+    (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+      (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (inl (car some)))
+            (none ⇒ (inr sole))))
+      (let (prev : (DoublyLinkedList → 1 DoublyLinkedList))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (! (car (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
+      (let (next : (DoublyLinkedList → 1 DoublyLinkedList))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (! (cdr (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
+      (let (my_list : DoublyLinkedList)
+        (fold (inl
+          (pair 413
+          (pair (new ((fold (inr sole)) : DoublyLinkedList))
+                (new ((fold (inr sole)) : DoublyLinkedList))))))
+      (prev my_list))))))
+      'DoublyLinkedList)))
diff --git a/tests/stlc-ext.rkt b/tests/stlc-ext.rkt
new file mode 100644
index 0000000..ee39145
--- /dev/null
+++ b/tests/stlc-ext.rkt
@@ -0,0 +1,11 @@
+#lang racket
+(require (except-in rackunit check))
+(require "../stlc-ext.rkt")
+
+(check-true (equiv-term '(λ a a) '(λ b b) #hash()))
+(check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash()))
+(check-true (equiv-term '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash()))
+(check-eq? (interpret '(if #t 1 0)) 1)
+(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
+(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
+(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
diff --git a/tests/stlc-imp.rkt b/tests/stlc-imp.rkt
new file mode 100644
index 0000000..44e0c17
--- /dev/null
+++ b/tests/stlc-imp.rkt
@@ -0,0 +1,29 @@
+#lang racket
+(require (except-in rackunit check))
+(require "../stlc-imp.rkt")
+
+(define-test-suite landins-knot
+  (check-exn
+    exn:fail?
+    (λ () (infer '
+      (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (set r f
+      (f 0))))))))
+
+  (check-eq? ; fixme: this should fail
+    (infer '
+      (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (f 0)))))
+    'Nat)
+
+  (check-true
+    (check '
+      (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (f 0))))
+      'Nat)))
diff --git a/tests/stlc-pred.rkt b/tests/stlc-pred.rkt
new file mode 100644
index 0000000..f7afc43
--- /dev/null
+++ b/tests/stlc-pred.rkt
@@ -0,0 +1,29 @@
+#lang racket
+(require (except-in rackunit check))
+(require "../stlc-pred.rkt")
+
+(define-test-suite landins-knot
+  (check-exn
+    exn:fail?
+    (λ () (infer '
+      (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (set r f
+      (f 0))))))))
+
+  (check-eq?
+    (infer '
+      (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (f 0)))))
+    'Nat)
+
+  (check-true
+    (check '
+      (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
+      (f 0))))
+      'Nat)))
diff --git a/tests/stlc.rkt b/tests/stlc.rkt
new file mode 100644
index 0000000..154e77d
--- /dev/null
+++ b/tests/stlc.rkt
@@ -0,0 +1,8 @@
+#lang racket
+(require (except-in rackunit check))
+(require "../stlc.rkt")
+
+(check-equal? (interpret '(λ x x)) '(λ x x #hash()))
+(check-equal? (interpret '((λ a a) (x y))) '(x y))
+(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y))
+(check-equal? (interpret '((λ a (a y)) x)) '(x y))
-- 
cgit v1.2.3-70-g09d2