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