@@ -225,11 +225,11 @@ deriving instance ( GCompare k
225225-- @oLocal@ composes two @From@s.
226226data To (k :: a -> *) (p :: a -> a -> *) :: a -> * where
227227 -- | Delete or leave in place
228− To_NonMove :: To k p a0
228+ To_NonMove :: To k p from
229229 -- | Move the value from the given key @k a@ to this key. The target key
230230 -- should also have an entry in the patch giving the current key in
231231 -- @_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
233233
234234deriving instance ( Show (k a)
235235 , Show (p a a)
@@ -240,24 +240,15 @@ deriving instance ( Read (k a)
240240 , Read (PatchTarget1 p a)
241241 ) => Read (To k p a)
242242
243−instance ( GEq k
244− , HasZip Eq k p
245− , Eq (PatchTarget1 p a)
246− ) => Eq (To k p a) where
247− To_NonMove == To_NonMove = True
248− To_Move k0 p0 == To_Move k1 p1 = case geq k0 k1 of
249− Nothing -> False
250− Just Refl -> has @(DupC Eq p) k0 $ p0 == p1
243+deriving instance ( GEq k
244+ , HasZip Eq k p
245+ , Eq (PatchTarget1 p a)
246+ ) => Eq (To k p a)
251247
252−instance ( GCompare k
253− , HasZip Ord k p
254− , Ord (PatchTarget1 p a)
255− ) => Ord (To k p a) where
256− To_NonMove `compare` To_NonMove = EQ
257− To_Move k0 p0 `compare` To_Move k1 p1 = case gcompare k0 k1 of
258− DMap.GGT -> GT
259− DMap.GEQ -> has @(DupC Ord p) k0 $ p0 `compare` p1
260− DMap.GLT -> LT
248+deriving instance ( GCompare k
249+ , HasZip Ord k p
250+ , Ord (PatchTarget1 p a)
251+ ) => Ord (To k p a)
261252
262253--oToFrom
263254-- :: ( PatchSource1 p ~ PatchTarget1 p
@@ -292,20 +283,20 @@ validationErrorsForPatchDMapWithMove m =
292283 noSelfMoves = mapMaybe selfMove . DMap.toAscList $ m
293284 selfMove (dst :=> NodeInfo (From_Move (src :=> _)) _)
294285 | 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 :=> _)))
296287 | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
297288 selfMove _ = Nothing
298289 movesBalanced = mapMaybe unbalancedMove . DMap.toAscList $ m
299290 unbalancedMove (dst :=> NodeInfo (From_Move (src :=> _)) _) =
300291 case DMap.lookup src m of
301292 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' :=> _))) ->
303294 if isNothing (dst' `geq` dst)
304295 then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
305296 else Nothing
306297 _ ->
307298 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 :=> _))) =
309300 case DMap.lookup dst m of
310301 Nothing -> Just $ " unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
311302 Just (NodeInfo (From_Move (src' :=> _)) _) ->
@@ -331,6 +322,7 @@ instance ( GCompare k
331322 , Cat.Semigroupoid p
332323 -- , DecidablyEmpty p
333324 , PatchHet2 p
325+ , PatchSource1 p ~ PatchTarget1 p
334326 ) => Semigroup (PatchDMapWithMove k p) where
335327 PatchDMapWithMove ma <> PatchDMapWithMove mb = PatchDMapWithMove m
336328 where
@@ -339,21 +331,26 @@ instance ( GCompare k
339331 (\_ a b -> Pair1 (_nodeInfo_to a) (_nodeInfo_from b))
340332 ma
341333 mb
342− h :: DSum k (Pair1 k (From k v)) -> [DSum k (Fixup k v)]
343− h (between :=> Pair1 editAfter editBefore) = case (editAfter, editBefore) of
344− (To_Move toAfter p1, From_Move (fromBefore :=> p0)) -> case toAfter `geq` fromBefore of
345− Just Refl | isNull p0 ->
346− [ toAfter :=> Fixup_Delete ]
347− _ ->
348− [ toAfter :=> Fixup_Update (This editBefore)
349− , fromBefore :=> Fixup_Update (That editAfter)
350− ]
334+ h :: DSum k (Pair1 (To k p) (From k p)) -> [DSum k (Fixup k p)]
335+ h ((between :: k between) :=> Pair1 editAfter editBefore) = case (editAfter, editBefore) of
336+ (To_Move ((toAfter :: k after) :=> p1), From_Move ((fromBefore :: k before) :=> Flip p0)) ->
337+ case toAfter `geq` fromBefore of
338+ Just Refl | isNull p0 ->
339+ [ toAfter :=> Fixup_Delete ]
340+ _ ->
341+ [ toAfter :=> Fixup_Update (This $ From_Move $ fromBefore :=> (Flip $ p1 `o` p0))
342+ , fromBefore :=> Fixup_Update (That $ To_Move $ toAfter :=> (p1 `o` p0))
343+ ]
351344 (To_NonMove, From_Move (fromBefore :=> _)) ->
352345 -- The item is destroyed in the second patch, so indicate that it is
353346 -- destroyed in the source map
354− [fromBefore :=> Fixup_Update (That (ComposeMaybe editAfter))]
355− (Just toAfter, _) -> [toAfter :=> Fixup_Update (This editBefore)]
356− (Nothing, _) -> []
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) ->
351+ [toAfter :=> Fixup_Update (This From_Delete)]
352+ (To_NonMove, _) ->
353+ []
357354 mergeFixups _ Fixup_Delete Fixup_Delete = Fixup_Delete
358355 mergeFixups _ (Fixup_Update a) (Fixup_Update b)
359356 | This x <- a, That y <- b
@@ -369,13 +366,7 @@ instance ( GCompare k
369366 applyFixup _ ni = \case
370367 Fixup_Delete -> Nothing
371368 Fixup_Update u -> Just $ NodeInfo
372− { _nodeInfo_from = case _nodeInfo_from ni of
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"
369+ { _nodeInfo_from = fromMaybe (_nodeInfo_from ni) $ getHere u
379370 , _nodeInfo_to = fromMaybe (_nodeInfo_to ni) $ getThere u
380371 }
381372 m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
@@ -390,8 +381,14 @@ instance ( GCompare k
390381 These _ b -> Just b
391382 That b -> Just b
392383
393−-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
394−instance GCompare k => Monoid (PatchDMapWithMove k v) where
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
389+ , PatchHet2 p
390+ , PatchSource1 p ~ PatchTarget1 p
391+ ) => Monoid (PatchDMapWithMove k p) where
395392 mempty = PatchDMapWithMove mempty
396393 mappend = (<>)
397394
@@ -420,18 +417,18 @@ PatchDMapWithMove dstAfter srcAfter `mappendPatchDMapWithMoveSlow` PatchDMapWith
420417-- |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'.
421418insertDMapKey :: k a -> PatchTarget1 p a -> PatchDMapWithMove k p
422419insertDMapKey k v =
423− PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) (ComposeMaybe Nothing)
420+ PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) To_NonMove
424421
425422-- |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:
426423--
427424-- @
428425-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
429426-- @
430−moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
427+moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k (Proxy2 v)
431428moveDMapKey src dst = case src `geq` dst of
432429 Nothing -> PatchDMapWithMove $ DMap.fromList
433− [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) (ComposeMaybe Nothing)
434− , src :=> NodeInfo From_Delete (ComposeMaybe $ Just dst)
430+ [ dst :=> NodeInfo (From_Move (src :=> Cat.id)) To_NonMove
431+ , src :=> NodeInfo From_Delete (To_Move $ dst :=> Proxy2)
435432 ]
436433 Just _ -> mempty
437434
@@ -448,7 +445,7 @@ swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
448445swapDMapKey src dst = case src `geq` dst of
449446 Nothing -> PatchDMapWithMove $ DMap.fromList
450447 [ 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)
452449 ]
453450 Just _ -> mempty
454451