SortedMap uses any comparator
This commit is contained in:
@@ -82,7 +82,7 @@ strongConnect {k} st vtx =
|
||||
-- to ignore ambiguity from indirect solutions
|
||||
tarjan : ∀ k. {{Eq k}} {{Ord k}} → List (k × List k) → List (List k)
|
||||
tarjan {k} nodes =
|
||||
let g = foldMap const EmptyMap $ map mkVertex nodes in
|
||||
let g = foldMap const emptyMap $ map mkVertex nodes in
|
||||
.result $ foldl checkVertex (MkTState 0 Nil Nil g) $ map fst nodes
|
||||
where
|
||||
mkVertex : k × List k → k × TVertex k
|
||||
|
||||
@@ -2,50 +2,52 @@ module Data.SortedMap
|
||||
|
||||
import Prelude
|
||||
|
||||
-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
|
||||
|
||||
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
|
||||
Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
|
||||
|
||||
lookupT23 : ∀ h k v. {{Ord k}} -> k -> T23 h k v -> Maybe (k × v)
|
||||
lookupT23 key (Leaf k v)= case compare k key of
|
||||
lookupT23 : ∀ h k v. (k → k → Ordering) -> k -> T23 h k v -> Maybe (k × v)
|
||||
lookupT23 compare key (Leaf k v)= case compare k key of
|
||||
EQ => Just (k,v)
|
||||
_ => Nothing
|
||||
lookupT23 key (Node2 t1 k1 t2) =
|
||||
if key <= k1 then lookupT23 key t1 else lookupT23 key t2
|
||||
lookupT23 key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then lookupT23 key t1
|
||||
else if key <= k2 then lookupT23 key t2
|
||||
else lookupT23 key t3
|
||||
lookupT23 compare key (Node2 t1 k1 t2) =
|
||||
case compare key k1 of
|
||||
GT => lookupT23 compare key t2
|
||||
_ => lookupT23 compare key t1
|
||||
lookupT23 compare key (Node3 t1 k1 t2 k2 t3) =
|
||||
case compare key k1 of
|
||||
GT => case compare key k2 of
|
||||
GT => lookupT23 compare key t3
|
||||
_ => lookupT23 compare key t2
|
||||
_ => lookupT23 compare key t1
|
||||
|
||||
insertT23 : ∀ h k v. {{Ord k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
|
||||
insertT23 key value (Leaf k v) = case compare key k of
|
||||
insertT23 : ∀ h k v. (k → k → Ordering) -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
|
||||
insertT23 compare key value (Leaf k v) = case compare key k of
|
||||
EQ => Left (Leaf key value)
|
||||
LT => Right (Leaf key value, key, Leaf k v)
|
||||
GT => Right (Leaf k v, k, Leaf key value)
|
||||
insertT23 key value (Node2 t1 k1 t2) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node2 t1' k1 t2)
|
||||
Right (a,b,c) => Left (Node3 a b c k1 t2)
|
||||
else case insertT23 key value t2 of
|
||||
insertT23 compare key value (Node2 t1 k1 t2) =
|
||||
case compare key k1 of
|
||||
GT => case insertT23 compare key value t2 of
|
||||
Left t2' => Left (Node2 t1 k1 t2')
|
||||
Right (a,b,c) => Left (Node3 t1 k1 a b c)
|
||||
insertT23 key value (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node3 t1' k1 t2 k2 t3)
|
||||
Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
|
||||
else if key <= k2 then
|
||||
case insertT23 key value t2 of
|
||||
Left t2' => Left (Node3 t1 k1 t2' k2 t3)
|
||||
Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
|
||||
else
|
||||
case insertT23 key value t3 of
|
||||
Left t3' => Left (Node3 t1 k1 t2 k2 t3')
|
||||
Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
|
||||
_ => case insertT23 compare key value t1 of
|
||||
Left t1' => Left (Node2 t1' k1 t2)
|
||||
Right (a,b,c) => Left (Node3 a b c k1 t2)
|
||||
insertT23 compare key value (Node3 t1 k1 t2 k2 t3) =
|
||||
case compare key k1 of
|
||||
GT => case compare key k2 of
|
||||
GT => case insertT23 compare key value t3 of
|
||||
Left t3' => Left (Node3 t1 k1 t2 k2 t3')
|
||||
Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
|
||||
_ => case insertT23 compare key value t2 of
|
||||
Left t2' => Left (Node3 t1 k1 t2' k2 t3)
|
||||
Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
|
||||
_ =>
|
||||
case insertT23 compare key value t1 of
|
||||
Left t1' => Left (Node3 t1' k1 t2 k2 t3)
|
||||
Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
|
||||
|
||||
-- This is cribbed from Idris. Deleting nodes takes a bit of code.
|
||||
Hole : Nat → U → U → U
|
||||
@@ -84,52 +86,57 @@ merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l
|
||||
|
||||
-- height is erased in the data everywhere but the top, but needed for case
|
||||
-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
|
||||
deleteT23 : ∀ k v. {{Ord k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
|
||||
deleteT23 Z key (Leaf k v) = case compare k key of
|
||||
deleteT23 : ∀ k v. (k → k → Ordering) → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
|
||||
deleteT23 compare Z key (Leaf k v) = case compare k key of
|
||||
EQ => Right MkUnit
|
||||
_ => Left (Leaf k v)
|
||||
deleteT23 (S Z) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 Z key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right _ => Right t2
|
||||
else case deleteT23 Z key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right MkUnit => Right t1
|
||||
deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right MkUnit => Left (Node2 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t2)
|
||||
deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 (S h) key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right t1 => case t2 of
|
||||
Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
|
||||
Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
|
||||
else case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right t2 => case t1 of
|
||||
Node2 a b c => Right (Node3 a b c k1 t2)
|
||||
Node3 a b c d e => Left (Node4 a b c d e k1 t2)
|
||||
deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t1 => Left (merge1 t1 k1 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t2 => Left (merge2 t1 k1 t2 k2 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t3 => Left (merge3 t1 k1 t2 k2 t3)
|
||||
deleteT23 compare (S Z) key (Node2 t1 k1 t2) =
|
||||
case compare key k1 of
|
||||
GT => case deleteT23 compare Z key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right MkUnit => Right t1
|
||||
_ => case deleteT23 compare Z key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right _ => Right t2
|
||||
deleteT23 compare (S Z) key (Node3 t1 k1 t2 k2 t3) =
|
||||
case compare key k1 of
|
||||
GT => case compare key k2 of
|
||||
GT => case deleteT23 compare _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t2)
|
||||
_ => case deleteT23 compare _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t3)
|
||||
_ => case deleteT23 compare _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right MkUnit => Left (Node2 t2 k2 t3)
|
||||
deleteT23 compare (S (S h)) key (Node2 t1 k1 t2) =
|
||||
case compare key k1 of
|
||||
GT => case deleteT23 compare _ key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right t2 => case t1 of
|
||||
Node2 a b c => Right (Node3 a b c k1 t2)
|
||||
Node3 a b c d e => Left (Node4 a b c d e k1 t2)
|
||||
_ => case deleteT23 compare (S h) key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right t1 => case t2 of
|
||||
Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
|
||||
Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
|
||||
|
||||
|
||||
deleteT23 compare (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
|
||||
case compare key k1 of
|
||||
GT => case compare key k2 of
|
||||
GT => case deleteT23 compare _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t3 => Left (merge3 t1 k1 t2 k2 t3)
|
||||
_ => case deleteT23 compare _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t2 => Left (merge2 t1 k1 t2 k2 t3)
|
||||
_ => case deleteT23 compare _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t1 => Left (merge1 t1 k1 t2 k2 t3)
|
||||
|
||||
|
||||
treeLeft : ∀ h k v. T23 h k v → (k × v)
|
||||
treeLeft (Leaf k v) = (k, v)
|
||||
@@ -143,51 +150,51 @@ treeRight (Node3 _ _ _ _ t3) = treeRight t3
|
||||
|
||||
|
||||
data SortedMap : U -> U -> U where
|
||||
EmptyMap : ∀ k v. SortedMap k v
|
||||
-- not erased so we know what happens in delete
|
||||
MapOf : ∀ k v. {h : Nat} → T23 h k v -> SortedMap k v
|
||||
EmptyMap : ∀ k v. (k → k → Ordering) → SortedMap k v
|
||||
-- h not erased so we know what happens in delete
|
||||
MapOf : ∀ k v. {h : Nat} → (k → k → Ordering) → T23 h k v → SortedMap k v
|
||||
|
||||
deleteMap : ∀ k v. {{Ord k}} → k → SortedMap k v → SortedMap k v
|
||||
deleteMap key EmptyMap = EmptyMap
|
||||
deleteMap : ∀ k v. k → SortedMap k v → SortedMap k v
|
||||
deleteMap key m@(EmptyMap _) = m
|
||||
-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
|
||||
deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
|
||||
Left t => MapOf t
|
||||
Right t => EmptyMap
|
||||
deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
|
||||
Left t => MapOf t
|
||||
Right t => MapOf t
|
||||
deleteMap key (MapOf {k} {v} {Z} compare tree) = case deleteT23 compare Z key tree of
|
||||
Left t => MapOf compare t
|
||||
Right t => EmptyMap compare
|
||||
deleteMap key (MapOf {k} {v} {S n} compare tree) = case deleteT23 compare (S n) key tree of
|
||||
Left t => MapOf compare t
|
||||
Right t => MapOf compare t
|
||||
|
||||
leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
leftMost EmptyMap = Nothing
|
||||
leftMost (MapOf m) = Just (treeLeft m)
|
||||
leftMost (MapOf compare m) = Just (treeLeft m)
|
||||
leftMost _ = Nothing
|
||||
|
||||
rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
rightMost EmptyMap = Nothing
|
||||
rightMost (MapOf m) = Just (treeRight m)
|
||||
rightMost (MapOf compare m) = Just (treeRight m)
|
||||
rightMost _ = Nothing
|
||||
|
||||
-- TODO issue with metas and case if written as `do` block
|
||||
pop : ∀ k v. {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
|
||||
pop : ∀ k v. SortedMap k v → Maybe ((k × v) × SortedMap k v)
|
||||
pop m = case leftMost m of
|
||||
Just (k,v) => Just ((k,v), deleteMap k m)
|
||||
Nothing => Nothing
|
||||
|
||||
lookupMap : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe (k × v)
|
||||
lookupMap k EmptyMap = Nothing
|
||||
lookupMap k (MapOf map) = lookupT23 k map
|
||||
lookupMap : ∀ k v. k -> SortedMap k v -> Maybe (k × v)
|
||||
lookupMap k (MapOf compare map) = lookupT23 compare k map
|
||||
lookupMap k _ = Nothing
|
||||
|
||||
lookupMap' : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe v
|
||||
lookupMap' k EmptyMap = Nothing
|
||||
lookupMap' k (MapOf map) = snd <$> lookupT23 k map
|
||||
lookupMap' : ∀ k v. k -> SortedMap k v -> Maybe v
|
||||
lookupMap' k (MapOf compare map) = snd <$> lookupT23 compare k map
|
||||
lookupMap' k _ = Nothing
|
||||
|
||||
|
||||
updateMap : ∀ k v. {{Ord k}} -> k -> v -> SortedMap k v -> SortedMap k v
|
||||
updateMap k v EmptyMap = MapOf $ Leaf k v
|
||||
updateMap k v (MapOf map) = case insertT23 k v map of
|
||||
Left map' => MapOf map'
|
||||
Right (a, b, c) => MapOf (Node2 a b c)
|
||||
updateMap : ∀ k v. k -> v -> SortedMap k v -> SortedMap k v
|
||||
updateMap k v (EmptyMap compare) = MapOf compare $ Leaf k v
|
||||
updateMap k v (MapOf compare map) = case insertT23 compare k v map of
|
||||
Left map' => MapOf compare map'
|
||||
Right (a, b, c) => MapOf compare (Node2 a b c)
|
||||
|
||||
toList : ∀ k v. SortedMap k v → List (k × v)
|
||||
toList {k} {v} (MapOf smap) = reverse $ go smap Nil
|
||||
toList {k} {v} (MapOf compare smap) = reverse $ go smap Nil
|
||||
where
|
||||
go : ∀ h. T23 h k v → List (k × v) → List (k × v)
|
||||
go (Leaf k v) acc = (k, v) :: acc
|
||||
@@ -195,14 +202,17 @@ toList {k} {v} (MapOf smap) = reverse $ go smap Nil
|
||||
go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
|
||||
toList _ = Nil
|
||||
|
||||
mapFromList : ∀ k v. {{Ord k}} {{Eq k}} → List (k × v) → SortedMap k v
|
||||
mapFromList {k} {v} stuff = foldl go EmptyMap stuff
|
||||
emptyMap : ∀ k v. {{Ord k}} → SortedMap k v
|
||||
emptyMap = EmptyMap compare
|
||||
|
||||
mapFromList : ∀ k v. {{Ord k}} → List (k × v) → SortedMap k v
|
||||
mapFromList {k} {v} stuff = foldl go emptyMap stuff
|
||||
where
|
||||
go : SortedMap k v → k × v → SortedMap k v
|
||||
go map (k, v) = updateMap k v map
|
||||
|
||||
|
||||
foldMap : ∀ a b. {{Ord a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
|
||||
foldMap : ∀ a b. (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
|
||||
foldMap f m Nil = m
|
||||
foldMap f m ((a,b) :: xs) = case lookupMap a m of
|
||||
Nothing => foldMap f (updateMap a b m) xs
|
||||
|
||||
Reference in New Issue
Block a user