split lib into lib and base; move tests to separate files & directory

5 files changed, 302 insertions, 0 deletions

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))