-------------------------------------------------------------------------------- -- | -- Module : Data.Finite -- Copyright : (C) 2022-2023 mniip -- License : BSD3 -- Maintainer : mniip -- 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 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 = I.finite -- | Convert a 'Finite' into the corresponding 'Integer'. getFinite :: forall n. Finite n -> Integer getFinite = I.getFinite