{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Types.GenSym
-- Copyright   :  (C) 2018, HERE Europe B.V.
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-----------------------------------------------------------------------------

module Test.StateMachine.Types.GenSym
  ( GenSym
  , runGenSym
  , genSym
  , Counter
  , newCounter
  )
  where

import           Control.Monad.State
                   (State, get, put, runState)
import           Data.Typeable
                   (Typeable)
import           Prelude

import           Test.StateMachine.Types.References

------------------------------------------------------------------------

newtype GenSym a = GenSym (State Counter a)
  deriving newtype (a -> GenSym b -> GenSym a
(a -> b) -> GenSym a -> GenSym b
(forall a b. (a -> b) -> GenSym a -> GenSym b)
-> (forall a b. a -> GenSym b -> GenSym a) -> Functor GenSym
forall a b. a -> GenSym b -> GenSym a
forall a b. (a -> b) -> GenSym a -> GenSym b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> GenSym b -> GenSym a
$c<$ :: forall a b. a -> GenSym b -> GenSym a
fmap :: (a -> b) -> GenSym a -> GenSym b
$cfmap :: forall a b. (a -> b) -> GenSym a -> GenSym b
Functor, Functor GenSym
a -> GenSym a
Functor GenSym
-> (forall a. a -> GenSym a)
-> (forall a b. GenSym (a -> b) -> GenSym a -> GenSym b)
-> (forall a b c.
    (a -> b -> c) -> GenSym a -> GenSym b -> GenSym c)
-> (forall a b. GenSym a -> GenSym b -> GenSym b)
-> (forall a b. GenSym a -> GenSym b -> GenSym a)
-> Applicative GenSym
GenSym a -> GenSym b -> GenSym b
GenSym a -> GenSym b -> GenSym a
GenSym (a -> b) -> GenSym a -> GenSym b
(a -> b -> c) -> GenSym a -> GenSym b -> GenSym c
forall a. a -> GenSym a
forall a b. GenSym a -> GenSym b -> GenSym a
forall a b. GenSym a -> GenSym b -> GenSym b
forall a b. GenSym (a -> b) -> GenSym a -> GenSym b
forall a b c. (a -> b -> c) -> GenSym a -> GenSym b -> GenSym c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: GenSym a -> GenSym b -> GenSym a
$c<* :: forall a b. GenSym a -> GenSym b -> GenSym a
*> :: GenSym a -> GenSym b -> GenSym b
$c*> :: forall a b. GenSym a -> GenSym b -> GenSym b
liftA2 :: (a -> b -> c) -> GenSym a -> GenSym b -> GenSym c
$cliftA2 :: forall a b c. (a -> b -> c) -> GenSym a -> GenSym b -> GenSym c
<*> :: GenSym (a -> b) -> GenSym a -> GenSym b
$c<*> :: forall a b. GenSym (a -> b) -> GenSym a -> GenSym b
pure :: a -> GenSym a
$cpure :: forall a. a -> GenSym a
$cp1Applicative :: Functor GenSym
Applicative, Applicative GenSym
a -> GenSym a
Applicative GenSym
-> (forall a b. GenSym a -> (a -> GenSym b) -> GenSym b)
-> (forall a b. GenSym a -> GenSym b -> GenSym b)
-> (forall a. a -> GenSym a)
-> Monad GenSym
GenSym a -> (a -> GenSym b) -> GenSym b
GenSym a -> GenSym b -> GenSym b
forall a. a -> GenSym a
forall a b. GenSym a -> GenSym b -> GenSym b
forall a b. GenSym a -> (a -> GenSym b) -> GenSym b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> GenSym a
$creturn :: forall a. a -> GenSym a
>> :: GenSym a -> GenSym b -> GenSym b
$c>> :: forall a b. GenSym a -> GenSym b -> GenSym b
>>= :: GenSym a -> (a -> GenSym b) -> GenSym b
$c>>= :: forall a b. GenSym a -> (a -> GenSym b) -> GenSym b
$cp1Monad :: Applicative GenSym
Monad)

runGenSym :: GenSym a -> Counter -> (a, Counter)
runGenSym :: GenSym a -> Counter -> (a, Counter)
runGenSym (GenSym State Counter a
m) = State Counter a -> Counter -> (a, Counter)
forall s a. State s a -> s -> (a, s)
runState State Counter a
m

genSym :: Typeable a => GenSym (Reference a Symbolic)
genSym :: GenSym (Reference a Symbolic)
genSym  = State Counter (Reference a Symbolic)
-> GenSym (Reference a Symbolic)
forall a. State Counter a -> GenSym a
GenSym (State Counter (Reference a Symbolic)
 -> GenSym (Reference a Symbolic))
-> State Counter (Reference a Symbolic)
-> GenSym (Reference a Symbolic)
forall a b. (a -> b) -> a -> b
$ do
  Counter Int
i <- StateT Counter Identity Counter
forall s (m :: * -> *). MonadState s m => m s
get
  Counter -> StateT Counter Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Counter
Counter (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
  Reference a Symbolic -> State Counter (Reference a Symbolic)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbolic a -> Reference a Symbolic
forall a (r :: * -> *). r a -> Reference a r
Reference (Var -> Symbolic a
forall a. Typeable a => Var -> Symbolic a
Symbolic (Int -> Var
Var Int
i)))

newtype Counter = Counter Int
  deriving stock Int -> Counter -> ShowS
[Counter] -> ShowS
Counter -> String
(Int -> Counter -> ShowS)
-> (Counter -> String) -> ([Counter] -> ShowS) -> Show Counter
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Counter] -> ShowS
$cshowList :: [Counter] -> ShowS
show :: Counter -> String
$cshow :: Counter -> String
showsPrec :: Int -> Counter -> ShowS
$cshowsPrec :: Int -> Counter -> ShowS
Show

newCounter :: Counter
newCounter :: Counter
newCounter = Int -> Counter
Counter Int
0