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