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

{-# LANGUAGE StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Module, providing singleton boilerplate for
-- 'T' data types.
--
-- Some functions from Data.Singletons are provided alternative version here.

module Morley.Michelson.Typed.Sing
  ( SingT (..)
  , castSingE
  , castM
  , eqP
  , requireEq
  ) where

import Data.Singletons (Demote, KindOf, SingI(..), demote)
import Data.Singletons.TH (genSingletons, singDecideInstance)
import Data.Singletons.TH.Options (Options(..), defaultOptions, withOptions)
import Data.Type.Equality ((:~:)(..))
import Language.Haskell.TH (Name, mkName, nameBase)

import Fmt ((+||), (||+))
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.Sing (SingI1(..), castSing, eqI)

-- | 'SingI' and 'Data.Singletons.TH.SDecide' instances for the 'T' kind.
$(let singPrefix, sPrefix :: Name -> Name
      singPrefix nm = mkName ("Sing" ++ nameBase nm)
      sPrefix nm = mkName ("S" ++ nameBase nm) in

  withOptions defaultOptions{singledDataConName = sPrefix, singledDataTypeName = singPrefix} $
  concat <$> sequence [genSingletons [''T], singDecideInstance ''T]
  )

---------------------------------------------
-- 'Data.Singletons.withSingI' usage
--------------------------------------------

-- | Previously, we were using 'SingI' constraints in 'SingT'
-- constructors. That was not so optimal because we have been
-- spending too much space at runtime. Instead of that, we process
-- values of 'SingT' using the function 'Data.Singletons.withSingI' in those places
-- where the 'SingI' constraint is required. 'Data.Singletons.withSingI' allows one
-- to create the 'SingI' context for a given t'Data.Singletons.Sing'.

---------------------------------------------
-- Singleton-related helpers for T
----------------------------------------------
instance SingI1 'TList where
  withSingI1 x = x

instance SingI k => SingI1 ('TMap k) where
  withSingI1 x = x

castSingE
  :: forall (a :: T) (b :: T) t. (SingI a, SingI b)
  => t a -> Either Text (t b)
castSingE = maybeToRight errMsg . castSing
  where
    errMsg = "Type mismatch: expected " +|| demote @a ||+
                               ", got " +|| demote @b ||+ ""

-- | Monadic version of 'castSing'.
-- Throws an error using the given function if the cast fails.
castM
  :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m)
  => t a
  -> (forall x. Demote (KindOf a) -> Demote (KindOf b) -> m x)
  -> m (t b)
castM a throwErr =
  requireEq @a @b throwErr <&> \Refl -> a

-- | Monadic version of 'eqI'.
-- Throws an error using the given function if the two types are not equal.
requireEq
  :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m)
  => (forall x. Demote (KindOf a) -> Demote (KindOf b) -> m x)
  -> m (a :~: b)
requireEq throwErr =
  case eqI @a @b of
    Just p -> pure p
    Nothing -> throwErr (demote @a) (demote @b)

-- | Version of 'eqI' that uses 'Proxy'
eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)
eqP _ _ = eqI @a @b