{-|
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 =
    forall (tp :: BaseType).
IncrHash
-> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
ArrayUpdateNote (IncrHash
hx forall a. Semigroup a => a -> a -> a
<> IncrHash
hy) BaseTypeRepr tp
tpr (forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tpr forall a b. (a -> b) -> a -> b
$ 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 = 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 -> forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ 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 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 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  -> forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
111::Int)
      Just ArrayUpdateNote tp
aun -> forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (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 = forall (tp :: BaseType).
IncrHash
-> BaseTypeRepr tp -> AbstractValue tp -> ArrayUpdateNote tp
ArrayUpdateNote (Int -> IncrHash
mkIncrHash (forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF (forall a. Hashable a => a -> Int
hash Assignment IndexLit ctx
idx) e tp
e)) BaseTypeRepr tp
tpr (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) = forall (tp :: BaseType). ArrayUpdateNote tp -> AbstractValue tp
aunAbs forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap (forall k v a.
(Ord k, Semigroup v) =>
[(k, v, a)] -> AnnotatedMap k v a
AM.fromAscList (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, 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) = 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) = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: 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) = 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) = forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap (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) = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap forall a b. (a -> b) -> a -> b
$ forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ 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       = forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (ArrayUpdateNote tp
v,e tp
x))
   | Bool
otherwise = forall (m :: Type -> Type) a. Monad m => a -> m a
return 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 = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap (forall k v a.
(Ord k, Semigroup v) =>
k -> v -> a -> AnnotatedMap k v a
AM.singleton Assignment IndexLit ctx
idx (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) =  forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap (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 (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 = forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap 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) =
  forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
-> ArrayUpdateMap e ctx tp
ArrayUpdateMap forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = (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 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 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 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) = forall a. Eq a => [a] -> Set a
Set.fromAscList (forall a b. (a, b) -> a
fst forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList (forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Assignment IndexLit ctx) (ArrayUpdateNote tp) (e tp)
m)