-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

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

-- | Module, providing singleton boilerplate for
-- 'T' 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
  ( SingT (..)
  , KnownT
  , withSomeSingT
  , fromSingT
  ) where

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

import Michelson.Typed.T (T(..))


-- | Instance of data family 'Sing' for 'T'.
-- Custom instance is implemented in order to inject 'Typeable'
-- constraint for some of constructors.
data SingT :: T -> Type where
  STKey :: SingT  'TKey
  STUnit :: SingT  'TUnit
  STSignature :: SingT  'TSignature
  STChainId :: SingT  'TChainId
  STOption :: KnownT a => Sing a -> SingT ( 'TOption a)
  STList :: KnownT a => Sing a -> SingT ( 'TList a )
  STSet :: KnownT a => Sing a -> SingT ( 'TSet a )
  STOperation  :: SingT 'TOperation
  STContract   :: (KnownT a)
               => Sing a -> SingT ( 'TContract a )
  STPair       :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TPair a b)
  STOr         :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TOr a b)
  STLambda     :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TLambda a b)
  STMap        :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TMap a b)
  STBigMap     :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TBigMap a b)
  STInt :: SingT  'TInt
  STNat :: SingT  'TNat
  STString :: SingT  'TString
  STBytes :: SingT  'TBytes
  STMutez :: SingT  'TMutez
  STBool :: SingT  'TBool
  STKeyHash :: SingT  'TKeyHash
  STTimestamp :: SingT  'TTimestamp
  STAddress :: SingT  'TAddress

type instance Sing = SingT

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

-- | 'Typeable' + 'SingI' constraints.
--
-- This restricts a type to be a constructible type of 'T' kind.
class (Typeable t, SingI t) => KnownT (t :: T)
instance (Typeable t, SingI t) => KnownT t

-- | Version of 'SomeSing' with 'Typeable' constraint,
-- specialized for use with 'T' kind.
data SomeSingT where
  SomeSingT :: forall (a :: T). (KnownT 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). (KnownT 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
  STKey -> TKey
  STUnit -> TUnit
  STSignature -> TSignature
  STChainId -> TChainId
  STOption t -> TOption (fromSingT t)
  STList t -> TList (fromSingT t)
  STSet t -> TSet (fromSingT 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 (fromSingT a) (fromSingT b)
  STBigMap a b -> TBigMap (fromSingT a) (fromSingT b)
  STInt -> TInt
  STNat -> TNat
  STString -> TString
  STBytes -> TBytes
  STMutez -> TMutez
  STBool -> TBool
  STKeyHash -> TKeyHash
  STTimestamp -> TTimestamp
  STAddress -> TAddress

-- | Version of 'toSing' which creates 'SomeSingT'.
toSingT :: T -> SomeSingT
toSingT = \case
  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 -> withSomeSingT 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 ->
    withSomeSingT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STMap lSing rSing
  TBigMap l r ->
    withSomeSingT l $ \lSing ->
    withSomeSingT r $ \rSing ->
      SomeSingT $ STBigMap lSing rSing
  TInt -> SomeSingT STInt
  TNat -> SomeSingT STNat
  TString -> SomeSingT STString
  TBytes -> SomeSingT STBytes
  TMutez -> SomeSingT STMutez
  TBool -> SomeSingT STBool
  TKeyHash -> SomeSingT STKeyHash
  TTimestamp -> SomeSingT STTimestamp
  TAddress -> SomeSingT STAddress

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

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 (KnownT a) => SingI ( 'TOption (a :: T)) where
  sing = STOption sing
instance (KnownT a) => SingI ( 'TList (a :: T)) where
  sing = STList sing
instance (KnownT a) => SingI ( 'TSet (a :: T)) where
  sing = STSet sing
instance SingI 'TOperation where
  sing = STOperation
instance (KnownT a) =>
          SingI ( 'TContract (a :: T)) where
  sing = STContract sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TPair a b) where
  sing = STPair sing sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TOr a b) where
  sing = STOr sing sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TLambda a b) where
  sing = STLambda sing sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TMap a b) where
  sing = STMap sing sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TBigMap a b) where
  sing = STBigMap sing sing
instance SingI  'TInt where
  sing = STInt
instance SingI  'TNat where
  sing = STNat
instance SingI  'TString where
  sing = STString
instance SingI  'TBytes where
  sing = STBytes
instance SingI  'TMutez where
  sing = STMutez
instance SingI  'TBool where
  sing = STBool
instance SingI  'TKeyHash where
  sing = STKeyHash
instance SingI  'TTimestamp where
  sing = STTimestamp
instance SingI  'TAddress where
  sing = STAddress