stlc-dll: reduce annotations on tests, reimplement doubly linked lists

1 files changed, 86 insertions, 28 deletions

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 927161a..98b6f85 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -263,7 +263,7 @@
     [`(! ,e)
       (match (infer-core e Γ)
         [`(Ref ,t) t]
-        [t (err "attempting to deref term not of Ref type!")])]
+        [t (err (format "attempting to deref term ~a of type ~a" e t))])]
     [`(set ,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(Ref ,t)
@@ -434,13 +434,17 @@
 
 (check-equal?
   (interpret
-    '((λ (p1 : DoublyLinkedList) (car (unfold p1)))
+    '((λ p1 (car (unfold p1)))
       (fold
         (pair 413
-        (pair ((inl sole) : (Unit ⊕ DoublyLinkedList))
-              ((inl sole) : (Unit ⊕ DoublyLinkedList)))))))
+        (pair (inl sole)
+              (inl sole))))))
   413)
 
+
+;; initial implementation of doubly linked lists:
+;; (type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))
+
 (check-equal?
   (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
    (let get
@@ -453,7 +457,6 @@
    (get my_list)))))
   413)
 
-
 (check-equal?
   (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
    (let prev
@@ -469,7 +472,6 @@
    (prev my_list)))))
   '(inl sole))
 
-
 (check-equal?
   (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
    (let next
@@ -487,8 +489,8 @@
 
 (check-equal?
   (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-    (λ (p3 : DoublyLinkedList)
-       (case (cdr (cdr (unfold p3)))
+    (λ (self : DoublyLinkedList)
+       (case (cdr (cdr (unfold self)))
         (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
         (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))))
   '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
@@ -496,8 +498,8 @@
 (check-true
   (check
     '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-      (λ (p3 : DoublyLinkedList)
-         (case (cdr (cdr (unfold p3)))
+      (λ (self : DoublyLinkedList)
+         (case (cdr (cdr (unfold self)))
           (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
           (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))
     '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))))
@@ -505,17 +507,17 @@
 (check-equal?
   (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
     (let (get : (DoublyLinkedList → 1 Nat))
-      (λ (p1 : DoublyLinkedList) (car (unfold p1)))
+      (λ self (car (unfold self)))
     (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ (p2 : DoublyLinkedList)
-        (case (car (cdr (unfold p2)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))
+      (λ self
+        (case (car (cdr (unfold self)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
     (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ (p3 : DoublyLinkedList)
-        (case (cdr (cdr (unfold p3)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))
+      (λ self
+        (case (cdr (cdr (unfold self)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
     (let (my_list : DoublyLinkedList)
       (fold
         (pair 413
@@ -527,17 +529,17 @@
 (check-true
   (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
     (let (get : (DoublyLinkedList → 1 Nat))
-      (λ (p1 : DoublyLinkedList) (car (unfold p1)))
+      (λ self (car (unfold self)))
     (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ (p2 : DoublyLinkedList)
-        (case (car (cdr (unfold p2)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))
+      (λ self
+        (case (car (cdr (unfold self)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
     (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ (p3 : DoublyLinkedList)
-        (case (cdr (cdr (unfold p3)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))
+      (λ self
+        (case (cdr (cdr (unfold self)))
+          (x ⇒ (inl (! x)))
+          (x ⇒ (inr sole))))
     (let (my_list : DoublyLinkedList)
       (fold
         (pair 413
@@ -545,3 +547,59 @@
               ((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)))
+
+(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))
+
+; issue: we only need annotations on the first case here because stlc-dll will try and return (μ Self (Nat × (Ref Self) × (Ref Self))) instead. this is perhaps bad, there should be some way to recover the original bindings... maybe??
+; todo: check should be able to place annotations on the right place idk
+; ok that is done. still original issue tho
+(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))))))
+  '(DoublyLinkedList → 1 DoublyLinkedList))
+
+(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))