{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module ScheduledMergesTestQLS (tests) where

import           Control.Monad.ST
import           Control.Tracer (Tracer, nullTracer)
import           Data.Constraint (Dict (..))
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe (fromJust)
import           Data.Proxy
import           Data.Semigroup (First (..))
import           Prelude hiding (lookup)

import           ScheduledMerges as LSM

import           Test.QuickCheck
import           Test.QuickCheck.StateModel hiding (lookUpVar)
import           Test.QuickCheck.StateModel.Lockstep hiding (ModelOp)
import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep
import qualified Test.QuickCheck.StateModel.Lockstep.Run as Lockstep
import           Test.Tasty
import           Test.Tasty.QuickCheck (testProperty)

tests :: TestTree
tests :: TestTree
tests =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"ScheduledMerges vs model" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ (ModelLSM -> ModelLSM)
-> (Actions (Lockstep Model) -> Property) -> Property
forall prop.
Testable prop =>
(ModelLSM -> ModelLSM) -> prop -> Property
mapSize (ModelLSM -> ModelLSM -> ModelLSM
forall a. Num a => a -> a -> a
*ModelLSM
10) Actions (Lockstep Model) -> Property
prop_LSM  -- still <10s

-- TODO: add tagging, e.g. how often ASupplyUnion makes progress or completes a
-- union merge.
prop_LSM :: Actions (Lockstep Model) -> Property
prop_LSM :: Actions (Lockstep Model) -> Property
prop_LSM = Proxy Model -> Actions (Lockstep Model) -> Property
forall state e.
(RunLockstep state IO, e ~ Error (Lockstep state),
 forall a. IsPerformResult e a) =>
Proxy state -> Actions (Lockstep state) -> Property
Lockstep.runActions (Proxy Model
forall {k} (t :: k). Proxy t
Proxy :: Proxy Model)

-------------------------------------------------------------------------------
-- QLS infrastructure
--

type ModelLSM = Int

newtype Model = Model { Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table }
  deriving stock (ModelLSM -> Model -> ShowS
[Model] -> ShowS
Model -> TestName
(ModelLSM -> Model -> ShowS)
-> (Model -> TestName) -> ([Model] -> ShowS) -> Show Model
forall a.
(ModelLSM -> a -> ShowS)
-> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: ModelLSM -> Model -> ShowS
showsPrec :: ModelLSM -> Model -> ShowS
$cshow :: Model -> TestName
show :: Model -> TestName
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show)

data Table = Table {
      Table -> Map Key (Value, Maybe Blob)
tableContent  :: !(Map Key (Value, Maybe Blob))
    , Table -> Bool
tableHasUnion :: !Bool
    }
  deriving stock ModelLSM -> Table -> ShowS
[Table] -> ShowS
Table -> TestName
(ModelLSM -> Table -> ShowS)
-> (Table -> TestName) -> ([Table] -> ShowS) -> Show Table
forall a.
(ModelLSM -> a -> ShowS)
-> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: ModelLSM -> Table -> ShowS
showsPrec :: ModelLSM -> Table -> ShowS
$cshow :: Table -> TestName
show :: Table -> TestName
$cshowList :: [Table] -> ShowS
showList :: [Table] -> ShowS
Show

emptyTable :: Table
emptyTable :: Table
emptyTable = Map Key (Value, Maybe Blob) -> Bool -> Table
Table Map Key (Value, Maybe Blob)
forall k a. Map k a
Map.empty Bool
False

onContent ::
     (Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob))
  -> ModelLSM
  -> Model
  -> Model
onContent :: (Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob))
-> ModelLSM -> Model -> Model
onContent Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob)
f ModelLSM
k (Model Map ModelLSM Table
m) = Map ModelLSM Table -> Model
Model ((Table -> Table)
-> ModelLSM -> Map ModelLSM Table -> Map ModelLSM Table
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust Table -> Table
f' ModelLSM
k Map ModelLSM Table
m)
  where
    f' :: Table -> Table
f' Table
t = Table
t { tableContent = f (tableContent t) }

type ModelOp r = Model -> (r, Model)

initModel :: Model
initModel :: Model
initModel = Model { mlsms :: Map ModelLSM Table
mlsms = Map ModelLSM Table
forall k a. Map k a
Map.empty }

resolveValueAndBlob :: (Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob)
resolveValueAndBlob :: (Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob)
resolveValueAndBlob (Value
v, Maybe Blob
b) (Value
v', Maybe Blob
b') = (Value -> Value -> Value
resolveValue Value
v Value
v', First (Maybe Blob) -> Maybe Blob
forall a. First a -> a
getFirst (Maybe Blob -> First (Maybe Blob)
forall a. a -> First a
First Maybe Blob
b First (Maybe Blob) -> First (Maybe Blob) -> First (Maybe Blob)
forall a. Semigroup a => a -> a -> a
<> Maybe Blob -> First (Maybe Blob)
forall a. a -> First a
First Maybe Blob
b'))

modelNew         ::                                           ModelOp ModelLSM
modelInsert      :: ModelLSM -> Key -> Value -> Maybe Blob -> ModelOp ()
modelDelete      :: ModelLSM -> Key ->                        ModelOp ()
modelMupsert     :: ModelLSM -> Key -> Value ->               ModelOp ()
modelLookup      :: ModelLSM -> Key ->                        ModelOp (LookupResult Value Blob)
modelDuplicate   :: ModelLSM ->                               ModelOp ModelLSM
modelUnions      :: [ModelLSM] ->                             ModelOp ModelLSM
modelSupplyUnion :: ModelLSM -> NonNegative UnionCredits ->   ModelOp ()
modelDump        :: ModelLSM ->                               ModelOp (Map Key (Value, Maybe Blob))

modelNew :: ModelOp ModelLSM
modelNew Model {Map ModelLSM Table
mlsms :: Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table
mlsms} =
    (ModelLSM
mlsm, Model { mlsms :: Map ModelLSM Table
mlsms = ModelLSM -> Table -> Map ModelLSM Table -> Map ModelLSM Table
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModelLSM
mlsm Table
emptyTable Map ModelLSM Table
mlsms })
  where
    mlsm :: ModelLSM
mlsm = Map ModelLSM Table -> ModelLSM
forall k a. Map k a -> ModelLSM
Map.size Map ModelLSM Table
mlsms

modelInsert :: ModelLSM -> Key -> Value -> Maybe Blob -> ModelOp ()
modelInsert ModelLSM
mlsm Key
k Value
v Maybe Blob
b Model
model =
    ((), (Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob))
-> ModelLSM -> Model -> Model
onContent (Key
-> (Value, Maybe Blob)
-> Map Key (Value, Maybe Blob)
-> Map Key (Value, Maybe Blob)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
k (Value
v, Maybe Blob
b)) ModelLSM
mlsm Model
model)

modelDelete :: ModelLSM -> Key -> ModelOp ()
modelDelete ModelLSM
mlsm Key
k Model
model =
    ((), (Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob))
-> ModelLSM -> Model -> Model
onContent (Key -> Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Key
k) ModelLSM
mlsm Model
model)

modelMupsert :: ModelLSM -> Key -> Value -> ModelOp ()
modelMupsert ModelLSM
mlsm Key
k Value
v Model
model =
    ((), (Map Key (Value, Maybe Blob) -> Map Key (Value, Maybe Blob))
-> ModelLSM -> Model -> Model
onContent (((Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob))
-> Key
-> (Value, Maybe Blob)
-> Map Key (Value, Maybe Blob)
-> Map Key (Value, Maybe Blob)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob)
resolveValueAndBlob Key
k (Value
v, Maybe Blob
forall a. Maybe a
Nothing)) ModelLSM
mlsm Model
model)

modelLookup :: ModelLSM -> Key -> ModelOp (LookupResult Value Blob)
modelLookup ModelLSM
mlsm Key
k model :: Model
model@Model {Map ModelLSM Table
mlsms :: Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table
mlsms} =
    (LookupResult Value Blob
result, Model
model)
  where
    Just Table
mval = ModelLSM -> Map ModelLSM Table -> Maybe Table
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModelLSM
mlsm Map ModelLSM Table
mlsms
    result :: LookupResult Value Blob
result    = case Key -> Map Key (Value, Maybe Blob) -> Maybe (Value, Maybe Blob)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Key
k (Table -> Map Key (Value, Maybe Blob)
tableContent Table
mval) of
                  Maybe (Value, Maybe Blob)
Nothing      -> LookupResult Value Blob
forall v b. LookupResult v b
NotFound
                  Just (Value
v, Maybe Blob
mb) -> Value -> Maybe Blob -> LookupResult Value Blob
forall v b. v -> Maybe b -> LookupResult v b
Found Value
v Maybe Blob
mb

modelDuplicate :: ModelLSM -> ModelOp ModelLSM
modelDuplicate ModelLSM
mlsm Model {Map ModelLSM Table
mlsms :: Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table
mlsms} =
    (ModelLSM
mlsm', Model { mlsms :: Map ModelLSM Table
mlsms = ModelLSM -> Table -> Map ModelLSM Table -> Map ModelLSM Table
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModelLSM
mlsm' Table
mval Map ModelLSM Table
mlsms })
  where
    Just Table
mval = ModelLSM -> Map ModelLSM Table -> Maybe Table
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModelLSM
mlsm Map ModelLSM Table
mlsms
    mlsm' :: ModelLSM
mlsm'     = Map ModelLSM Table -> ModelLSM
forall k a. Map k a -> ModelLSM
Map.size Map ModelLSM Table
mlsms

modelUnions :: [ModelLSM] -> ModelOp ModelLSM
modelUnions [ModelLSM]
inputs Model {Map ModelLSM Table
mlsms :: Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table
mlsms} =
    (ModelLSM
mlsm', Model { mlsms :: Map ModelLSM Table
mlsms = ModelLSM -> Table -> Map ModelLSM Table -> Map ModelLSM Table
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModelLSM
mlsm' Table
mval' Map ModelLSM Table
mlsms })
  where
    contents :: [Map Key (Value, Maybe Blob)]
contents   = (ModelLSM -> Map Key (Value, Maybe Blob))
-> [ModelLSM] -> [Map Key (Value, Maybe Blob)]
forall a b. (a -> b) -> [a] -> [b]
map (\ModelLSM
i -> Table -> Map Key (Value, Maybe Blob)
tableContent (Maybe Table -> Table
forall a. HasCallStack => Maybe a -> a
fromJust (ModelLSM -> Map ModelLSM Table -> Maybe Table
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModelLSM
i Map ModelLSM Table
mlsms))) [ModelLSM]
inputs
    hasUnion :: Bool
hasUnion   = Bool
True
    mval' :: Table
mval'      = Map Key (Value, Maybe Blob) -> Bool -> Table
Table (((Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob))
-> [Map Key (Value, Maybe Blob)] -> Map Key (Value, Maybe Blob)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith (Value, Maybe Blob) -> (Value, Maybe Blob) -> (Value, Maybe Blob)
resolveValueAndBlob [Map Key (Value, Maybe Blob)]
contents) Bool
hasUnion
    mlsm' :: ModelLSM
mlsm'      = Map ModelLSM Table -> ModelLSM
forall k a. Map k a -> ModelLSM
Map.size Map ModelLSM Table
mlsms

modelSupplyUnion :: ModelLSM -> NonNegative UnionCredits -> ModelOp ()
modelSupplyUnion ModelLSM
_mlsm NonNegative UnionCredits
_credit Model
model =
    ((), Model
model)

modelDump :: ModelLSM -> ModelOp (Map Key (Value, Maybe Blob))
modelDump ModelLSM
mlsm model :: Model
model@Model {Map ModelLSM Table
mlsms :: Model -> Map ModelLSM Table
mlsms :: Map ModelLSM Table
mlsms} =
    (Map Key (Value, Maybe Blob)
mval, Model
model)
  where
    Just (Table Map Key (Value, Maybe Blob)
mval Bool
_) = ModelLSM -> Map ModelLSM Table -> Maybe Table
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModelLSM
mlsm Map ModelLSM Table
mlsms

instance StateModel (Lockstep Model) where
  data Action (Lockstep Model) a where
    ANew    :: Action (Lockstep Model) (LSM RealWorld)

    AInsert :: ModelVar Model (LSM RealWorld)
            -> Either (ModelVar Model Key) Key -- to refer to a prior key
            -> Value
            -> Maybe Blob
            -> Action (Lockstep Model) (Key)

    ADelete :: ModelVar Model (LSM RealWorld)
            -> Either (ModelVar Model Key) Key
            -> Action (Lockstep Model) ()

    AMupsert :: ModelVar Model (LSM RealWorld)
             -> Either (ModelVar Model Key) Key
             -> Value
             -> Action (Lockstep Model) (Key)

    ALookup :: ModelVar Model (LSM RealWorld)
            -> Either (ModelVar Model Key) Key
            -> Action (Lockstep Model) (LookupResult Value Blob)

    ADuplicate :: ModelVar Model (LSM RealWorld)
               -> Action (Lockstep Model) (LSM RealWorld)

    AUnions :: [ModelVar Model (LSM RealWorld)]
            -> Action (Lockstep Model) (LSM RealWorld)

    ASupplyUnion :: ModelVar Model (LSM RealWorld)
                 -> NonNegative UnionCredits
                 -> Action (Lockstep Model) ()

    ADump   :: ModelVar Model (LSM RealWorld)
            -> Action (Lockstep Model) (Map Key (Value, Maybe Blob))

  initialState :: Lockstep Model
initialState    = Model -> Lockstep Model
forall state. state -> Lockstep state
Lockstep.initialState Model
initModel
  nextState :: forall a.
Typeable a =>
Lockstep Model
-> Action (Lockstep Model) a -> Var a -> Lockstep Model
nextState       = Lockstep Model -> LockstepAction Model a -> Var a -> Lockstep Model
forall state a.
(InLockstep state, Typeable a) =>
Lockstep state -> LockstepAction state a -> Var a -> Lockstep state
Lockstep.nextState
  precondition :: forall a. Lockstep Model -> Action (Lockstep Model) a -> Bool
precondition    = Lockstep Model -> LockstepAction Model a -> Bool
forall state a.
InLockstep state =>
Lockstep state -> LockstepAction state a -> Bool
Lockstep.precondition
  arbitraryAction :: VarContext -> Lockstep Model -> Gen (Any (Action (Lockstep Model)))
arbitraryAction = VarContext -> Lockstep Model -> Gen (Any (Action (Lockstep Model)))
forall state.
InLockstep state =>
VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
Lockstep.arbitraryAction
  shrinkAction :: forall a.
Typeable a =>
VarContext
-> Lockstep Model
-> Action (Lockstep Model) a
-> [Any (Action (Lockstep Model))]
shrinkAction    = VarContext
-> Lockstep Model
-> LockstepAction Model a
-> [Any (Action (Lockstep Model))]
forall state a.
InLockstep state =>
VarContext
-> Lockstep state
-> LockstepAction state a
-> [Any (LockstepAction state)]
Lockstep.shrinkAction

instance RunModel (Lockstep Model) IO where
  perform :: forall a.
Typeable a =>
Lockstep Model
-> Action (Lockstep Model) a
-> LookUp IO
-> IO (PerformResult (Error (Lockstep Model)) (Realized IO a))
perform       = \Lockstep Model
_state -> Action (Lockstep Model) a -> LookUp IO -> IO a
Action (Lockstep Model) a
-> LookUp IO
-> IO (PerformResult (Error (Lockstep Model)) (Realized IO a))
forall a. Action (Lockstep Model) a -> LookUp IO -> IO a
runActionIO
  postcondition :: forall a.
(Lockstep Model, Lockstep Model)
-> Action (Lockstep Model) a
-> LookUp IO
-> Realized IO a
-> PostconditionM IO Bool
postcondition = (Lockstep Model, Lockstep Model)
-> LockstepAction Model a
-> LookUp IO
-> Realized IO a
-> PostconditionM IO Bool
forall (m :: * -> *) state a.
RunLockstep state m =>
(Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
Lockstep.postcondition
  monitoring :: forall a.
(Lockstep Model, Lockstep Model)
-> Action (Lockstep Model) a
-> LookUp IO
-> Either (Error (Lockstep Model)) (Realized IO a)
-> Property
-> Property
monitoring    = Proxy IO
-> (Lockstep Model, Lockstep Model)
-> Action (Lockstep Model) a
-> LookUp IO
-> Either (Error (Lockstep Model)) (Realized IO a)
-> Property
-> Property
forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp m
-> Either (Error (Lockstep state)) (Realized m a)
-> Property
-> Property
Lockstep.monitoring (Proxy IO
forall {k} (t :: k). Proxy t
Proxy :: Proxy IO)

instance InLockstep Model where
  data ModelValue Model a where
    MLSM    :: ModelLSM
            -> ModelValue Model (LSM RealWorld)
    MUnit   :: ()
            -> ModelValue Model ()
    MInsert :: Key
            -> ModelValue Model Key
    MLookup :: LookupResult Value Blob
            -> ModelValue Model (LookupResult Value Blob)
    MDump   :: Map Key (Value, Maybe Blob)
            -> ModelValue Model (Map Key (Value, Maybe Blob))

  data Observable Model a where
    ORef :: Observable Model (LSM RealWorld)
    OId  :: (Show a, Eq a) => a -> Observable Model a

  observeModel :: forall a. ModelValue Model a -> Observable Model a
observeModel (MLSM    ModelLSM
_) = Observable Model a
Observable Model (LSM RealWorld)
ORef
  observeModel (MUnit   ()
x) = a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
()
x
  observeModel (MInsert Key
x) = a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
Key
x
  observeModel (MLookup LookupResult Value Blob
x) = a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
LookupResult Value Blob
x
  observeModel (MDump   Map Key (Value, Maybe Blob)
x) = a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
Map Key (Value, Maybe Blob)
x

  usedVars :: forall a. LockstepAction Model a -> [AnyGVar (ModelOp Model)]
usedVars  LockstepAction Model a
R:ActionLockstepa a
ANew               = []
  usedVars (AInsert ModelVar Model (LSM RealWorld)
v Either (ModelVar Model Key) Key
evk Value
_ Maybe Blob
_) = GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v
                               AnyGVar Op -> [AnyGVar Op] -> [AnyGVar Op]
forall a. a -> [a] -> [a]
: case Either (ModelVar Model Key) Key
evk of Left ModelVar Model Key
vk -> [GVar Op Key -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op Key
ModelVar Model Key
vk]; Either (ModelVar Model Key) Key
_ -> []
  usedVars (ADelete ModelVar Model (LSM RealWorld)
v Either (ModelVar Model Key) Key
evk)     = GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v
                               AnyGVar Op -> [AnyGVar Op] -> [AnyGVar Op]
forall a. a -> [a] -> [a]
: case Either (ModelVar Model Key) Key
evk of Left ModelVar Model Key
vk -> [GVar Op Key -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op Key
ModelVar Model Key
vk]; Either (ModelVar Model Key) Key
_ -> []
  usedVars (AMupsert ModelVar Model (LSM RealWorld)
v Either (ModelVar Model Key) Key
evk Value
_)  = GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v
                               AnyGVar Op -> [AnyGVar Op] -> [AnyGVar Op]
forall a. a -> [a] -> [a]
: case Either (ModelVar Model Key) Key
evk of Left ModelVar Model Key
vk -> [GVar Op Key -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op Key
ModelVar Model Key
vk]; Either (ModelVar Model Key) Key
_ -> []
  usedVars (ALookup ModelVar Model (LSM RealWorld)
v Either (ModelVar Model Key) Key
evk)     = GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v
                               AnyGVar Op -> [AnyGVar Op] -> [AnyGVar Op]
forall a. a -> [a] -> [a]
: case Either (ModelVar Model Key) Key
evk of Left ModelVar Model Key
vk -> [GVar Op Key -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op Key
ModelVar Model Key
vk]; Either (ModelVar Model Key) Key
_ -> []
  usedVars (ADuplicate ModelVar Model (LSM RealWorld)
v)      = [GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v]
  usedVars (AUnions [ModelVar Model (LSM RealWorld)]
vs)        = [GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
v | GVar Op (LSM RealWorld)
v <- [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vs]
  usedVars (ASupplyUnion ModelVar Model (LSM RealWorld)
v NonNegative UnionCredits
_)  = [GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v]
  usedVars (ADump ModelVar Model (LSM RealWorld)
v)           = [GVar Op (LSM RealWorld) -> AnyGVar Op
forall (op :: * -> * -> *) y. GVar op y -> AnyGVar op
SomeGVar GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v]

  modelNextState :: forall a.
LockstepAction Model a
-> ModelVarContext Model -> Model -> (ModelValue Model a, Model)
modelNextState = Action (Lockstep Model) a
-> ModelVarContext Model -> Model -> (ModelValue Model a, Model)
forall a.
LockstepAction Model a
-> ModelVarContext Model -> Model -> (ModelValue Model a, Model)
runModel

  arbitraryWithVars :: ModelVarContext Model
-> Model -> Gen (Any (Action (Lockstep Model)))
arbitraryWithVars ModelVarContext Model
ctx Model
model =
    case ModelVarContext Model -> ModelFindVariables Model
forall state.
InLockstep state =>
ModelVarContext state -> ModelFindVariables state
findVars ModelVarContext Model
ctx (Proxy (LSM RealWorld)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (LSM RealWorld)) of
      []   -> Any (Action (Lockstep Model))
-> Gen (Any (Action (Lockstep Model)))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action (Lockstep Model) (LSM RealWorld)
ANew)
      [ModelVar Model (LSM RealWorld)]
vars ->
        let kvars :: [ModelVar Model Key]
kvars = ModelVarContext Model -> ModelFindVariables Model
forall state.
InLockstep state =>
ModelVarContext state -> ModelFindVariables state
findVars ModelVarContext Model
ctx (Proxy Key
forall {k} (t :: k). Proxy t
Proxy :: Proxy Key)
            existingKey :: Gen (Either (GVar Op Key) Key)
existingKey = GVar Op Key -> Either (GVar Op Key) Key
forall a b. a -> Either a b
Left (GVar Op Key -> Either (GVar Op Key) Key)
-> Gen (GVar Op Key) -> Gen (Either (GVar Op Key) Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op Key] -> Gen (GVar Op Key)
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op Key]
[ModelVar Model Key]
kvars
            freshKey :: Gen (Either a Key)
freshKey = Key -> Either a Key
forall a b. b -> Either a b
Right (Key -> Either a Key) -> Gen Key -> Gen (Either a Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Key
        in [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> Gen (Any (Action (Lockstep Model)))
forall a. HasCallStack => [(ModelLSM, Gen a)] -> Gen a
frequency ([(ModelLSM, Gen (Any (Action (Lockstep Model))))]
 -> Gen (Any (Action (Lockstep Model))))
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
          -- inserts of potentially fresh keys
          [ (ModelLSM
3, (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) Key)
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Value
 -> Maybe Blob
 -> Action (Lockstep Model) Key)
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key
      -> Value -> Maybe Blob -> Action (Lockstep Model) Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen
  (Either (GVar Op Key) Key
   -> Value -> Maybe Blob -> Action (Lockstep Model) Key)
-> Gen (Either (GVar Op Key) Key)
-> Gen (Value -> Maybe Blob -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
forall {a}. Gen (Either a Key)
freshKey
                          Gen (Value -> Maybe Blob -> Action (Lockstep Model) Key)
-> Gen Value -> Gen (Maybe Blob -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Value
                          Gen (Maybe Blob -> Action (Lockstep Model) Key)
-> Gen (Maybe Blob) -> Gen (Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @(Maybe Blob))
          ]
          -- inserts of the same keys as used earlier
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) Key)
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Value
 -> Maybe Blob
 -> Action (Lockstep Model) Key)
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key
      -> Value -> Maybe Blob -> Action (Lockstep Model) Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen
  (Either (GVar Op Key) Key
   -> Value -> Maybe Blob -> Action (Lockstep Model) Key)
-> Gen (Either (GVar Op Key) Key)
-> Gen (Value -> Maybe Blob -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
existingKey
                          Gen (Value -> Maybe Blob -> Action (Lockstep Model) Key)
-> Gen Value -> Gen (Maybe Blob -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Value
                          Gen (Maybe Blob -> Action (Lockstep Model) Key)
-> Gen (Maybe Blob) -> Gen (Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @(Maybe Blob))
          | Bool -> Bool
not ([GVar Op Key] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op Key]
[ModelVar Model Key]
kvars)
          ]
          -- deletes of arbitrary keys:
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) ())
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key -> Action (Lockstep Model) ()
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key -> Action (Lockstep Model) ()
ADelete (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key -> Action (Lockstep Model) ())
-> Gen (GVar Op (LSM RealWorld))
-> Gen (Either (GVar Op Key) Key -> Action (Lockstep Model) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen (Either (GVar Op Key) Key -> Action (Lockstep Model) ())
-> Gen (Either (GVar Op Key) Key)
-> Gen (Action (Lockstep Model) ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
forall {a}. Gen (Either a Key)
freshKey)
          ]
          -- deletes of the same key as inserted earlier:
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) ())
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key -> Action (Lockstep Model) ()
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key -> Action (Lockstep Model) ()
ADelete (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key -> Action (Lockstep Model) ())
-> Gen (GVar Op (LSM RealWorld))
-> Gen (Either (GVar Op Key) Key -> Action (Lockstep Model) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen (Either (GVar Op Key) Key -> Action (Lockstep Model) ())
-> Gen (Either (GVar Op Key) Key)
-> Gen (Action (Lockstep Model) ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
existingKey)
          | Bool -> Bool
not ([GVar Op Key] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op Key]
[ModelVar Model Key]
kvars)
          ]
          -- mupserts of potentially fresh keys
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) Key)
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Action (Lockstep Model) Key
AMupsert (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Value
 -> Action (Lockstep Model) Key)
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                           Gen
  (Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key)
-> Gen (Either (GVar Op Key) Key)
-> Gen (Value -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
forall {a}. Gen (Either a Key)
freshKey
                           Gen (Value -> Action (Lockstep Model) Key)
-> Gen Value -> Gen (Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Value)
          ]
          -- mupserts of the same keys as used earlier
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) Key)
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) Key)
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Action (Lockstep Model) Key
AMupsert (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Value
 -> Action (Lockstep Model) Key)
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                           Gen
  (Either (GVar Op Key) Key -> Value -> Action (Lockstep Model) Key)
-> Gen (Either (GVar Op Key) Key)
-> Gen (Value -> Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
existingKey
                           Gen (Value -> Action (Lockstep Model) Key)
-> Gen Value -> Gen (Action (Lockstep Model) Key)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @Value)
          | Bool -> Bool
not ([GVar Op Key] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op Key]
[ModelVar Model Key]
kvars)
          ]
          -- lookup of arbitrary keys:
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) (LookupResult Value Blob)
 -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) (LookupResult Value Blob)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) (LookupResult Value Blob))
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key
-> Action (Lockstep Model) (LookupResult Value Blob)
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Action (Lockstep Model) (LookupResult Value Blob)
ALookup (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key
      -> Action (Lockstep Model) (LookupResult Value Blob))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen
  (Either (GVar Op Key) Key
   -> Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Either (GVar Op Key) Key)
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
forall {a}. Gen (Either a Key)
freshKey)
          ]
          -- lookup of the same key as inserted earlier:
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
3, (Action (Lockstep Model) (LookupResult Value Blob)
 -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) (LookupResult Value Blob)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) (LookupResult Value Blob))
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Either (GVar Op Key) Key
-> Action (Lockstep Model) (LookupResult Value Blob)
ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Action (Lockstep Model) (LookupResult Value Blob)
ALookup (GVar Op (LSM RealWorld)
 -> Either (GVar Op Key) Key
 -> Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (GVar Op (LSM RealWorld))
-> Gen
     (Either (GVar Op Key) Key
      -> Action (Lockstep Model) (LookupResult Value Blob))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
                          Gen
  (Either (GVar Op Key) Key
   -> Action (Lockstep Model) (LookupResult Value Blob))
-> Gen (Either (GVar Op Key) Key)
-> Gen (Action (Lockstep Model) (LookupResult Value Blob))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Either (GVar Op Key) Key)
existingKey)
          | Bool -> Bool
not ([GVar Op Key] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op Key]
[ModelVar Model Key]
kvars)
          ]
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) (LSM RealWorld)
 -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) (LSM RealWorld))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) (LSM RealWorld))
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) (LSM RealWorld))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld) -> Action (Lockstep Model) (LSM RealWorld)
ModelVar Model (LSM RealWorld)
-> Action (Lockstep Model) (LSM RealWorld)
ADuplicate (GVar Op (LSM RealWorld)
 -> Action (Lockstep Model) (LSM RealWorld))
-> Gen (GVar Op (LSM RealWorld))
-> Gen (Action (Lockstep Model) (LSM RealWorld))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars)
          ]
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) (LSM RealWorld)
 -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) (LSM RealWorld))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) (LSM RealWorld))
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) (LSM RealWorld))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$ do
                  -- bias towards binary, only go high when many tables exist
                  ModelLSM
len <- [ModelLSM] -> Gen ModelLSM
forall a. HasCallStack => [a] -> Gen a
elements ([ModelLSM
2, ModelLSM
2] [ModelLSM] -> [ModelLSM] -> [ModelLSM]
forall a. [a] -> [a] -> [a]
++ ModelLSM -> [ModelLSM] -> [ModelLSM]
forall a. ModelLSM -> [a] -> [a]
take ([GVar Op (LSM RealWorld)] -> ModelLSM
forall a. [a] -> ModelLSM
forall (t :: * -> *) a. Foldable t => t a -> ModelLSM
length [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars) [ModelLSM
1..ModelLSM
5])
                  [GVar Op (LSM RealWorld)]
-> Action (Lockstep Model) (LSM RealWorld)
[ModelVar Model (LSM RealWorld)]
-> Action (Lockstep Model) (LSM RealWorld)
AUnions ([GVar Op (LSM RealWorld)]
 -> Action (Lockstep Model) (LSM RealWorld))
-> Gen [GVar Op (LSM RealWorld)]
-> Gen (Action (Lockstep Model) (LSM RealWorld))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelLSM
-> Gen (GVar Op (LSM RealWorld)) -> Gen [GVar Op (LSM RealWorld)]
forall a. ModelLSM -> Gen a -> Gen [a]
vectorOf ModelLSM
len ([GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars))
          ]
          -- only supply to tables with unions
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
2, (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) ())
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) ())
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> NonNegative UnionCredits -> Action (Lockstep Model) ()
ModelVar Model (LSM RealWorld)
-> NonNegative UnionCredits -> Action (Lockstep Model) ()
ASupplyUnion (GVar Op (LSM RealWorld)
 -> NonNegative UnionCredits -> Action (Lockstep Model) ())
-> Gen (GVar Op (LSM RealWorld))
-> Gen (NonNegative UnionCredits -> Action (Lockstep Model) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
varsWithUnion
                               Gen (NonNegative UnionCredits -> Action (Lockstep Model) ())
-> Gen (NonNegative UnionCredits)
-> Gen (Action (Lockstep Model) ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (NonNegative UnionCredits)
forall a. Arbitrary a => Gen a
arbitrary)
          | let hasUnion :: GVar Op (LSM RealWorld) -> Bool
hasUnion GVar Op (LSM RealWorld)
v = let MLSM ModelLSM
m = ModelVarContext Model -> ModelLookUp Model
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext Model
ctx GVar Op (LSM RealWorld)
ModelVar Model (LSM RealWorld)
v in
                             case ModelLSM -> Map ModelLSM Table -> Maybe Table
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModelLSM
m (Model -> Map ModelLSM Table
mlsms Model
model) of
                               Maybe Table
Nothing -> Bool
False
                               Just Table
t  -> Table -> Bool
tableHasUnion Table
t
          , let varsWithUnion :: [GVar Op (LSM RealWorld)]
varsWithUnion = (GVar Op (LSM RealWorld) -> Bool)
-> [GVar Op (LSM RealWorld)] -> [GVar Op (LSM RealWorld)]
forall a. (a -> Bool) -> [a] -> [a]
filter GVar Op (LSM RealWorld) -> Bool
hasUnion [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars
          , Bool -> Bool
not ([GVar Op (LSM RealWorld)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op (LSM RealWorld)]
varsWithUnion)
          ]
       [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
-> [(ModelLSM, Gen (Any (Action (Lockstep Model))))]
forall a. [a] -> [a] -> [a]
++ [ (ModelLSM
1, (Action (Lockstep Model) (Map Key (Value, Maybe Blob))
 -> Any (Action (Lockstep Model)))
-> Gen (Action (Lockstep Model) (Map Key (Value, Maybe Blob)))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep Model) (Map Key (Value, Maybe Blob))
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen (Action (Lockstep Model) (Map Key (Value, Maybe Blob)))
 -> Gen (Any (Action (Lockstep Model))))
-> Gen (Action (Lockstep Model) (Map Key (Value, Maybe Blob)))
-> Gen (Any (Action (Lockstep Model)))
forall a b. (a -> b) -> a -> b
$
                  GVar Op (LSM RealWorld)
-> Action (Lockstep Model) (Map Key (Value, Maybe Blob))
ModelVar Model (LSM RealWorld)
-> Action (Lockstep Model) (Map Key (Value, Maybe Blob))
ADump (GVar Op (LSM RealWorld)
 -> Action (Lockstep Model) (Map Key (Value, Maybe Blob)))
-> Gen (GVar Op (LSM RealWorld))
-> Gen (Action (Lockstep Model) (Map Key (Value, Maybe Blob)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GVar Op (LSM RealWorld)] -> Gen (GVar Op (LSM RealWorld))
forall a. HasCallStack => [a] -> Gen a
elements [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars)
          ]

  shrinkWithVars :: forall a.
ModelVarContext Model
-> Model
-> LockstepAction Model a
-> [Any (Action (Lockstep Model))]
shrinkWithVars ModelVarContext Model
_ctx Model
_model (AInsert ModelVar Model (LSM RealWorld)
var (Right Key
k) Value
v Maybe Blob
b) =
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k') Value
v' Maybe Blob
b' | (Key
k', Value
v', Maybe Blob
b') <- (Key, Value, Maybe Blob) -> [(Key, Value, Maybe Blob)]
forall a. Arbitrary a => a -> [a]
shrink (Key
k, Value
v, Maybe Blob
b) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (AInsert ModelVar Model (LSM RealWorld)
var (Left ModelVar Model Key
_kv) Value
v Maybe Blob
b) =
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k') Value
v' Maybe Blob
b' | (Key
k', Value
v', Maybe Blob
b') <- (Key, Value, Maybe Blob) -> [(Key, Value, Maybe Blob)]
forall a. Arbitrary a => a -> [a]
shrink (ModelLSM -> Key
K ModelLSM
100, Value
v, Maybe Blob
b) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (ADelete ModelVar Model (LSM RealWorld)
var (Right Key
k)) =
    [ Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key -> Action (Lockstep Model) ()
ADelete ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k') | Key
k' <- Key -> [Key]
forall a. Arbitrary a => a -> [a]
shrink Key
k ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (ADelete ModelVar Model (LSM RealWorld)
var (Left ModelVar Model Key
_kv)) =
    [ Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key -> Action (Lockstep Model) ()
ADelete ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k) | Key
k <- Key -> [Key]
forall a. Arbitrary a => a -> [a]
shrink (ModelLSM -> Key
K ModelLSM
100) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (AMupsert ModelVar Model (LSM RealWorld)
var (Right Key
k) Value
v) =
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k) Value
v Maybe Blob
forall a. Maybe a
Nothing ] [Any (Action (Lockstep Model))]
-> [Any (Action (Lockstep Model))]
-> [Any (Action (Lockstep Model))]
forall a. [a] -> [a] -> [a]
++
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Action (Lockstep Model) Key
AMupsert ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k') Value
v' | (Key
k', Value
v') <- (Key, Value) -> [(Key, Value)]
forall a. Arbitrary a => a -> [a]
shrink (Key
k, Value
v) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (AMupsert ModelVar Model (LSM RealWorld)
var (Left ModelVar Model Key
kv) Value
v) =
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Maybe Blob
-> Action (Lockstep Model) Key
AInsert ModelVar Model (LSM RealWorld)
var (GVar Op Key -> Either (GVar Op Key) Key
forall a b. a -> Either a b
Left GVar Op Key
ModelVar Model Key
kv) Value
v Maybe Blob
forall a. Maybe a
Nothing ] [Any (Action (Lockstep Model))]
-> [Any (Action (Lockstep Model))]
-> [Any (Action (Lockstep Model))]
forall a. [a] -> [a] -> [a]
++
    [ Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) Key -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) Key -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Either (ModelVar Model Key) Key
-> Value
-> Action (Lockstep Model) Key
AMupsert ModelVar Model (LSM RealWorld)
var (Key -> Either (GVar Op Key) Key
forall a b. b -> Either a b
Right Key
k') Value
v' | (Key
k', Value
v') <- (Key, Value) -> [(Key, Value)]
forall a. Arbitrary a => a -> [a]
shrink (ModelLSM -> Key
K ModelLSM
100, Value
v) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (AUnions [ModelVar Model (LSM RealWorld)
var]) =
    [ Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) (LSM RealWorld)
 -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> Action (Lockstep Model) (LSM RealWorld)
ADuplicate ModelVar Model (LSM RealWorld)
var ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (AUnions [ModelVar Model (LSM RealWorld)]
vars) =
    [ Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) (LSM RealWorld)
 -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) (LSM RealWorld)
-> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ [ModelVar Model (LSM RealWorld)]
-> Action (Lockstep Model) (LSM RealWorld)
AUnions [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vs | [GVar Op (LSM RealWorld)]
vs <- (GVar Op (LSM RealWorld) -> [GVar Op (LSM RealWorld)])
-> [GVar Op (LSM RealWorld)] -> [[GVar Op (LSM RealWorld)]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([GVar Op (LSM RealWorld)]
-> GVar Op (LSM RealWorld) -> [GVar Op (LSM RealWorld)]
forall a b. a -> b -> a
const []) [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars, Bool -> Bool
not ([GVar Op (LSM RealWorld)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GVar Op (LSM RealWorld)]
vs) ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model (ASupplyUnion ModelVar Model (LSM RealWorld)
var NonNegative UnionCredits
c) =
    [ Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep Model) () -> Any (Action (Lockstep Model)))
-> Action (Lockstep Model) () -> Any (Action (Lockstep Model))
forall a b. (a -> b) -> a -> b
$ ModelVar Model (LSM RealWorld)
-> NonNegative UnionCredits -> Action (Lockstep Model) ()
ASupplyUnion ModelVar Model (LSM RealWorld)
var NonNegative UnionCredits
c' | NonNegative UnionCredits
c' <- NonNegative UnionCredits -> [NonNegative UnionCredits]
forall a. Arbitrary a => a -> [a]
shrink NonNegative UnionCredits
c ]

  shrinkWithVars ModelVarContext Model
_ctx Model
_model LockstepAction Model a
_action = []

deriving newtype instance Arbitrary UnionCredits

instance RunLockstep Model IO where
  observeReal :: forall a.
Proxy IO
-> LockstepAction Model a -> Realized IO a -> Observable Model a
observeReal Proxy IO
_ LockstepAction Model a
action Realized IO a
result =
    case (LockstepAction Model a
action, a
Realized IO a
result) of
      (LockstepAction Model a
R:ActionLockstepa a
ANew,           a
_) -> Observable Model a
Observable Model (LSM RealWorld)
ORef
      (AInsert{},      a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x
      (ADelete{},      a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x
      (AMupsert{},     a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x
      (ALookup{},      a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x
      (ADuplicate{},   a
_) -> Observable Model a
Observable Model (LSM RealWorld)
ORef
      (AUnions{},      a
_) -> Observable Model a
Observable Model (LSM RealWorld)
ORef
      (ASupplyUnion{}, a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x
      (ADump{},        a
x) -> a -> Observable Model a
forall a. (Show a, Eq a) => a -> Observable Model a
OId a
x

  showRealResponse :: forall a.
Proxy IO
-> LockstepAction Model a -> Maybe (Dict (Show (Realized IO a)))
showRealResponse Proxy IO
_ LockstepAction Model a
R:ActionLockstepa a
ANew           = Maybe (Dict (Show (Realized IO a)))
Maybe (Dict (Show (LSM RealWorld)))
forall a. Maybe a
Nothing
  showRealResponse Proxy IO
_ AInsert{}      = Dict (Show Key) -> Maybe (Dict (Show Key))
forall a. a -> Maybe a
Just Dict (Show Key)
forall (a :: Constraint). a => Dict a
Dict
  showRealResponse Proxy IO
_ ADelete{}      = Dict (Show ()) -> Maybe (Dict (Show ()))
forall a. a -> Maybe a
Just Dict (Show ())
forall (a :: Constraint). a => Dict a
Dict
  showRealResponse Proxy IO
_ AMupsert{}     = Dict (Show Key) -> Maybe (Dict (Show Key))
forall a. a -> Maybe a
Just Dict (Show Key)
forall (a :: Constraint). a => Dict a
Dict
  showRealResponse Proxy IO
_ ALookup{}      = Dict (Show (LookupResult Value Blob))
-> Maybe (Dict (Show (LookupResult Value Blob)))
forall a. a -> Maybe a
Just Dict (Show (LookupResult Value Blob))
forall (a :: Constraint). a => Dict a
Dict
  showRealResponse Proxy IO
_ ADuplicate{}   = Maybe (Dict (Show (Realized IO a)))
Maybe (Dict (Show (LSM RealWorld)))
forall a. Maybe a
Nothing
  showRealResponse Proxy IO
_ AUnions{}      = Maybe (Dict (Show (Realized IO a)))
Maybe (Dict (Show (LSM RealWorld)))
forall a. Maybe a
Nothing
  showRealResponse Proxy IO
_ ASupplyUnion{} = Maybe (Dict (Show ()))
Maybe (Dict (Show (Realized IO a)))
forall a. Maybe a
Nothing
  showRealResponse Proxy IO
_ ADump{}        = Dict (Show (Map Key (Value, Maybe Blob)))
-> Maybe (Dict (Show (Map Key (Value, Maybe Blob))))
forall a. a -> Maybe a
Just Dict (Show (Map Key (Value, Maybe Blob)))
forall (a :: Constraint). a => Dict a
Dict

deriving stock instance Show (Action (Lockstep Model) a)
deriving stock instance Show (Observable Model a)
deriving stock instance Show (ModelValue Model a)

deriving stock instance Eq (Action (Lockstep Model) a)
deriving stock instance Eq (Observable Model a)
deriving stock instance Eq (ModelValue Model a)


runActionIO :: Action (Lockstep Model) a
            -> LookUp IO
            -> IO a
runActionIO :: forall a. Action (Lockstep Model) a -> LookUp IO -> IO a
runActionIO Action (Lockstep Model) a
action LookUp IO
lookUp =
  ST RealWorld a -> IO a
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld a -> IO a) -> ST RealWorld a -> IO a
forall a b. (a -> b) -> a -> b
$
  case Action (Lockstep Model) a
action of
    Action (Lockstep Model) a
R:ActionLockstepa a
ANew                -> ST RealWorld a
ST RealWorld (LSM RealWorld)
forall s. ST s (LSM s)
new
    AInsert ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk Value
v Maybe Blob
b -> Tracer (ST RealWorld) Event
-> LSM RealWorld -> Key -> Value -> Maybe Blob -> ST RealWorld ()
forall s.
Tracer (ST s) Event
-> LSM s -> Key -> Value -> Maybe Blob -> ST s ()
insert Tracer (ST RealWorld) Event
tr (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var) Key
k Value
v Maybe Blob
b ST RealWorld () -> ST RealWorld a -> ST RealWorld a
forall a b. ST RealWorld a -> ST RealWorld b -> ST RealWorld b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ST RealWorld a
forall a. a -> ST RealWorld a
forall (m :: * -> *) a. Monad m => a -> m a
return a
Key
k
      where k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
forall a. ModelVar Model a -> a
lookUpVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk
    ADelete ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk     -> Tracer (ST RealWorld) Event
-> LSM RealWorld -> Key -> ST RealWorld ()
forall s. Tracer (ST s) Event -> LSM s -> Key -> ST s ()
delete Tracer (ST RealWorld) Event
tr (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var) Key
k ST RealWorld () -> ST RealWorld a -> ST RealWorld a
forall a b. ST RealWorld a -> ST RealWorld b -> ST RealWorld b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ST RealWorld a
forall a. a -> ST RealWorld a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      where k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
forall a. ModelVar Model a -> a
lookUpVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk
    AMupsert ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk Value
v  -> Tracer (ST RealWorld) Event
-> LSM RealWorld -> Key -> Value -> ST RealWorld ()
forall s. Tracer (ST s) Event -> LSM s -> Key -> Value -> ST s ()
mupsert Tracer (ST RealWorld) Event
tr (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var) Key
k Value
v ST RealWorld () -> ST RealWorld a -> ST RealWorld a
forall a b. ST RealWorld a -> ST RealWorld b -> ST RealWorld b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ST RealWorld a
forall a. a -> ST RealWorld a
forall (m :: * -> *) a. Monad m => a -> m a
return a
Key
k
      where k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
forall a. ModelVar Model a -> a
lookUpVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk
    ALookup ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk     -> LSM RealWorld -> Key -> ST RealWorld (LookupResult Value Blob)
forall s. LSM s -> Key -> ST s (LookupResult Value Blob)
lookup (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var) Key
k
      where k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
forall a. ModelVar Model a -> a
lookUpVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk
    ADuplicate ModelVar Model (LSM RealWorld)
var      -> LSM RealWorld -> ST RealWorld (LSM RealWorld)
forall s. LSM s -> ST s (LSM s)
duplicate (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var)
    AUnions [ModelVar Model (LSM RealWorld)]
vars        -> [LSM RealWorld] -> ST RealWorld (LSM RealWorld)
forall s. [LSM s] -> ST s (LSM s)
unions ((GVar Op (LSM RealWorld) -> LSM RealWorld)
-> [GVar Op (LSM RealWorld)] -> [LSM RealWorld]
forall a b. (a -> b) -> [a] -> [b]
map GVar Op (LSM RealWorld) -> LSM RealWorld
ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars)
    ASupplyUnion ModelVar Model (LSM RealWorld)
var NonNegative UnionCredits
c  -> LSM RealWorld -> UnionCredits -> ST RealWorld UnionCredits
forall s. LSM s -> UnionCredits -> ST s UnionCredits
supplyUnionCredits (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var) (NonNegative UnionCredits -> UnionCredits
forall a. NonNegative a -> a
getNonNegative NonNegative UnionCredits
c) ST RealWorld UnionCredits -> ST RealWorld a -> ST RealWorld a
forall a b. ST RealWorld a -> ST RealWorld b -> ST RealWorld b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ST RealWorld a
forall a. a -> ST RealWorld a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    ADump      ModelVar Model (LSM RealWorld)
var      -> LSM RealWorld -> ST RealWorld (Map Key (Value, Maybe Blob))
forall s. LSM s -> ST s (Map Key (Value, Maybe Blob))
logicalValue (ModelVar Model (LSM RealWorld) -> LSM RealWorld
forall a. ModelVar Model a -> a
lookUpVar ModelVar Model (LSM RealWorld)
var)
  where
    lookUpVar :: ModelVar Model a -> a
    lookUpVar :: forall a. ModelVar Model a -> a
lookUpVar = Proxy IO -> LookUp IO -> GVar Op a -> Realized IO a
forall (op :: * -> * -> *) (m :: * -> *) a.
InterpretOp op (WrapRealized m) =>
Proxy m -> LookUp m -> GVar op a -> Realized m a
lookUpGVar (Proxy IO
forall {k} (t :: k). Proxy t
Proxy :: Proxy IO) Var a -> Realized IO a
LookUp IO
lookUp

    tr :: Tracer (ST RealWorld) Event
    tr :: Tracer (ST RealWorld) Event
tr = Tracer (ST RealWorld) Event
forall (m :: * -> *) a. Monad m => Tracer m a
nullTracer

runModel :: Action (Lockstep Model) a
         -> ModelVarContext Model
         -> Model
         -> (ModelValue Model a, Model)
runModel :: forall a.
LockstepAction Model a
-> ModelVarContext Model -> Model -> (ModelValue Model a, Model)
runModel Action (Lockstep Model) a
action ModelVarContext Model
ctx Model
m =
  case Action (Lockstep Model) a
action of
    Action (Lockstep Model) a
R:ActionLockstepa a
ANew -> (ModelLSM -> ModelValue Model (LSM RealWorld)
MLSM ModelLSM
mlsm, Model
m')
      where (ModelLSM
mlsm, Model
m') = ModelOp ModelLSM
modelNew Model
m

    AInsert ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk Value
v Maybe Blob
b -> (Key -> ModelValue Model Key
MInsert Key
k, Model
m')
      where ((), Model
m') = ModelLSM -> Key -> Value -> Maybe Blob -> ModelOp ()
modelInsert (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Key
k Value
v Maybe Blob
b Model
m
            k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
lookUpKeyVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk

    ADelete ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk -> (() -> ModelValue Model ()
MUnit (), Model
m')
      where ((), Model
m') = ModelLSM -> Key -> ModelOp ()
modelDelete (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Key
k Model
m
            k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
lookUpKeyVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk

    AMupsert ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk Value
v -> (Key -> ModelValue Model Key
MInsert Key
k, Model
m')
      where ((), Model
m') = ModelLSM -> Key -> Value -> ModelOp ()
modelMupsert (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Key
k Value
v Model
m
            k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
lookUpKeyVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk

    ALookup ModelVar Model (LSM RealWorld)
var Either (ModelVar Model Key) Key
evk -> (LookupResult Value Blob
-> ModelValue Model (LookupResult Value Blob)
MLookup LookupResult Value Blob
mv, Model
m')
      where (LookupResult Value Blob
mv, Model
m') = ModelLSM -> Key -> ModelOp (LookupResult Value Blob)
modelLookup (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Key
k Model
m
            k :: Key
k = (GVar Op Key -> Key)
-> (Key -> Key) -> Either (GVar Op Key) Key -> Key
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GVar Op Key -> Key
ModelVar Model Key -> Key
lookUpKeyVar Key -> Key
forall a. a -> a
id Either (GVar Op Key) Key
Either (ModelVar Model Key) Key
evk

    ADuplicate ModelVar Model (LSM RealWorld)
var -> (ModelLSM -> ModelValue Model (LSM RealWorld)
MLSM ModelLSM
mlsm', Model
m')
      where (ModelLSM
mlsm', Model
m') = ModelLSM -> ModelOp ModelLSM
modelDuplicate (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Model
m

    AUnions [ModelVar Model (LSM RealWorld)]
vars -> (ModelLSM -> ModelValue Model (LSM RealWorld)
MLSM ModelLSM
mlsm', Model
m')
      where (ModelLSM
mlsm', Model
m') = [ModelLSM] -> ModelOp ModelLSM
modelUnions ((GVar Op (LSM RealWorld) -> ModelLSM)
-> [GVar Op (LSM RealWorld)] -> [ModelLSM]
forall a b. (a -> b) -> [a] -> [b]
map GVar Op (LSM RealWorld) -> ModelLSM
ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar [GVar Op (LSM RealWorld)]
[ModelVar Model (LSM RealWorld)]
vars) Model
m

    ASupplyUnion ModelVar Model (LSM RealWorld)
var NonNegative UnionCredits
c -> (() -> ModelValue Model ()
MUnit (), Model
m')
      where ((), Model
m') = ModelLSM -> NonNegative UnionCredits -> ModelOp ()
modelSupplyUnion (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) NonNegative UnionCredits
c Model
m

    ADump ModelVar Model (LSM RealWorld)
var -> (Map Key (Value, Maybe Blob)
-> ModelValue Model (Map Key (Value, Maybe Blob))
MDump Map Key (Value, Maybe Blob)
mapping, Model
m)
      where (Map Key (Value, Maybe Blob)
mapping, Model
_) = ModelLSM -> ModelOp (Map Key (Value, Maybe Blob))
modelDump (ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var) Model
m
  where
    lookUpLsMVar :: ModelVar Model (LSM RealWorld) -> ModelLSM
    lookUpLsMVar :: ModelVar Model (LSM RealWorld) -> ModelLSM
lookUpLsMVar ModelVar Model (LSM RealWorld)
var = case ModelVarContext Model -> ModelLookUp Model
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext Model
ctx ModelVar Model (LSM RealWorld)
var of MLSM ModelLSM
r -> ModelLSM
r

    lookUpKeyVar :: ModelVar Model Key -> Key
    lookUpKeyVar :: ModelVar Model Key -> Key
lookUpKeyVar ModelVar Model Key
var = case ModelVarContext Model -> ModelLookUp Model
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext Model
ctx ModelVar Model Key
var of MInsert Key
k -> Key
k