@@ -46,17 +46,17 @@ type family Combine (a :: v) (b :: v) :: v
4646
4747{-| Delete elements from a map by key -}
4848type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
49− '[] :\ k = '[]
50− ((k :-> v) ': m) :\ k = m :\ k
51− (kvp ': m) :\ k = kvp ': (m :\ k)
49+ '[] :\ k = '[]
50+ ((k :-> v) ': m) :\ k = m :\ k
51+ (kvp ': m) :\ k = kvp ': (m :\ k)
5252
53−{-| Type-level lookup of elements from a map -}
53+{-| Lookup elements from a map -}
5454type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
5555 Lookup '[] k = Nothing
5656 Lookup ((k :-> v) ': m) k = Just v
5757 Lookup (kvp ': m) k = Lookup m k
5858
59−{-| Membership test as type function -}
59+{-| Membership test -}
6060type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
6161 Member k '[] = False
6262 Member k ((k :-> v) ': m) = True
@@ -84,7 +84,7 @@ class IsMember v t m where
8484instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where
8585 lookp _ (Ext _ x _) = x
8686
87−instance {-# OVERLAPPABLE #-} IsMember v t m => IsMember v t (x ': m) where
87+instance IsMember v t m => IsMember v t (x ': m) where
8888 lookp v (Ext _ _ m) = lookp v m
8989
9090
@@ -100,12 +100,8 @@ instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) wher
100100instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
101101 update (Ext w y m) v x = Ext w y (update m v x)
102102
103−-- instance Updatable v t '[] '[v ':-> t] where
104−-- update Empty v x = Ext v x Empty
105−
106−instance Updatable v t s ((v ':-> t) ': s) where
107− update xs v x = Ext v x xs
108−
103+instance Updatable v t '[] '[v ':-> t] where
104+ update Empty v x = Ext v x Empty
109105
110106{-| Predicate to check if in normalised map form -}
111107type IsMap s = (s ~ Nub (Sort s))
@@ -121,7 +117,7 @@ instance Show (Map '[]) where
121117 show Empty = "{}"
122118
123119instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
124− show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"
120+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
125121
126122class Show' t where
127123 show' :: t -> String
@@ -133,22 +129,15 @@ instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s))
133129instance Eq (Map '[]) where
134130 Empty == Empty = True
135131
136−instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
137− (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
138−
139−instance Ord (Map '[]) where
140− compare Empty Empty = EQ
132+instance (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'
141134
142−instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where
143− compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'
144−
145−{-| Union of two finite maps (normalising) -}
135+{-| Union of two finite maps -}
146136union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
147137union s t = nub (quicksort (append s t))
148138
149139type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
150140
151−{-| Append of two finite maps (non normalising) -}
152141append :: Map s -> Map t -> Map (s :++ t)
153142append Empty x = x
154143append (Ext k v xs) ys = Ext k v (append xs ys)
@@ -163,15 +152,11 @@ class Sortable xs where
163152instance Sortable '[] where
164153 quicksort Empty = Empty
165154
166−instance (Sortable (Filter FMin (k :-> v) xs)
167− , Sortable (Filter FMax (k :-> v) xs)
168− , FilterV FMin k v xs
169− , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
170− quicksort (Ext k v xs) =
171− quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)
172− where
173− less = filterV (Proxy::(Proxy FMin))
174− more = filterV (Proxy::(Proxy FMax))
155+instance (Sortable (Filter 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
157+ quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))
158+ where less = filterV (Proxy::(Proxy FMin))
159+ more = filterV (Proxy::(Proxy FMax))
175160
176161{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
177162class FilterV (f::Flag) k v xs where
@@ -180,19 +165,13 @@ class FilterV (f::Flag) k v xs where
180165instance FilterV f k v '[] where
181166 filterV _ k v Empty = Empty
182167
183−instance (Conder (Cmp x (k :-> v) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
184− filterV f@Proxy k v (Ext k' v' xs) =
185− cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))
186− (Ext k' v' (filterV f k v xs))
187− (filterV f k v xs)
168+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)))
170+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
188171
189−instance
190− (Conder ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ)), FilterV FMax k v xs)
191− => FilterV FMax k v (x ': xs) where
192− filterV f@Proxy k v (Ext k' v' xs) =
193− cond (Proxy::(Proxy ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ))))
194− (Ext k' v' (filterV f k v xs))
195− (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
173+ filterV f@Proxy k v (Ext k' v' xs) = 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)
196175
197176class Combinable t t' where
198177 combine :: t -> t' -> Combine t t'
@@ -212,8 +191,7 @@ instance {-# OVERLAPPABLE #-}
212191 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
213192
214193instance {-# OVERLAPS #-}
215− (Combinable v v', Nubable ((k :-> Combine v v') ': s))
216− => Nubable ((k :-> v) ': (k :-> v') ': s) where
194+ (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where
217195 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
218196
219197