--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite
-- Copyright   :  (C) 2022-2023 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE CPP #-}
module Data.Finite.Internal
    (
        Finite, pattern Finite,
        finite, getFinite
    )
    where

import GHC.TypeLits

import qualified Data.Finite.Internal.Integral as I

-- | Finite number type. The type @'Finite' n@ is inhabited by exactly @n@
-- values in the range @[0, n)@ including @0@ but excluding @n@. Invariants:
--
-- prop> getFinite x < natVal x
-- prop> getFinite x >= 0
type Finite = I.Finite Integer

#if __GLASGOW_HASKELL__ >= 710
pattern Finite :: forall n. Integer -> Finite n
#endif
pattern $mFinite :: forall {r} {n :: Nat}.
Finite n -> (Integer -> r) -> ((# #) -> r) -> r
$bFinite :: forall (n :: Nat). Integer -> Finite n
Finite x = I.Finite (x :: Integer)

-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out
-- of bounds.
finite :: forall n. KnownNat n => Integer -> Finite n
finite :: forall (n :: Nat). KnownNat n => Integer -> Finite n
finite = Integer -> Finite Integer n
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
I.finite

-- | Convert a 'Finite' into the corresponding 'Integer'.
getFinite :: forall n. Finite n -> Integer
getFinite :: forall (n :: Nat). Finite n -> Integer
getFinite = Finite Integer n -> Integer
forall (n :: Nat) a. Finite a n -> a
I.getFinite