module Lorentz.EntryPoints.Helpers
  ( ctorNameToAnn
  , CanHaveEntryPoints
  , ShouldHaveEntryPoints (..)
  , RequireSumType
  ) where

import qualified Data.Kind as Kind

import Michelson.Typed.Haskell
import Michelson.Typed.T
import Michelson.Untyped (FieldAnn, ann)
import Util.Text
import Util.Type
import Util.TypeLits

ctorNameToAnn :: forall ctor. (KnownSymbol ctor, HasCallStack) => FieldAnn
ctorNameToAnn = ann . headToLower $ (symbolValT' @ctor)

-- | A special type which wraps over a primitive type and states that it has
-- entrypoints (one).
--
-- Assuming that any type can have entrypoints makes use of Lorentz entrypoints
-- too annoying, so for declaring entrypoints for not sum types we require an
-- explicit wrapper.
newtype ShouldHaveEntryPoints a = ShouldHaveEntryPoints { unHasEntryPoints :: a }
  deriving stock Generic
  deriving anyclass IsoValue

-- | Used to understand whether a type can potentially declare any entrypoints.
type family CanHaveEntryPoints (p :: Kind.Type) :: Bool where
  CanHaveEntryPoints (ShouldHaveEntryPoints _) = 'True
  CanHaveEntryPoints p = CanHaveEntryPointsT (ToT p)

type family CanHaveEntryPointsT (t :: T) :: Bool where
  CanHaveEntryPointsT ('TOr _ _) = 'True
  CanHaveEntryPointsT _ = 'False

-- | Ensure that given type is a sum type.
--
-- This helps to prevent attempts to apply a function to, for instance, a pair.
type family RequireSumType (a :: Kind.Type) :: Constraint where
  RequireSumType a =
    If (CanHaveEntryPoints a)
       (() :: Constraint)
       (TypeError ('Text "Expected Michelson sum type"))