{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module ReWire.Finite where

import ReWire

-- | Convert an Integer into a @'Finite' n@, throws an error if negative or >= @n@.
{-# INLINE finite #-}
finite :: KnownNat n => Integer -> Finite n
finite :: forall (n :: Nat). KnownNat n => Integer -> Finite n
finite = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
rwPrimFinite

-- | Converts argument bitvector to Finite, raising error if unrepresentable.
{-# INLINE toFinite #-}
toFinite :: KnownNat n => W m -> Finite n
toFinite :: forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite = Vec m Bool -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
rwPrimToFinite

{-# INLINE minBound #-}
minBound :: KnownNat n => Finite n
minBound :: forall (n :: Nat). KnownNat n => Finite n
minBound = Finite n
forall (n :: Nat). KnownNat n => Finite n
rwPrimFiniteMinBound

{-# INLINE maxBound #-}
maxBound :: KnownNat n => Finite n
maxBound :: forall (n :: Nat). KnownNat n => Finite n
maxBound = Finite n
forall (n :: Nat). KnownNat n => Finite n
rwPrimFiniteMaxBound

-- | Converts argument bitvector to Finite n, reducing modulo n if necessary
--   (without raising error; @n@ must be positive, as @'Finite' 0@ is
--   uninhabited).
{-# INLINE toFinite' #-}
toFinite' :: KnownNat n => W m -> Finite n
toFinite' :: forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' = Vec m Bool -> Finite n
forall (m :: Nat) (n :: Nat). KnownNat n => Vec m Bool -> Finite n
rwPrimToFiniteMod

{-# INLINE fromFinite #-}
fromFinite :: KnownNat m => Finite n -> W m
fromFinite :: forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite = Finite n -> Vec m Bool
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
rwPrimFromFinite