-- 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 ((+|), (|+))

import Morley.Michelson.Printer.Util (RenderDoc(..))
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 :: forall (a :: T) (b :: T) (t :: T -> *).
(SingI a, SingI b) =>
t a -> Either Text (t b)
castSingE = Text -> Maybe (t b) -> Either Text (t b)
forall l r. l -> Maybe r -> Either l r
maybeToRight Text
errMsg (Maybe (t b) -> Either Text (t b))
-> (t a -> Maybe (t b)) -> t a -> Either Text (t b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Maybe (t b)
forall {k} (a :: k) (b :: k) (t :: k -> *).
(SingI a, SingI b, SDecide k) =>
t a -> Maybe (t b)
castSing
  where
    errMsg :: Text
errMsg = Builder
"Type mismatch: expected '" Builder -> Builder -> Text
forall b. FromBuilder b => Builder -> Builder -> b
+| forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+
                          Builder
"', but got '" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
"'"

-- | 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 :: forall (a :: T) (b :: T) (t :: T -> *) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
t a -> (forall x. MismatchError T -> m x) -> m (t b)
castM t a
a forall x. MismatchError T -> m x
throwErr =
  forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. MismatchError T -> m x) -> m (a :~: b)
requireEq @a @b forall x. MismatchError T -> m x
throwErr m (a :~: b) -> ((a :~: b) -> t b) -> m (t b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \a :~: b
Refl -> t a
t b
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 :: forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. MismatchError T -> m x) -> m (a :~: b)
requireEq forall x. MismatchError T -> m x
throwErr =
  case forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @a @b of
    Just a :~: b
p -> (a :~: b) -> m (a :~: b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a :~: b
p
    Maybe (a :~: b)
Nothing -> MismatchError T -> m (a :~: b)
forall x. MismatchError T -> m x
throwErr MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError
      { meActual :: T
meActual = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a
      , meExpected :: T
meExpected = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
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 :: forall (a :: T) (b :: T).
(SingI a, SingI b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
eqP Proxy a
_ Proxy b
_ = forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @a @b

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

deriveGADTNFData ''SingT

instance RenderDoc (SingT t) where
  renderDoc :: RenderContext -> SingT t -> Doc
renderDoc RenderContext
pn SingT t
s = RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn (T -> Doc) -> T -> Doc
forall a b. (a -> b) -> a -> b
$ Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
SingT t
s