--------------------------------------------------------------------------------

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

-- | 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 Copilot.Core.Type.Equality
import Copilot.Core.Type.Dynamic

import GHC.Float

import qualified Copilot.Theorem.TransSys.Type as K

--------------------------------------------------------------------------------

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

-- | 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 (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

--------------------------------------------------------------------------------