    {-|
    Module      : What4.Expr.ArrayUpdateMap
    Description : Datastructure for representing a sequence of updates to an SMT array
    Copyright   : (c) Galois Inc, 2019-2020
    License     : BSD3
    Maintainer  : rdockins@galois.com
    -}

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}

    module What4.Expr.ArrayUpdateMap
    ( ArrayUpdateMap
    , arrayUpdateAbs
    , empty
    , null
    , lookup
    , filter
    , singleton
    , insert
    , delete
    , fromAscList
    , toList
    , toMap
    , keysSet
    , traverseArrayUpdateMap
    , mergeM
    ) where

    import           Prelude hiding (lookup, null, filter)

    import           Data.Functor.Identity
    import           Data.Hashable
    import           Data.Maybe
    import           Data.Parameterized.Classes
    import qualified Data.Parameterized.Context as Ctx
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import           What4.BaseTypes
    import           What4.IndexLit
    import           What4.Utils.AbstractDomains
    import qualified What4.Utils.AnnotatedMap as AM
    import           What4.Utils.IncrHash

    ------------------------------------------------------------------------
    -- ArrayUpdateMap

    data ArrayUpdateNote tp =
      ArrayUpdateNote
      { forall (tp :: BaseType). ArrayUpdateNote tp -> IncrHash
    aunHash :: !IncrHash
      , forall (tp :: BaseType). ArrayUpdateNote tp -> BaseTypeRepr tp
    _aunRepr :: !(BaseTypeRepr tp)
      , forall (tp :: BaseType). ArrayUpdateNote tp -> AbstractValue tp
    aunAbs  :: !(AbstractValue tp)
      }

    instance Semigroup (ArrayUpdateNote tp) where
      ArrayUpdateNote IncrHash
    hx BaseTypeRepr tp
    tpr AbstractValue tp
    ax <> :: ArrayUpdateNote tp -> ArrayUpdateNote tp -> ArrayUpdateNote tp
    <> ArrayUpdateNote IncrHash
    hy BaseTypeRepr tp
    _ AbstractValue tp
    ay =
        IncrHash
    -> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
    forall (tp :: BaseType).
    IncrHash
    -> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
    ArrayUpdateNote (IncrHash
    hx IncrHash -> IncrHash -> IncrHash
    forall a. Semigroup a => a -> a -> a
    <> IncrHash
    hy) BaseTypeRepr tp
    tpr (BaseTypeRepr tp
    -> (Abstractable tp => AbstractValue tp) -> AbstractValue tp
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr tp
    tpr ((Abstractable tp => AbstractValue tp) -> AbstractValue tp)
    -> (Abstractable tp => AbstractValue tp) -> AbstractValue tp
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
    avJoin BaseTypeRepr tp
    tpr AbstractValue tp
    ax AbstractValue tp
    ay)

    newtype ArrayUpdateMap e ctx tp =
      ArrayUpdateMap ( AM.AnnotatedMap (Ctx.Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp) )

    instance TestEquality e => Eq (ArrayUpdateMap e ctx tp) where
      ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m1 == :: ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp -> Bool
    == ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m2 = (e tp -> e tp -> Bool)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> Bool
    forall k a v.
    Eq k =>
    (a -> a -> Bool)
    -> AnnotatedMap k v a -> AnnotatedMap k v a -> Bool
    AM.eqBy (\ e tp
    x e tp
    y -> Maybe (tp :~: tp) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (tp :~: tp) -> Bool) -> Maybe (tp :~: tp) -> Bool
    forall a b. (a -> b) -> a -> b
    $ e tp -> e tp -> Maybe (tp :~: tp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    e a -> e b -> Maybe (a :~: b)
    testEquality e tp
    x e tp
    y) AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m1 AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m2

    instance TestEquality e => Hashable (ArrayUpdateMap e ctx tp) where
      hashWithSalt :: Int -> ArrayUpdateMap e ctx tp -> Int
    hashWithSalt Int
    s (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) =
        case AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> Maybe (ArrayUpdateNote tp)
    forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a -> Maybe v
    AM.annotation AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m of
          Maybe (ArrayUpdateNote tp)
    Nothing  -> Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s (Int
    111::Int)
          Just ArrayUpdateNote tp
    aun -> Int -> IncrHash -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s (ArrayUpdateNote tp -> IncrHash
    forall (tp :: BaseType). ArrayUpdateNote tp -> IncrHash
    aunHash ArrayUpdateNote tp
    aun)

    mkNote :: (HashableF e, HasAbsValue e) => BaseTypeRepr tp -> Ctx.Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote :: forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    idx e tp
    e = IncrHash
    -> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
    forall (tp :: BaseType).
    IncrHash
    -> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
    ArrayUpdateNote (Int -> IncrHash
    mkIncrHash (Int -> e tp -> Int
    forall k (f :: k -> Type) (tp :: k).
    HashableF f =>
    Int -> f tp -> Int
    forall (tp :: BaseType). Int -> e tp -> Int
    hashWithSaltF (Assignment IndexLit ctx -> Int
    forall a. Hashable a => a -> Int
    hash Assignment IndexLit ctx
    idx) e tp
    e)) BaseTypeRepr tp
    tpr (e tp -> AbstractValue tp
    forall (tp :: BaseType). e tp -> AbstractValue tp
    forall (f :: BaseType -> Type) (tp :: BaseType).
    HasAbsValue f =>
    f tp -> AbstractValue tp
    getAbsValue e tp
    e)

    arrayUpdateAbs :: ArrayUpdateMap e ct tp -> Maybe (AbstractValue tp)
    arrayUpdateAbs :: forall (e :: BaseType -> Type) (ct :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ct tp -> Maybe (AbstractValue tp)
    arrayUpdateAbs (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ct) (ArrayUpdateNote tp) (e tp)
    m) = ArrayUpdateNote tp -> AbstractValue tp
    forall (tp :: BaseType). ArrayUpdateNote tp -> AbstractValue tp
    aunAbs (ArrayUpdateNote tp -> AbstractValue tp)
    -> Maybe (ArrayUpdateNote tp) -> Maybe (AbstractValue tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> AnnotatedMap (Assignment IndexLit ct) (ArrayUpdateNote tp) (e tp)
    -> Maybe (ArrayUpdateNote tp)
    forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a -> Maybe v
    AM.annotation AnnotatedMap (Assignment IndexLit ct) (ArrayUpdateNote tp) (e tp)
    m

    fromAscList :: (HasAbsValue e, HashableF e) =>
      BaseTypeRepr tp -> [(Ctx.Assignment IndexLit ctx, e tp)] -> ArrayUpdateMap e ctx tp
    fromAscList :: forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HasAbsValue e, HashableF e) =>
    BaseTypeRepr tp
    -> [(Assignment IndexLit ctx, e tp)] -> ArrayUpdateMap e ctx tp
    fromAscList BaseTypeRepr tp
    tpr [(Assignment IndexLit ctx, e tp)]
    xs = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap ([(Assignment IndexLit ctx, ArrayUpdateNote tp, e tp)]
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall k v a.
    (Ord k, Semigroup v) =>
    [(k, v, a)] -> AnnotatedMap k v a
    AM.fromAscList (((Assignment IndexLit ctx, e tp)
     -> (Assignment IndexLit ctx, ArrayUpdateNote tp, e tp))
    -> [(Assignment IndexLit ctx, e tp)]
    -> [(Assignment IndexLit ctx, ArrayUpdateNote tp, e tp)]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Assignment IndexLit ctx, e tp)
    -> (Assignment IndexLit ctx, ArrayUpdateNote tp, e tp)
    f [(Assignment IndexLit ctx, e tp)]
    xs))
     where
     f :: (Assignment IndexLit ctx, e tp)
    -> (Assignment IndexLit ctx, ArrayUpdateNote tp, e tp)
    f (Assignment IndexLit ctx
    k,e tp
    e) = (Assignment IndexLit ctx
    k, BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    k e tp
    e, e tp
    e)

    toList :: ArrayUpdateMap e ctx tp -> [(Ctx.Assignment IndexLit ctx, e tp)]
    toList :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)]
    toList (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> [(Assignment IndexLit ctx, e tp)]
    forall k v a. AnnotatedMap k v a -> [(k, a)]
    AM.toList AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m

    traverseArrayUpdateMap :: Applicative m =>
      (e tp -> m (f tp)) ->
      ArrayUpdateMap e ctx tp ->
      m (ArrayUpdateMap f ctx tp)
    traverseArrayUpdateMap :: forall (m :: Type -> Type) (e :: BaseType -> Type) (tp :: BaseType)
           (f :: BaseType -> Type) (ctx :: Ctx BaseType).
    Applicative m =>
    (e tp -> m (f tp))
    -> ArrayUpdateMap e ctx tp -> m (ArrayUpdateMap f ctx tp)
    traverseArrayUpdateMap e tp -> m (f tp)
    f (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp)
    -> ArrayUpdateMap f ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp)
     -> ArrayUpdateMap f ctx tp)
    -> m (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp))
    -> m (ArrayUpdateMap f ctx tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (e tp -> m (f tp))
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> m (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp))
    forall (t :: Type -> Type) (f :: Type -> Type) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b)
    -> AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) a
    -> f (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) b)
    traverse e tp -> m (f tp)
    f AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m

    null :: ArrayUpdateMap e ctx tp -> Bool
    null :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp -> Bool
    null (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> Bool
    forall k v a. AnnotatedMap k v a -> Bool
    AM.null AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m

    lookup :: Ctx.Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> Maybe (e tp)
    lookup :: forall (ctx :: Ctx BaseType) (e :: BaseType -> Type)
           (tp :: BaseType).
    Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> Maybe (e tp)
    lookup Assignment IndexLit ctx
    idx (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = (ArrayUpdateNote tp, e tp) -> e tp
    forall a b. (a, b) -> b
    snd ((ArrayUpdateNote tp, e tp) -> e tp)
    -> Maybe (ArrayUpdateNote tp, e tp) -> Maybe (e tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Assignment IndexLit ctx
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> Maybe (ArrayUpdateNote tp, e tp)
    forall k v a.
    (Ord k, Semigroup v) =>
    k -> AnnotatedMap k v a -> Maybe (v, a)
    AM.lookup Assignment IndexLit ctx
    idx AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m

    delete :: Ctx.Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp
    delete :: forall (ctx :: Ctx BaseType) (e :: BaseType -> Type)
           (tp :: BaseType).
    Assignment IndexLit ctx
    -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp
    delete Assignment IndexLit ctx
    idx (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (Assignment IndexLit ctx
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall k v a.
    (Ord k, Semigroup v) =>
    k -> AnnotatedMap k v a -> AnnotatedMap k v a
    AM.delete Assignment IndexLit ctx
    idx AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m)

    filter :: (e tp -> Bool) -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp
    filter :: forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (e tp -> Bool)
    -> ArrayUpdateMap e ctx tp -> ArrayUpdateMap e ctx tp
    filter e tp -> Bool
    p (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
     -> ArrayUpdateMap e ctx tp)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall a b. (a -> b) -> a -> b
    $ Identity
      (AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp))
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall a. Identity a -> a
    runIdentity (Identity
       (AnnotatedMap
          (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp))
     -> AnnotatedMap
          (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp))
    -> Identity
         (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp))
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall a b. (a -> b) -> a -> b
    $ (Assignment IndexLit ctx
     -> ArrayUpdateNote tp
     -> e tp
     -> Identity (Maybe (ArrayUpdateNote tp, e tp)))
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> Identity
         (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp))
    forall (f :: Type -> Type) k v2 v1 a1 a2.
    (Applicative f, Ord k, Semigroup v2) =>
    (k -> v1 -> a1 -> f (Maybe (v2, a2)))
    -> AnnotatedMap k v1 a1 -> f (AnnotatedMap k v2 a2)
    AM.traverseMaybeWithKey Assignment IndexLit ctx
    -> ArrayUpdateNote tp
    -> e tp
    -> Identity (Maybe (ArrayUpdateNote tp, e tp))
    f AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m
     where
     f :: Assignment IndexLit ctx
    -> ArrayUpdateNote tp
    -> e tp
    -> Identity (Maybe (ArrayUpdateNote tp, e tp))
    f Assignment IndexLit ctx
    _k ArrayUpdateNote tp
    v e tp
    x
       | e tp -> Bool
    p e tp
    x       = Maybe (ArrayUpdateNote tp, e tp)
    -> Identity (Maybe (ArrayUpdateNote tp, e tp))
    forall a. a -> Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((ArrayUpdateNote tp, e tp) -> Maybe (ArrayUpdateNote tp, e tp)
    forall a. a -> Maybe a
    Just (ArrayUpdateNote tp
    v,e tp
    x))
       | Bool
    otherwise = Maybe (ArrayUpdateNote tp, e tp)
    -> Identity (Maybe (ArrayUpdateNote tp, e tp))
    forall a. a -> Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe (ArrayUpdateNote tp, e tp)
    forall a. Maybe a
    Nothing

    singleton ::
      (HashableF e, HasAbsValue e) =>
      BaseTypeRepr tp ->
      Ctx.Assignment IndexLit ctx ->
      e tp ->
      ArrayUpdateMap e ctx tp
    singleton :: forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateMap e ctx tp
    singleton BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    idx e tp
    e = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (Assignment IndexLit ctx
    -> ArrayUpdateNote tp
    -> e tp
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall k v a.
    (Ord k, Semigroup v) =>
    k -> v -> a -> AnnotatedMap k v a
    AM.singleton Assignment IndexLit ctx
    idx (BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    idx e tp
    e) e tp
    e)

    insert ::
      (HashableF e, HasAbsValue e) =>
      BaseTypeRepr tp ->
      Ctx.Assignment IndexLit ctx ->
      e tp ->
      ArrayUpdateMap e ctx tp ->
      ArrayUpdateMap e ctx tp
    insert :: forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx
    -> e tp
    -> ArrayUpdateMap e ctx tp
    -> ArrayUpdateMap e ctx tp
    insert BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    idx e tp
    e (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) =  AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (Assignment IndexLit ctx
    -> ArrayUpdateNote tp
    -> e tp
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall k v a.
    (Ord k, Semigroup v) =>
    k -> v -> a -> AnnotatedMap k v a -> AnnotatedMap k v a
    AM.insert Assignment IndexLit ctx
    idx (BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    idx e tp
    e) e tp
    e AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m)

    empty :: ArrayUpdateMap e ctx tp
    empty :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp
    empty = AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a
    AM.empty

    mergeM :: (Applicative m, HashableF g, HasAbsValue g) =>
      BaseTypeRepr tp ->
      (Ctx.Assignment IndexLit ctx -> e tp -> f tp -> m (g tp)) ->
      (Ctx.Assignment IndexLit ctx -> e tp -> m (g tp)) ->
      (Ctx.Assignment IndexLit ctx -> f tp -> m (g tp)) ->
      ArrayUpdateMap e ctx tp ->
      ArrayUpdateMap f ctx tp ->
      m (ArrayUpdateMap g ctx tp)
    mergeM :: forall (m :: Type -> Type) (g :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType) (e :: BaseType -> Type)
           (f :: BaseType -> Type).
    (Applicative m, HashableF g, HasAbsValue g) =>
    BaseTypeRepr tp
    -> (Assignment IndexLit ctx -> e tp -> f tp -> m (g tp))
    -> (Assignment IndexLit ctx -> e tp -> m (g tp))
    -> (Assignment IndexLit ctx -> f tp -> m (g tp))
    -> ArrayUpdateMap e ctx tp
    -> ArrayUpdateMap f ctx tp
    -> m (ArrayUpdateMap g ctx tp)
    mergeM BaseTypeRepr tp
    tpr Assignment IndexLit ctx -> e tp -> f tp -> m (g tp)
    both Assignment IndexLit ctx -> e tp -> m (g tp)
    left Assignment IndexLit ctx -> f tp -> m (g tp)
    right (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    ml) (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp)
    mr) =
      AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (g tp)
    -> ArrayUpdateMap g ctx tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> ArrayUpdateMap e ctx tp
    ArrayUpdateMap (AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (g tp)
     -> ArrayUpdateMap g ctx tp)
    -> m (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (g tp))
    -> m (ArrayUpdateMap g ctx tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Assignment IndexLit ctx
     -> (ArrayUpdateNote tp, e tp)
     -> (ArrayUpdateNote tp, f tp)
     -> m (ArrayUpdateNote tp, g tp))
    -> (Assignment IndexLit ctx
        -> (ArrayUpdateNote tp, e tp) -> m (ArrayUpdateNote tp, g tp))
    -> (Assignment IndexLit ctx
        -> (ArrayUpdateNote tp, f tp) -> m (ArrayUpdateNote tp, g tp))
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> AnnotatedMap
         (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp)
    -> m (AnnotatedMap
            (Assignment IndexLit ctx) (ArrayUpdateNote tp) (g tp))
    forall k u v w (m :: Type -> Type) a b c.
    (Ord k, Semigroup u, Semigroup v, Semigroup w, Applicative m) =>
    (k -> (u, a) -> (v, b) -> m (w, c))
    -> (k -> (u, a) -> m (w, c))
    -> (k -> (v, b) -> m (w, c))
    -> AnnotatedMap k u a
    -> AnnotatedMap k v b
    -> m (AnnotatedMap k w c)
    AM.mergeWithKeyM Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, e tp)
    -> (ArrayUpdateNote tp, f tp)
    -> m (ArrayUpdateNote tp, g tp)
    both' Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, e tp) -> m (ArrayUpdateNote tp, g tp)
    left' Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, f tp) -> m (ArrayUpdateNote tp, g tp)
    right' AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    ml AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (f tp)
    mr
     where
     mk :: Assignment IndexLit ctx -> g tp -> (ArrayUpdateNote tp, g tp)
    mk Assignment IndexLit ctx
    k g tp
    x = (BaseTypeRepr tp
    -> Assignment IndexLit ctx -> g tp -> ArrayUpdateNote tp
    forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx -> e tp -> ArrayUpdateNote tp
    mkNote BaseTypeRepr tp
    tpr Assignment IndexLit ctx
    k g tp
    x, g tp
    x)

     both' :: Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, e tp)
    -> (ArrayUpdateNote tp, f tp)
    -> m (ArrayUpdateNote tp, g tp)
    both' Assignment IndexLit ctx
    k (ArrayUpdateNote tp
    _,e tp
    x) (ArrayUpdateNote tp
    _,f tp
    y) = Assignment IndexLit ctx -> g tp -> (ArrayUpdateNote tp, g tp)
    mk Assignment IndexLit ctx
    k (g tp -> (ArrayUpdateNote tp, g tp))
    -> m (g tp) -> m (ArrayUpdateNote tp, g tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Assignment IndexLit ctx -> e tp -> f tp -> m (g tp)
    both Assignment IndexLit ctx
    k e tp
    x f tp
    y
     left' :: Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, e tp) -> m (ArrayUpdateNote tp, g tp)
    left' Assignment IndexLit ctx
    k (ArrayUpdateNote tp
    _,e tp
    x) = Assignment IndexLit ctx -> g tp -> (ArrayUpdateNote tp, g tp)
    mk Assignment IndexLit ctx
    k (g tp -> (ArrayUpdateNote tp, g tp))
    -> m (g tp) -> m (ArrayUpdateNote tp, g tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Assignment IndexLit ctx -> e tp -> m (g tp)
    left Assignment IndexLit ctx
    k e tp
    x
     right' :: Assignment IndexLit ctx
    -> (ArrayUpdateNote tp, f tp) -> m (ArrayUpdateNote tp, g tp)
    right' Assignment IndexLit ctx
    k (ArrayUpdateNote tp
    _,f tp
    y) = Assignment IndexLit ctx -> g tp -> (ArrayUpdateNote tp, g tp)
    mk Assignment IndexLit ctx
    k (g tp -> (ArrayUpdateNote tp, g tp))
    -> m (g tp) -> m (ArrayUpdateNote tp, g tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Assignment IndexLit ctx -> f tp -> m (g tp)
    right Assignment IndexLit ctx
    k f tp
    y

    keysSet :: ArrayUpdateMap e ctx tp -> Set.Set (Ctx.Assignment IndexLit ctx)
    keysSet :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp -> Set (Assignment IndexLit ctx)
    keysSet (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = [Assignment IndexLit ctx] -> Set (Assignment IndexLit ctx)
    forall a. Eq a => [a] -> Set a
    Set.fromAscList ((Assignment IndexLit ctx, e tp) -> Assignment IndexLit ctx
    forall a b. (a, b) -> a
    fst ((Assignment IndexLit ctx, e tp) -> Assignment IndexLit ctx)
    -> [(Assignment IndexLit ctx, e tp)] -> [Assignment IndexLit ctx]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> [(Assignment IndexLit ctx, e tp)]
    forall k v a. AnnotatedMap k v a -> [(k, a)]
    AM.toList AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m)

    toMap :: ArrayUpdateMap e ctx tp -> Map.Map (Ctx.Assignment IndexLit ctx) (e tp)
    toMap :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp -> Map (Assignment IndexLit ctx) (e tp)
    toMap (ArrayUpdateMap AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m) = [(Assignment IndexLit ctx, e tp)]
    -> Map (Assignment IndexLit ctx) (e tp)
    forall k a. Eq k => [(k, a)] -> Map k a
    Map.fromAscList (AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    -> [(Assignment IndexLit ctx, e tp)]
    forall k v a. AnnotatedMap k v a -> [(k, a)]
    AM.toList AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
    m)