@@ -225,11 +225,11 @@ deriving instance ( GCompare k
225-- @oLocal@ composes two @From@s.
225-- @oLocal@ composes two @From@s.
226data To (k :: a -> *) (p :: a -> a -> *) :: a -> * where
226data To (k :: a -> *) (p :: a -> a -> *) :: a -> * where
227 -- | Delete or leave in place
227 -- | Delete or leave in place
228− To_NonMove :: To k p a0
228+ To_NonMove :: To k p from
229 -- | Move the value from the given key @k a@ to this key. The target key
229 -- | Move the value from the given key @k a@ to this key. The target key
230 -- should also have an entry in the patch giving the current key in
230 -- should also have an entry in the patch giving the current key in
231 -- @_nodeInfo_from@, usually but not necessarily with @To_Delete@.
231 -- @_nodeInfo_from@, usually but not necessarily with @To_Delete@.
232− To_Move :: !(k a1) -> p a0 a1 -> To k p a0
232+ To_Move :: !(DSum k (p from)) -> To k p from
234deriving instance ( Show (k a)
234deriving instance ( Show (k a)
235 , Show (p a a)
235 , Show (p a a)
@@ -240,24 +240,15 @@ deriving instance ( Read (k a)
240 , Read (PatchTarget1 p a)
240 , Read (PatchTarget1 p a)
241 ) => Read (To k p a)
241 ) => Read (To k p a)
243−instance ( GEq k
243+deriving instance ( GEq k
244− , HasZip Eq k p
244+ , HasZip Eq k p
245− , Eq (PatchTarget1 p a)
245+ , Eq (PatchTarget1 p a)
246− ) => Eq (To k p a) where
246+ ) => Eq (To k p a)
247− To_NonMove == To_NonMove = True
248− To_Move k0 p0 == To_Move k1 p1 = case geq k0 k1 of
250− Just Refl -> has @(DupC Eq p) k0 $ p0 == p1
252−instance ( GCompare k
248+deriving instance ( GCompare k
253− , HasZip Ord k p
249+ , HasZip Ord k p
254− , Ord (PatchTarget1 p a)
250+ , Ord (PatchTarget1 p a)
255− ) => Ord (To k p a) where
251+ ) => Ord (To k p a)
256− To_NonMove `compare` To_NonMove = EQ
257− To_Move k0 p0 `compare` To_Move k1 p1 = case gcompare k0 k1 of
259− DMap.GEQ -> has @(DupC Ord p) k0 $ p0 `compare` p1
263-- :: ( PatchSource1 p ~ PatchTarget1 p
254-- :: ( PatchSource1 p ~ PatchTarget1 p
@@ -292,20 +283,20 @@ validationErrorsForPatchDMapWithMove m =
292 noSelfMoves = mapMaybe selfMove . DMap.toAscList $ m
283 noSelfMoves = mapMaybe selfMove . DMap.toAscList $ m
293 selfMove (dst :=> NodeInfo (From_Move (src :=> _)) _)
284 selfMove (dst :=> NodeInfo (From_Move (src :=> _)) _)
294 | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
285 | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
295− selfMove (src :=> NodeInfo _ (To_Move dst _))
286+ selfMove (src :=> NodeInfo _ (To_Move (dst :=> _)))
296 | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
287 | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
297 selfMove _ = Nothing
288 selfMove _ = Nothing
298 movesBalanced = mapMaybe unbalancedMove . DMap.toAscList $ m
289 movesBalanced = mapMaybe unbalancedMove . DMap.toAscList $ m
299 unbalancedMove (dst :=> NodeInfo (From_Move (src :=> _)) _) =
290 unbalancedMove (dst :=> NodeInfo (From_Move (src :=> _)) _) =
300 case DMap.lookup src m of
291 case DMap.lookup src m of
301 Nothing -> Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key is not in the patch"
292 Nothing -> Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key is not in the patch"
302− Just (NodeInfo _ (To_Move dst' _)) ->
293+ Just (NodeInfo _ (To_Move (dst' :=> _))) ->
303 if isNothing (dst' `geq` dst)
294 if isNothing (dst' `geq` dst)
304 then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
295 then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
305 else Nothing
296 else Nothing
307 Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key has no move to key"
298 Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key has no move to key"
308− unbalancedMove (src :=> NodeInfo _ (To_Move dst _)) =
299+ unbalancedMove (src :=> NodeInfo _ (To_Move (dst :=> _))) =
309 case DMap.lookup dst m of
300 case DMap.lookup dst m of
310 Nothing -> Just $ " unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
301 Nothing -> Just $ " unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
311 Just (NodeInfo (From_Move (src' :=> _)) _) ->
302 Just (NodeInfo (From_Move (src' :=> _)) _) ->
@@ -331,6 +322,7 @@ instance ( GCompare k
331 , Cat.Semigroupoid p
322 , Cat.Semigroupoid p
332 -- , DecidablyEmpty p
323 -- , DecidablyEmpty p
333 , PatchHet2 p
324 , PatchHet2 p
325+ , PatchSource1 p ~ PatchTarget1 p
334 ) => Semigroup (PatchDMapWithMove k p) where
326 ) => Semigroup (PatchDMapWithMove k p) where
335 PatchDMapWithMove ma <> PatchDMapWithMove mb = PatchDMapWithMove m
327 PatchDMapWithMove ma <> PatchDMapWithMove mb = PatchDMapWithMove m
@@ -339,21 +331,26 @@ instance ( GCompare k
339 (\_ a b -> Pair1 (_nodeInfo_to a) (_nodeInfo_from b))
331 (\_ a b -> Pair1 (_nodeInfo_to a) (_nodeInfo_from b))
342− h :: DSum k (Pair1 k (From k v)) -> [DSum k (Fixup k v)]
334+ h :: DSum k (Pair1 (To k p) (From k p)) -> [DSum k (Fixup k p)]
343− h (between :=> Pair1 editAfter editBefore) = case (editAfter, editBefore) of
335+ h ((between :: k between) :=> Pair1 editAfter editBefore) = case (editAfter, editBefore) of
344− (To_Move toAfter p1, From_Move (fromBefore :=> p0)) -> case toAfter `geq` fromBefore of
336+ (To_Move ((toAfter :: k after) :=> p1), From_Move ((fromBefore :: k before) :=> Flip p0)) ->
337+ case toAfter `geq` fromBefore of
345− Just Refl | isNull p0 ->
338+ Just Refl | isNull p0 ->
346− [ toAfter :=> Fixup_Delete ]
339+ [ toAfter :=> Fixup_Delete ]
348− [ toAfter :=> Fixup_Update (This editBefore)
341+ [ toAfter :=> Fixup_Update (This $ From_Move $ fromBefore :=> (Flip $ p1 `o` p0))
349− , fromBefore :=> Fixup_Update (That editAfter)
342+ , fromBefore :=> Fixup_Update (That $ To_Move $ toAfter :=> (p1 `o` p0))
351 (To_NonMove, From_Move (fromBefore :=> _)) ->
344 (To_NonMove, From_Move (fromBefore :=> _)) ->
352 -- The item is destroyed in the second patch, so indicate that it is
345 -- The item is destroyed in the second patch, so indicate that it is
353 -- destroyed in the source map
346 -- destroyed in the source map
354− [fromBefore :=> Fixup_Update (That (ComposeMaybe editAfter))]
347+ [fromBefore :=> Fixup_Update (That To_NonMove)]
348+ (To_Move (toAfter :=> p), From_Insert val) ->
349+ [toAfter :=> Fixup_Update (This $ From_Insert $ applyAlwaysHet2 p val)]
350+ (To_Move (toAfter :=> p), From_Delete) ->
355− (Just toAfter, _) -> [toAfter :=> Fixup_Update (This editBefore)]
351+ [toAfter :=> Fixup_Update (This From_Delete)]
356− (Nothing, _) -> []
352+ (To_NonMove, _) ->
357 mergeFixups _ Fixup_Delete Fixup_Delete = Fixup_Delete
354 mergeFixups _ Fixup_Delete Fixup_Delete = Fixup_Delete
358 mergeFixups _ (Fixup_Update a) (Fixup_Update b)
355 mergeFixups _ (Fixup_Update a) (Fixup_Update b)
359 | This x <- a, That y <- b
356 | This x <- a, That y <- b
@@ -369,13 +366,7 @@ instance ( GCompare k
369 applyFixup _ ni = \case
366 applyFixup _ ni = \case
370 Fixup_Delete -> Nothing
367 Fixup_Delete -> Nothing
371 Fixup_Update u -> Just $ NodeInfo
368 Fixup_Update u -> Just $ NodeInfo
372− { _nodeInfo_from = case _nodeInfo_from ni of
369+ { _nodeInfo_from = fromMaybe (_nodeInfo_from ni) $ getHere u
373− f@(From_Move (_ :=> p')) -> case _here u of -- The `from` fixup comes from the "old" patch
374− Nothing -> f -- If there's no `from` fixup, just use the "new" `from`
375− Just (From_Insert v) -> From_Insert $ applyAlways p' v
376− Just From_Delete -> From_Delete
377− Just (From_Move (oldKey :=> p)) -> From_Move $ oldKey :=> (p' <> p)
378− _ -> error "DPatchMapWithMove: fixup for non-move From"
379 , _nodeInfo_to = fromMaybe (_nodeInfo_to ni) $ getThere u
370 , _nodeInfo_to = fromMaybe (_nodeInfo_to ni) $ getThere u
381 m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
372 m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
@@ -390,8 +381,14 @@ instance ( GCompare k
390 These _ b -> Just b
381 These _ b -> Just b
391 That b -> Just b
382 That b -> Just b
393−-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
384+-- | Compose patches having the same effect as applying the patches in turn:
385+-- @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
386+instance ( GCompare k
387+ , Cat.Semigroupoid p
388+ -- , DecidablyEmpty p
390+ , PatchSource1 p ~ PatchTarget1 p
394−instance GCompare k => Monoid (PatchDMapWithMove k v) where
391+ ) => Monoid (PatchDMapWithMove k p) where
395 mempty = PatchDMapWithMove mempty
392 mempty = PatchDMapWithMove mempty
396 mappend = (<>)
393 mappend = (<>)
@@ -420,18 +417,18 @@ PatchDMapWithMove dstAfter srcAfter `mappendPatchDMapWithMoveSlow` PatchDMapWith
420-- |Make a @'PatchDMapWithMove' k v@ which has the effect of inserting or updating a value @PatchTarget1 p a@ to the given key @k a@, like 'DMap.insert'.
417-- |Make a @'PatchDMapWithMove' k v@ which has the effect of inserting or updating a value @PatchTarget1 p a@ to the given key @k a@, like 'DMap.insert'.
421insertDMapKey :: k a -> PatchTarget1 p a -> PatchDMapWithMove k p
418insertDMapKey :: k a -> PatchTarget1 p a -> PatchDMapWithMove k p
422insertDMapKey k v =
419insertDMapKey k v =
423− PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) (ComposeMaybe Nothing)
420+ PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) To_NonMove
425-- |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:
422-- |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:
428-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
425-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
430−moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
427+moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k (Proxy2 v)
431moveDMapKey src dst = case src `geq` dst of
428moveDMapKey src dst = case src `geq` dst of
432 Nothing -> PatchDMapWithMove $ DMap.fromList
429 Nothing -> PatchDMapWithMove $ DMap.fromList
433− [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) (ComposeMaybe Nothing)
430+ [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) To_NonMove
434− , src :=> NodeInfo From_Delete (ComposeMaybe $ Just dst)
431+ , src :=> NodeInfo From_Delete (To_Move $ dst :=> Proxy2)
436 Just _ -> mempty
433 Just _ -> mempty
@@ -448,7 +445,7 @@ swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
448swapDMapKey src dst = case src `geq` dst of
445swapDMapKey src dst = case src `geq` dst of
449 Nothing -> PatchDMapWithMove $ DMap.fromList
446 Nothing -> PatchDMapWithMove $ DMap.fromList
450 [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) (ComposeMaybe $ Just src)
447 [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) (ComposeMaybe $ Just src)
451− , src :=> NodeInfo (From_Move (dst :=> Cat.id)) (ComposeMaybe $ Just dst)
448+ , src :=> NodeInfo (From_Move (dst :=> Cat.id)) (To_Move $ dst :=> Proxy2)
453 Just _ -> mempty
450 Just _ -> mempty