-- 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.
-- 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 (..)
  , castSingE
  , castM
  , eqP
  , requireEq
  ) where

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

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

-- | 'SingI' and '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]
  )

---------------------------------------------
-- '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 'withSingI' in those places
-- where the 'SingI' constraint is required. 'withSingI' allows one
-- to create the 'SingI' context for a given 'Sing'.

---------------------------------------------
-- Singleton-related helpers for T
----------------------------------------------
instance SingI1 'TList where
  withSingI1 :: (SingI ('TList x) => r) -> r
withSingI1 SingI ('TList x) => r
x = r
SingI ('TList x) => r
x

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

castSingE
  :: forall (a :: T) (b :: T) t. (SingI a, SingI b)
  => t a -> Either Text (t b)
castSingE :: 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
+|| (SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a T -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+
                               Builder
", got " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|| (SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b T -> Builder -> Builder
forall a b. (Show 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. Demote (KindOf a) -> Demote (KindOf b) -> m x)
  -> m (t b)
castM :: t a -> (forall x. Demote T -> Demote T -> m x) -> m (t b)
castM t a
a forall x. Demote T -> Demote T -> m x
throwErr =
  (forall x. Demote T -> Demote T -> m x) -> m (a :~: b)
forall (a :: T) (b :: T) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
(forall x. Demote T -> Demote T -> m x) -> m (a :~: b)
requireEq @a @b forall x. Demote T -> Demote 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. Demote (KindOf a) -> Demote (KindOf b) -> m x)
  -> m (a :~: b)
requireEq :: (forall x. Demote T -> Demote T -> m x) -> m (a :~: b)
requireEq forall x. Demote T -> Demote T -> m x
throwErr =
  case (SingI a, SingI b, TestEquality Sing) => Maybe (a :~: b)
forall k (a :: k) (b :: k).
(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 -> Demote T -> Demote T -> m (a :~: b)
forall x. Demote T -> Demote T -> m x
throwErr ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
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 :: Proxy a -> Proxy b -> Maybe (a :~: b)
eqP Proxy a
_ Proxy b
_ = (SingI a, SingI b, TestEquality Sing) => Maybe (a :~: b)
forall k (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @a @b