{-|
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
  { ArrayUpdateNote tp -> IncrHash
aunHash :: !IncrHash
  , ArrayUpdateNote tp -> BaseTypeRepr tp
_aunRepr :: !(BaseTypeRepr tp)
  , 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)
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 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 :: 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
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 (f :: BaseType -> Type) (tp :: BaseType).
HasAbsValue f =>
f tp -> AbstractValue tp
getAbsValue e tp
e)

arrayUpdateAbs :: ArrayUpdateMap e ct tp -> Maybe (AbstractValue tp)
arrayUpdateAbs :: 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 :: 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 (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 :: 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 :: (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)
traverse e tp -> m (f tp)
f AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
m

null :: ArrayUpdateMap e ctx tp -> Bool
null :: 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 :: 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 :: 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 :: (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 v1 v2 a1 a2.
(Applicative f, Ord k, Semigroup v1, 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 (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 (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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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)