-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# 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 (SingI(..), demote, fromSing)
import Data.Type.Equality ((:~:)(..))
import Fmt (Buildable(..), fmt, nameF)

import Morley.Michelson.Typed.T (T(..))
import Morley.Util.MismatchError
import Morley.Util.Sing (castSing, eqI, genSingletonsType)
import Morley.Util.TH (deriveGADTNFData)

-- | 'SingI' and 'Data.Singletons.TH.SDecide' instances for the 'T' kind.
$(genSingletonsType ''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
----------------------------------------------
castSingE
  :: forall (a :: T) (b :: T) t. (SingI a, SingI b)
  => t a -> Either Text (t b)
castSingE = maybeToRight errMsg . castSing
  where
    errMsg = fmt
      $ nameF "Type mismatch"
      $ build MkMismatchError{ meExpected = demote @a, meActual = 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. MismatchError T -> 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. MismatchError T -> m x)
  -> m (a :~: b)
requireEq throwErr =
  case eqI @a @b of
    Just p -> pure p
    Nothing -> throwErr MkMismatchError
      { meActual = demote @a
      , meExpected = 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

deriving stock instance Show (SingT x)
deriving stock instance Eq (SingT x)

deriveGADTNFData ''SingT

instance Buildable (SingT t) where
  build = build . fromSing