{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Module, providing singleton boilerplate for
-- 'T' and 'CT' data types.
--
-- Some functions from Data.Singletons are provided alternative version here.
-- Some instances which are usually generated with TH are manually implemented
-- as they require some specific constraints, namely 'Typeable' and/or
-- 'Converge', not provided in instances generated by TH.

module Michelson.Typed.Sing
  ( Sing (..)
  , withSomeSingT
  , withSomeSingCT
  , fromSingT
  , fromSingCT
  ) where

import Data.Kind (Type)
import Data.Singletons (Sing(..), SingI(..), SingKind(..), SomeSing(..))

import Michelson.Typed.T (CT(..), T(..))

-- | Instance of data family 'Sing' for 'CT'.
data instance Sing :: CT -> Type where
  SCInt :: Sing  'CInt
  SCNat :: Sing  'CNat
  SCString :: Sing  'CString
  SCBytes :: Sing  'CBytes
  SCMutez :: Sing  'CMutez
  SCBool :: Sing  'CBool
  SCKeyHash :: Sing  'CKeyHash
  SCTimestamp :: Sing  'CTimestamp
  SCAddress :: Sing  'CAddress

-- | Instance of data family 'Sing' for 'T'.
-- Custom instance is implemented in order to inject 'Typeable'
-- constraint for some of constructors.
data instance Sing :: T -> Type where
  STc :: (SingI a, Typeable a) => Sing a -> Sing ( 'Tc a)
  STKey :: Sing  'TKey
  STUnit :: Sing  'TUnit
  STSignature :: Sing  'TSignature
  STChainId :: Sing  'TChainId
  STOption :: (SingI a, Typeable a) => Sing a -> Sing ( 'TOption a)
  STList :: (SingI a, Typeable a) => Sing a -> Sing ( 'TList a )
  STSet :: (SingI a, Typeable a) => Sing a -> Sing ( 'TSet a )
  STOperation  :: Sing 'TOperation
  STContract   :: (SingI a, Typeable a)
                => Sing a -> Sing ( 'TContract a )
  STPair       :: (SingI a, SingI b, Typeable a, Typeable b)
                => Sing a -> Sing b -> Sing ('TPair a b)
  STOr         :: (SingI a, SingI b, Typeable a, Typeable b)
                => Sing a -> Sing b -> Sing ('TOr a b)
  STLambda     :: (SingI a, SingI b, Typeable a, Typeable b)
                => Sing a -> Sing b -> Sing ('TLambda a b)
  STMap        :: (SingI a, SingI b, Typeable a, Typeable b)
                => Sing a -> Sing b -> Sing ('TMap a b)
  STBigMap    :: (SingI a, SingI b, Typeable a, Typeable b)
                => Sing a -> Sing b -> Sing ('TBigMap a b)

---------------------------------------------
-- Singleton-related instances for CT
---------------------------------------------

-- | Version of 'SomeSing' with 'Typeable' constraint,
-- specialized for use with 'CT' kind.
data SomeSingCT where
  SomeSingCT :: forall (a :: CT). (SingI a, Typeable a) => Sing a -> SomeSingCT

-- | Version of 'withSomeSing' with 'Typeable' constraint
-- provided to processing function.
--
-- Required for not to erase this useful constraint when doing
-- conversion from value of type 'CT' to its singleton representation.
withSomeSingCT
  :: CT -> (forall (a :: CT). (SingI a, Typeable a) => Sing a -> r) -> r
withSomeSingCT ct f = (\(SomeSingCT s) -> f s) (toSingCT ct)

fromSingCT :: Sing (a :: CT) -> CT
fromSingCT = \case
  SCInt -> CInt
  SCNat -> CNat
  SCString -> CString
  SCBytes -> CBytes
  SCMutez -> CMutez
  SCBool -> CBool
  SCKeyHash -> CKeyHash
  SCTimestamp -> CTimestamp
  SCAddress -> CAddress

-- | Version of 'toSing' which creates 'SomeSingCT'.
toSingCT :: CT -> SomeSingCT
toSingCT = \case
  CInt -> SomeSingCT SCInt
  CNat -> SomeSingCT SCNat
  CString -> SomeSingCT SCString
  CBytes -> SomeSingCT SCBytes
  CMutez -> SomeSingCT SCMutez
  CBool -> SomeSingCT SCBool
  CKeyHash -> SomeSingCT SCKeyHash
  CTimestamp -> SomeSingCT SCTimestamp
  CAddress -> SomeSingCT SCAddress

instance SingKind CT where
  type Demote CT = CT
  fromSing  = fromSingCT
  toSing t = case toSingCT t of SomeSingCT s -> SomeSing s

instance SingI  'CInt where
  sing = SCInt
instance SingI  'CNat where
  sing = SCNat
instance SingI  'CString where
  sing = SCString
instance SingI  'CBytes where
  sing = SCBytes
instance SingI  'CMutez where
  sing = SCMutez
instance SingI  'CBool where
  sing = SCBool
instance SingI  'CKeyHash where
  sing = SCKeyHash
instance SingI  'CTimestamp where
  sing = SCTimestamp
instance SingI  'CAddress where
  sing = SCAddress

---------------------------------------------
-- Singleton-related helpers for T
--------------------------------------------

-- | Version of 'SomeSing' with 'Typeable' constraint,
-- specialized for use with 'T' kind.
data SomeSingT where
  SomeSingT :: forall (a :: T). (Typeable a, SingI a)
            => Sing a -> SomeSingT

-- | Version of 'withSomeSing' with 'Typeable' constraint
-- provided to processing function.
--
-- Required for not to erase these useful constraints when doing
-- conversion from value of type 'T' to its singleton representation.
withSomeSingT
  :: T
  -> (forall (a :: T). (Typeable a, SingI a) => Sing a -> r)
  -> r
withSomeSingT t f = (\(SomeSingT s) -> f s) (toSingT t)

-- | Version of 'fromSing' specialized for use with
-- @data instance Sing :: T -> Type@ which requires 'Typeable'
-- constraint for some of its constructors
fromSingT :: Sing (a :: T) -> T
fromSingT = \case
  STc t -> Tc (fromSingCT t)
  STKey -> TKey
  STUnit -> TUnit
  STSignature -> TSignature
  STChainId -> TChainId
  STOption t -> TOption (fromSingT t)
  STList t -> TList (fromSingT t)
  STSet t -> TSet (fromSingCT t)
  STOperation -> TOperation
  STContract t -> TContract (fromSingT t)
  STPair a b -> TPair (fromSingT a) (fromSingT b)
  STOr a b -> TOr (fromSingT a) (fromSingT b)
  STLambda a b -> TLambda (fromSingT a) (fromSingT b)
  STMap a b -> TMap (fromSingCT a) (fromSingT b)
  STBigMap a b -> TBigMap (fromSingCT a) (fromSingT b)

-- | Version of 'toSing' which creates 'SomeSingT'.
toSingT :: T -> SomeSingT
toSingT = \case
  Tc ct -> withSomeSingCT ct $ \ctSing -> SomeSingT $ STc ctSing
  TKey -> SomeSingT STKey
  TUnit -> SomeSingT STUnit
  TSignature -> SomeSingT STSignature
  TChainId -> SomeSingT STChainId
  TOption t -> withSomeSingT t $ \tSing -> SomeSingT $ STOption tSing
  TList t -> withSomeSingT t $ \tSing -> SomeSingT $ STList tSing
  TSet ct -> withSomeSingCT ct $ \ctSing -> SomeSingT $ STSet ctSing
  TOperation -> SomeSingT STOperation
  TContract t -> withSomeSingT t $ \tSing -> SomeSingT $ STContract tSing
  TPair l r ->
    withSomeSingT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STPair lSing rSing
  TOr l r ->
    withSomeSingT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STOr lSing rSing
  TLambda l r ->
    withSomeSingT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STLambda lSing rSing
  TMap l r ->
    withSomeSingCT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STMap lSing rSing
  TBigMap l r ->
    withSomeSingCT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STBigMap lSing rSing

instance SingKind T where
  type Demote T = T
  fromSing  = fromSingT
  toSing t = case toSingT t of SomeSingT s -> SomeSing s

instance (SingI t, Typeable t) => SingI ( 'Tc (t :: CT)) where
  sing = STc sing
instance SingI  'TKey where
  sing = STKey
instance SingI  'TUnit where
  sing = STUnit
instance SingI  'TSignature where
  sing = STSignature
instance SingI  'TChainId where
  sing = STChainId
instance (SingI a, Typeable a) => SingI ( 'TOption (a :: T)) where
  sing = STOption sing
instance (SingI a, Typeable a) => SingI ( 'TList (a :: T)) where
  sing = STList sing
instance (SingI a, Typeable a) => SingI ( 'TSet (a :: CT)) where
  sing = STSet sing
instance SingI 'TOperation where
  sing = STOperation
instance (SingI a, Typeable a) =>
          SingI ( 'TContract (a :: T)) where
  sing = STContract sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
          SingI ( 'TPair a b) where
  sing = STPair sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
          SingI ( 'TOr a b) where
  sing = STOr sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
          SingI ( 'TLambda a b) where
  sing = STLambda sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
          SingI ( 'TMap a b) where
  sing = STMap sing sing
instance (SingI a, Typeable a, Typeable b, SingI b) =>
          SingI ( 'TBigMap a b) where
  sing = STBigMap sing sing