-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Nat singletons represented by Int
--   
--   This package implements a type <a>SInt</a> that links a runtime
--   <a>Int</a> with a type-level <a>Nat</a>, along with some arithmetic
--   and reflection capabilities.
--   
--   This is useful when mixing type-level <a>Nat</a>s with GHC array
--   primitives that expect <a>Int</a>s as sizes and indices.
--   
--   See the module intro of <a>Data.SInt</a> for more details.
@package sint
@version 0.2.0


-- | Provides a singleton type for a subset of <a>Nat</a>s, represented by
--   <a>Int</a>.
--   
--   This is particularly useful when working with length-indexed array
--   types, since the array primitives generally expect lengths and indices
--   to be <a>Int</a>s. Thus, there's no need to pay the runtime cost of
--   lugging around <a>Natural</a>s to handle greater-than-maxInt-length
--   arrays, since the underlying primitives don't handle them either.
--   
--   An <tt><a>SInt</a> n</tt> is trusted absolutely by downstream code to
--   contain an <a>Int</a> <tt>n'</tt> s.t. <tt>fromIntegral n' == natVal'
--   @n Proxy#</tt>. In particular, this trust extends to a willingness to
--   use two runtime-equal <a>SInt</a>s as proof that their type parameters
--   are equal, or to use GHC primitives in a way that's only memory-safe
--   if this property holds. This means it should be considered
--   <i>unsafe</i> to construct an <a>SInt</a> in any way that's not
--   statically guaranteed to produce the correct runtime value, and to
--   construct one with an incorrect runtime value is equivalent to using
--   <a>unsafeCoerce</a> incorrectly.
--   
--   <a>SInt</a> should be seen as a more efficient implementation of
--   <tt>data SNat n = KnownNat n =&gt; SNat</tt>, so that constructing an
--   incorrect <a>SInt</a> would be equivalent to producing an incorrect
--   <a>KnownNat</a> instance.
--   
--   <a>SInt</a>s are constructed safely by <a>staticSIntVal</a> with no
--   overhead, by <a>sintVal</a> with runtime bounds checks based on a
--   <a>KnownNat</a> instance, or by various arithmetic functions.
module Data.SInt

-- | A singleton type linking a runtime <a>Int</a> and a type-level
--   <a>Nat</a>.
data SInt (n :: Nat)

-- | Construct an <a>SInt</a> unsafely. Incorrect uses cause undefined
--   behavior.
--   
--   See the module intro for more details; prefer to use safe methods to
--   construct <a>SInt</a>s, and treat this constructor equivalently to
--   <a>unsafeCoerce</a>.
pattern SI# :: Int -> SInt n

-- | A unidirectional pattern for safely deconstructing <a>SInt</a>s.
--   
--   This lets us export <a>unSInt</a> as if it were a field selector,
--   without making it legal to use in record updates (because this pattern
--   is unidirectional).
pattern SI :: Int -> SInt n

-- | Produce an <a>SInt</a> for a given <a>KnownNat</a>, or <a>Nothing</a>
--   if out of range.
trySIntVal :: forall n. KnownNat n => Maybe (SInt n)

-- | Produce an <a>SInt</a> for a given <a>KnownNat</a>, or <a>error</a> if
--   out of range.
sintVal :: forall n. (HasCallStack, KnownNat n) => SInt n

-- | Bring an <a>SInt</a> back into the type level as a <a>KnownNat</a>
--   instance.
reifySInt :: forall n r. SInt n -> (KnownNat n => r) -> r

-- | Use an <a>Int</a> as an existentially-quantified <a>SInt</a>.
withSInt :: HasCallStack => Int -> (forall n. SInt n -> r) -> r

-- | Add two <a>SInt</a>s with bounds checks; <a>error</a> if the result
--   overflows.
addSInt :: HasCallStack => SInt m -> SInt n -> SInt (m + n)

-- | Subtract two <a>SInt</a>s with bounds checks; <a>error</a> if the
--   result is negative.
subSInt :: HasCallStack => SInt m -> SInt n -> SInt (m - n)

-- | Subtract two <a>SInt</a>s, using an inequality constraint to rule out
--   overflow.
subSIntLE :: n <= m => SInt m -> SInt n -> SInt (m - n)

-- | "Un-add" an <a>SInt</a> from another <a>SInt</a>, on the left.
--   
--   This form of <a>subSInt</a> is more convenient in certain cases when a
--   type signature ensures a particular <a>SInt</a> is of the form <tt>m +
--   n</tt>.
subSIntL :: SInt (m + n) -> SInt m -> SInt n

-- | Multiply two <a>SInt</a>s with bounds checks; <a>error</a> if the
--   result overflows.
mulSInt :: HasCallStack => SInt m -> SInt n -> SInt (m * n)

-- | "Un-multiply" an <a>SInt</a> by another <a>SInt</a>, on the left.
--   
--   This form of <tt>divSInt</tt> is more convenient in certain cases when
--   a type signature ensures a particular <a>SInt</a> is of the form <tt>m
--   * n</tt>.
divSIntL :: SInt (m * n) -> SInt m -> SInt n

-- | "Un-multiply" an <a>SInt</a> by another <a>SInt</a>, on the right.
--   
--   This form of <tt>divSInt</tt> is more convenient in certain cases when
--   a type signature ensures a particular <a>SInt</a> is of the form <tt>m
--   * n</tt>.
divSIntR :: SInt (m * n) -> SInt n -> SInt m

-- | Like <a>sintVal</a>, but with static proof that it's in-bounds.
--   
--   This optimizes down to an actual primitive literal wrapped in the
--   appropriate constructors, unlike <a>sintVal</a>, where the bounds
--   checking gets in the way. If you're constructing a statically-known
--   <a>SInt</a>, use <a>staticSIntVal</a>; while if you're constructing an
--   <a>SInt</a> from a runtime <a>KnownNat</a> instance, you'll have to
--   use <a>sintVal</a>.
staticSIntVal :: forall n. (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n

-- | One more than the maximum representable <a>Int</a> on the current
--   platform.
type IntMaxP1 = 2 ^ (64 - 1)
instance Data.Portray.Diff.Diff (Data.SInt.SInt n)
instance Data.Portray.Portray (Data.SInt.SInt n)
instance GHC.Show.Show (Data.SInt.SInt n)