{-# 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 :: 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 :: 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 :: 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 (Dynamic a1
v Type a1
tv)
| Just Equal a1 Int8
Refl <- Type a1
tv Type a1 -> Type Int8 -> Maybe (Equal a1 Int8)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Int8
Int8 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Int16
Refl <- Type a1
tv Type a1 -> Type Int16 -> Maybe (Equal a1 Int16)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Int16
Int16 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Int32
Refl <- Type a1
tv Type a1 -> Type Int32 -> Maybe (Equal a1 Int32)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Int32
Int32 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Int64
Refl <- Type a1
tv Type a1 -> Type Int64 -> Maybe (Equal a1 Int64)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Int64
Int64 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Word16
Refl <- Type a1
tv Type a1 -> Type Word16 -> Maybe (Equal a1 Word16)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Word16
Word16 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Word8
Refl <- Type a1
tv Type a1 -> Type Word8 -> Maybe (Equal a1 Word8)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Word8
Word8 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Word32
Refl <- Type a1
tv Type a1 -> Type Word32 -> Maybe (Equal a1 Word32)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Word32
Word32 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Just Equal a1 Word64
Refl <- Type a1
tv Type a1 -> Type Word64 -> Maybe (Equal a1 Word64)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Word64
Word64 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Integral a => a -> Integer
toInteger a1
v
| Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
instance Casted Bool where
_cast :: Dyn -> Maybe Bool
_cast (Dynamic a1
v Type a1
tv)
| Just Equal a1 Bool
Refl <- Type a1
tv Type a1 -> Type Bool -> Maybe (Equal a1 Bool)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Bool
Bool = a1 -> Maybe a1
forall a. a -> Maybe a
Just a1
v
| Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
instance Casted Double where
_cast :: Dyn -> Maybe Double
_cast (Dynamic a1
v Type a1
tv)
| Just Equal a1 Float
Refl <- Type a1
tv Type a1 -> Type Float -> Maybe (Equal a1 Float)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Float
Float = 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 a1
Float
v
| Just Equal a1 Double
Refl <- Type a1
tv Type a1 -> Type Double -> Maybe (Equal a1 Double)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= Type Double
Double = a1 -> Maybe a1
forall a. a -> Maybe a
Just a1
v
| Bool
otherwise = Maybe Double
forall a. Maybe a
Nothing