@@ -10,6 +10,9 @@
10{-# LANGUAGE ScopedTypeVariables #-}
10{-# LANGUAGE ScopedTypeVariables #-}
11{-# LANGUAGE TypeFamilies #-}
11{-# LANGUAGE TypeFamilies #-}
12{-# LANGUAGE UndecidableInstances #-}
12{-# LANGUAGE UndecidableInstances #-}
14+-- |Module containing @'PatchDMapWithMove' k v@ and associated functions, which represents a 'Patch' to a @'DMap' k v@ which can insert, update, delete, and
15+-- move values between keys.
13module Reflex.Patch.DMapWithMove where
16module Reflex.Patch.DMapWithMove where
15import Reflex.Patch.Class
18import Reflex.Patch.Class
@@ -23,6 +26,7 @@ import Data.Functor.Constant
23import Data.Functor.Misc
26import Data.Functor.Misc
24import Data.Functor.Product
27import Data.Functor.Product
25import Data.GADT.Compare (GEq (..))
28import Data.GADT.Compare (GEq (..))
29+import Data.GADT.Show (GShow, gshow)
26import qualified Data.Map as Map
30import qualified Data.Map as Map
27import Data.Maybe
31import Data.Maybe
28import Data.Semigroup (Semigroup (..), (<>))
32import Data.Semigroup (Semigroup (..), (<>))
@@ -36,15 +40,25 @@ import Data.GADT.Show (GShow (..))
36import Data.Typeable (Proxy (..))
40import Data.Typeable (Proxy (..))
39−-- | Like 'PatchMapWithMove', but for 'DMap'.
43+-- | Like 'PatchMapWithMove', but for 'DMap'. Each key carries a 'NodeInfo' which describes how it will be changed by the patch and connects move sources and
48+-- * A key should not move to itself.
49+-- * A move should always be represented with both the destination key (as a 'From_Move') and the source key (as a @'ComposeMaybe' ('Just' destination)@)
40newtype PatchDMapWithMove k v = PatchDMapWithMove (DMap k (NodeInfo k v))
50newtype PatchDMapWithMove k v = PatchDMapWithMove (DMap k (NodeInfo k v))
41#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
51#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES
42 deriving (Show)
52 deriving (Show)
55+-- |Structure which represents what changes apply to a particular key. @_nodeInfo_from@ specifies what happens to this key, and in particular what other key
56+-- the current key is moving from, while @_nodeInfo_to@ specifies what key the current key is moving to if involved in a move.
45data NodeInfo k v a = NodeInfo
57data NodeInfo k v a = NodeInfo
46 { _nodeInfo_from :: !(From k v a)
58 { _nodeInfo_from :: !(From k v a)
59+ -- ^Change applying to the current key, be it an insert, move, or delete.
47 , _nodeInfo_to :: !(To k a)
60 , _nodeInfo_to :: !(To k a)
61+ -- ^Where this key is moving to, if involved in a move. Should only be @ComposeMaybe (Just k)@ when there is a corresponding 'From_Move'.
49 deriving (Show)
63 deriving (Show)
@@ -56,36 +70,73 @@ instance {-# INCOHERENT #-} (GEq k, EqTag k v) => EqTag k (From k v) where
56 eqTagToEq k _ r = eqTagToEq k (Proxy :: Proxy v) (geqToEq k r)
70 eqTagToEq k _ r = eqTagToEq k (Proxy :: Proxy v) (geqToEq k r)
73+-- |Structure describing a particular change to a key, be it inserting a new key (@From_Insert@), updating an existing key (@From_Insert@ again), deleting a
74+-- key (@From_Delete@), or moving a key (@From_Move@).
59data From (k :: a -> *) (v :: a -> *) :: a -> * where
75data From (k :: a -> *) (v :: a -> *) :: a -> * where
60 From_Insert :: v a -> From k v a
76 From_Insert :: v a -> From k v a
77+ -- ^Insert a new or update an existing key with the given value @v a@
61 From_Delete :: From k v a
78 From_Delete :: From k v a
79+ -- ^Delete the existing key
62 From_Move :: !(k a) -> From k v a
80 From_Move :: !(k a) -> From k v a
81+ -- ^Move the value from the given key @k a@ to this key. The source key should also have an entry in the patch giving the current key as @_nodeInfo_to@,
82+ -- usually but not necessarily with @From_Delete@.
63 deriving (Show, Read, Eq, Ord)
83 deriving (Show, Read, Eq, Ord)
85+-- |Type alias for the "to" part of a 'NodeInfo'. @'ComposeMaybe' ('Just' k)@ means the key is moving to another key, @ComposeMaybe Nothing@ for any other
65type To = ComposeMaybe
87type To = ComposeMaybe
89+-- |Test whether a 'PatchDMapWithMove' satisfies its invariants.
67−validPatchDMapWithMove :: forall k v. (GCompare k, EqTag k (ComposeMaybe k)) => PatchDMapWithMove k v -> Bool
90+validPatchDMapWithMove :: forall k v. (GCompare k, GEq k, GShow k) => DMap k (NodeInfo k v) -> Bool
68−validPatchDMapWithMove (PatchDMapWithMove m) = src == srcFromDst
91+validPatchDMapWithMove = not . null . validPatchDMapWithMove'
93+-- |Test whether a 'PatchDMapWithMove' satisfies its invariants and give reasons why it doesn't.
94+validPatchDMapWithMove' :: forall k v. (GCompare k, GEq k, GShow k) => DMap k (NodeInfo k v) -> [String]
95+validPatchDMapWithMove' m =
96+ noSelfMoves `mappend` movesBalanced
70− src = DMap.map _nodeInfo_to m
98+ noSelfMoves = catMaybes . map selfMove . DMap.toAscList $ m
71− dst = DMap.map _nodeInfo_from m
99+ selfMove (dst :=> NodeInfo (From_Move src) _) | Just _ <- dst `geq` src = Just $ "self move of key " <> gshow src <> " at destination side"
72− srcFromDst :: DMap k (ComposeMaybe k)
100+ selfMove (src :=> NodeInfo _ (ComposeMaybe (Just dst))) | Just _ <- src `geq` dst = Just $ "self move of key " <> gshow dst <> " at source side"
73− srcFromDst = DMap.fromList $ flip fmap (DMap.toList dst) $ \(to :=> edit) -> case edit of
101+ selfMove _ = Nothing
74− From_Move from -> from :=> ComposeMaybe (Just to)
102+ movesBalanced = catMaybes . map unbalancedMove . DMap.toAscList $ m
75− _ -> to :=> ComposeMaybe Nothing
103+ unbalancedMove (dst :=> NodeInfo (From_Move src) _) =
104+ case DMap.lookup src m of
105+ Nothing -> Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key is not in the patch"
106+ Just (NodeInfo _ (ComposeMaybe (Just dst'))) ->
107+ if isNothing (dst' `geq` dst)
108+ then Just $ "unbalanced move at destination key " <> gshow dst <> " from " <> gshow src <> " is going to " <> gshow dst' <> " instead"
111+ Just $ "unbalanced move at destination key " <> gshow dst <> " supposedly from " <> gshow src <> " but source key has no move to key"
112+ unbalancedMove (src :=> NodeInfo _ (ComposeMaybe (Just dst))) =
113+ case DMap.lookup dst m of
114+ Nothing -> Just $ " unbalancved move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not in the patch"
115+ Just (NodeInfo (From_Move src') _) ->
116+ if isNothing (src' `geq` src)
117+ then Just $ "unbalanced move at source key " <> gshow src <> " to " <> gshow dst <> " is coming from " <> gshow src' <> " instead"
121+ Just $ "unbalanced move at source key " <> gshow src <> " supposedly going to " <> gshow dst <> " but destination key is not moving"
122+ unbalancedMove _ = Nothing
77instance EqTag k (NodeInfo k v) => Eq (PatchDMapWithMove k v) where
124instance EqTag k (NodeInfo k v) => Eq (PatchDMapWithMove k v) where
78 PatchDMapWithMove a == PatchDMapWithMove b = a == b
125 PatchDMapWithMove a == PatchDMapWithMove b = a == b
127+-- |Higher kinded 2-tuple, identical to @Data.Functor.Product@ from base ≥ 4.9
80data Pair1 f g a = Pair1 (f a) (g a)
128data Pair1 f g a = Pair1 (f a) (g a)
130+-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
82instance GCompare k => Semigroup (PatchDMapWithMove k v) where
131instance GCompare k => Semigroup (PatchDMapWithMove k v) where
83 (<>) = mappend
132 (<>) = mappend
134+-- |Helper data structure used for composing patches using the monoid instance.
85data Fixup k v a
135data Fixup k v a
86 = Fixup_Delete
136 = Fixup_Delete
87 | Fixup_Update (These (From k v a) (To k a))
137 | Fixup_Update (These (From k v a) (To k a))
139+-- |Compose patches having the same effect as applying the patches in turn: @'applyAlways' (p <> q) == 'applyAlways' p . 'applyAlways' q@
89instance GCompare k => Monoid (PatchDMapWithMove k v) where
140instance GCompare k => Monoid (PatchDMapWithMove k v) where
90 mempty = PatchDMapWithMove mempty
141 mempty = PatchDMapWithMove mempty
91 PatchDMapWithMove ma `mappend` PatchDMapWithMove mb = PatchDMapWithMove m
142 PatchDMapWithMove ma `mappend` PatchDMapWithMove mb = PatchDMapWithMove m
@@ -123,12 +174,14 @@ instance GCompare k => Monoid (PatchDMapWithMove k v) where
124 m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
175 m = DMap.differenceWithKey applyFixup (DMap.unionWithKey combineNodeInfos ma mb) fixups
177+-- |Project the @a@ from a @'These' a b@, identical to @preview '_Here'@ but without using preview
126getHere :: These a b -> Maybe a
178getHere :: These a b -> Maybe a
127getHere = \case
179getHere = \case
128 This a -> Just a
180 This a -> Just a
129 These a _ -> Just a
181 These a _ -> Just a
130 That _ -> Nothing
182 That _ -> Nothing
184+-- |Project the @b@ from a @'These' a b@, identical to @preview '_There'@ but without using preview
132getThere :: These a b -> Maybe b
185getThere :: These a b -> Maybe b
133getThere = \case
186getThere = \case
134 This _ -> Nothing
187 This _ -> Nothing
@@ -157,6 +210,16 @@ PatchDMapWithMove dstAfter srcAfter `mappendPatchDMapWithMoveSlow` PatchDMapWith
157 src = DMap.mapMaybeWithKey g $ DMap.union srcAfter srcBefore
210 src = DMap.mapMaybeWithKey g $ DMap.union srcAfter srcBefore
213+-- |Make a @'PatchDMapWithMove' k v@ which has the effect of inserting or updating a value @v a@ to the given key @k a@, like 'DMap.insert'.
214+insertDMapKey :: k a -> v a -> PatchDMapWithMove k v
216+ PatchDMapWithMove . DMap.singleton k $ NodeInfo (From_Insert v) (ComposeMaybe Nothing)
218+-- |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:
221+-- 'DMap.delete' src (maybe dmap ('DMap.insert' dst) (DMap.lookup src dmap))
160moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
223moveDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
161moveDMapKey src dst = case src `geq` dst of
224moveDMapKey src dst = case src `geq` dst of
162 Nothing -> PatchDMapWithMove $ DMap.fromList
225 Nothing -> PatchDMapWithMove $ DMap.fromList
@@ -165,6 +228,24 @@ moveDMapKey src dst = case src `geq` dst of
166 Just _ -> mempty
229 Just _ -> mempty
231+-- |Make a @'PatchDMapWithMove' k v@ which has the effect of swapping two keys in the mapping, equivalent to:
234+-- let aMay = DMap.lookup a dmap
235+-- bMay = DMap.lookup b dmap
236+-- in maybe id (DMap.insert a) (bMay `mplus` aMay)
237+-- . maybe id (DMap.insert b) (aMay `mplus` bMay)
238+-- . DMap.delete a . DMap.delete b $ dmap
240+swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithMove k v
241+swapDMapKey src dst = case src `geq` dst of
242+ Nothing -> PatchDMapWithMove $ DMap.fromList
243+ [ dst :=> NodeInfo (From_Move src) (ComposeMaybe $ Just src)
244+ , src :=> NodeInfo (From_Move dst) (ComposeMaybe $ Just dst)
248+-- |Make a @'PatchDMapWithMove' k v@ which has the effect of deleting a key in the mapping, equivalent to 'DMap.delete'.
168deleteDMapKey :: k a -> PatchDMapWithMove k v
249deleteDMapKey :: k a -> PatchDMapWithMove k v
169deleteDMapKey k = PatchDMapWithMove $ DMap.singleton k $ NodeInfo From_Delete $ ComposeMaybe Nothing
250deleteDMapKey k = PatchDMapWithMove $ DMap.singleton k $ NodeInfo From_Delete $ ComposeMaybe Nothing
@@ -192,14 +273,25 @@ dst (PatchDMapWithMove x _) = x
192src (PatchDMapWithMove _ x) = x
273src (PatchDMapWithMove _ x) = x
276+-- |Extract the 'DMap' representing the patch changes from the 'PatchDMapWithMove'.
195unPatchDMapWithMove :: PatchDMapWithMove k v -> DMap k (NodeInfo k v)
277unPatchDMapWithMove :: PatchDMapWithMove k v -> DMap k (NodeInfo k v)
196unPatchDMapWithMove (PatchDMapWithMove p) = p
278unPatchDMapWithMove (PatchDMapWithMove p) = p
280+-- |Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove', without checking any invariants.
198−-- | Warning: when using this function, you must ensure that the invariants of
282+-- __Warning:__ when using this function, you must ensure that the invariants of 'PatchDMapWithMove' are preserved; they will not be checked.
199−-- 'PatchDMapWithMove' are preserved; they will not be checked.
200unsafePatchDMapWithMove :: DMap k (NodeInfo k v) -> PatchDMapWithMove k v
283unsafePatchDMapWithMove :: DMap k (NodeInfo k v) -> PatchDMapWithMove k v
201unsafePatchDMapWithMove = PatchDMapWithMove
284unsafePatchDMapWithMove = PatchDMapWithMove
286+-- |Wrap a 'DMap' representing patch changes into a 'PatchDMapWithMove' while checking invariants. If the invariants are satisfied, @Right p@ is returned
287+-- otherwise @Left errors@.
288+patchDMapWithMove :: (GCompare k, GEq k, GShow k) => DMap k (NodeInfo k v) -> Either [String] (PatchDMapWithMove k v)
289+patchDMapWithMove dm =
290+ case validPatchDMapWithMove' dm of
291+ [] -> Right $ unsafePatchDMapWithMove dm
294+-- |Map a natural transform @v -> v'@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @'PatchDMapWithMove' k v'@.
203mapPatchDMapWithMove :: forall k v v'. (forall a. v a -> v' a) -> PatchDMapWithMove k v -> PatchDMapWithMove k v'
295mapPatchDMapWithMove :: forall k v v'. (forall a. v a -> v' a) -> PatchDMapWithMove k v -> PatchDMapWithMove k v'
204mapPatchDMapWithMove f (PatchDMapWithMove p) = PatchDMapWithMove $
296mapPatchDMapWithMove f (PatchDMapWithMove p) = PatchDMapWithMove $
205 DMap.map (\ni -> ni { _nodeInfo_from = g $ _nodeInfo_from ni }) p
297 DMap.map (\ni -> ni { _nodeInfo_from = g $ _nodeInfo_from ni }) p
@@ -209,9 +301,11 @@ mapPatchDMapWithMove f (PatchDMapWithMove p) = PatchDMapWithMove $
209 From_Delete -> From_Delete
301 From_Delete -> From_Delete
210 From_Move k -> From_Move k
302 From_Move k -> From_Move k
304+-- |Traverse an effectful function @forall a. v a -> m (v ' a)@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @m ('PatchDMapWithMove' k v')@.
212traversePatchDMapWithMove :: forall m k v v'. Applicative m => (forall a. v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
305traversePatchDMapWithMove :: forall m k v v'. Applicative m => (forall a. v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
213traversePatchDMapWithMove f = traversePatchDMapWithMoveWithKey $ const f
306traversePatchDMapWithMove f = traversePatchDMapWithMoveWithKey $ const f
308+-- |Map an effectful function @forall a. k a -> v a -> m (v ' a)@ over the given patch, transforming @'PatchDMapWithMove' k v@ into @m ('PatchDMapWithMove' k v')@.
215traversePatchDMapWithMoveWithKey :: forall m k v v'. Applicative m => (forall a. k a -> v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
309traversePatchDMapWithMoveWithKey :: forall m k v v'. Applicative m => (forall a. k a -> v a -> m (v' a)) -> PatchDMapWithMove k v -> m (PatchDMapWithMove k v')
216traversePatchDMapWithMoveWithKey f (PatchDMapWithMove p) = PatchDMapWithMove <$> DMap.traverseWithKey (nodeInfoMapFromM . g) p
310traversePatchDMapWithMoveWithKey f (PatchDMapWithMove p) = PatchDMapWithMove <$> DMap.traverseWithKey (nodeInfoMapFromM . g) p
217 where g :: forall a. k a -> From k v a -> m (From k v' a)
311 where g :: forall a. k a -> From k v a -> m (From k v' a)
@@ -220,12 +314,16 @@ traversePatchDMapWithMoveWithKey f (PatchDMapWithMove p) = PatchDMapWithMove <$>
220 From_Delete -> pure From_Delete
314 From_Delete -> pure From_Delete
221 From_Move fromKey -> pure $ From_Move fromKey
315 From_Move fromKey -> pure $ From_Move fromKey
317+-- |Map a function which transforms @'From' k v a@ into a @'From' k v' a@ over a @'NodeInfo' k v a@.
223nodeInfoMapFrom :: (From k v a -> From k v' a) -> NodeInfo k v a -> NodeInfo k v' a
318nodeInfoMapFrom :: (From k v a -> From k v' a) -> NodeInfo k v a -> NodeInfo k v' a
224nodeInfoMapFrom f ni = ni { _nodeInfo_from = f $ _nodeInfo_from ni }
319nodeInfoMapFrom f ni = ni { _nodeInfo_from = f $ _nodeInfo_from ni }
321+-- |Map an effectful function which transforms @'From' k v a@ into a @f ('From' k v' a)@ over a @'NodeInfo' k v a@.
226nodeInfoMapFromM :: Functor f => (From k v a -> f (From k v' a)) -> NodeInfo k v a -> f (NodeInfo k v' a)
322nodeInfoMapFromM :: Functor f => (From k v a -> f (From k v' a)) -> NodeInfo k v a -> f (NodeInfo k v' a)
227nodeInfoMapFromM f ni = fmap (\result -> ni { _nodeInfo_from = result }) $ f $ _nodeInfo_from ni
323nodeInfoMapFromM f ni = fmap (\result -> ni { _nodeInfo_from = result }) $ f $ _nodeInfo_from ni
325+-- |Weaken a 'PatchDMapWithMove' to a 'PatchMapWithMove' by weakening the keys from @k a@ to @'Some' k@ and applying a given weakening function @v a -> v'@ to
229weakenPatchDMapWithMoveWith :: forall k v v'. (forall a. v a -> v') -> PatchDMapWithMove k v -> PatchMapWithMove (Some k) v'
327weakenPatchDMapWithMoveWith :: forall k v v'. (forall a. v a -> v') -> PatchDMapWithMove k v -> PatchMapWithMove (Some k) v'
230weakenPatchDMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ weakenDMapWith g p
328weakenPatchDMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ weakenDMapWith g p
231 where g :: forall a. NodeInfo k v a -> MapWithMove.NodeInfo (Some k) v'
329 where g :: forall a. NodeInfo k v a -> MapWithMove.NodeInfo (Some k) v'
@@ -237,9 +335,11 @@ weakenPatchDMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ weakenD
237 , MapWithMove._nodeInfo_to = Some.This <$> getComposeMaybe (_nodeInfo_to ni)
335 , MapWithMove._nodeInfo_to = Some.This <$> getComposeMaybe (_nodeInfo_to ni)
338+-- |"Weaken" a @'PatchDMapWithMove' (Const2 k a) v@ to a @'PatchMapWithMove' k v'@. Weaken is in scare quotes because the 'Const2' has already disabled any
339+-- dependency in the typing and all points are already @a@, hence the function to map each value to @v'@ is not higher rank.
240−patchDMapWithMoveToPatchMapWithMoveWith :: forall k f v v'. (f v -> v') -> PatchDMapWithMove (Const2 k v) f -> PatchMapWithMove k v'
340+patchDMapWithMoveToPatchMapWithMoveWith :: forall k v v' a. (v a -> v') -> PatchDMapWithMove (Const2 k a) v -> PatchMapWithMove k v'
241patchDMapWithMoveToPatchMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ dmapToMapWith g p
341patchDMapWithMoveToPatchMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMove $ dmapToMapWith g p
242− where g :: NodeInfo (Const2 k v) f v -> MapWithMove.NodeInfo k v'
342+ where g :: NodeInfo (Const2 k a) v a -> MapWithMove.NodeInfo k v'
243 g ni = MapWithMove.NodeInfo
343 g ni = MapWithMove.NodeInfo
244 { MapWithMove._nodeInfo_from = case _nodeInfo_from ni of
344 { MapWithMove._nodeInfo_from = case _nodeInfo_from ni of
245 From_Insert v -> MapWithMove.From_Insert $ f v
345 From_Insert v -> MapWithMove.From_Insert $ f v
@@ -248,9 +348,12 @@ patchDMapWithMoveToPatchMapWithMoveWith f (PatchDMapWithMove p) = PatchMapWithMo
248 , MapWithMove._nodeInfo_to = unConst2 <$> getComposeMaybe (_nodeInfo_to ni)
348 , MapWithMove._nodeInfo_to = unConst2 <$> getComposeMaybe (_nodeInfo_to ni)
351+-- |"Strengthen" a @'PatchMapWithMove' k v@ into a @'PatchDMapWithMove ('Const2' k a)@; that is, turn a non-dependently-typed patch into a dependently typed
352+-- one but which always has a constant key type represented by 'Const2'. Apply the given function to each @v@ to produce a @v' a@.
353+-- Completemented by 'patchDMapWithMoveToPatchMapWithMoveWith'
251−const2PatchDMapWithMoveWith :: forall k v f a. (v -> f a) -> PatchMapWithMove k v -> PatchDMapWithMove (Const2 k a) f
354+const2PatchDMapWithMoveWith :: forall k v v' a. (v -> v' a) -> PatchMapWithMove k v -> PatchDMapWithMove (Const2 k a) v'
252const2PatchDMapWithMoveWith f (PatchMapWithMove p) = PatchDMapWithMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
355const2PatchDMapWithMoveWith f (PatchMapWithMove p) = PatchDMapWithMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
253− where g :: (k, MapWithMove.NodeInfo k v) -> DSum (Const2 k a) (NodeInfo (Const2 k a) f)
356+ where g :: (k, MapWithMove.NodeInfo k v) -> DSum (Const2 k a) (NodeInfo (Const2 k a) v')
254 g (k, ni) = Const2 k :=> NodeInfo
357 g (k, ni) = Const2 k :=> NodeInfo
255 { _nodeInfo_from = case MapWithMove._nodeInfo_from ni of
358 { _nodeInfo_from = case MapWithMove._nodeInfo_from ni of
256 MapWithMove.From_Insert v -> From_Insert $ f v
359 MapWithMove.From_Insert v -> From_Insert $ f v