@@ -1,100 +1,222 @@
11{-# LANGUAGE CPP #-}
2+{-# LANGUAGE ConstraintKinds #-}
23{-# LANGUAGE FlexibleContexts #-}
34{-# LANGUAGE FlexibleInstances #-}
45{-# LANGUAGE GADTs #-}
6+{-# LANGUAGE InstanceSigs #-}
57{-# LANGUAGE LambdaCase #-}
68{-# LANGUAGE MultiParamTypeClasses #-}
79{-# LANGUAGE PatternGuards #-}
810{-# LANGUAGE PolyKinds #-}
911{-# LANGUAGE Rank2Types #-}
1012{-# LANGUAGE ScopedTypeVariables #-}
13+{-# LANGUAGE StandaloneDeriving #-}
1114{-# LANGUAGE TypeFamilies #-}
1215{-# LANGUAGE UndecidableInstances #-}
16+{-# LANGUAGE UndecidableSuperClasses #-}
1317
1418-- |Module containing @'PatchDMapWithMove' k v@ and associated functions, which represents a 'Patch' to a @'DMap' k v@ which can insert, update, delete, and
1519-- move values between keys.
1620module Data.Patch.DMapWithMove where
1721
18−import Data.Patch.Class
19−import Data.Patch.MapWithMove (PatchMapWithMove (..))
20−import qualified Data.Patch.MapWithMove as MapWithMove
21−
22−import Data.Constraint.Extras
23−import Data.Dependent.Map (DMap, DSum (..), GCompare (..))
22+import qualified Control.Category as Cat
23+--import qualified Control.Category.DecidablyEmpty as Cat
24+import Data.Constraint.Extras (Has')
25+import Data.Dependent.Map (DMap)
26+import Data.Dependent.Sum (DSum (..))
2427import qualified Data.Dependent.Map as DMap
25−import Data.Functor.Constant
28+import Data.Functor.Constant (Constant (..))
2629import Data.Functor.Misc
27−import Data.Functor.Product
28−import Data.GADT.Compare (GEq (..))
29−import Data.GADT.Show (GShow, gshow)
30+ ( Const2 (..), Proxy3 (..)
31+ , weakenDMapWith
32+ , dmapToMapWith
33+ )
34+import Data.Functor.Product (Product (..))
35+import Data.GADT.Compare (GEq (..), GCompare (..))
36+import Data.GADT.Show (GRead, GShow, gshow)
3037import qualified Data.Map as Map
3138import Data.Maybe
3239import Data.Semigroup (Semigroup (..), (<>))
40+import Data.Semigroupoid as Cat
3341import Data.Some (Some(Some))
34−import Data.These
42+import Data.Proxy (Proxy (..))
43+import Data.These (These (..))
3544
36−-- | Like 'PatchMapWithMove', but for 'DMap'. Each key carries a 'NodeInfo' which describes how it will be changed by the patch and connects move sources and
37−-- destinations.
45+import Data.Patch.Class
46+ ( Patch (..), PatchHet (..)
47+ , PatchHet2 (..), PatchSource1, PatchTarget1
48+ , applyAlwaysHet2
49+ )
50+import Data.Patch.MapWithMove (PatchMapWithMove (..))
51+import qualified Data.Patch.MapWithMove as MapWithMove
52+
53+-- | Like 'PatchMapWithMove', but for 'DMap'. Each key carries a 'NodeInfo'
54+-- which describes how it will be changed by the patch and connects move sources
55+-- and destinations.
3856--
3957-- Invariants:
4058--
41−-- * A key should not move to itself.
42−-- * A move should always be represented with both the destination key (as a 'From_Move') and the source key (as a @'ComposeMaybe' ('Just' destination)@)
59+-- * A key should not move to itself.
60+--
61+-- * A move should always be represented with both the destination key (as a
62+-- 'From_Move') and the source key (as a @'ComposeMaybe' ('Just'
63+-- destination)@)
4364newtype PatchDMapWithMove k v = PatchDMapWithMove (DMap k (NodeInfo k v))
4465
45−-- |Structure which represents what changes apply to a particular key. @_nodeInfo_from@ specifies what happens to this key, and in particular what other key
46−-- the current key is moving from, while @_nodeInfo_to@ specifies what key the current key is moving to if involved in a move.
47−data NodeInfo k v a = NodeInfo
48− { _nodeInfo_from :: !(From k v a)
49− -- ^Change applying to the current key, be it an insert, move, or delete.
50− , _nodeInfo_to :: !(To k a)
51− -- ^Where this key is moving to, if involved in a move. Should only be @ComposeMaybe (Just k)@ when there is a corresponding 'From_Move'.
66+--deriving instance ( GShow k
67+-- , HasZip Show k p
68+-- , Has' Show k (PatchTarget1 p)
69+-- ) => Show (PatchDMapWithMove k p)
70+--deriving instance ( GRead k
71+-- , HasZip Read k p
72+-- , Has' Read k (PatchTarget1 p)
73+-- ) => Read (PatchDMapWithMove k p)
74+--deriving instance ( GEq k
75+-- , HasZip Eq k p
76+-- , Has' Eq k (PatchTarget1 p)
77+-- ) => Eq (PatchDMapWithMove k p)
78+--deriving instance ( GCompare k
79+-- , HasZip Ord k p
80+-- , Has' Ord k (PatchTarget1 p)
81+-- ) => Ord (PatchDMapWithMove k p)
82+
83+-- | Structure which represents what changes apply to a particular key.
84+-- @_nodeInfo_from@ specifies what happens to this key, and in particular what
85+-- other key the current key is moving from, while @_nodeInfo_to@ specifies what
86+-- key the current key is moving to if involved in a move.
87+data NodeInfo k p a = NodeInfo
88+ { _nodeInfo_from :: !(From k p a)
89+ -- ^ Change applying to the current key, be it an insert, move, or delete.
90+ , _nodeInfo_to :: !(To k p a)
91+ -- ^ Where this key is moving to, if involved in a move. Should only be
92+ -- @ComposeMaybe (Just k)@ when there is a corresponding 'From_Move'.
5293 }
53− deriving (Show)
54−
55−-- |Structure describing a particular change to a key, be it inserting a new key (@From_Insert@), updating an existing key (@From_Insert@ again), deleting a
56−-- key (@From_Delete@), or moving a key (@From_Move@).
57−data From (k :: a -> *) (v :: a -> *) :: a -> * where
58− -- |Insert a new or update an existing key with the given value @v a@
59− From_Insert :: v a -> From k v a
60− -- |Delete the existing key
61− From_Delete :: From k v a
62− -- |Move the value from the given key @k a@ to this key. The source key should also have an entry in the patch giving the current key as @_nodeInfo_to@,
63− -- usually but not necessarily with @From_Delete@.
64− From_Move :: !(k a) -> From k v a
65− deriving (Show, Read, Eq, Ord)
66−
67−-- |Type alias for the "to" part of a 'NodeInfo'. @'ComposeMaybe' ('Just' k)@ means the key is moving to another key, @ComposeMaybe Nothing@ for any other
68−-- operation.
69−type To = ComposeMaybe
94+
95+--deriving instance ( Show (k a)
96+-- , Show (p a a)
97+-- , Show (PatchTarget1 p a)
98+-- ) => Show (NodeInfo k p a)
99+--deriving instance ( Read (k a)
100+-- , Read (p a a)
101+-- , Read (PatchTarget1 p a)
102+-- ) => Read (NodeInfo k p a)
103+--deriving instance ( Eq (k a)
104+-- , Eq (p a a)
105+-- , Eq (PatchTarget1 p a)
106+-- ) => Eq (NodeInfo k p a)
107+--deriving instance ( Ord (k a)
108+-- , Ord (p a a)
109+-- , Ord (PatchTarget1 p a)
110+-- ) => Ord (NodeInfo k p a)
111+
112+-- | Structure describing a particular change to a key, be it inserting a new
113+-- key (@From_Insert@), updating an existing key (@From_Insert@ again), deleting
114+-- a key (@From_Delete@), or moving a key (@From_Move@).
115+--
116+-- This type isn't used directly as the from field patch, but is instead wrapped
117+-- in an existential. However, it is nice to be able to reason about this in
118+-- isolation as it is itself a @Semigroupoid@ when the underlying patch is.
119+data From (k :: a -> *) (p :: a -> a -> *) :: a -> * where
120+ -- | Insert a new or update an existing key with the given value @PatchTarget1
121+ -- p a@
122+ From_Insert :: PatchTarget1 p to -> From k p to
123+ -- | Delete the existing key
124+ From_Delete :: From k p to
125+ -- | Move the value from the given key @k a@ to this key. The source key
126+ -- should also have an entry in the patch giving the current key as
127+ -- @_nodeInfo_to@, usually but not necessarily with @From_Delete@.
128+ From_Move :: !(DSum k (Flip p to)) -> From k p to
129+
130+deriving instance ( Show (k a), GShow k
131+ , Has' Show k (Flip p a)
132+ , Show (PatchTarget1 p a)
133+ ) => Show (From k p a)
134+deriving instance ( Read (k a), GRead k
135+ , Has' Read k (Flip p a)
136+ , Read (PatchTarget1 p a)
137+ ) => Read (From k p a)
138+deriving instance ( GEq k
139+ , Has' Eq k (Flip p a)
140+ , Eq (PatchTarget1 p a)
141+ ) => Eq (From k p a)
142+deriving instance ( GCompare k
143+ , Has' Eq k (Flip p a) -- superclass bug
144+ , Has' Ord k (Flip p a)
145+ , Ord (PatchTarget1 p a)
146+ ) => Ord (From k p a)
147+
148+newtype Flip p to from = Flip (p from to)
149+
150+instance Cat.Category p => Cat.Category (Flip (p :: k -> k -> *)) where
151+ id = Flip Cat.id
152+ Flip y . Flip x = Flip $ x Cat.. y
153+
154+-- | The "to" part of a 'NodeInfo'. Rather than be built out of @From@ like @From@
155+-- is, we store just the information necessary to compose a @To@ and @From@ like
156+-- @oLocal@ composes two @From@s.
157+data To (k :: a -> *) (p :: a -> a -> *) :: a -> * where
158+ -- | Delete or leave in place
159+ To_NonMove :: To k p from
160+ -- | Move the value from the given key @k a@ to this key. The target key
161+ -- should also have an entry in the patch giving the current key in
162+ -- @_nodeInfo_from@, usually but not necessarily with @To_Delete@.
163+ To_Move :: !(DSum k (p from)) -> To k p from
164+
165+deriving instance ( Show (k a), GShow k
166+ , Has' Show k (p a)
167+ , Show (PatchTarget1 p a)
168+ ) => Show (To k p a)
169+deriving instance ( Read (k a), GRead k
170+ , Has' Read k (p a)
171+ , Read (PatchTarget1 p a)
172+ ) => Read (To k p a)
173+deriving instance ( GEq k
174+ , Has' Eq k (p a)
175+ , Eq (PatchTarget1 p a)
176+ ) => Eq (To k p a)
177+deriving instance ( GCompare k
178+ , Has' Eq k (p a) -- superclass bug
179+ , Has' Ord k (p a)
180+ , Ord (PatchTarget1 p a)
181+ ) => Ord (To k p a)
70182
71183-- |Test whether a 'PatchDMapWithMove' satisfies its invariants.
72−validPatchDMapWithMove :: forall k v. (GCompare k, GShow k) => DMap k (NodeInfo k v) -> Bool
184+validPatchDMapWithMove
185+ :: forall k v
186+ . (GCompare k, GShow k)
187+ => DMap k (NodeInfo k v)
188+ -> Bool
73189validPatchDMapWithMove = not . null . validationErrorsForPatchDMapWithMove
74190
75191-- |Enumerate what reasons a 'PatchDMapWithMove' doesn't satisfy its invariants, returning @[]@ if it's valid.
76−validationErrorsForPatchDMapWithMove :: forall k v. (GCompare k, GShow k) => DMap k (NodeInfo k v) -> [String]
192+validationErrorsForPatchDMapWithMove
193+ :: forall k v
194+ . (GCompare k, GShow k)
195+ => DMap k (NodeInfo k v)
196+ -> [String]
77197validationErrorsForPatchDMapWithMove m =
78198 noSelfMoves <> movesBalanced
79199 where
80200 noSelfMoves = mapMaybe selfMove . DMap.toAscList $ m
81− selfMove (dst :=> NodeInfo (From_Move src) _) | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
82− selfMove (src :=> NodeInfo _ (ComposeMaybe (Just dst))) | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
201+ selfMove (dst :=> NodeInfo (From_Move (src :=> _)) _)
202+ | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
203+ selfMove (src :=> NodeInfo _ (To_Move (dst :=> _)))
204+ | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
83205 selfMove _ = Nothing
84206 movesBalanced = mapMaybe unbalancedMove . DMap.toAscList $ m
85− unbalancedMove (dst :=> NodeInfo (From_Move src) _) =
207+ unbalancedMove (dst :=> NodeInfo (From_Move (src :=> _)) _) =
86208 case DMap.lookup src m of
87209 Nothing -> Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key is not in the patch"
88− Just (NodeInfo _ (ComposeMaybe (Just dst'))) ->
210+ Just (NodeInfo _ (To_Move (dst' :=> _))) ->
89211 if isNothing (dst' `geq` dst)
90212 then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
91213 else Nothing
92214 _ ->
93215 Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key has no move to key"
94− unbalancedMove (src :=> NodeInfo _ (ComposeMaybe (Just dst))) =
216+ unbalancedMove (src :=> NodeInfo _ (To_Move (dst :=> _))) =
95217 case DMap.lookup dst m of
96218 Nothing -> Just $ " unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
97− Just (NodeInfo (From_Move src') _) ->
219+ Just (NodeInfo (From_Move (src' :=> _)) _) ->
98220 if isNothing (src' `geq` src)
99221 then Just $ "unbalanced move at source key " <> gshow src <> " to " <> gshow dst <> " is coming from " <> gshow src' <> " instead"
100222 else Nothing
@@ -103,35 +225,49 @@ validationErrorsForPatchDMapWithMove m =
103225 Just $ "unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not moving"
104226 unbalancedMove _ = Nothing
105227
106−-- |Test whether two @'PatchDMapWithMove' k v@ contain the same patch operations.
107−instance (GEq k, Has' Eq k (NodeInfo k v)) => Eq (PatchDMapWithMove k v) where
108− PatchDMapWithMove a == PatchDMapWithMove b = a == b
109−
110228-- |Higher kinded 2-tuple, identical to @Data.Functor.Product@ from base ≥ 4.9
111229data Pair1 f g a = Pair1 (f a) (g a)
112230
113231-- |Helper data structure used for composing patches using the monoid instance.
114−data Fixup k v a
232+data Fixup k p a
115233 = Fixup_Delete
116− | Fixup_Update (These (From k v a) (To k a))
117−
118−-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
119−instance GCompare k => Semigroup (PatchDMapWithMove k v) where
234+ | Fixup_Update (These (From k p a) (To k p a))
235+
236+-- | Compose patches having the same effect as applying the patches in turn:
237+-- @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
238+instance ( GCompare k
239+ , Cat.Semigroupoid p
240+ -- , Cat.DecidablyEmpty p
241+ , PatchHet2 p
242+ , PatchSource1 p ~ PatchTarget1 p
243+ ) => Semigroup (PatchDMapWithMove k p) where
120244 PatchDMapWithMove ma <> PatchDMapWithMove mb = PatchDMapWithMove m
121245 where
122− connections = DMap.toList $ DMap.intersectionWithKey (\_ a b -> Pair1 (_nodeInfo_to a) (_nodeInfo_from b)) ma mb
123− h :: DSum k (Pair1 (ComposeMaybe k) (From k v)) -> [DSum k (Fixup k v)]
124− h (_ :=> Pair1 (ComposeMaybe mToAfter) editBefore) = case (mToAfter, editBefore) of
125− (Just toAfter, From_Move fromBefore)
126− | isJust $ fromBefore `geq` toAfter
127− -> [toAfter :=> Fixup_Delete]
128− | otherwise
129− -> [ toAfter :=> Fixup_Update (This editBefore)
130− , fromBefore :=> Fixup_Update (That (ComposeMaybe mToAfter))
131− ]
132− (Nothing, From_Move fromBefore) -> [fromBefore :=> Fixup_Update (That (ComposeMaybe mToAfter))] -- The item is destroyed in the second patch, so indicate that it is destroyed in the source map
133− (Just toAfter, _) -> [toAfter :=> Fixup_Update (This editBefore)]
134− (Nothing, _) -> []
246+ connections :: [DSum k (Pair1 (To k p) (From k p))]
247+ connections = DMap.toList $ DMap.intersectionWithKey
248+ (\_ a b -> Pair1 (_nodeInfo_to a) (_nodeInfo_from b))
249+ ma
250+ mb
251+ h :: DSum k (Pair1 (To k p) (From k p)) -> [DSum k (Fixup k p)]
252+ h ((_ :: k between) :=> Pair1 editAfter editBefore) = case (editAfter, editBefore) of
253+ (To_Move ((toAfter :: k after) :=> p1), From_Move ((fromBefore :: k before) :=> Flip p0)) ->
254+ --case toAfter `geq` fromBefore of
255+ -- Just Refl | Just Refl <- Cat.isId p0 ->
256+ -- [ toAfter :=> Fixup_Delete ]
257+ -- _ ->
258+ [ toAfter :=> Fixup_Update (This $ From_Move $ fromBefore :=> (Flip $ p1 `o` p0))
259+ , fromBefore :=> Fixup_Update (That $ To_Move $ toAfter :=> (p1 `o` p0))
260+ ]
261+ (To_NonMove, From_Move (fromBefore :=> _)) ->
262+ -- The item is destroyed in the second patch, so indicate that it is
263+ -- destroyed in the source map
264+ [fromBefore :=> Fixup_Update (That To_NonMove)]
265+ (To_Move (toAfter :=> p), From_Insert val) ->
266+ [toAfter :=> Fixup_Update (This $ From_Insert $ applyAlwaysHet2 p val)]
267+ (To_Move (toAfter :=> _), From_Delete) ->
268+ [toAfter :=> Fixup_Update (This From_Delete)]
269+ (To_NonMove, _) ->
270+ []
135271 mergeFixups _ Fixup_Delete Fixup_Delete = Fixup_Delete
136272 mergeFixups _ (Fixup_Update a) (Fixup_Update b)
137273 | This x <- a, That y <- b
@@ -162,13 +298,19 @@ instance GCompare k => Semigroup (PatchDMapWithMove k v) where
162298 These _ b -> Just b
163299 That b -> Just b
164300
165−-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
166−instance GCompare k => Monoid (PatchDMapWithMove k v) where
301+-- | Compose patches having the same effect as applying the patches in turn:
302+-- @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
303+instance ( GCompare k
304+ , Cat.Semigroupoid p
305+ -- , DecidablyEmpty p
306+ , PatchHet2 p
307+ , PatchSource1 p ~ PatchTarget1 p
308+ ) => Monoid (PatchDMapWithMove k p) where
167309 mempty = PatchDMapWithMove mempty
168310 mappend = (<>)
169311
170312{-
171−mappendPatchDMapWithMoveSlow :: forall k v. (ShowTag k v, GCompare k) => PatchDMapWithMove k v -> PatchDMapWithMove k v -> PatchDMapWithMove k v
313+mappendPatchDMapWithMoveSlow :: forall k v. (ShowTag k v, GCompare k) => PatchDMapWithMove k v -> PatchDMapWithMove k v -> PatchDMapWithMove k v
172314PatchDMapWithMove dstAfter srcAfter `mappendPatchDMapWithMoveSlow` PatchDMapWithMove dstBefore srcBefore = PatchDMapWithMove dst src
173315 where
174316 getDstAction k m = fromMaybe (From_Move k) $ DMap.lookup k m -- Any key that isn't present is treated as that key moving to itself
@@ -189,25 +331,31 @@ PatchDMapWithMove dstAfter srcAfter `mappendPatchDMapWithMoveSlow` PatchDMapWith
189331 src = DMap.mapMaybeWithKey g $ DMap.union srcAfter srcBefore
190332-}
191333
192−-- |Make a @'PatchDMapWithMove' k v@ which has the effect of inserting or updating a value @v a@ to the given key @k a@, like 'DMap.insert'.
193−insertDMapKey :: k a -> v a -> PatchDMapWithMove k v
334+-- | Make a @'PatchDMapWithMove' k v@ which has the effect of inserting or
335+-- updating a value @PatchTarget1 p a@ to the given key @k a@, like
336+-- 'DMap.insert'.
337+insertDMapKey :: k a -> PatchTarget1 p a -> PatchDMapWithMove k p
194338insertDMapKey k v =
195− PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) (ComposeMaybe Nothing)
339+ PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) To_NonMove
196340
197−-- |Make a @'PatchDMapWithMove' k v@ which has the effect of moving the value from the first key @k a@ to the second key @k a@, equivalent to:
341+-- | Make a @'PatchDMapWithMove' k v@ which has the effect of moving the value
342+-- from the first key @k a@ to the second key @k a@, equivalent to:
198343--
199344-- @
200345-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
201346-- @
202−moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
347+moveDMapKey
348+ :: GCompare k
349+ => k a -> k a -> PatchDMapWithMove k (Proxy3 v)
203350moveDMapKey src dst = case src `geq` dst of
204351 Nothing -> PatchDMapWithMove $ DMap.fromList
205− [ dst :=> NodeInfo (From_Move src) (ComposeMaybe Nothing)
206− , src :=> NodeInfo From_Delete (ComposeMaybe $ Just dst)
352+ [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) To_NonMove
353+ , src :=> NodeInfo From_Delete (To_Move $ dst :=> Proxy3)
207354 ]
208− Just _ -> mempty
355+ Just _ -> PatchDMapWithMove DMap.empty
209356
210−-- |Make a @'PatchDMapWithMove' k v@ which has the effect of swapping two keys in the mapping, equivalent to:
357+-- | Make a @'PatchDMapWithMove' k v@ which has the effect of swapping two keys
358+-- in the mapping, equivalent to:
211359--
212360-- @
213361-- let aMay = DMap.lookup a dmap
@@ -216,17 +364,18 @@ moveDMapKey src dst = case src `geq` dst of
216364-- . maybe id (DMap.insert b) (aMay `mplus` bMay)
217365-- . DMap.delete a . DMap.delete b $ dmap
218366-- @
219−swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
367+swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k (Proxy3 v)
220368swapDMapKey src dst = case src `geq` dst of
221369 Nothing -> PatchDMapWithMove $ DMap.fromList
222− [ dst :=> NodeInfo (From_Move src) (ComposeMaybe $ Just src)
223− , src :=> NodeInfo (From_Move dst) (ComposeMaybe $ Just dst)
370+ [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) (To_Move $ src :=> Proxy3)
371+ , src :=> NodeInfo (From_Move (dst :=> Flip Proxy3)) (To_Move $ dst :=> Proxy3)
224372 ]
225− Just _ -> mempty
373+ Just _ -> PatchDMapWithMove DMap.empty
226374
227−-- |Make a @'PatchDMapWithMove' k v@ which has the effect of deleting a key in the mapping, equivalent to 'DMap.delete'.
375+-- | Make a @'PatchDMapWithMove' k v@ which has the effect of deleting a key in
376+-- the mapping, equivalent to 'DMap.delete'.
228377deleteDMapKey :: k a -> PatchDMapWithMove k v
229−deleteDMapKey k = PatchDMapWithMove $ DMap.singleton k $ NodeInfo From_Delete $ ComposeMaybe Nothing
378+deleteDMapKey k = PatchDMapWithMove $ DMap.singleton k $ NodeInfo From_Delete To_NonMove
230379
231380{-
232381k1, k2 :: Const2 Int () ()
@@ -252,17 +401,20 @@ dst (PatchDMapWithMove x _) = x
252401src (PatchDMapWithMove _ x) = x
253402-}
254403
255−-- |Extract the 'DMap' representing the patch changes from the 'PatchDMapWithMove'.
404+-- | Extract the 'DMap' representing the patch changes from the
405+-- 'PatchDMapWithMove'.
256406unPatchDMapWithMove :: PatchDMapWithMove k v -> DMap k (NodeInfo k v)
257407unPatchDMapWithMove (PatchDMapWithMove p) = p
258408
259−-- |Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove', without checking any invariants.
409+-- | Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove',
410+-- without checking any invariants.
260411--
261412-- __Warning:__ when using this function, you must ensure that the invariants of 'PatchDMapWithMove' are preserved; they will not be checked.
262413unsafePatchDMapWithMove :: DMap k (NodeInfo k v) -> PatchDMapWithMove k v
263414unsafePatchDMapWithMove = PatchDMapWithMove
264415
265−-- |Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove' while checking invariants. If the invariants are satisfied, @Right p@ is returned
416+-- | Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove' while
417+-- checking invariants. If the invariants are satisfied, @Right p@ is returned
266418-- otherwise @Left errors@.
267419patchDMapWithMove :: (GCompare k, GShow k) => DMap k (NodeInfo k v) -> Either [String] (PatchDMapWithMove k v)
268420patchDMapWithMove dm =
@@ -270,94 +422,196 @@ patchDMapWithMove dm =
270422 [] -> Right $ unsafePatchDMapWithMove dm
271423 errs -> Left errs
272424
273−-- |Map a natural transform @v -> v'@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @'PatchDMapWithMove' k v'@.
274−mapPatchDMapWithMove :: forall k v v'. (forall a. v a -> v' a) -> PatchDMapWithMove k v -> PatchDMapWithMove k v'
275−mapPatchDMapWithMove f (PatchDMapWithMove p) = PatchDMapWithMove $
276− DMap.map (\ni -> ni { _nodeInfo_from = g $ _nodeInfo_from ni }) p
277− where g :: forall a. From k v a -> From k v' a
278− g = \case
425+-- | Map a natural transform @v -> v'@ over the given patch, transforming
426+-- @'PatchDMapWithMove' k v@ into @'PatchDMapWithMove' k v'@.
427+mapPatchDMapWithMove
428+ :: forall k p p'
429+ . (forall a. PatchTarget1 p a -> PatchTarget1 p' a)
430+ -> (forall from to. p from to -> p' from to)
431+ -> PatchDMapWithMove k p
432+ -> PatchDMapWithMove k p'
433+mapPatchDMapWithMove f g (PatchDMapWithMove m) =
434+ PatchDMapWithMove $ DMap.map (\ni -> NodeInfo
435+ { _nodeInfo_from = h $ _nodeInfo_from ni
436+ , _nodeInfo_to = j $ _nodeInfo_to ni
437+ }) m
438+ where h :: forall a. From k p a -> From k p' a
439+ h = \case
279440 From_Insert v -> From_Insert $ f v
280441 From_Delete -> From_Delete
281− From_Move k -> From_Move k
282−
283−-- |Traverse an effectful function @forall a. v a -> m (v ' a)@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @m ('PatchDMapWithMove' k v')@.
284−traversePatchDMapWithMove :: forall m k v v'. Applicative m => (forall a. v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
285−traversePatchDMapWithMove f = traversePatchDMapWithMoveWithKey $ const f
286−
287−-- |Map an effectful function @forall a. k a -> v a -> m (v ' a)@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @m ('PatchDMapWithMove' k v')@.
288−traversePatchDMapWithMoveWithKey :: forall m k v v'. Applicative m => (forall a. k a -> v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
289−traversePatchDMapWithMoveWithKey f (PatchDMapWithMove p) = PatchDMapWithMove <$> DMap.traverseWithKey (nodeInfoMapFromM . g) p
290− where g :: forall a. k a -> From k v a -> m (From k v' a)
291− g k = \case
442+ From_Move (k :=> Flip p) -> From_Move $ k :=> Flip (g p)
443+ j :: forall a. To k p a -> To k p' a
444+ j = \case
445+ To_NonMove -> To_NonMove
446+ To_Move (k :=> p) -> To_Move $ k :=> g p
447+
448+-- | Traverse an effectful function @forall a. PatchTarget1 p a -> m (v ' a)@
449+-- over the given patch, transforming @'PatchDMapWithMove' k v@ into @m
450+-- ('PatchDMapWithMove' k v')@.
451+traversePatchDMapWithMove
452+ :: forall m k p p'
453+ . Applicative m
454+ => (forall a. PatchTarget1 p a -> m (PatchTarget1 p' a))
455+ -> (forall from to. p from to -> m (p' from to))
456+ -> PatchDMapWithMove k p
457+ -> m (PatchDMapWithMove k p')
458+traversePatchDMapWithMove f g = traversePatchDMapWithMoveWithKey
459+ (\_ -> f)
460+ (\_ _ -> g)
461+
462+-- | Map an effectful function @forall a. k a -> PatchTarget1 p a -> m (v ' a)@
463+-- over the given patch, transforming @'PatchDMapWithMove' k v@ into @m
464+-- ('PatchDMapWithMove' k v')@.
465+traversePatchDMapWithMoveWithKey
466+ :: forall m k p p'
467+ . Applicative m
468+ => (forall a. k a -> PatchTarget1 p a -> m (PatchTarget1 p' a))
469+ -> (forall from to. k from -> k to -> p from to -> m (p' from to))
470+ -> PatchDMapWithMove k p
471+ -> m (PatchDMapWithMove k p')
472+traversePatchDMapWithMoveWithKey f g (PatchDMapWithMove m) =
473+ PatchDMapWithMove <$> DMap.traverseWithKey (\k ni -> NodeInfo
474+ <$> h k (_nodeInfo_from ni)
475+ <*> j k (_nodeInfo_to ni)) m
476+ where h :: forall a. k a -> From k p a -> m (From k p' a)
477+ h k = \case
292478 From_Insert v -> From_Insert <$> f k v
293479 From_Delete -> pure From_Delete
294− From_Move fromKey -> pure $ From_Move fromKey
295−
296−-- |Map a function which transforms @'From' k v a@ into a @'From' k v' a@ over a @'NodeInfo' k v a@.
297−nodeInfoMapFrom :: (From k v a -> From k v' a) -> NodeInfo k v a -> NodeInfo k v' a
298−nodeInfoMapFrom f ni = ni { _nodeInfo_from = f $ _nodeInfo_from ni }
299−
300−-- |Map an effectful function which transforms @'From' k v a@ into a @f ('From' k v' a)@ over a @'NodeInfo' k v a@.
301−nodeInfoMapFromM :: Functor f => (From k v a -> f (From k v' a)) -> NodeInfo k v a -> f (NodeInfo k v' a)
302−nodeInfoMapFromM f ni = fmap (\result -> ni { _nodeInfo_from = result }) $ f $ _nodeInfo_from ni
303−
304−-- |Weaken a 'PatchDMapWithMove' to a 'PatchMapWithMove' by weakening the keys from @k a@ to @'Some' k@ and applying a given weakening function @v a -> v'@ to
305−-- values.
306−weakenPatchDMapWithMoveWith :: forall k v v'. (forall a. v a -> v') -> PatchDMapWithMove k v -> PatchMapWithMove (Some k) v'
307−weakenPatchDMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ weakenDMapWith g p
308− where g :: forall a. NodeInfo k v a -> MapWithMove.NodeInfo (Some k) v'
309− g ni = MapWithMove.NodeInfo
480+ From_Move (fromKey :=> Flip p) -> From_Move . (fromKey :=>) . Flip <$> g fromKey k p
481+ j :: forall a. k a -> To k p a -> m (To k p' a)
482+ j k = \case
483+ To_NonMove -> pure To_NonMove
484+ To_Move (toKey :=> p) -> To_Move . (toKey :=>) <$> g k toKey p
485+
486+-- | Map a function which transforms @'From k PatchTarget1 p a@ into a @'From k
487+-- PatchTarget1 p' a@ over a @'NodeInfo' k PatchTarget1 p a@.
488+nodeInfoMapFrom
489+ :: (From k p a -> From k p' a)
490+ -> (To k p a -> To k p' a)
491+ -> NodeInfo k p a
492+ -> NodeInfo k p' a
493+nodeInfoMapFrom f g ni = NodeInfo
494+ { _nodeInfo_from = f $ _nodeInfo_from ni
495+ , _nodeInfo_to = g $ _nodeInfo_to ni
496+ }
497+
498+-- | Map an effectful function which transforms @'From k PatchTarget1 p a@ into
499+-- a @f ('From k PatchTarget1 p' a)@ over a @'NodeInfo' k PatchTarget1 p a@.
500+nodeInfoMapFromM
501+ :: Applicative f
502+ => (From k p a -> f (From k p' a))
503+ -> (To k p a -> f (To k p' a))
504+ -> NodeInfo k p a
505+ -> f (NodeInfo k p' a)
506+nodeInfoMapFromM f g ni = NodeInfo
507+ <$> f (_nodeInfo_from ni)
508+ <*> g (_nodeInfo_to ni)
509+
510+-- | Weaken a 'PatchDMapWithMove' to a 'PatchMapWithMove' by weakening the keys
511+-- from @k a@ to @'Some' k@ and applying a given weakening function
512+-- @PatchTarget1 p a -> v'@ to values.
513+weakenPatchDMapWithMoveWith
514+ :: forall k p p'
515+ . (forall a. PatchTarget1 p a -> PatchTarget p')
516+ -> (forall from to. p from to -> p')
517+ -> PatchDMapWithMove k p
518+ -> PatchMapWithMove (Some k) p'
519+weakenPatchDMapWithMoveWith f g (PatchDMapWithMove m) =
520+ PatchMapWithMove $ weakenDMapWith h m
521+ where h :: forall a. NodeInfo k p a -> MapWithMove.NodeInfo (Some k) p'
522+ h ni = MapWithMove.NodeInfo
310523 { MapWithMove._nodeInfo_from = case _nodeInfo_from ni of
311524 From_Insert v -> MapWithMove.From_Insert $ f v
312525 From_Delete -> MapWithMove.From_Delete
313− From_Move k -> MapWithMove.From_Move $ Some k
314− , MapWithMove._nodeInfo_to = Some <$> getComposeMaybe (_nodeInfo_to ni)
526+ From_Move (k :=> Flip p) -> MapWithMove.From_Move (Some k) $ g p
527+ , MapWithMove._nodeInfo_to = case _nodeInfo_to ni of
528+ To_NonMove -> MapWithMove.To_NonMove
529+ To_Move (k :=> p) -> MapWithMove.To_Move (Some k) $ g p
315530 }
316531
317−-- |"Weaken" a @'PatchDMapWithMove' (Const2 k a) v@ to a @'PatchMapWithMove' k v'@. Weaken is in scare quotes because the 'Const2' has already disabled any
318−-- dependency in the typing and all points are already @a@, hence the function to map each value to @v'@ is not higher rank.
319−patchDMapWithMoveToPatchMapWithMoveWith :: forall k v v' a. (v a -> v') -> PatchDMapWithMove (Const2 k a) v -> PatchMapWithMove k v'
320−patchDMapWithMoveToPatchMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ dmapToMapWith g p
321− where g :: NodeInfo (Const2 k a) v a -> MapWithMove.NodeInfo k v'
322− g ni = MapWithMove.NodeInfo
532+-- | "Weaken" a @'PatchDMapWithMove' (Const2 k a) v@ to a @'PatchMapWithMove' k
533+-- v'@. Weaken is in scare quotes because the 'Const2' has already disabled any
534+-- dependency in the typing and all points are already @a@, hence the function
535+-- to map each value to @v'@ is not higher rank.
536+patchDMapWithMoveToPatchMapWithMoveWith
537+ :: forall k p p' a
538+ . (PatchTarget1 p a -> PatchTarget p')
539+ -> (p a a -> p')
540+ -> PatchDMapWithMove (Const2 k a) p
541+ -> PatchMapWithMove k p'
542+patchDMapWithMoveToPatchMapWithMoveWith f g (PatchDMapWithMove m) =
543+ PatchMapWithMove $ dmapToMapWith h m
544+ where h :: NodeInfo (Const2 k a) p a -> MapWithMove.NodeInfo k p'
545+ h ni = MapWithMove.NodeInfo
323546 { MapWithMove._nodeInfo_from = case _nodeInfo_from ni of
324547 From_Insert v -> MapWithMove.From_Insert $ f v
325548 From_Delete -> MapWithMove.From_Delete
326− From_Move (Const2 k) -> MapWithMove.From_Move k
327− , MapWithMove._nodeInfo_to = unConst2 <$> getComposeMaybe (_nodeInfo_to ni)
549+ From_Move (Const2 k :=> Flip p) -> MapWithMove.From_Move k $ g p
550+ , MapWithMove._nodeInfo_to = case _nodeInfo_to ni of
551+ To_NonMove -> MapWithMove.To_NonMove
552+ To_Move (Const2 k :=> p) -> MapWithMove.To_Move k $ g p
328553 }
329554
330−-- |"Strengthen" a @'PatchMapWithMove' k v@ into a @'PatchDMapWithMove ('Const2' k a)@; that is, turn a non-dependently-typed patch into a dependently typed
331−-- one but which always has a constant key type represented by 'Const2'. Apply the given function to each @v@ to produce a @v' a@.
332−-- Completemented by 'patchDMapWithMoveToPatchMapWithMoveWith'
333−const2PatchDMapWithMoveWith :: forall k v v' a. (v -> v' a) -> PatchMapWithMove k v -> PatchDMapWithMove (Const2 k a) v'
334−const2PatchDMapWithMoveWith f (PatchMapWithMove p) = PatchDMapWithMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
335− where g :: (k, MapWithMove.NodeInfo k v) -> DSum (Const2 k a) (NodeInfo (Const2 k a) v')
555+-- | "Strengthen" a @'PatchMapWithMove' k v@ into a @'PatchDMapWithMove
556+-- ('Const2' k a)@; that is, turn a non-dependently-typed patch into a
557+-- dependently typed one but which always has a constant key type represented by
558+-- 'Const2'. Apply the given function to each @v@ to produce a @PatchTarget1 p'
559+-- a@. Completemented by 'patchDMapWithMoveToPatchMapWithMoveWith'
560+const2PatchDMapWithMoveWith
561+ :: forall k v v' a
562+ . (v -> v' a)
563+ -> PatchMapWithMove k (Proxy v)
564+ -> PatchDMapWithMove (Const2 k a) (Proxy3 v')
565+const2PatchDMapWithMoveWith f (PatchMapWithMove p) =
566+ PatchDMapWithMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
567+ where g :: (k, MapWithMove.NodeInfo k (Proxy v))
568+ -> DSum (Const2 k a) (NodeInfo (Const2 k a) (Proxy3 v'))
336569 g (k, ni) = Const2 k :=> NodeInfo
337570 { _nodeInfo_from = case MapWithMove._nodeInfo_from ni of
338571 MapWithMove.From_Insert v -> From_Insert $ f v
339572 MapWithMove.From_Delete -> From_Delete
340− MapWithMove.From_Move fromKey -> From_Move $ Const2 fromKey
341− , _nodeInfo_to = ComposeMaybe $ Const2 <$> MapWithMove._nodeInfo_to ni
573+ MapWithMove.From_Move fromKey Proxy -> From_Move $ Const2 fromKey :=> Flip Proxy3
574+ , _nodeInfo_to = case MapWithMove._nodeInfo_to ni of
575+ MapWithMove.To_NonMove -> To_NonMove
576+ MapWithMove.To_Move toKey Proxy -> To_Move $ Const2 toKey :=> Proxy3
342577 }
343578
344579-- | Apply the insertions, deletions, and moves to a given 'DMap'.
345−instance GCompare k => Patch (PatchDMapWithMove k v) where
346− type PatchTarget (PatchDMapWithMove k v) = DMap k v
347− apply (PatchDMapWithMove p) old = Just $! insertions `DMap.union` (old `DMap.difference` deletions) --TODO: return Nothing sometimes --Note: the strict application here is critical to ensuring that incremental merges don't hold onto all their prerequisite events forever; can we make this more robust?
348− where insertions = DMap.mapMaybeWithKey insertFunc p
349− insertFunc :: forall a. k a -> NodeInfo k v a -> Maybe (v a)
580+instance ( GCompare k
581+ , PatchHet2 p
582+ , PatchSource1 p ~ PatchTarget1 p
583+ ) => PatchHet (PatchDMapWithMove k p) where
584+ type PatchSource (PatchDMapWithMove k p) = DMap k (PatchSource1 p)
585+ type PatchTarget (PatchDMapWithMove k p) = DMap k (PatchTarget1 p)
586+
587+instance ( GCompare k
588+ , PatchHet2 p
589+ , PatchSource1 p ~ PatchTarget1 p
590+ ) => Patch (PatchDMapWithMove k p) where
591+ apply (PatchDMapWithMove m) old = Just $! insertions `DMap.union` (old `DMap.difference` deletions)
592+ -- TODO: return Nothing sometimes --Note: the strict application here is
593+ -- critical to ensuring that incremental merges don't hold onto all their
594+ -- prerequisite events forever; can we make this more robust?
595+ where insertions = DMap.mapMaybeWithKey insertFunc m
596+ insertFunc :: forall a. k a -> NodeInfo k p a -> Maybe (PatchTarget1 p a)
350597 insertFunc _ ni = case _nodeInfo_from ni of
351598 From_Insert v -> Just v
352− From_Move k -> DMap.lookup k old
599+ From_Move (k :=> Flip p) -> applyAlwaysHet2 p <$> DMap.lookup k old
353600 From_Delete -> Nothing
354− deletions = DMap.mapMaybeWithKey deleteFunc p
355− deleteFunc :: forall a. k a -> NodeInfo k v a -> Maybe (Constant () a)
601+ deletions = DMap.mapMaybeWithKey deleteFunc m
602+ deleteFunc :: forall a. k a -> NodeInfo k p a -> Maybe (Constant () a)
356603 deleteFunc _ ni = case _nodeInfo_from ni of
357604 From_Delete -> Just $ Constant ()
358605 _ -> Nothing
359606
360−-- | Get the values that will be replaced, deleted, or moved if the given patch is applied to the given 'DMap'.
361−getDeletionsAndMoves :: GCompare k => PatchDMapWithMove k v -> DMap k v' -> DMap k (Product v' (ComposeMaybe k))
607+-- | Get the values that will be replaced, deleted, or moved if the given patch
608+-- is applied to the given 'DMap'.
609+getDeletionsAndMoves
610+ :: ( GCompare k
611+ , PatchSource1 p ~ PatchTarget1 p
612+ )
613+ => PatchDMapWithMove k p
614+ -> DMap k (PatchSource1 p)
615+ -> DMap k (Product (PatchTarget1 p) (To k p))
362616getDeletionsAndMoves (PatchDMapWithMove p) m = DMap.intersectionWithKey f m p
363617 where f _ v ni = Pair v $ _nodeInfo_to ni