{-# 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Environment] -> ShowS
$cshowList :: [Environment] -> ShowS
show :: Environment -> String
$cshow :: Environment -> String
showsPrec :: Int -> Environment -> ShowS
$cshowsPrec :: Int -> Environment -> ShowS
Show)
  deriving newtype (NonEmpty Environment -> Environment
Environment -> Environment -> 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
stimes :: forall b. Integral b => b -> Environment -> Environment
$cstimes :: forall b. Integral b => b -> Environment -> Environment
sconcat :: NonEmpty Environment -> Environment
$csconcat :: NonEmpty Environment -> Environment
<> :: Environment -> Environment -> Environment
$c<> :: Environment -> Environment -> Environment
Semigroup, Semigroup Environment
Environment
[Environment] -> Environment
Environment -> Environment -> Environment
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Environment] -> Environment
$cmconcat :: [Environment] -> Environment
mappend :: Environment -> Environment -> Environment
$cmappend :: Environment -> Environment -> Environment
mempty :: Environment
$cmempty :: Environment
Monoid)

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

-- | Create an empty environment.
emptyEnvironment :: Environment
emptyEnvironment :: Environment
emptyEnvironment = Map Var Dynamic -> Environment
Environment 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
var Dynamic
dyn 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
_   =
  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 forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn of
    Maybe a
Nothing ->
      forall a b. a -> Either a b
Left (TypeRep -> TypeRep -> EnvironmentError
EnvironmentTypeError (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a)) (Dynamic -> TypeRep
dynTypeRep Dynamic
dyn))
    Just a
x ->
      forall a b. b -> Either a b
Right (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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
n Map Var Dynamic
vars of
    Maybe Dynamic
Nothing ->
      forall a b. a -> Either a b
Left (Var -> EnvironmentError
EnvironmentValueNotFound Var
n)
    Just Dynamic
dyn ->
      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 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)
Rank2.traverse (Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
vars)