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

import qualified Data.Kind as Kind
import qualified GHC.Generics as G

import Michelson.Typed.Haskell.Instr.Sum (IsPrimitiveValue)
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)

-- | Used to understand whether a type can potentially declare any entrypoints.
--
-- This type family is conservative, if we are not sure, we suppose that type
-- /may/ have entrypoints.
type CanHaveEntryPoints a =
  If (IsPrimitiveValue a)
     'False
     (GCanHaveEntryPoints (G.Rep a))

type family GCanHaveEntryPoints (x :: Kind.Type -> Kind.Type) :: Bool where
  GCanHaveEntryPoints (G.M1 _ _ x) = GCanHaveEntryPoints x
  GCanHaveEntryPoints (_ G.:+: _) = 'True
  GCanHaveEntryPoints G.V1 =
    TypeError ('Text "Void-like type cannot be a parameter")
  GCanHaveEntryPoints (_ G.:*: _) = 'False
  GCanHaveEntryPoints G.U1 = 'False
  GCanHaveEntryPoints (G.Rec0 _) = 'True
    --- ^ Returning True for the sake of newtypes

-- | 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 sum type"))