{-# 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 :: 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 :: 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 :: 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