CEnum.hs

-- | C enumerations
--
-- This module is intended to be imported qualified.
--
-- > import HsBindgen.Runtime.Prelude
-- > import HsBindgen.Runtime.CEnum qualified as CEnum
module HsBindgen.Runtime.CEnum (
  -- * Type classes
  CEnum (..),
  SequentialCEnum (..),

  -- * Deriving via support
  AsCEnum (..),
  AsSequentialCEnum (..),

  -- * API
  getNames,

  -- * Instance support
  DeclaredValues,
  declaredValuesFromList,
  show,
  shows,
  showsWrappedUndeclared,
  readEither,
  readPrec,
  readPrecWrappedUndeclared,
  seqIsDeclared,
  seqMkDeclared,

  -- ** Exceptions
  CEnumException (..),
) where

import Control.Exception (Exception (displayException), throw)
import Data.Bifunctor (Bifunctor (first))
import Data.Coerce (Coercible, coerce)
import Data.List qualified as List
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Proxy (Proxy (Proxy))
import GHC.Show (appPrec, appPrec1, showSpace)
import Text.ParserCombinators.ReadP qualified as ReadP
import Text.ParserCombinators.ReadPrec qualified as ReadPrec
import Text.Read (ReadPrec, minPrec, (+++))
import Text.Read qualified as Read
import Text.Read.Lex (Lexeme (..), expect)
import Prelude hiding (show, shows)
import Prelude qualified

{-------------------------------------------------------------------------------
  Type classes
-------------------------------------------------------------------------------}

-- | C enumeration
--
-- This class implements an API for Haskell representations of C enumerations.
-- C @enum@ declarations only declare values; they do not limit the range of the
-- corresponding integral type.  They may have negative values, non-sequential
-- values, and multiple names for a single value.
--
-- At a low level, @hs-bindgen@ generates a @newtype@ wrapper around the
-- integral representation type to represent a C @enum@. An instance of this
-- class is generated automatically. A 'Show' instance defined using 'shows' is
-- also generated by default. 'Bounded' and 'Prelude.Enum' instances are /not/
-- generated automatically because values do not technically need to be
-- declared. Users may optionally derive these instances using 'AsCEnum' or
-- 'AsSequentialCEnum' when appropriate.
--
-- This class may also be used with Haskell sum-type representations of
-- enumerations.
class (Integral (CEnumZ a)) => CEnum a where
  -- | Integral representation type
  type CEnumZ a

  -- | Construct a value from the integral representation
  --
  -- prop> fromCEnum . toCEnum === id
  toCEnum :: CEnumZ a -> a
  default toCEnum :: (Coercible a (CEnumZ a)) => CEnumZ a -> a
  toCEnum = coerce

  -- | Get the integral representation for a value
  --
  -- prop> toCEnum . fromCEnum === id
  --
  -- If @a@ has an 'Ord' instance, it should be compatible with the 'Ord'
  -- instance on the underlying integral value:
  --
  -- prop> \x y -> (x <= y) === (fromCEnum x <= fromCEnum y)
  fromCEnum :: a -> CEnumZ a
  default fromCEnum :: (Coercible a (CEnumZ a)) => a -> CEnumZ a
  fromCEnum = coerce

  -- | Declared values and associated names
  declaredValues :: proxy a -> DeclaredValues a

  -- | Show undeclared value
  --
  -- Like any 'Show' related function, this should generate a valid Haskell
  -- expression. In this case, a valid Haskell expression for values /outside/
  -- of the set of declared values (that is, for which 'isDeclared' will return
  -- 'False').
  --
  -- The default definition just shows the underlying integer value; this is
  -- valid if the Haskell wrapper has a 'Num' instance. If the Haskell type is
  -- simply a newtype wrapper around the underlying C type, you can use
  -- 'showsWrappedUndeclared'. Finally, if the Haskell type /cannot/ represent
  -- undeclared values, this can be defined using @error@.
  --
  -- > showsUndeclared _ = \_ x ->
  -- >   error $ "Unexpected value " ++ show x ++ " for type Foo"
  showsUndeclared :: proxy a -> Int -> CEnumZ a -> ShowS
  default showsUndeclared
    :: (Show (CEnumZ a))
    => proxy a -> Int -> CEnumZ a -> ShowS
  showsUndeclared _ = showsPrec

  -- | Read undeclared value
  --
  -- See 'showsUndeclared', 'showsWrappedUndeclared', and
  -- 'readPrecWrappedUndeclared'.
  readPrecUndeclared :: ReadPrec a

  -- | Determine if the specified value is declared
  --
  -- This has a default definition in terms of 'declaredValues', but you may
  -- wish to override this with a more efficient implementation (in particular,
  -- see 'seqIsDeclared').
  isDeclared :: a -> Bool
  isDeclared x = (fromCEnum x) `Map.member` getIntegralToDeclaredValues (Proxy :: Proxy a)

  -- | Construct a value only if it is declared
  --
  -- See also 'seqMkDeclared'.
  mkDeclared :: CEnumZ a -> Maybe a
  mkDeclared i
    | i `Map.member` getIntegralToDeclaredValues (Proxy :: Proxy a) = Just (toCEnum i)
    | otherwise = Nothing

-- | C enumeration with sequential values
--
-- 'Bounded' and 'Enum' methods may be implemented more efficiently when the
-- values of an enumeration are sequential.  An instance of this class is
-- generated automatically in this case.  Users may optionally derive these
-- instances using 'AsSequentialCEnum' when appropriate.
--
-- This class may also be used with Haskell sum-type representations of
-- enumerations.
--
-- prop> all isDeclared [minDeclaredValue..maxDeclaredValue]
class (CEnum a) => SequentialCEnum a where
  -- | The minimum declared value
  --
  -- prop> minDeclaredValue == minimum (filter isDeclared (map toCEnum [minBound..]))
  minDeclaredValue :: a

  -- | The maximum declared value
  --
  -- prop> maxDeclaredValue == maximum (filter isDeclared (map toCEnum [minBound..]))
  maxDeclaredValue :: a

{-------------------------------------------------------------------------------
  API
-------------------------------------------------------------------------------}

-- | Get all names associated with a value
--
-- An empty list is returned when the specified value is not declared.
getNames :: forall a. (CEnum a) => a -> [String]
getNames x =
  maybe [] NonEmpty.toList $
    Map.lookup (fromCEnum x) (getIntegralToDeclaredValues (Proxy :: Proxy a))

{-------------------------------------------------------------------------------
  Instance support
-------------------------------------------------------------------------------}

-- | Declared values (opaque)
data DeclaredValues a = DeclaredValues
  { integralToDeclaredValues :: !(Map (CEnumZ a) (NonEmpty String))
  , declaredValueToIntegral :: !(Map String (CEnumZ a))
  }

-- | Construct t'DeclaredValues' from a list of values and associated names
declaredValuesFromList
  :: (Ord (CEnumZ a))
  => [(CEnumZ a, NonEmpty String)]
  -> DeclaredValues a
declaredValuesFromList xs =
  DeclaredValues
    { integralToDeclaredValues = Map.fromList xs
    , declaredValueToIntegral =
        Map.fromList [(n, i) | (i, ns) <- xs, n <- NonEmpty.toList ns]
    }

declaredValuesList :: DeclaredValues a -> [String]
declaredValuesList = Map.keys . declaredValueToIntegral

-- | Show the specified value
--
-- Examples for a hypothetical enumeration type, using generated defaults:
--
-- > showCEnum StatusOK == "StatusOK"
--
-- > showCEnum (StatusCode 418) == "StatusCode 418"
show :: forall a. (CEnum a) => a -> String
show x = shows 0 x ""

-- | Generalization of 'Prelude.show' (akin to 'Prelude.shows').
--
-- This function may be used in the definition of a 'Show' instance for a
-- @newtype@ representation of a C enumeration.
--
-- When the value is declared, a corresponding name is returned.  Otherwise,
-- 'showsUndeclared' is called.
shows :: forall a. (CEnum a) => Int -> a -> ShowS
shows prec x =
  case Map.lookup i (getIntegralToDeclaredValues (Proxy :: Proxy a)) of
    Just (name :| _names) -> showString name
    Nothing -> showsUndeclared (Proxy :: Proxy a) prec i
 where
  i :: CEnumZ a
  i = fromCEnum x

-- | Read a 'CEnum' from string
--
-- Examples for a hypothetical enumeration type, using generated defaults:
--
-- > (readEitherCEnum "StatusCode 200" :: StatusCode) == Right StatusOK
--
-- > (readEitherCEnum "StatusOK" :: StatusCode) == Right StatusOK
--
-- > (readEitherCEnum "StatusCode 123" :: StatusCode) == Right (StatusCode 123)
readEither :: forall a. (CEnum a) => String -> Either String a
readEither s =
  case [x | (x, "") <- ReadPrec.readPrec_to_S read' minPrec s] of
    [x] -> Right x
    [] -> Left "readEitherCEnum: no parse"
    _xs -> Left "readEitherCEnum: ambiguous parse"
 where
  read' =
    do
      x <- readPrec
      ReadPrec.lift ReadP.skipSpaces
      return x

-- | Helper function for defining 'showsUndeclared'
--
-- This helper can be used in the case where @a@ is a newtype wrapper around
-- the underlying @CEnumZ a@.
showsWrappedUndeclared
  :: (Show (CEnumZ a))
  => String -> proxy a -> Int -> CEnumZ a -> ShowS
showsWrappedUndeclared constructorName _ p x =
  showParen (p >= appPrec1) $
    showString constructorName
      . showSpace
      . showsPrec appPrec1 x

-- | Read a declared 'CEnum' value
readPrecDeclaredValue :: forall proxy a. (CEnum a) => proxy a -> ReadPrec a
readPrecDeclaredValue proxy = Read.parens $ ReadPrec.prec appPrec1 $ do
  declaredValue <-
    ReadPrec.lift $
      ReadP.choice $
        map ReadP.string $
          declaredValuesList $
            declaredValues proxy
  pure $ toCEnum $ (declaredValueToIntegral $ declaredValues proxy) Map.! declaredValue

-- | Helper function for defining 'readPrecUndeclared'
--
-- This helper can be used in the case where @a@ is a newtype wrapper around
-- the underlying @CEnumZ a@.
readPrecWrappedUndeclared
  :: forall a. (CEnum a, Read (CEnumZ a)) => String -> ReadPrec a
readPrecWrappedUndeclared constructorName = Read.parens $ ReadPrec.prec appPrec $ do
  ReadPrec.lift $ expect $ Ident constructorName
  n <- Read.step (Read.readPrec :: ReadPrec (CEnumZ a))
  pure $ toCEnum n

-- | Read a 'CEnum' from string
--
-- This function may be used in the definition of a 'Read' instance for a
-- @newtype@ representation of a C enumeration.
readPrec :: forall a. (CEnum a) => ReadPrec a
readPrec = readPrecDeclaredValue (Proxy :: Proxy a) +++ readPrecUndeclared

-- | Determine if the specified value is declared
--
-- This implementation is optimized for 'SequentialCEnum'.
seqIsDeclared :: forall a. (SequentialCEnum a) => a -> Bool
seqIsDeclared x = i >= minZ && i <= maxZ
 where
  minZ, maxZ, i :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x

-- | Construct a value only if it is declared
--
-- This implementation is optimized for 'SequentialCEnum'.
seqMkDeclared :: forall a. (SequentialCEnum a) => CEnumZ a -> Maybe a
seqMkDeclared i
  | i >= minZ && i <= maxZ = Just (toCEnum i)
  | otherwise = Nothing
 where
  minZ, maxZ :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)

{-------------------------------------------------------------------------------
  Deriving via support
-------------------------------------------------------------------------------}

-- | Type used to derive classes using @DerivingVia@ a type with a 'CEnum'
-- instance
--
-- When the values are sequential, 'AsSequentialCEnum' provides better
-- performance and should therefore be used instead.
--
-- The following classes may be derived:
--
-- * 'Bounded' may be derived using the bounds of the declared values.  This is
--   /not/ derived by default.
-- * 'Enum' may be derived using the bounds of the declared values.  This
--   instance assumes that only the declared values are valid and throws a
--   'CEnumException' if passed a value that is not declared.  This is /not/
--   derived by default.
--
-- For /declared/ values we have
--
-- prop> toEnum   === coerce       . toCENum   . fromIntegral
-- prop> fromEnum === fromIntegral . fromCEnum . coerce
--
-- In addition we guarantee that where 'pred' or 'succ' are defined, we have
--
-- prop> \x -> (pred x < x) && (x < succ x)
newtype AsCEnum a = WrapCEnum {unwrapCEnum :: a}

instance (CEnum a) => Bounded (AsCEnum a) where
  minBound = WrapCEnum minBoundGen
  maxBound = WrapCEnum maxBoundGen

instance (CEnum a) => Enum (AsCEnum a) where
  succ = WrapCEnum . succGen . unwrapCEnum
  pred = WrapCEnum . predGen . unwrapCEnum

  toEnum = WrapCEnum . toEnumGen
  fromEnum = fromEnumGen . unwrapCEnum

  enumFrom (WrapCEnum x) = WrapCEnum <$> enumFromGen x
  enumFromThen (WrapCEnum x) (WrapCEnum y) = WrapCEnum <$> enumFromThenGen x y
  enumFromTo (WrapCEnum x) (WrapCEnum z) = WrapCEnum <$> enumFromToGen x z
  enumFromThenTo (WrapCEnum x) (WrapCEnum y) (WrapCEnum z) =
    WrapCEnum <$> enumFromThenToGen x y z

-- | Type used to derive classes using @DerivingVia@ a type with a
-- 'SequentialCEnum' instance
--
-- The following classes may be derived:
--
-- * 'Bounded' may be derived using the bounds of the declared values.  This is
--   /not/ derived by default.
-- * 'Enum' may be derived using the bounds of the declared values.  This
--   instance assumes that only the declared values are valid and throws a
--   'CEnumException' if passed a value that is not declared.  This is /not/
--   derived by default.
--
-- 'AsSequentialCEnum' should have the same properties as 'AsCEnum'.
newtype AsSequentialCEnum a = WrapSequentialCEnum {unwrapSequentialCEnum :: a}

instance (SequentialCEnum a) => Bounded (AsSequentialCEnum a) where
  minBound = WrapSequentialCEnum minBoundSeq
  maxBound = WrapSequentialCEnum maxBoundSeq

instance (SequentialCEnum a) => Enum (AsSequentialCEnum a) where
  succ = WrapSequentialCEnum . succSeq . unwrapSequentialCEnum
  pred = WrapSequentialCEnum . predSeq . unwrapSequentialCEnum

  toEnum = WrapSequentialCEnum . toEnumSeq
  fromEnum = fromEnumSeq . unwrapSequentialCEnum

  enumFrom (WrapSequentialCEnum x) = WrapSequentialCEnum <$> enumFromSeq x
  enumFromThen (WrapSequentialCEnum x) (WrapSequentialCEnum y) =
    WrapSequentialCEnum <$> enumFromThenSeq x y
  enumFromTo (WrapSequentialCEnum x) (WrapSequentialCEnum z) =
    WrapSequentialCEnum <$> enumFromToSeq x z
  enumFromThenTo
    (WrapSequentialCEnum x)
    (WrapSequentialCEnum y)
    (WrapSequentialCEnum z) =
      WrapSequentialCEnum <$> enumFromThenToSeq x y z

{-------------------------------------------------------------------------------
  Exceptions
-------------------------------------------------------------------------------}

-- | Exceptions used by optional C enumeration instances
data CEnumException
  = CEnumNotDeclared Integer
  | CEnumNoSuccessor Integer
  | CEnumNoPredecessor Integer
  | CEnumEmpty
  | CEnumFromEqThen Integer
  deriving stock (Eq, Show)

instance Exception CEnumException where
  displayException = \case
    CEnumNotDeclared i -> "C enumeration value not declared: " ++ Prelude.show i
    CEnumNoSuccessor i ->
      "C enumeration value has no declared successor: " ++ Prelude.show i
    CEnumNoPredecessor i ->
      "C enumeration value has no declared predecessor: " ++ Prelude.show i
    CEnumEmpty -> "C enumeration has no declared values"
    CEnumFromEqThen i -> "enumeration from and then values equal: " ++ Prelude.show i

{-------------------------------------------------------------------------------
  Bounded instance implementation
-------------------------------------------------------------------------------}

minBoundGen :: forall a. (CEnum a) => a
minBoundGen = case Map.lookupMin (getIntegralToDeclaredValues (Proxy :: Proxy a)) of
  Just (i, _names) -> toCEnum i
  Nothing -> throw CEnumEmpty

minBoundSeq :: (SequentialCEnum a) => a
minBoundSeq = minDeclaredValue

maxBoundGen :: forall a. (CEnum a) => a
maxBoundGen = case Map.lookupMax (getIntegralToDeclaredValues (Proxy :: Proxy a)) of
  Just (k, _names) -> toCEnum k
  Nothing -> throw CEnumEmpty

maxBoundSeq :: (SequentialCEnum a) => a
maxBoundSeq = maxDeclaredValue

{-------------------------------------------------------------------------------
  Enum instance implementation
-------------------------------------------------------------------------------}

succGen :: forall a. (CEnum a) => a -> a
succGen x = either (throw . CEnumNotDeclared) id $ do
  (_ltMap, gtMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
  case Map.lookupMin gtMap of
    Just (j, _names) -> return $ toCEnum j
    Nothing -> throw $ CEnumNoSuccessor (toInteger i)
 where
  i :: CEnumZ a
  i = fromCEnum x

succSeq :: forall a. (SequentialCEnum a) => a -> a
succSeq x
  | i >= minZ && i < maxZ = toCEnum (i + 1)
  | i == maxZ = throw $ CEnumNoSuccessor (toInteger i)
  | otherwise = throw $ CEnumNotDeclared (toInteger i)
 where
  minZ, maxZ, i :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x

predGen :: forall a. (CEnum a) => a -> a
predGen y = either (throw . CEnumNotDeclared) id $ do
  (ltMap, _gtMap) <- splitMap j (getIntegralToDeclaredValues (Proxy :: Proxy a))
  case Map.lookupMax ltMap of
    Just (i, _names) -> return $ toCEnum i
    Nothing -> throw $ CEnumNoPredecessor (toInteger j)
 where
  j :: CEnumZ a
  j = fromCEnum y

predSeq :: forall a. (SequentialCEnum a) => a -> a
predSeq y
  | j > minZ && j <= maxZ = toCEnum (j - 1)
  | j == minZ = throw $ CEnumNoPredecessor (toInteger j)
  | otherwise = throw $ CEnumNotDeclared (toInteger j)
 where
  minZ, maxZ, j :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  j = fromCEnum y

toEnumGen :: (CEnum a) => Int -> a
toEnumGen i = case mkDeclared (fromIntegral i) of
  Just x -> x
  Nothing -> throw $ CEnumNotDeclared (toInteger i)

toEnumSeq :: forall a. (SequentialCEnum a) => Int -> a
toEnumSeq n
  | i >= minZ && i <= maxZ = toCEnum i
  | otherwise = throw $ CEnumNotDeclared (toInteger i)
 where
  minZ, maxZ, i :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromIntegral n

fromEnumGen :: forall a. (CEnum a) => a -> Int
fromEnumGen x
  | i `Map.member` getIntegralToDeclaredValues (Proxy :: Proxy a) = fromIntegral i
  | otherwise = throw $ CEnumNotDeclared (toInteger i)
 where
  i :: CEnumZ a
  i = fromCEnum x

fromEnumSeq :: forall a. (SequentialCEnum a) => a -> Int
fromEnumSeq x
  | i >= minZ && i <= maxZ = fromIntegral i
  | otherwise = throw $ CEnumNotDeclared (toInteger i)
 where
  minZ, maxZ, i :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x

enumFromGen :: forall a. (CEnum a) => a -> [a]
enumFromGen x = either (throw . CEnumNotDeclared) id $ do
  (_ltMap, gtMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
  return $ x : map toCEnum (Map.keys gtMap)
 where
  i :: CEnumZ a
  i = fromCEnum x

enumFromSeq :: forall a. (SequentialCEnum a) => a -> [a]
enumFromSeq x
  | i >= minZ && i <= maxZ = map toCEnum [i .. maxZ]
  | otherwise = throw $ CEnumNotDeclared (toInteger i)
 where
  minZ, maxZ, i :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x

enumFromThenGen :: forall a. (CEnum a) => a -> a -> [a]
enumFromThenGen x y = case compare i j of
  LT -> either (throw . CEnumNotDeclared) id $ do
    (_ltIMap, gtIMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
    (ltJMap, gtJMap) <- splitMap j gtIMap
    let w = Map.size ltJMap + 1
        js = j : Map.keys gtJMap
    return $ x : map (toCEnum . NonEmpty.head) (nonEmptyChunksOf w js)
  GT -> either (throw . CEnumNotDeclared) id $ do
    (ltIMap, _gtIMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
    (ltJMap, gtJMap) <- splitMap j ltIMap
    let w = Map.size gtJMap + 1
        js = j : reverse (Map.keys ltJMap)
    return $ x : map (toCEnum . NonEmpty.head) (nonEmptyChunksOf w js)
  EQ -> throw $ CEnumFromEqThen (toInteger i)
 where
  i, j :: CEnumZ a
  i = fromCEnum x
  j = fromCEnum y

enumFromThenSeq :: forall a. (SequentialCEnum a) => a -> a -> [a]
enumFromThenSeq x y
  | i == j = throw $ CEnumFromEqThen (toInteger i)
  | i < minZ || i > maxZ = throw $ CEnumNotDeclared (toInteger i)
  | j < minZ || j > maxZ = throw $ CEnumNotDeclared (toInteger j)
  | i < j = map toCEnum [i, j .. maxZ]
  | otherwise = map toCEnum [i, j .. minZ]
 where
  minZ, maxZ, i, j :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x
  j = fromCEnum y

enumFromToGen :: forall a. (CEnum a) => a -> a -> [a]
enumFromToGen x z = either (throw . CEnumNotDeclared) id $ do
  (_ltIMap, gtIMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
  if i == k then
    return [x]
  else do
    (ltKMap, _gtKMap) <- splitMap k gtIMap
    return $ x : map toCEnum (Map.keys ltKMap) ++ [z]
 where
  i, k :: CEnumZ a
  i = fromCEnum x
  k = fromCEnum z

enumFromToSeq :: forall a. (SequentialCEnum a) => a -> a -> [a]
enumFromToSeq x z
  | i < minZ || i > maxZ = throw $ CEnumNotDeclared (toInteger i)
  | k < minZ || k > maxZ = throw $ CEnumNotDeclared (toInteger k)
  | otherwise = map toCEnum [i .. k]
 where
  minZ, maxZ, i, k :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x
  k = fromCEnum z

enumFromThenToGen :: forall a. (CEnum a) => a -> a -> a -> [a]
enumFromThenToGen x y z = case compare i j of
  LT -> either (throw . CEnumNotDeclared) id $ do
    (_ltIMap, gtIMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
    (ltJMap, gtJMap) <- splitMap j gtIMap
    (ltKMap, _gtKMap) <- splitMap k gtJMap
    let w = Map.size ltJMap + 1
        js = j : Map.keys ltKMap ++ [k]
    return $ x : map (toCEnum . NonEmpty.head) (nonEmptyChunksOf w js)
  GT -> either (throw . CEnumNotDeclared) id $ do
    (ltIMap, _gtIMap) <- splitMap i (getIntegralToDeclaredValues (Proxy :: Proxy a))
    (ltJMap, gtJMap) <- splitMap j ltIMap
    (_ltKMap, gtKMap) <- splitMap k ltJMap
    let w = Map.size gtJMap + 1
        js = j : reverse (k : Map.keys gtKMap)
    return $ x : map (toCEnum . NonEmpty.head) (nonEmptyChunksOf w js)
  EQ -> throw $ CEnumFromEqThen (toInteger i)
 where
  i, j, k :: CEnumZ a
  i = fromCEnum x
  j = fromCEnum y
  k = fromCEnum z

enumFromThenToSeq :: forall a. (SequentialCEnum a) => a -> a -> a -> [a]
enumFromThenToSeq x y z
  | i == j = throw $ CEnumFromEqThen (toInteger i)
  | i < minZ || i > maxZ = throw $ CEnumNotDeclared (toInteger i)
  | j < minZ || j > maxZ = throw $ CEnumNotDeclared (toInteger j)
  | k < minZ || k > maxZ = throw $ CEnumNotDeclared (toInteger k)
  | otherwise = map toCEnum [i, j .. k]
 where
  minZ, maxZ, i, j, k :: CEnumZ a
  minZ = fromCEnum (minDeclaredValue @a)
  maxZ = fromCEnum (maxDeclaredValue @a)
  i = fromCEnum x
  j = fromCEnum y
  k = fromCEnum z

{-------------------------------------------------------------------------------
  Auxiliary Functions
-------------------------------------------------------------------------------}

getIntegralToDeclaredValues :: (CEnum a) => proxy a -> Map (CEnumZ a) (NonEmpty String)
getIntegralToDeclaredValues = integralToDeclaredValues . declaredValues

nonEmptyChunksOf :: Int -> [a] -> [NonEmpty a]
nonEmptyChunksOf n xs
  | n > 0 = aux xs
  | otherwise = error $ "nonEmptyChunksOf: n must be positive, got " ++ Prelude.show n
 where
  aux :: [a] -> [NonEmpty a]
  aux xs' = case first NonEmpty.nonEmpty (List.splitAt n xs') of
    (Just ne, rest) -> ne : aux rest
    (Nothing, _rest) -> []

splitMap :: (Integral k) => k -> Map k v -> Either Integer (Map k v, Map k v)
splitMap n m = case Map.splitLookup n m of
  (ltMap, Just{}, gtMap) -> Right (ltMap, gtMap)
  (_ltMap, Nothing, _gtMap) -> Left (toInteger n)