{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Cast
( Dyn
, toDyn
, cast
, castedType
, casting
) where
import Copilot.Core as C
import Copilot.Core.Type.Equality
import Copilot.Core.Type.Dynamic
import GHC.Float
import qualified Copilot.Theorem.TransSys.Type as K
type Dyn = Dynamic Type
castedType :: Type t -> K.U K.Type
castedType t = case t of
Bool -> K.U K.Bool
Int8 -> K.U K.Integer
Int16 -> K.U K.Integer
Int32 -> K.U K.Integer
Int64 -> K.U K.Integer
Word8 -> K.U K.Integer
Word16 -> K.U K.Integer
Word32 -> K.U K.Integer
Word64 -> K.U K.Integer
Float -> K.U K.Real
Double -> K.U K.Real
cast :: K.Type t -> Dyn -> t
cast t v
| K.Integer <- t, Just (vi :: Integer) <- _cast v = vi
| K.Bool <- t, Just (vb :: Bool) <- _cast v = vb
| K.Real <- t, Just (vr :: Double) <- _cast v = vr
| otherwise = error "Bad type cast"
casting :: Type t -> (forall t' . K.Type t' -> a) -> a
casting t f = case castedType t of
K.U K.Bool -> f K.Bool
K.U K.Integer -> f K.Integer
K.U K.Real -> f K.Real
class Casted b where
_cast :: Dyn -> Maybe b
instance Casted Integer where
_cast (Dynamic v tv)
| Just Refl <- tv =~= Int8 = Just $ toInteger v
| Just Refl <- tv =~= Int16 = Just $ toInteger v
| Just Refl <- tv =~= Int32 = Just $ toInteger v
| Just Refl <- tv =~= Int64 = Just $ toInteger v
| Just Refl <- tv =~= Word16 = Just $ toInteger v
| Just Refl <- tv =~= Word8 = Just $ toInteger v
| Just Refl <- tv =~= Word32 = Just $ toInteger v
| Just Refl <- tv =~= Word64 = Just $ toInteger v
| otherwise = Nothing
instance Casted Bool where
_cast (Dynamic v tv)
| Just Refl <- tv =~= Bool = Just v
| otherwise = Nothing
instance Casted Double where
_cast (Dynamic v tv)
| Just Refl <- tv =~= Float = Just $ float2Double v
| Just Refl <- tv =~= Double = Just v
| otherwise = Nothing