{-# 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
  { unEnvironment :: Map Var Dynamic
  }
  deriving stock   (Show)
  deriving newtype (Semigroup, Monoid)

-- | Environment errors.
data EnvironmentError
  = EnvironmentValueNotFound !Var
  | EnvironmentTypeError !TypeRep !TypeRep
  deriving stock (Eq, Ord, Show)

-- | Create an empty environment.
emptyEnvironment :: Environment
emptyEnvironment = Environment M.empty

-- | Insert a symbolic / concrete pairing in to the environment.
insertConcrete :: Var -> Dynamic -> Environment -> Environment
insertConcrete var dyn = Environment . M.insert var dyn . unEnvironment

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

-- | Cast a 'Dynamic' in to a concrete value.
reifyDynamic :: forall a. Typeable a => Dynamic
             -> Either EnvironmentError (Concrete a)
reifyDynamic dyn =
  case fromDynamic dyn of
    Nothing ->
      Left (EnvironmentTypeError (typeRep (Proxy :: Proxy a)) (dynTypeRep dyn))
    Just x ->
      Right (Concrete 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 vars) (Symbolic n) =
  case M.lookup n vars of
    Nothing ->
      Left (EnvironmentValueNotFound n)
    Just dyn ->
      reifyDynamic 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 vars = Rank2.traverse (reifyEnvironment vars)