@@ -0,0 +1,624 @@
1+{-# LANGUAGE CPP #-}
2+{-# LANGUAGE ConstraintKinds #-}
3+{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE FlexibleInstances #-}
5+{-# LANGUAGE GADTs #-}
6+{-# LANGUAGE InstanceSigs #-}
7+{-# LANGUAGE LambdaCase #-}
8+{-# LANGUAGE MultiParamTypeClasses #-}
9+{-# LANGUAGE PatternGuards #-}
10+{-# LANGUAGE PolyKinds #-}
11+{-# LANGUAGE Rank2Types #-}
12+{-# LANGUAGE ScopedTypeVariables #-}
13+{-# LANGUAGE StandaloneDeriving #-}
14+{-# LANGUAGE TypeFamilies #-}
15+{-# LANGUAGE UndecidableInstances #-}
16+{-# LANGUAGE UndecidableSuperClasses #-}
17+
18+-- |Module containing @'PatchDMapWithPatchingMove' k v@ and associated functions, which represents a 'Patch' to a @'DMap' k v@ which can insert, update, delete, and
19+-- move values between keys.
20+module Data.Patch.DMapWithPatchingMove where
21+
22+import qualified Control.Category as Cat
23+--import qualified Control.Category.DecidablyEmpty as Cat
24+
25+import Data.Constraint.Extras (Has')
26+import Data.Dependent.Map (DMap)
27+import Data.Dependent.Sum (DSum (..))
28+import qualified Data.Dependent.Map as DMap
29+import Data.Functor.Constant (Constant (..))
30+import Data.Functor.Misc
31+ ( Const2 (..), Proxy3 (..)
32+ , weakenDMapWith
33+ , dmapToMapWith
34+ )
35+import Data.Functor.Const (Const (..))
36+import Data.Functor.Product (Product (..))
37+import Data.GADT.Compare (GEq (..), GCompare (..))
38+import Data.GADT.Show (GRead, GShow, gshow)
39+import qualified Data.Map as Map
40+import Data.Maybe
41+import Data.Monoid.DecidablyEmpty
42+import Data.Semigroupoid as Cat
43+#if !MIN_VERSION_base(4,11,0)
44+import Data.Semigroup (Semigroup (..), (<>))
45+#endif
46+import Data.Some (Some (Some), mkSome)
47+import Data.Proxy (Proxy (..))
48+import Data.These (These (..))
49+import Data.Type.Equality ((:~:)(..))
50+
51+import Data.Patch.Class
52+ ( Patch (..), PatchHet (..)
53+ , PatchHet2 (..), PatchSource1, PatchTarget1
54+ , applyAlwaysHet2
55+ )
56+import Data.Patch.MapWithPatchingMove (PatchMapWithPatchingMove (..))
57+import qualified Data.Patch.MapWithPatchingMove as MapWithPatchingMove
58+
59+-- | Like 'PatchMapWithPatchingMove', but for 'DMap'. Each key carries a 'NodeInfo'
60+-- which describes how it will be changed by the patch and connects move sources
61+-- and destinations.
62+--
63+-- Invariants:
64+--
65+-- * A key should not move to itself.
66+--
67+-- * A move should always be represented with both the destination key (as a
68+-- 'From_Move') and the source key (as a @'ComposeMaybe' ('Just'
69+-- destination)@)
70+newtype PatchDMapWithPatchingMove k v = PatchDMapWithPatchingMove (DMap k (NodeInfo k v))
71+
72+--deriving instance ( GShow k
73+-- , HasZip Show k p
74+-- , Has' Show k (PatchTarget1 p)
75+-- ) => Show (PatchDMapWithPatchingMove k p)
76+--deriving instance ( GRead k
77+-- , HasZip Read k p
78+-- , Has' Read k (PatchTarget1 p)
79+-- ) => Read (PatchDMapWithPatchingMove k p)
80+--deriving instance ( GEq k
81+-- , HasZip Eq k p
82+-- , Has' Eq k (PatchTarget1 p)
83+-- ) => Eq (PatchDMapWithPatchingMove k p)
84+--deriving instance ( GCompare k
85+-- , HasZip Ord k p
86+-- , Has' Ord k (PatchTarget1 p)
87+-- ) => Ord (PatchDMapWithPatchingMove k p)
88+
89+-- It won't let me derive for some reason
90+instance ( GCompare k
91+ , Cat.Semigroupoid v
92+ , PatchHet2 v
93+ , PatchSource1 v ~ PatchTarget1 v
94+ ) => DecidablyEmpty (PatchDMapWithPatchingMove k v) where
95+ isEmpty (PatchDMapWithPatchingMove m) = DMap.null m
96+
97+-- | Structure which represents what changes apply to a particular key.
98+-- @_nodeInfo_from@ specifies what happens to this key, and in particular what
99+-- other key the current key is moving from, while @_nodeInfo_to@ specifies what
100+-- key the current key is moving to if involved in a move.
101+data NodeInfo k p a = NodeInfo
102+ { _nodeInfo_from :: !(From k p a)
103+ -- ^ Change applying to the current key, be it an insert, move, or delete.
104+ , _nodeInfo_to :: !(To k)
105+ -- ^ Where this key is moving to, if involved in a move. Should only be
106+ -- @ComposeMaybe (Just k)@ when there is a corresponding 'From_Move'.
107+ }
108+
109+--deriving instance ( Show (k a)
110+-- , Show (p a a)
111+-- , Show (PatchTarget1 p a)
112+-- ) => Show (NodeInfo k p a)
113+--deriving instance ( Read (k a)
114+-- , Read (p a a)
115+-- , Read (PatchTarget1 p a)
116+-- ) => Read (NodeInfo k p a)
117+--deriving instance ( Eq (k a)
118+-- , Eq (p a a)
119+-- , Eq (PatchTarget1 p a)
120+-- ) => Eq (NodeInfo k p a)
121+--deriving instance ( Ord (k a)
122+-- , Ord (p a a)
123+-- , Ord (PatchTarget1 p a)
124+-- ) => Ord (NodeInfo k p a)
125+
126+-- | Structure describing a particular change to a key, be it inserting a new
127+-- key (@From_Insert@), updating an existing key (@From_Insert@ again), deleting
128+-- a key (@From_Delete@), or moving a key (@From_Move@).
129+--
130+-- This type isn't used directly as the from field patch, but is instead wrapped
131+-- in an existential. However, it is nice to be able to reason about this in
132+-- isolation as it is itself a @Semigroupoid@ when the underlying patch is.
133+data From (k :: a -> *) (p :: a -> a -> *) :: a -> * where
134+ -- | Insert a new or update an existing key with the given value @PatchTarget1
135+ -- p a@
136+ From_Insert :: PatchTarget1 p to -> From k p to
137+ -- | Delete the existing key
138+ From_Delete :: From k p to
139+ -- | Move the value from the given key @k a@ to this key. The source key
140+ -- should also have an entry in the patch giving the current key as
141+ -- @_nodeInfo_to@, usually but not necessarily with @From_Delete@.
142+ From_Move :: !(DSum k (Flip p to)) -> From k p to
143+
144+deriving instance ( Show (k a), GShow k
145+ , Has' Show k (Flip p a)
146+ , Show (PatchTarget1 p a)
147+ ) => Show (From k p a)
148+deriving instance ( Read (k a), GRead k
149+ , Has' Read k (Flip p a)
150+ , Read (PatchTarget1 p a)
151+ ) => Read (From k p a)
152+deriving instance ( GEq k
153+ , Has' Eq k (Flip p a)
154+ , Eq (PatchTarget1 p a)
155+ ) => Eq (From k p a)
156+deriving instance ( GCompare k
157+ , Has' Eq k (Flip p a) -- superclass bug
158+ , Has' Ord k (Flip p a)
159+ , Ord (PatchTarget1 p a)
160+ ) => Ord (From k p a)
161+
162+newtype Flip p to from = Flip (p from to)
163+
164+instance Cat.Category p => Cat.Category (Flip (p :: k -> k -> *)) where
165+ id = Flip Cat.id
166+ Flip y . Flip x = Flip $ x Cat.. y
167+
168+-- | The "to" part of a 'NodeInfo'. Rather than be built out of @From@ like @From@
169+-- is, we store just the information necessary to compose a @To@ and @From@ like
170+-- @oLocal@ composes two @From@s.
171+data To (k :: a -> *) where
172+ -- | Delete or leave in place
173+ To_NonMove :: To k
174+ -- | Move the value from the given key @k a@ to this key. The target key
175+ -- should also have an entry in the patch giving the current key in
176+ -- @_nodeInfo_from@, usually but not necessarily with @To_Delete@.
177+ To_Move :: !(Some k) -> To k
178+
179+deriving instance GShow k => Show (To k)
180+deriving instance GRead k => Read (To k)
181+deriving instance GEq k => Eq (To k)
182+deriving instance GCompare k => Ord (To k)
183+
184+-- |Test whether a 'PatchDMapWithPatchingMove' satisfies its invariants.
185+validPatchDMapWithPatchingMove
186+ :: forall k v
187+ . (GCompare k, GShow k)
188+ => DMap k (NodeInfo k v)
189+ -> Bool
190+validPatchDMapWithPatchingMove = not . null . validationErrorsForPatchDMapWithPatchingMove
191+
192+-- |Enumerate what reasons a 'PatchDMapWithPatchingMove' doesn't satisfy its invariants, returning @[]@ if it's valid.
193+validationErrorsForPatchDMapWithPatchingMove
194+ :: forall k v
195+ . (GCompare k, GShow k)
196+ => DMap k (NodeInfo k v)
197+ -> [String]
198+validationErrorsForPatchDMapWithPatchingMove m =
199+ noSelfMoves <> movesBalanced
200+ where
201+ noSelfMoves = mapMaybe selfMove . DMap.toAscList $ m
202+ selfMove (dst :=> NodeInfo (From_Move (src :=> _)) _)
203+ | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
204+ selfMove (src :=> NodeInfo _ (To_Move (Some dst)))
205+ | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
206+ selfMove _ = Nothing
207+ movesBalanced = mapMaybe unbalancedMove . DMap.toAscList $ m
208+ unbalancedMove (dst :=> NodeInfo (From_Move (src :=> _)) _) =
209+ case DMap.lookup src m of
210+ Nothing -> Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key is not in the patch"
211+ Just (NodeInfo _ (To_Move (Some dst'))) ->
212+ if isNothing (dst' `geq` dst)
213+ then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
214+ else Nothing
215+ _ ->
216+ Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key has no move to key"
217+ unbalancedMove (src :=> NodeInfo _ (To_Move (Some dst))) =
218+ case DMap.lookup dst m of
219+ Nothing -> Just $ " unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
220+ Just (NodeInfo (From_Move (src' :=> _)) _) ->
221+ if isNothing (src' `geq` src)
222+ then Just $ "unbalanced move at source key " <> gshow src <> " to " <> gshow dst <> " is coming from " <> gshow src' <> " instead"
223+ else Nothing
224+
225+ _ ->
226+ Just $ "unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not moving"
227+ unbalancedMove _ = Nothing
228+
229+
230+data ToFrom k p a = ToFrom (To k) (From k p a)
231+
232+-- | Helper data structure used for composing patches using the monoid instance.
233+data Fixup k p a
234+ = Fixup_Delete
235+ | Fixup_Update (These (DSum k (From k p)) (To k))
236+
237+-- | Compose patches having the same effect as applying the patches in turn:
238+-- @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
239+instance forall k p
240+ . ( GCompare k
241+ , Cat.Semigroupoid p
242+ -- , Cat.DecidablyEmpty p
243+ , PatchHet2 p
244+ , PatchSource1 p ~ PatchTarget1 p
245+ )
246+ => Semigroup (PatchDMapWithPatchingMove k p) where
247+ PatchDMapWithPatchingMove ma <> PatchDMapWithPatchingMove mb = PatchDMapWithPatchingMove m
248+ where
249+ connections :: [DSum k (ToFrom k p)]
250+ connections = DMap.toList $ DMap.intersectionWithKey
251+ (\_ a b -> ToFrom (_nodeInfo_to a) (_nodeInfo_from b))
252+ ma
253+ mb
254+ h :: DSum k (ToFrom k p) -> [DSum k (Fixup k p)]
255+ h ((between :: k between) :=> ToFrom editAfter editBefore) = case (editAfter, editBefore) of
256+ (To_Move (Some (toAfter :: k after)), From_Move ((fromBefore :: k before) :=> Flip p) :: From k p between) ->
257+ --case toAfter `geq` fromBefore of
258+ -- Just Refl | Just Refl <- Cat.isId p0 ->
259+ -- [ toAfter :=> Fixup_Delete ]
260+ -- _ ->
261+ [ toAfter :=> Fixup_Update (This $ between :=> From_Move (fromBefore :=> Flip p))
262+ , fromBefore :=> Fixup_Update (That $ To_Move $ Some toAfter)
263+ ]
264+ (To_NonMove, From_Move (fromBefore :=> _)) ->
265+ -- The item is destroyed in the second patch, so indicate that it is
266+ -- destroyed in the source map
267+ [fromBefore :=> Fixup_Update (That To_NonMove)]
268+ --(To_Move (Some toAfter), From_Insert val) ->
269+ -- [toAfter :=> Fixup_Update (This $ From_Insert $ applyAlwaysHet2 p val)]
270+ --(To_Move (Some toAfter), From_Delete) ->
271+ -- [toAfter :=> Fixup_Update (This From_Delete)]
272+ (To_Move (Some toAfter), _) ->
273+ [toAfter :=> Fixup_Update (This $ between :=> editBefore)]
274+ (To_NonMove, _) ->
275+ []
276+ mergeFixups _ Fixup_Delete Fixup_Delete = Fixup_Delete
277+ mergeFixups _ (Fixup_Update a) (Fixup_Update b)
278+ | This x <- a, That y <- b
279+ = Fixup_Update $ These x y
280+ | That y <- a, This x <- b
281+ = Fixup_Update $ These x y
282+ mergeFixups _ _ _ = error "PatchDMapWithPatchingMove: incompatible fixups"
283+ fixups = DMap.fromListWithKey mergeFixups $ concatMap h connections
284+ combineNodeInfos _ nia nib = NodeInfo
285+ { _nodeInfo_from = _nodeInfo_from nia
286+ , _nodeInfo_to = _nodeInfo_to nib
287+ }
288+ applyFixup :: k a -> NodeInfo k p a -> Fixup k p a -> Maybe (NodeInfo k p a)
289+ applyFixup _ ni = \case
290+ Fixup_Delete -> Nothing
291+ Fixup_Update u -> Just $ NodeInfo
292+ { _nodeInfo_from = case _nodeInfo_from ni of
293+ f@(From_Move ((between0 :: k between0) :=> Flip (p' :: p between0 a))) -> case getHere u of -- The `from` fixup comes from the "old" patch
294+ Nothing -> f -- If there's no `from` fixup, just use the "new" `from`
295+ Just ((between1 :: k between1) :=> frm) -> case geq between0 between1 of
296+ Nothing -> error "fixup joined-on key did not match"
297+ Just Refl -> case frm of
298+ From_Insert v -> From_Insert $ applyAlwaysHet2 p' v
299+ From_Delete -> From_Delete
300+ From_Move (oldKey :=> Flip (p :: p oldKey between1)) -> From_Move $ oldKey :=> Flip (p' `o` p :: p oldKey a)
301+ _ -> error "PatchMapWithPatchingMove: fixup for non-move From"
302+ , _nodeInfo_to = fromMaybe (_nodeInfo_to ni) $ getThere u
303+ }
304+ m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
305+ getHere :: These a b -> Maybe a
306+ getHere = \case
307+ This a -> Just a
308+ These a _ -> Just a
309+ That _ -> Nothing
310+ getThere :: These a b -> Maybe b
311+ getThere = \case
312+ This _ -> Nothing
313+ These _ b -> Just b
314+ That b -> Just b
315+
316+-- | Compose patches having the same effect as applying the patches in turn:
317+-- @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
318+instance ( GCompare k
319+ , Cat.Semigroupoid p
320+ -- , DecidablyEmpty p
321+ , PatchHet2 p
322+ , PatchSource1 p ~ PatchTarget1 p
323+ ) => Monoid (PatchDMapWithPatchingMove k p) where
324+ mempty = PatchDMapWithPatchingMove mempty
325+ mappend = (<>)
326+
327+{-
328+mappendPatchDMapWithPatchingMoveSlow :: forall k v. (ShowTag k v, GCompare k) => PatchDMapWithPatchingMove k v -> PatchDMapWithPatchingMove k v -> PatchDMapWithPatchingMove k v
329+PatchDMapWithPatchingMove dstAfter srcAfter `mappendPatchDMapWithPatchingMoveSlow` PatchDMapWithPatchingMove dstBefore srcBefore = PatchDMapWithPatchingMove dst src
330+ where
331+ 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
332+ removeRedundantDst toKey (From_Move fromKey) | isJust (toKey `geq` fromKey) = Nothing
333+ removeRedundantDst _ a = Just a
334+ f :: forall a. k a -> From k v a -> Maybe (From k v a)
335+ f toKey _ = removeRedundantDst toKey $ case getDstAction toKey dstAfter of
336+ From_Move fromKey -> getDstAction fromKey dstBefore
337+ nonMove -> nonMove
338+ dst = DMap.mapMaybeWithKey f $ DMap.union dstAfter dstBefore
339+ getSrcAction k m = fromMaybe (ComposeMaybe $ Just k) $ DMap.lookup k m
340+ removeRedundantSrc fromKey (ComposeMaybe (Just toKey)) | isJust (fromKey `geq` toKey) = Nothing
341+ removeRedundantSrc _ a = Just a
342+ g :: forall a. k a -> ComposeMaybe k a -> Maybe (ComposeMaybe k a)
343+ g fromKey _ = removeRedundantSrc fromKey $ case getSrcAction fromKey srcBefore of
344+ ComposeMaybe Nothing -> ComposeMaybe Nothing
345+ ComposeMaybe (Just toKeyBefore) -> getSrcAction toKeyBefore srcAfter
346+ src = DMap.mapMaybeWithKey g $ DMap.union srcAfter srcBefore
347+-}
348+
349+-- | Make a @'PatchDMapWithPatchingMove' k v@ which has the effect of inserting or
350+-- updating a value @PatchTarget1 p a@ to the given key @k a@, like
351+-- 'DMap.insert'.
352+insertDMapKey :: k a -> PatchTarget1 p a -> PatchDMapWithPatchingMove k p
353+insertDMapKey k v =
354+ PatchDMapWithPatchingMove . DMap.singleton k $ NodeInfo (From_Insert v) To_NonMove
355+
356+-- | Make a @'PatchDMapWithPatchingMove' k v@ which has the effect of moving the value
357+-- from the first key @k a@ to the second key @k a@, equivalent to:
358+--
359+-- @
360+-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
361+-- @
362+moveDMapKey
363+ :: GCompare k
364+ => k a -> k a -> PatchDMapWithPatchingMove k (Proxy3 v)
365+moveDMapKey src dst = case src `geq` dst of
366+ Nothing -> PatchDMapWithPatchingMove $ DMap.fromList
367+ [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) To_NonMove
368+ , src :=> NodeInfo From_Delete (To_Move $ Some dst)
369+ ]
370+ Just _ -> PatchDMapWithPatchingMove DMap.empty
371+
372+-- | Make a @'PatchDMapWithPatchingMove' k v@ which has the effect of swapping two keys
373+-- in the mapping, equivalent to:
374+--
375+-- @
376+-- let aMay = DMap.lookup a dmap
377+-- bMay = DMap.lookup b dmap
378+-- in maybe id (DMap.insert a) (bMay <> aMay)
379+-- . maybe id (DMap.insert b) (aMay <> bMay)
380+-- . DMap.delete a . DMap.delete b $ dmap
381+-- @
382+swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithPatchingMove k (Proxy3 v)
383+swapDMapKey src dst = case src `geq` dst of
384+ Nothing -> PatchDMapWithPatchingMove $ DMap.fromList
385+ [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) (To_Move $ Some src)
386+ , src :=> NodeInfo (From_Move (dst :=> Flip Proxy3)) (To_Move $ Some dst)
387+ ]
388+ Just _ -> PatchDMapWithPatchingMove DMap.empty
389+
390+-- | Make a @'PatchDMapWithPatchingMove' k v@ which has the effect of deleting a key in
391+-- the mapping, equivalent to 'DMap.delete'.
392+deleteDMapKey :: k a -> PatchDMapWithPatchingMove k v
393+deleteDMapKey k = PatchDMapWithPatchingMove $ DMap.singleton k $ NodeInfo From_Delete To_NonMove
394+
395+{-
396+k1, k2 :: Const2 Int () ()
397+k1 = Const2 1
398+k2 = Const2 2
399+p1, p2 :: PatchDMapWithPatchingMove (Const2 Int ()) Identity
400+p1 = moveDMapKey k1 k2
401+p2 = moveDMapKey k2 k1
402+p12 = p1 <> p2
403+p21 = p2 <> p1
404+p12Slow = p1 `mappendPatchDMapWithPatchingMoveSlow` p2
405+p21Slow = p2 `mappendPatchDMapWithPatchingMoveSlow` p1
406+
407+testPatchDMapWithPatchingMove = do
408+ print p1
409+ print p2
410+ print $ p12 == deleteDMapKey k1
411+ print $ p21 == deleteDMapKey k2
412+ print $ p12Slow == deleteDMapKey k1
413+ print $ p21Slow == deleteDMapKey k2
414+
415+dst (PatchDMapWithPatchingMove x _) = x
416+src (PatchDMapWithPatchingMove _ x) = x
417+-}
418+
419+-- | Extract the 'DMap' representing the patch changes from the
420+-- 'PatchDMapWithPatchingMove'.
421+unPatchDMapWithPatchingMove :: PatchDMapWithPatchingMove k v -> DMap k (NodeInfo k v)
422+unPatchDMapWithPatchingMove (PatchDMapWithPatchingMove p) = p
423+
424+-- | Wrap a 'DMap' representing patch changes into a 'PatchDMapWithPatchingMove',
425+-- without checking any invariants.
426+--
427+-- __Warning:__ when using this function, you must ensure that the invariants of 'PatchDMapWithPatchingMove' are preserved; they will not be checked.
428+unsafePatchDMapWithPatchingMove :: DMap k (NodeInfo k v) -> PatchDMapWithPatchingMove k v
429+unsafePatchDMapWithPatchingMove = PatchDMapWithPatchingMove
430+
431+-- | Wrap a 'DMap' representing patch changes into a 'PatchDMapWithPatchingMove' while
432+-- checking invariants. If the invariants are satisfied, @Right p@ is returned
433+-- otherwise @Left errors@.
434+patchDMapWithPatchingMove :: (GCompare k, GShow k) => DMap k (NodeInfo k v) -> Either [String] (PatchDMapWithPatchingMove k v)
435+patchDMapWithPatchingMove dm =
436+ case validationErrorsForPatchDMapWithPatchingMove dm of
437+ [] -> Right $ unsafePatchDMapWithPatchingMove dm
438+ errs -> Left errs
439+
440+-- | Map a natural transform @v -> v'@ over the given patch, transforming
441+-- @'PatchDMapWithPatchingMove' k v@ into @'PatchDMapWithPatchingMove' k v'@.
442+mapPatchDMapWithPatchingMove
443+ :: forall k p p'
444+ . (forall a. PatchTarget1 p a -> PatchTarget1 p' a)
445+ -> (forall from to. p from to -> p' from to)
446+ -> PatchDMapWithPatchingMove k p
447+ -> PatchDMapWithPatchingMove k p'
448+mapPatchDMapWithPatchingMove f g (PatchDMapWithPatchingMove m) =
449+ PatchDMapWithPatchingMove $ DMap.map (\ni -> NodeInfo
450+ { _nodeInfo_from = h $ _nodeInfo_from ni
451+ , _nodeInfo_to = _nodeInfo_to ni
452+ }) m
453+ where h :: forall a. From k p a -> From k p' a
454+ h = \case
455+ From_Insert v -> From_Insert $ f v
456+ From_Delete -> From_Delete
457+ From_Move (k :=> Flip p) -> From_Move $ k :=> Flip (g p)
458+
459+-- | Traverse an effectful function @forall a. PatchTarget1 p a -> m (v ' a)@
460+-- over the given patch, transforming @'PatchDMapWithPatchingMove' k v@ into @m
461+-- ('PatchDMapWithPatchingMove' k v')@.
462+traversePatchDMapWithPatchingMove
463+ :: forall m k p p'
464+ . Applicative m
465+ => (forall a. PatchTarget1 p a -> m (PatchTarget1 p' a))
466+ -> (forall from to. p from to -> m (p' from to))
467+ -> PatchDMapWithPatchingMove k p
468+ -> m (PatchDMapWithPatchingMove k p')
469+traversePatchDMapWithPatchingMove f g = traversePatchDMapWithPatchingMoveWithKey
470+ (\_ -> f)
471+ (\_ _ -> g)
472+
473+-- | Map an effectful function @forall a. k a -> PatchTarget1 p a -> m (v ' a)@
474+-- over the given patch, transforming @'PatchDMapWithPatchingMove' k v@ into @m
475+-- ('PatchDMapWithPatchingMove' k v')@.
476+traversePatchDMapWithPatchingMoveWithKey
477+ :: forall m k p p'
478+ . Applicative m
479+ => (forall a. k a -> PatchTarget1 p a -> m (PatchTarget1 p' a))
480+ -> (forall from to. k from -> k to -> p from to -> m (p' from to))
481+ -> PatchDMapWithPatchingMove k p
482+ -> m (PatchDMapWithPatchingMove k p')
483+traversePatchDMapWithPatchingMoveWithKey f g (PatchDMapWithPatchingMove m) =
484+ PatchDMapWithPatchingMove <$> DMap.traverseWithKey (\k ni -> NodeInfo
485+ <$> h k (_nodeInfo_from ni)
486+ <*> pure (_nodeInfo_to ni)) m
487+ where h :: forall a. k a -> From k p a -> m (From k p' a)
488+ h k = \case
489+ From_Insert v -> From_Insert <$> f k v
490+ From_Delete -> pure From_Delete
491+ From_Move (fromKey :=> Flip p) -> From_Move . (fromKey :=>) . Flip <$> g fromKey k p
492+
493+-- | Map a function which transforms @'From k PatchTarget1 p a@ into a @'From k
494+-- PatchTarget1 p' a@ over a @'NodeInfo' k PatchTarget1 p a@.
495+nodeInfoMapFrom
496+ :: (From k p a -> From k p' a)
497+ -> (To k -> To k)
498+ -> NodeInfo k p a
499+ -> NodeInfo k p' a
500+nodeInfoMapFrom f g ni = NodeInfo
501+ { _nodeInfo_from = f $ _nodeInfo_from ni
502+ , _nodeInfo_to = g $ _nodeInfo_to ni
503+ }
504+
505+-- | Map an effectful function which transforms @'From k PatchTarget1 p a@ into
506+-- a @f ('From k PatchTarget1 p' a)@ over a @'NodeInfo' k PatchTarget1 p a@.
507+nodeInfoMapFromM
508+ :: Applicative f
509+ => (From k p a -> f (From k p' a))
510+ -> (To k -> f (To k))
511+ -> NodeInfo k p a
512+ -> f (NodeInfo k p' a)
513+nodeInfoMapFromM f g ni = NodeInfo
514+ <$> f (_nodeInfo_from ni)
515+ <*> g (_nodeInfo_to ni)
516+
517+-- | Weaken a 'PatchDMapWithPatchingMove' to a 'PatchMapWithPatchingMove' by weakening the keys
518+-- from @k a@ to @'Some' k@ and applying a given weakening function
519+-- @PatchTarget1 p a -> v'@ to values.
520+weakenPatchDMapWithPatchingMoveWith
521+ :: forall k p p'
522+ . (forall a. PatchTarget1 p a -> PatchTarget p')
523+ -> (forall from to. p from to -> p')
524+ -> PatchDMapWithPatchingMove k p
525+ -> PatchMapWithPatchingMove (Some k) p'
526+weakenPatchDMapWithPatchingMoveWith f g (PatchDMapWithPatchingMove m) =
527+ PatchMapWithPatchingMove $ weakenDMapWith h m
528+ where h :: forall a. NodeInfo k p a -> MapWithPatchingMove.NodeInfo (Some k) p'
529+ h ni = MapWithPatchingMove.NodeInfo
530+ { MapWithPatchingMove._nodeInfo_from = case _nodeInfo_from ni of
531+ From_Insert v -> MapWithPatchingMove.From_Insert $ f v
532+ From_Delete -> MapWithPatchingMove.From_Delete
533+ From_Move (k :=> Flip p) -> MapWithPatchingMove.From_Move (mkSome k) $ g p
534+ , MapWithPatchingMove._nodeInfo_to = case _nodeInfo_to ni of
535+ To_NonMove -> Nothing
536+ To_Move (Some k) -> Just (mkSome k)
537+ }
538+
539+-- | "Weaken" a @'PatchDMapWithPatchingMove' (Const2 k a) v@ to a @'PatchMapWithPatchingMove' k
540+-- v'@. Weaken is in scare quotes because the 'Const2' has already disabled any
541+-- dependency in the typing and all points are already @a@, hence the function
542+-- to map each value to @v'@ is not higher rank.
543+patchDMapWithPatchingMoveToPatchMapWithPatchingMoveWith
544+ :: forall k p p' a
545+ . (PatchTarget1 p a -> PatchTarget p')
546+ -> (p a a -> p')
547+ -> PatchDMapWithPatchingMove (Const2 k a) p
548+ -> PatchMapWithPatchingMove k p'
549+patchDMapWithPatchingMoveToPatchMapWithPatchingMoveWith f g (PatchDMapWithPatchingMove m) =
550+ PatchMapWithPatchingMove $ dmapToMapWith h m
551+ where h :: NodeInfo (Const2 k a) p a -> MapWithPatchingMove.NodeInfo k p'
552+ h ni = MapWithPatchingMove.NodeInfo
553+ { MapWithPatchingMove._nodeInfo_from = case _nodeInfo_from ni of
554+ From_Insert v -> MapWithPatchingMove.From_Insert $ f v
555+ From_Delete -> MapWithPatchingMove.From_Delete
556+ From_Move (Const2 k :=> Flip p) -> MapWithPatchingMove.From_Move k $ g p
557+ , MapWithPatchingMove._nodeInfo_to = case _nodeInfo_to ni of
558+ To_NonMove -> Nothing
559+ To_Move (Some (Const2 k)) -> Just k
560+ }
561+
562+-- | "Strengthen" a @'PatchMapWithPatchingMove' k v@ into a @'PatchDMapWithPatchingMove
563+-- ('Const2' k a)@; that is, turn a non-dependently-typed patch into a
564+-- dependently typed one but which always has a constant key type represented by
565+-- 'Const2'. Apply the given function to each @v@ to produce a @PatchTarget1 p'
566+-- a@. Completemented by 'patchDMapWithPatchingMoveToPatchMapWithPatchingMoveWith'
567+const2PatchDMapWithPatchingMoveWith
568+ :: forall k v v' a
569+ . (v -> v' a)
570+ -> PatchMapWithPatchingMove k (Proxy v)
571+ -> PatchDMapWithPatchingMove (Const2 k a) (Proxy3 v')
572+const2PatchDMapWithPatchingMoveWith f (PatchMapWithPatchingMove p) =
573+ PatchDMapWithPatchingMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
574+ where g :: (k, MapWithPatchingMove.NodeInfo k (Proxy v))
575+ -> DSum (Const2 k a) (NodeInfo (Const2 k a) (Proxy3 v'))
576+ g (k, ni) = Const2 k :=> NodeInfo
577+ { _nodeInfo_from = case MapWithPatchingMove._nodeInfo_from ni of
578+ MapWithPatchingMove.From_Insert v -> From_Insert $ f v
579+ MapWithPatchingMove.From_Delete -> From_Delete
580+ MapWithPatchingMove.From_Move fromKey Proxy -> From_Move $ Const2 fromKey :=> Flip Proxy3
581+ , _nodeInfo_to = case MapWithPatchingMove._nodeInfo_to ni of
582+ Nothing -> To_NonMove
583+ Just toKey -> To_Move $ Some (Const2 toKey)
584+ }
585+
586+-- | Apply the insertions, deletions, and moves to a given 'DMap'.
587+instance ( GCompare k
588+ , PatchHet2 p
589+ , PatchSource1 p ~ PatchTarget1 p
590+ ) => PatchHet (PatchDMapWithPatchingMove k p) where
591+ type PatchSource (PatchDMapWithPatchingMove k p) = DMap k (PatchSource1 p)
592+ type PatchTarget (PatchDMapWithPatchingMove k p) = DMap k (PatchTarget1 p)
593+
594+instance ( GCompare k
595+ , PatchHet2 p
596+ , PatchSource1 p ~ PatchTarget1 p
597+ ) => Patch (PatchDMapWithPatchingMove k p) where
598+ apply (PatchDMapWithPatchingMove m) old = Just $! insertions `DMap.union` (old `DMap.difference` deletions)
599+ -- TODO: return Nothing sometimes --Note: the strict application here is
600+ -- critical to ensuring that incremental merges don't hold onto all their
601+ -- prerequisite events forever; can we make this more robust?
602+ where insertions = DMap.mapMaybeWithKey insertFunc m
603+ insertFunc :: forall a. k a -> NodeInfo k p a -> Maybe (PatchTarget1 p a)
604+ insertFunc _ ni = case _nodeInfo_from ni of
605+ From_Insert v -> Just v
606+ From_Move (k :=> Flip p) -> applyAlwaysHet2 p <$> DMap.lookup k old
607+ From_Delete -> Nothing
608+ deletions = DMap.mapMaybeWithKey deleteFunc m
609+ deleteFunc :: forall a. k a -> NodeInfo k p a -> Maybe (Constant () a)
610+ deleteFunc _ ni = case _nodeInfo_from ni of
611+ From_Delete -> Just $ Constant ()
612+ _ -> Nothing
613+
614+-- | Get the values that will be replaced, deleted, or moved if the given patch
615+-- is applied to the given 'DMap'.
616+getDeletionsAndMoves
617+ :: ( GCompare k
618+ , PatchSource1 p ~ PatchTarget1 p
619+ )
620+ => PatchDMapWithPatchingMove k p
621+ -> DMap k (PatchSource1 p)
622+ -> DMap k (Product (PatchTarget1 p) (Const (To k)))
623+getDeletionsAndMoves (PatchDMapWithPatchingMove p) m = DMap.intersectionWithKey f m p
624+ where f _ v ni = Pair v $ Const $ _nodeInfo_to ni