@@ -46,17 +46,17 @@ type family Combine (a :: v) (b :: v) :: v
47{-| Delete elements from a map by key -}
47{-| Delete elements from a map by key -}
48type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
48type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
49− '[] :\ k = '[]
49+ '[] :\ k = '[]
50− ((k :-> v) ': m) :\ k = m :\ k
50+ ((k :-> v) ': m) :\ k = m :\ k
51− (kvp ': m) :\ k = kvp ': (m :\ k)
51+ (kvp ': m) :\ k = kvp ': (m :\ k)
53−{-| Lookup elements from a map -}
53+{-| Type-level lookup of elements from a map -}
54type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
54type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
55 Lookup '[] k = Nothing
55 Lookup '[] k = Nothing
56 Lookup ((k :-> v) ': m) k = Just v
56 Lookup ((k :-> v) ': m) k = Just v
57 Lookup (kvp ': m) k = Lookup m k
57 Lookup (kvp ': m) k = Lookup m k
59−{-| Membership test -}
59+{-| Membership test as type function -}
60type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
60type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
61 Member k '[] = False
61 Member k '[] = False
62 Member k ((k :-> v) ': m) = True
62 Member k ((k :-> v) ': m) = True
@@ -117,7 +117,7 @@ instance Show (Map '[]) where
117 show Empty = "{}"
117 show Empty = "{}"
119instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
119instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
120− show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
120+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"
122class Show' t where
122class Show' t where
123 show' :: t -> String
123 show' :: t -> String
@@ -132,12 +132,13 @@ instance Eq (Map '[]) where
132instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
132instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
133 (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'
133 (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'
135−{-| Union of two finite maps -}
135+{-| Union of two finite maps (normalising) -}
136union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
136union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
137union s t = nub (quicksort (append s t))
137union s t = nub (quicksort (append s t))
139type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
139type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
141+{-| Append of two finite maps (non normalising) -}
141append :: Map s -> Map t -> Map (s :++ t)
142append :: Map s -> Map t -> Map (s :++ t)
142append Empty x = x
143append Empty x = x
143append (Ext k v xs) ys = Ext k v (append xs ys)
144append (Ext k v xs) ys = Ext k v (append xs ys)
@@ -152,11 +153,15 @@ class Sortable xs where
152instance Sortable '[] where
153instance Sortable '[] where
153 quicksort Empty = Empty
154 quicksort Empty = Empty
155−instance (Sortable (Filter FMin (k :-> v) xs),
156+instance (Sortable (Filter FMin (k :-> v) xs)
157+ , Sortable (Filter FMax (k :-> v) xs)
158+ , FilterV FMin k v xs
156− Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
159+ , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
160+ quicksort (Ext k v xs) =
157− quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))
161+ quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)
158− where less = filterV (Proxy::(Proxy FMin))
163+ less = filterV (Proxy::(Proxy FMin))
159− more = filterV (Proxy::(Proxy FMax))
164+ more = filterV (Proxy::(Proxy FMax))
161{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
166{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
162class FilterV (f::Flag) k v xs where
167class FilterV (f::Flag) k v xs where
@@ -165,13 +170,19 @@ class FilterV (f::Flag) k v xs where
165instance FilterV f k v '[] where
170instance FilterV f k v '[] where
166 filterV _ k v Empty = Empty
171 filterV _ k v Empty = Empty
168−instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
173+instance (Conder (Cmp x (k :-> v) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
169− filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))
174+ filterV f@Proxy k v (Ext k' v' xs) =
175+ cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))
170− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
176+ (Ext k' v' (filterV f k v xs))
172−instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where
180+ (Conder ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ)), FilterV FMax k v xs)
181+ => FilterV FMax k v (x ': xs) where
182+ filterV f@Proxy k v (Ext k' v' xs) =
173− filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))
183+ cond (Proxy::(Proxy ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ))))
174− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
184+ (Ext k' v' (filterV f k v xs))
176class Combinable t t' where
187class Combinable t t' where
177 combine :: t -> t' -> Combine t t'
188 combine :: t -> t' -> Combine t t'
@@ -191,7 +202,8 @@ instance {-# OVERLAPPABLE #-}
191 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
202 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
193instance {-# OVERLAPS #-}
204instance {-# OVERLAPS #-}
194− (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where
205+ (Combinable v v', Nubable ((k :-> Combine v v') ': s))
206+ => Nubable ((k :-> v) ': (k :-> v') ': s) where
195 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
207 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)