{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Types.Environment
-- Copyright   :  (C) 2017, Jacob Stanley
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module contains environments that are used to translate between
-- symbolic and concrete references. It's taken from the Hedgehog
-- <https://hackage.haskell.org/package/hedgehog library>.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Types.Environment
  ( Environment(..)
  , EnvironmentError(..)
  , emptyEnvironment
  , insertConcrete
  , insertConcretes
  , reifyDynamic
  , reifyEnvironment
  , reify
  ) where

import           Data.Dynamic
                   (Dynamic, Typeable, dynTypeRep, fromDynamic)
import           Data.Map
                   (Map)
import qualified Data.Map                           as M
import           Data.Semigroup
import           Data.Typeable
                   (Proxy(Proxy), TypeRep, typeRep)
import           Prelude

import qualified Test.StateMachine.Types.Rank2      as Rank2
import           Test.StateMachine.Types.References

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

-- | A mapping of symbolic values to concrete values.
newtype Environment = Environment
  { Environment -> Map Var Dynamic
unEnvironment :: Map Var Dynamic
  }
  deriving stock   (Int -> Environment -> ShowS
[Environment] -> ShowS
Environment -> String
(Int -> Environment -> ShowS)
-> (Environment -> String)
-> ([Environment] -> ShowS)
-> Show Environment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Environment -> ShowS
showsPrec :: Int -> Environment -> ShowS
$cshow :: Environment -> String
show :: Environment -> String
$cshowList :: [Environment] -> ShowS
showList :: [Environment] -> ShowS
Show)
  deriving newtype (NonEmpty Environment -> Environment
Environment -> Environment -> Environment
(Environment -> Environment -> Environment)
-> (NonEmpty Environment -> Environment)
-> (forall b. Integral b => b -> Environment -> Environment)
-> Semigroup Environment
forall b. Integral b => b -> Environment -> Environment
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: Environment -> Environment -> Environment
<> :: Environment -> Environment -> Environment
$csconcat :: NonEmpty Environment -> Environment
sconcat :: NonEmpty Environment -> Environment
$cstimes :: forall b. Integral b => b -> Environment -> Environment
stimes :: forall b. Integral b => b -> Environment -> Environment
Semigroup, Semigroup Environment
Environment
Semigroup Environment =>
Environment
-> (Environment -> Environment -> Environment)
-> ([Environment] -> Environment)
-> Monoid Environment
[Environment] -> Environment
Environment -> Environment -> Environment
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: Environment
mempty :: Environment
$cmappend :: Environment -> Environment -> Environment
mappend :: Environment -> Environment -> Environment
$cmconcat :: [Environment] -> Environment
mconcat :: [Environment] -> Environment
Monoid)

-- | Environment errors.
data EnvironmentError
  = EnvironmentValueNotFound !Var
  | EnvironmentTypeError !TypeRep !TypeRep
  deriving stock (EnvironmentError -> EnvironmentError -> Bool
(EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> Eq EnvironmentError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EnvironmentError -> EnvironmentError -> Bool
== :: EnvironmentError -> EnvironmentError -> Bool
$c/= :: EnvironmentError -> EnvironmentError -> Bool
/= :: EnvironmentError -> EnvironmentError -> Bool
Eq, Eq EnvironmentError
Eq EnvironmentError =>
(EnvironmentError -> EnvironmentError -> Ordering)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> EnvironmentError)
-> (EnvironmentError -> EnvironmentError -> EnvironmentError)
-> Ord EnvironmentError
EnvironmentError -> EnvironmentError -> Bool
EnvironmentError -> EnvironmentError -> Ordering
EnvironmentError -> EnvironmentError -> EnvironmentError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: EnvironmentError -> EnvironmentError -> Ordering
compare :: EnvironmentError -> EnvironmentError -> Ordering
$c< :: EnvironmentError -> EnvironmentError -> Bool
< :: EnvironmentError -> EnvironmentError -> Bool
$c<= :: EnvironmentError -> EnvironmentError -> Bool
<= :: EnvironmentError -> EnvironmentError -> Bool
$c> :: EnvironmentError -> EnvironmentError -> Bool
> :: EnvironmentError -> EnvironmentError -> Bool
$c>= :: EnvironmentError -> EnvironmentError -> Bool
>= :: EnvironmentError -> EnvironmentError -> Bool
$cmax :: EnvironmentError -> EnvironmentError -> EnvironmentError
max :: EnvironmentError -> EnvironmentError -> EnvironmentError
$cmin :: EnvironmentError -> EnvironmentError -> EnvironmentError
min :: EnvironmentError -> EnvironmentError -> EnvironmentError
Ord, Int -> EnvironmentError -> ShowS
[EnvironmentError] -> ShowS
EnvironmentError -> String
(Int -> EnvironmentError -> ShowS)
-> (EnvironmentError -> String)
-> ([EnvironmentError] -> ShowS)
-> Show EnvironmentError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EnvironmentError -> ShowS
showsPrec :: Int -> EnvironmentError -> ShowS
$cshow :: EnvironmentError -> String
show :: EnvironmentError -> String
$cshowList :: [EnvironmentError] -> ShowS
showList :: [EnvironmentError] -> ShowS
Show)

-- | Create an empty environment.
emptyEnvironment :: Environment
emptyEnvironment :: Environment
emptyEnvironment = Map Var Dynamic -> Environment
Environment Map Var Dynamic
forall k a. Map k a
M.empty

-- | Insert a symbolic / concrete pairing in to the environment.
insertConcrete :: Var -> Dynamic -> Environment -> Environment
insertConcrete :: Var -> Dynamic -> Environment -> Environment
insertConcrete Var
var Dynamic
dyn = Map Var Dynamic -> Environment
Environment (Map Var Dynamic -> Environment)
-> (Environment -> Map Var Dynamic) -> Environment -> Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Dynamic -> Map Var Dynamic -> Map Var Dynamic
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
var Dynamic
dyn (Map Var Dynamic -> Map Var Dynamic)
-> (Environment -> Map Var Dynamic)
-> Environment
-> Map Var Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment -> Map Var Dynamic
unEnvironment

insertConcretes :: [Var] -> [Dynamic] -> Environment -> Environment
insertConcretes :: [Var] -> [Dynamic] -> Environment -> Environment
insertConcretes []           []           Environment
env = Environment
env
insertConcretes (Var
var : [Var]
vars) (Dynamic
dyn : [Dynamic]
dyns) Environment
env =
  [Var] -> [Dynamic] -> Environment -> Environment
insertConcretes [Var]
vars [Dynamic]
dyns (Var -> Dynamic -> Environment -> Environment
insertConcrete Var
var Dynamic
dyn Environment
env)
insertConcretes [Var]
_            [Dynamic]
_            Environment
_   =
  String -> Environment
forall a. HasCallStack => String -> a
error String
"insertConcrets: impossible."

-- | Cast a 'Dynamic' in to a concrete value.
reifyDynamic :: forall a. Typeable a => Dynamic
             -> Either EnvironmentError (Concrete a)
reifyDynamic :: forall a.
Typeable a =>
Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn =
  case Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn of
    Maybe a
Nothing ->
      EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. a -> Either a b
Left (TypeRep -> TypeRep -> EnvironmentError
EnvironmentTypeError (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a)) (Dynamic -> TypeRep
dynTypeRep Dynamic
dyn))
    Just a
x ->
      Concrete a -> Either EnvironmentError (Concrete a)
forall a b. b -> Either a b
Right (a -> Concrete a
forall a. Typeable a => a -> Concrete a
Concrete a
x)

-- | Turns an environment in to a function for looking up a concrete value from
--   a symbolic one.
reifyEnvironment :: Environment
                 -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))
reifyEnvironment :: Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment (Environment Map Var Dynamic
vars) (Symbolic Var
n) =
  case Var -> Map Var Dynamic -> Maybe Dynamic
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
n Map Var Dynamic
vars of
    Maybe Dynamic
Nothing ->
      EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. a -> Either a b
Left (Var -> EnvironmentError
EnvironmentValueNotFound Var
n)
    Just Dynamic
dyn ->
      Dynamic -> Either EnvironmentError (Concrete a)
forall a.
Typeable a =>
Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn

-- | Convert a symbolic structure to a concrete one, using the provided
--   environment.
reify :: Rank2.Traversable t
      => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify :: forall (t :: (* -> *) -> *).
Traversable t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
vars = (forall a. Symbolic a -> Either EnvironmentError (Concrete a))
-> t Symbolic -> Either EnvironmentError (t Concrete)
forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
       (q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> t p -> f (t q)
Rank2.traverse (Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
vars)