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