    {-# LANGUAGE GADTs               #-}
    {-# LANGUAGE RankNTypes          #-}
    {-# LANGUAGE Safe                #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    -- | Casting of values with dynamic types and translating from Copilot core
    -- types to Copilot theorem types.

    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

    -- | Synonym for a dynamic type in Copilot core.
    type Dyn = Dynamic

    -- | Translation of a Copilot type into Copilot theorem's internal
    -- representation.
    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 a dynamic value to a given type.
    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"

    -- | Apply function to a corresponding type in Copilot theorem's internal
    -- representation.
    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