{-# LANGUAGE ScopedTypeVariables #-}

module Test.Util.QSM (
    Example
    -- opaque
  , example
  , run
  , run'
  ) where

import           Control.Monad
import qualified Control.Monad.Fail as Fail
import           Data.Typeable
import qualified Test.StateMachine.Logic as Logic
import           Test.StateMachine.Sequential
import           Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2

data Example cmd a =
    Done a
  | Run (cmd Symbolic) ([Var] -> Example cmd a)
  | Fail String

instance Functor (Example cmd) where
  fmap :: forall a b. (a -> b) -> Example cmd a -> Example cmd b
fmap = (a -> b) -> Example cmd a -> Example cmd b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative (Example cmd) where
  pure :: forall a. a -> Example cmd a
pure  = a -> Example cmd a
forall (cmd :: (* -> *) -> *) a. a -> Example cmd a
Done
  <*> :: forall a b. Example cmd (a -> b) -> Example cmd a -> Example cmd b
(<*>) = Example cmd (a -> b) -> Example cmd a -> Example cmd b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad (Example cmd) where
  return :: forall a. a -> Example cmd a
return         = a -> Example cmd a
forall a. a -> Example cmd a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Done a
a   >>= :: forall a b. Example cmd a -> (a -> Example cmd b) -> Example cmd b
>>= a -> Example cmd b
f = a -> Example cmd b
f a
a
  Run cmd Symbolic
c [Var] -> Example cmd a
k  >>= a -> Example cmd b
f = cmd Symbolic -> ([Var] -> Example cmd b) -> Example cmd b
forall (cmd :: (* -> *) -> *) a.
cmd Symbolic -> ([Var] -> Example cmd a) -> Example cmd a
Run cmd Symbolic
c ([Var] -> Example cmd a
k ([Var] -> Example cmd a)
-> (a -> Example cmd b) -> [Var] -> Example cmd b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> Example cmd b
f)
  Fail String
err >>= a -> Example cmd b
_ = String -> Example cmd b
forall (cmd :: (* -> *) -> *) a. String -> Example cmd a
Fail String
err

instance Fail.MonadFail (Example cmd) where
  fail :: forall a. String -> Example cmd a
fail = String -> Example cmd a
forall (cmd :: (* -> *) -> *) a. String -> Example cmd a
Fail

-- | Run a command, and capture its references
run :: Typeable a => cmd Symbolic -> Example cmd [Reference a Symbolic]
run :: forall a (cmd :: (* -> *) -> *).
Typeable a =>
cmd Symbolic -> Example cmd [Reference a Symbolic]
run cmd Symbolic
cmd = cmd Symbolic
-> ([Var] -> Example cmd [Reference a Symbolic])
-> Example cmd [Reference a Symbolic]
forall (cmd :: (* -> *) -> *) a.
cmd Symbolic -> ([Var] -> Example cmd a) -> Example cmd a
Run cmd Symbolic
cmd ([Reference a Symbolic] -> Example cmd [Reference a Symbolic]
forall (cmd :: (* -> *) -> *) a. a -> Example cmd a
Done ([Reference a Symbolic] -> Example cmd [Reference a Symbolic])
-> ([Var] -> [Reference a Symbolic])
-> [Var]
-> Example cmd [Reference a Symbolic]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Reference a Symbolic) -> [Var] -> [Reference a Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (Symbolic a -> Reference a Symbolic
forall a (r :: * -> *). r a -> Reference a r
Reference (Symbolic a -> Reference a Symbolic)
-> (Var -> Symbolic a) -> Var -> Reference a Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbolic a
forall a. Typeable a => Var -> Symbolic a
Symbolic))

-- | Run a command, ignoring its references
run' :: cmd Symbolic -> Example cmd ()
run' :: forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' cmd Symbolic
cmd = cmd Symbolic -> ([Var] -> Example cmd ()) -> Example cmd ()
forall (cmd :: (* -> *) -> *) a.
cmd Symbolic -> ([Var] -> Example cmd a) -> Example cmd a
Run cmd Symbolic
cmd (\[Var]
_vars -> () -> Example cmd ()
forall (cmd :: (* -> *) -> *) a. a -> Example cmd a
Done ())

example :: forall model cmd m resp. (Rank2.Foldable resp, Show (cmd Symbolic))
        => StateMachine model cmd m resp
        -> Example cmd ()
        -> Commands cmd resp
example :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (cmd Symbolic)) =>
StateMachine model cmd m resp
-> Example cmd () -> Commands cmd resp
example StateMachine model cmd m resp
sm =
    [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> Commands cmd resp)
-> (Example cmd () -> [Command cmd resp])
-> Example cmd ()
-> Commands cmd resp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Command cmd resp], Counter) -> [Command cmd resp]
forall a b. (a, b) -> a
fst (([Command cmd resp], Counter) -> [Command cmd resp])
-> (Example cmd () -> ([Command cmd resp], Counter))
-> Example cmd ()
-> [Command cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenSym [Command cmd resp]
 -> Counter -> ([Command cmd resp], Counter))
-> Counter
-> GenSym [Command cmd resp]
-> ([Command cmd resp], Counter)
forall a b c. (a -> b -> c) -> b -> a -> c
flip GenSym [Command cmd resp]
-> Counter -> ([Command cmd resp], Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym Counter
newCounter (GenSym [Command cmd resp] -> ([Command cmd resp], Counter))
-> (Example cmd () -> GenSym [Command cmd resp])
-> Example cmd ()
-> ([Command cmd resp], Counter)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
go (StateMachine model cmd m resp -> forall (r :: * -> *). model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine model cmd m resp
sm)
  where
    go :: model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
    go :: model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
go model Symbolic
_ (Done ())   = [Command cmd resp] -> GenSym [Command cmd resp]
forall a. a -> GenSym a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    go model Symbolic
_ (Fail String
err)  = String -> GenSym [Command cmd resp]
forall a. HasCallStack => String -> a
error (String -> GenSym [Command cmd resp])
-> String -> GenSym [Command cmd resp]
forall a b. (a -> b) -> a -> b
$ String
"example: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
    go model Symbolic
m (Run cmd Symbolic
cmd [Var] -> Example cmd ()
k) = do
        case Logic -> Value
Logic.logic (StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition StateMachine model cmd m resp
sm model Symbolic
m cmd Symbolic
cmd) of
          Logic.VFalse Counterexample
counterexample ->
            String -> GenSym [Command cmd resp]
forall a. HasCallStack => String -> a
error (String -> GenSym [Command cmd resp])
-> String -> GenSym [Command cmd resp]
forall a b. (a -> b) -> a -> b
$ String
"Invalid command " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cmd Symbolic -> String
forall a. Show a => a -> String
show cmd Symbolic
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Counterexample -> String
forall a. Show a => a -> String
show Counterexample
counterexample
          Value
Logic.VTrue -> do
            resp Symbolic
resp <- StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock StateMachine model cmd m resp
sm model Symbolic
m cmd Symbolic
cmd

            let m' :: model Symbolic
                m' :: model Symbolic
m' = StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition StateMachine model cmd m resp
sm model Symbolic
m cmd Symbolic
cmd resp Symbolic
resp

                vars :: [Var]
                vars :: [Var]
vars = resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
resp

                cmd' :: Command cmd resp
                cmd' :: Command cmd resp
cmd' = cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
cmd resp Symbolic
resp [Var]
vars

            (Command cmd resp
cmd' Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
:) ([Command cmd resp] -> [Command cmd resp])
-> GenSym [Command cmd resp] -> GenSym [Command cmd resp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
go model Symbolic
m' ([Var] -> Example cmd ()
k [Var]
vars)