{-# 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 t = case t of
  Bool    -> K.U K.Bool
  Int8    -> K.U K.Integer
  Int16   -> K.U K.Integer
  Int32   -> K.U K.Integer
  Int64   -> K.U K.Integer
  Word8   -> K.U K.Integer
  Word16  -> K.U K.Integer
  Word32  -> K.U K.Integer
  Word64  -> K.U K.Integer
  Float   -> K.U K.Real
  Double  -> K.U K.Real

-- | Cast a dynamic value to a given type.
cast :: K.Type t -> Dyn -> t
cast t v
  | K.Integer <- t,  Just (vi :: Integer) <- _cast v = vi
  | K.Bool    <- t,  Just (vb :: Bool)    <- _cast v = vb
  | K.Real    <- t,  Just (vr :: Double)  <- _cast v = vr
  | otherwise = error "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 t f = case castedType t of
  K.U K.Bool    -> f K.Bool
  K.U K.Integer -> f K.Integer
  K.U K.Real    -> f K.Real

class Casted b where
  _cast :: Dyn -> Maybe b

instance Casted Integer where
  _cast d
    | Just (v :: Int8)   <- fromDynamic d = Just $ toInteger v
    | Just (v :: Int16)  <- fromDynamic d = Just $ toInteger v
    | Just (v :: Int32)  <- fromDynamic d = Just $ toInteger v
    | Just (v :: Int64)  <- fromDynamic d = Just $ toInteger v
    | Just (v :: Word8)  <- fromDynamic d = Just $ toInteger v
    | Just (v :: Word16) <- fromDynamic d = Just $ toInteger v
    | Just (v :: Word32) <- fromDynamic d = Just $ toInteger v
    | Just (v :: Word64) <- fromDynamic d = Just $ toInteger v
    | otherwise                           = Nothing

instance Casted Bool where
  _cast d
    | Just (v :: Bool) <- fromDynamic d = Just v
    | otherwise                         = Nothing

instance Casted Double where
  _cast d
    | Just (v :: Float)  <- fromDynamic d = Just $ float2Double v
    | Just (v :: Double) <- fromDynamic d = Just v
    | otherwise                           = Nothing