Day6

aoc2024/SortedMap.newt

@@ -1,5 +1,7 @@
 module SortedMap
 
+import Prelude
+
 data T23 : Nat -> U -> U -> U where
   Leaf : ∀ k v. k -> v -> T23 Z k v
   Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
@@ -41,7 +43,6 @@ insertT23 key value (Node3 t1 k1 t2 k2 t3) =
       Left t3' => Left (Node3 t1 k1 t2 k2 t3')
       Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
 
--- There is no empty tree23?
 data SortedMap : U -> U -> U where
   EmptyMap : ∀ k v. SortedMap k v
   MapOf : ∀ k v h. T23 h k v -> SortedMap k v
@@ -56,3 +57,19 @@ updateMap k v (MapOf map) = case insertT23 k v map of
   Left map' => MapOf map'
   Right (a, b, c) => MapOf (Node2 a b c)
 
+-- FIXME this doesn't work in a `where` because the erased args are un-erased
+toList' : ∀ k v h. T23 h k v → List (k × v) → List (k × v)
+toList' (Leaf k v) acc = (k, v) :: acc
+toList' (Node2 t1 k1 t2) acc = toList' t2 (toList' t1 acc)
+toList' (Node3 t1 k1 t2 k2 t3) acc = toList' t3 $ toList' t2 $ toList' t1 acc
+
+toList : ∀ k v. SortedMap k v → List (k × v)
+toList {k} {v} (MapOf smap) = reverse $ toList' smap Nil
+  -- FIXME erasure checking false positive - maybe because I'm not handling the top level args yet
+  -- where
+  --   foo : ∀ k v h. T23 h k v → List (k × v) → List (k × v)
+  --   foo (Leaf k v) acc = (k, v) :: acc
+  --   foo (Node2 t1 k1 t2) acc = foo t2 (foo t1 acc)
+  --   foo (Node3 t1 k1 t2 k2 t3) acc = foo t3 $ foo t2 $ foo t1 acc
+toList _ = Nil
+