-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- | Runtime witnesses of type-level integers.

module Data.SNumber
         ( -- * SNumber
           SNumber(SNumber, N#, SN, unSNumber), SNumberRepr(..)

           -- ** Creation
         , snumber, trySNumber

           -- *** Unsafe
         , unsafeUncheckedSNumber
         , unsafeMkSNumber, unsafeTryMkSNumber, unsafeUncheckedMkSNumber

           -- ** Existentials
         , SomeSNumber(..), someSNumberVal, withSNumber

           -- ** Comparison
         , compareSNumber, sameSNumber

           -- ** Arithmetic
         , OverflowArith(..)

           -- *** In 'Maybe'
         , tryAdd, trySub, tryMul

           -- *** Checked
         , UnrepresentableSNumber(..)
         , chkAdd, chkSub, chkMul

           -- ** Infallible
         , divExact

           -- ** Reification to Constraints
         , KnownSNumber(..), snumberVal
         , reifySNumber, reifySNumberAsNat

           -- * Miscellaneous
         , IntBits, IntMin, IntMaxP1
         , WordBits, WordMaxP1
         ) where

import Control.Exception (Exception, throw)
import Data.Kind (Constraint, Type)
import Data.Maybe (fromMaybe)
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import GHC.Exts
         ( Word(W#), addWordC#, subWordC#, timesWord2#
         , Int(I#), addIntC#, subIntC#, mulIntMayOflo#, (*#)
         )
import GHC.Stack (HasCallStack, withFrozenCallStack)
import GHC.TypeNats (type (^), KnownNat, Nat, SomeNat(..), someNatVal)
import Numeric.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)

import Data.SNumber.Internal
         ( NegativeReprUnsignedErr, OutOfReprRangeErr
         , IsAtLeastMinBound, IsLessThanMaxBound, ForbidNegZero
         )
import Kinds.Integer (CmpInteger, KnownInteger(..), pattern Pos, pattern Neg)
import qualified Kinds.Integer as K (Integer)
import Kinds.Ord (OrderingI(..))
import Kinds.Num (type (+), type (-), type (*))

#include "MachDeps.h"

-- | @SNumber a n@ is a runtime representation of the value of @n@.
--
-- For @N# n :: SNumber a n@ and @N# m :: SNumber a m@, the following must hold:
--
-- * @n ~ m@ iff @n == m@ (according to the 'Eq' instance of @a@).
-- * @CmpInteger m n ~ 'LT@ iff @compare m n == LT@ (according to 'Ord').
-- * @CmpInteger m n ~ 'EQ@ iff @compare m n == EQ@.
-- * @CmpInteger m n ~ 'GT@ iff @compare m n == GT@.
-- * @toInteger n == integerVal \@n@.
-- * @a@ upholds the 'Ord' laws.
--
-- These are exactly the set of things we're willing to 'unsafeCoerce' proofs
-- for.  It is /unsafe/ to construct an 'SNumber' that violates these by any
-- means.
--
-- Note that the first requirement means that you must never construct
-- @N# 0 :: SNumber _ ('Neg 0)@, because that would prove that
-- @'Neg 0 ~ 'Pos 0@.  In practice, we largely ignore the existence of
-- @'Neg 0@: 'trySNumber' (and, by extension, the instance derivation via
-- 'KnownInteger') will throw a runtime error when trying to construct
-- @'Neg 0@, and 'SafeSNumber' instances explicitly exclude @'Neg 0@ with
-- type-level checks.
--
-- There are six main ways to introduce an 'SNumber', from the cartesian
-- product of several choices
--
-- * How do you validate that the value is in-bounds for the representation
--   type?
--
--     * If by runtime checks, the function name has a "try" infix.
--     * If by trusting the caller blindly, the function name has an "unsafe"
--       prefix and an \"Unchecked\" infix.
--     * If by type-level bounds checks, the function name has neither of these.
--
-- * How do you validate that the runtime Integer value matches the type-level
--   Integer?
--
--     * If by trusting the user to pass in the right Integer, the function has
--       an "unsafe" prefix and a \"Mk" infix: we're "making" the 'SNumber'
--       from a runtime value rather than deriving it from KnownNat.
--     * If by getting it from a KnownNat instance, the function name doesn't
--       have that infix.
--
-- Thus:
--
-- * 'snumber': type-level checks, safe @KnownNat@.
-- * 'trySNumber': runtime checks, safe @KnownNat@.
-- * 'unsafeUncheckedSNumber': no checks, safe @KnownNat@.
-- * 'unsafeMkSNumber': type-level checks, unsafe @Integer@ parameter.
-- * 'unsafeTryMkSNumber': runtime checks, unsafe @Integer@ parameter.
-- * 'unsafeUncheckedMkSNumber': no checks, unsafe @a@ parameter.  a.k.a. 'N#'.
--
-- Finally, there's one other way to get an 'SNumber': by asking the constraint
-- solver to give you one, with a 'KnownSNumber' class and its 'snumberVal'
-- method.  Currently, this will be solved automatically from 'KnownNat' by
-- using 'trySNumber', and of course it can be solved from a matching instance
-- in the function's context (which compiles to an @a@ parameter for
-- @KnownSNumber a n@).
newtype SNumber a (n :: K.Integer) = MkSNumber# a
  deriving newtype Int -> SNumber a n -> ShowS
[SNumber a n] -> ShowS
SNumber a n -> String
(Int -> SNumber a n -> ShowS)
-> (SNumber a n -> String)
-> ([SNumber a n] -> ShowS)
-> Show (SNumber a n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (n :: Integer). Show a => Int -> SNumber a n -> ShowS
forall a (n :: Integer). Show a => [SNumber a n] -> ShowS
forall a (n :: Integer). Show a => SNumber a n -> String
showList :: [SNumber a n] -> ShowS
$cshowList :: forall a (n :: Integer). Show a => [SNumber a n] -> ShowS
show :: SNumber a n -> String
$cshow :: forall a (n :: Integer). Show a => SNumber a n -> String
showsPrec :: Int -> SNumber a n -> ShowS
$cshowsPrec :: forall a (n :: Integer). Show a => Int -> SNumber a n -> ShowS
Show

-- Note: we must be extremely careful to prevent GHC from solving
-- @Data.Coerce.Coercible (SNumber m) (SNumber n)@.  Given two applications of
-- the same type constructor @X m@ and @X n@, there are three ways GHC might
-- solve this constraint:
-- * If the two types are equal (in our case, if @m ~ n@), the two types are
--   equal, and therefore GHC will consider the constraint solved.  This is
--   obviously fine, and we don't need to prevent it from happening.
-- * If both types are newtypes, whose constructors are in scope, and the two
--   underlying types are coercible, GHC will consider the constraint solved.
--   In our case, the first and third conditions are unavoidably satisfied, so
--   we must prevent the newtype constructor from ever being in scope.  We
--   achieve this (except for inside this module) by omitting it from the
--   export list.  Instead, we export its behavior as the pattern synonym 'N#'
--   and the selector 'unSNumber'.
-- * If each pair of parameters with nominal role is equal, and each pair of
--   parameters with representational role is coercible (note: parameters with
--   phantom role are ignored), GHC will consider the constraint solved.  In
--   our case, the only parameter involved is the 'Integer'; its inferred role
--   is phantom, which means all coercions over it would be solved; so we must
--   use a role annotation to change it.  The choice between representational
--   and nominal doesn't matter in practice, because GHC will never solve
--   @Coercible {Integer} m n@ anyway.  But we set it to nominal just because
--   that feels more right.

-- The 'Type' parameter needs to have nominal role, because coercing between
-- types with different Eq/Ord instances is unsafe.
--
-- See above on 'SNumber' for a description of the coercion behavior of the
-- 'Integer' parameter.
type role SNumber nominal nominal

-- | Create an 'SNumber' for @n@, with no safety measures whatsoever.
--
-- This pattern is identical to the newtype constructor of 'SNumber' except
-- that it isn't actualy a newtype constructor, so having it in scope doesn't
-- allow unsound coercions across 'SNumber' types.
pattern N# :: forall (n :: K.Integer) a. a -> SNumber a n
pattern $bN# :: a -> SNumber a n
$mN# :: forall r (n :: Integer) a.
SNumber a n -> (a -> r) -> (Void# -> r) -> r
N# x = MkSNumber# x
{-# COMPLETE N# #-}

-- | A unidirectional pattern for matching 'SNumber's.
--
-- This allows the pseudo-field-selector 'unSNumber' to be exported bundled
-- with 'SNumber', so it can be imported by @SNumber(..)@ as if it were a
-- normal field selector of a record definition.  If this were done as part of
-- 'N#', it'd allow unsafely changing an 'SNumber'\'s representation without
-- using any identifiers that indicate unsafety, by way of record update
-- syntax.
pattern SN :: forall (n :: K.Integer) a. a -> SNumber a n
pattern $mSN :: forall r (n :: Integer) a.
SNumber a n -> (a -> r) -> (Void# -> r) -> r
SN {SNumber a n -> a
unSNumber} <- MkSNumber# unSNumber
{-# COMPLETE SN #-}

data KnownSNumberDict a n = KnownSNumber a n => KnownSNumberDict

-- | Treat 'SNumber' as if it were a GADT containing a 'KnownSNumber' instance.
pattern SNumber
  :: forall (n :: K.Integer) a. SNumberRepr a => KnownSNumber a n => SNumber a n
pattern $bSNumber :: SNumber a n
$mSNumber :: forall r (n :: Integer) a.
SNumberRepr a =>
SNumber a n -> (KnownSNumber a n => r) -> (Void# -> r) -> r
SNumber <-
  ((\x -> reifySNumber x (KnownSNumberDict @a @n)) -> KnownSNumberDict)
 where
  SNumber = SNumber a n
forall (n :: Integer) a. KnownSNumber a n => SNumber a n
snumberVal
{-# COMPLETE SNumber #-}

class LitIsAnything (n :: K.Integer)
instance ForbidNegZero n => LitIsAnything n

class LitIsUnsignedBits
        (w :: Nat)
        repr
        (a :: K.Integer -> Type)
        (n :: K.Integer)
instance ( IsAtLeastMinBound ('Pos 0) (NegativeReprUnsignedErr repr a) n
         , IsLessThanMaxBound
             ('Pos (2 ^ w))
             (OutOfReprRangeErr ('Pos 0) ('Pos (2 ^ w)) repr a)
             n
         , ForbidNegZero n
         )
      => LitIsUnsignedBits w repr a n

type SignedReprRangeErr w =
  OutOfReprRangeErr ('Neg (2 ^ (w - 1))) ('Pos (2 ^ (w - 1)))

class LitIsSignedBits (w :: Nat) repr (a :: K.Integer -> Type) (n :: K.Integer)
instance ( IsAtLeastMinBound
             ('Neg (2 ^ (w - 1)))
             (SignedReprRangeErr w repr a)
             n
         , IsLessThanMaxBound
             ('Pos (2 ^ (w - 1)))
             (SignedReprRangeErr w repr a)
             n
         , ForbidNegZero n
         )
      => LitIsSignedBits w repr a n

type LitIsNonNegative repr a =
  IsAtLeastMinBound ('Pos 0) (NegativeReprUnsignedErr repr a)

-- | The number of bits in the present system's 'Word' type.
type WordBits = WORD_SIZE_IN_BITS

-- | One more than the largest representable 'Word' value.
type WordMaxP1 = 'Pos (2 ^ WordBits)

-- | The number of bits in the present system's 'Int' type.
type IntBits = WORD_SIZE_IN_BITS

-- | The smallest representable 'Int' value.
type IntMin = 'Neg (2 ^ (IntBits - 1))

-- | One more than the largest representable 'Int' value.
type IntMaxP1 = 'Pos (2 ^ (IntBits - 1))

-- | The class of types that are suitable for use as integer value witnesses.
--
-- Implementing an instance of this class amounts to asserting that the type
-- and its 'Integral', 'Ord', and 'Eq' instances uphold the requirements of
-- 'SNumber', for any integer @n@ that satisfies @SafeSNumber a n@.
--
-- Furthermore, it requires that every value of @a@ is an integer, i.e. that
-- @forall x :: a. exists y :: Integer. x == fromInteger y, toInteger x == y@.
-- This ensures we can wrap any @a@ in @SomeSNumberVal@ and be sure it
-- corresponds to a valid @K.Integer@.
class Integral a => SNumberRepr a where
  -- | @SafeSNumber a n@ witnesses that @'N#' n@ is a valid @'SNumber' a n@.
  type SafeSNumber a :: K.Integer -> Constraint

instance SNumberRepr Int where
  type SafeSNumber Int = LitIsSignedBits IntBits Int (SNumber Int)

instance SNumberRepr Word where
  type SafeSNumber Word = LitIsUnsignedBits WordBits Word (SNumber Word)

instance SNumberRepr Integer where
  type SafeSNumber Integer = LitIsAnything

instance SNumberRepr Natural where
  type SafeSNumber Natural = LitIsNonNegative Natural (SNumber Natural)

-- | Construct an 'SNumber', doing all validation at the type level.
--
-- This is completely safe and cannot raise runtime errors.
snumber
  :: forall n a
   . (SNumberRepr a, SafeSNumber a n, KnownInteger n)
  => SNumber a n
snumber :: SNumber a n
snumber = a -> SNumber a n
forall (n :: Integer) a. SafeSNumber a n => a -> SNumber a n
unsafeMkSNumber (Integer -> a
forall a. Num a => Integer -> a
fromInteger (KnownInteger n => Integer
forall (n :: Integer). KnownInteger n => Integer
integerVal @n))

-- | Create an 'SNumber' for @n@, if it's faithfully represented by @a@.
--
-- This is completely safe, but it may raise runtime errors, because it tests
-- at runtime whether @a@ can represent @n@ correctly.
trySNumber
  :: forall n a
   . (SNumberRepr a, KnownInteger n)
  => Maybe (SNumber a n)
trySNumber :: Maybe (SNumber a n)
trySNumber = Integer -> Maybe (SNumber a n)
forall (n :: Integer) a.
SNumberRepr a =>
Integer -> Maybe (SNumber a n)
unsafeTryMkSNumber (KnownInteger n => Integer
forall (n :: Integer). KnownInteger n => Integer
integerVal @n)

-- | Create an 'SNumber' from a 'KnownInteger' constraint without any checks.
--
-- This will cause type unsoundness if the value is not correctly represented
-- by @a@ or if the instances of @a@ do not behave according to the safety
-- requirements described on 'SNumber'.
unsafeUncheckedSNumber :: forall n a. (Num a, KnownInteger n) => SNumber a n
unsafeUncheckedSNumber :: SNumber a n
unsafeUncheckedSNumber = a -> SNumber a n
forall (n :: Integer) a. a -> SNumber a n
unsafeUncheckedMkSNumber (Integer -> a
forall a. Num a => Integer -> a
fromInteger (KnownInteger n => Integer
forall (n :: Integer). KnownInteger n => Integer
integerVal @n))

-- | Semi-safely construct an 'SNumber' as if by 'N#'.
--
-- Callers must ensure that the @a@ argument is @fromInteger (integerVal @n)@
-- (semantically, not syntactically: @unsafeSNumber @('Pos 42) 42@ is fine and
-- is in fact the intended use case).
--
-- The extra constraint here compared to 'N#' ensures that if you write
-- @unsafeMkSNumber \@n (fromInteger n)@, the result is either a valid
-- 'SNumber' or a type error.  In particular, the cases this rules out are
-- those where @toInteger (fromInteger n :: a) /= n@ or where
-- @fromInteger m :: a == fromInteger n@ does not imply @m == n@.
unsafeMkSNumber :: forall n a. SafeSNumber a n => a -> SNumber a n
unsafeMkSNumber :: a -> SNumber a n
unsafeMkSNumber = a -> SNumber a n
forall (n :: Integer) a. a -> SNumber a n
N#

-- | Create an 'SNumber' for @n@, if it's faithfully represented by @a@.
--
-- As with 'unsafeMkSNumber', this trusts you to pass @integerVal \@n@, and
-- violating that will lead to type unsoundness.
--
-- This tests at runtime whether @a@ represents @n@ correctly.
unsafeTryMkSNumber
  :: forall n a. SNumberRepr a => Integer -> Maybe (SNumber a n)
unsafeTryMkSNumber :: Integer -> Maybe (SNumber a n)
unsafeTryMkSNumber Integer
x =
  let x' :: a
x' = Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
x
  in  if a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
x then Maybe (SNumber a n)
forall a. Maybe a
Nothing else SNumber a n -> Maybe (SNumber a n)
forall a. a -> Maybe a
Just (a -> SNumber a n
forall (n :: Integer) a. a -> SNumber a n
N# a
x')
{-# INLINE unsafeTryMkSNumber #-}

-- | Create an 'SNumber' for @n@, with no safety measures whatsoever.
unsafeUncheckedMkSNumber :: forall n a. a -> SNumber a n
unsafeUncheckedMkSNumber :: a -> SNumber a n
unsafeUncheckedMkSNumber = a -> SNumber a n
forall (n :: Integer) a. a -> SNumber a n
N#

-- | Like 'KnownNat', but represented by @a@ instead of 'Natural'.
--
-- This is currently solved automatically from 'KnownNat' via runtime checks,
-- to ease migration (we can incrementally strengthen 'KnownNat' constraints to
-- 'KnownSNumber' constraints), but in the future it may be changed to use
-- 'SafeSNumber', which will rule out runtime failures but will require
-- additional proofs in order to solve via 'KnownNat'.  For statically known
-- 'Integer's, these proofs will be entirely automatic.
--
-- This class is meant to be used primarily in instance contexts; for
-- standalone functions, it's probably better to pass an 'SNumber' explicitly.
class KnownSNumber a n where
  -- | Implementation of 'snumberVal'.
  --
  -- This has an inconvenient type variable order because it derives from the
  -- order they appear in the class head; see 'snumberVal'.
  snumberVal_ :: SNumber a n
  default snumberVal_ :: (SNumberRepr a, KnownInteger n) => SNumber a n
  snumberVal_ = SNumber a n -> Maybe (SNumber a n) -> SNumber a n
forall a. a -> Maybe a -> a
fromMaybe (String -> SNumber a n
forall a. HasCallStack => String -> a
error String
"KnownSNumber: unrepresentable") Maybe (SNumber a n)
forall (n :: Integer) a.
(SNumberRepr a, KnownInteger n) =>
Maybe (SNumber a n)
trySNumber

-- TODO(awpr): GHC might helpfully simplify this to KnownInteger in inferred
-- type signatures, so we'll still end up passing Integers around and have
-- runtime type conversions?  But we only infer signatures for bindings in
-- let/where clauses, so presumably GHC will solve a 'KnownSNumber' using
-- either a 'KnownSNumber' or 'KnownInteger' instance that's already available,
-- thus doing the best we could do in context?
instance (SNumberRepr a, KnownInteger n) => KnownSNumber a n

-- | Get an 'SNumber' out of the context from 'KnownSNumber' or 'KnownNat'.
--
-- This has the number as its first type parameter, for TypeApplications
-- convenience.
snumberVal :: forall n a. KnownSNumber a n => SNumber a n
snumberVal :: SNumber a n
snumberVal = SNumber a n
forall a (n :: Integer). KnownSNumber a n => SNumber a n
snumberVal_

-- TODO(awpr): Expose these functions as GEq/GOrd instances.

-- | Compare two type-level 'Integer's using their runtime witnesses.
compareSNumber
  :: forall m n a. Ord a => SNumber a m -> SNumber a n -> OrderingI m n
compareSNumber :: SNumber a m -> SNumber a n -> OrderingI m n
compareSNumber (N# a
x) (N# a
y) = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
  Ordering
LT -> case (Any :~: Any) -> CmpInteger m n :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: CmpInteger m n :~: 'LT of CmpInteger m n :~: 'LT
Refl -> OrderingI m n
forall k (m :: k) (n :: k). (Compare m n ~ 'LT) => OrderingI m n
LTI
  Ordering
EQ ->
    case (Any :~: Any) -> CmpInteger m n :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: CmpInteger m n :~: 'EQ of
      CmpInteger m n :~: 'EQ
Refl -> case (Any :~: Any) -> m :~: n
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: m :~: n of
        m :~: n
Refl -> OrderingI m n
forall k (m :: k). (Compare m m ~ 'EQ) => OrderingI m m
EQI
  Ordering
GT -> case (Any :~: Any) -> CmpInteger m n :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: CmpInteger m n :~: 'GT of CmpInteger m n :~: 'GT
Refl -> OrderingI m n
forall k (m :: k) (n :: k). (Compare m n ~ 'GT) => OrderingI m n
GTI

-- | Test equality of two type-level 'Integer's using their runtime witnesses.
sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n)
sameSNumber :: SNumber a m -> SNumber a n -> Maybe (m :~: n)
sameSNumber (N# a
x) (N# a
y)
  | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y    = (m :~: n) -> Maybe (m :~: n)
forall a. a -> Maybe a
Just ((Any :~: Any) -> m :~: n
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
  | Bool
otherwise = Maybe (m :~: n)
forall a. Maybe a
Nothing

newtype c :=> a = CArr (c => a)

-- | Stash an 'SNumber' at the type level as a 'KnownSNumber' instance.
reifySNumber :: forall a n r. SNumber a n -> (KnownSNumber a n => r) -> r
reifySNumber :: SNumber a n -> (KnownSNumber a n => r) -> r
reifySNumber SNumber a n
n KnownSNumber a n => r
r = SNumber a n -> r
f SNumber a n
n
 where
  f :: SNumber a n -> r
  f :: SNumber a n -> r
f = (KnownSNumber a n :=> r) -> SNumber a n -> r
forall a b. a -> b
unsafeCoerce ((KnownSNumber a n => r) -> KnownSNumber a n :=> r
forall (c :: Constraint) a. (c => a) -> c :=> a
CArr KnownSNumber a n => r
r :: KnownSNumber a n :=> r)

-- | Use a positive 'SNumber' to introduce a 'KnownNat' instance.
reifySNumberAsNat
  :: forall n r a
   . Integral a
  => SNumber a ('Pos n) -> (KnownNat n => r) -> r
reifySNumberAsNat :: SNumber a ('Pos n) -> (KnownNat n => r) -> r
reifySNumberAsNat (N# a
x) KnownNat n => r
r = case Natural -> SomeNat
someNatVal (a -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x) of
  SomeNat (Proxy n
_ :: Proxy m) -> case (Any :~: Any) -> n :~: n
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: n :~: m of n :~: n
Refl -> r
KnownNat n => r
r

-- | An 'SNumber' with an existential 'K.Integer' type parameter.
data SomeSNumber a = forall n. SomeSNumber (SNumber a n)

-- | Create an @'SNumber' a@ from any value of type @a@.
--
-- Since 'SNumberRepr' guarantees every @a@ value is an integer, we can freely
-- wrap up a value in an 'SNumber' with existential 'K.Integer' type parameter.
someSNumberVal :: SNumberRepr a => a -> SomeSNumber a
someSNumberVal :: a -> SomeSNumber a
someSNumberVal a
x = a
-> (forall (n :: Integer). SNumber a n -> SomeSNumber a)
-> SomeSNumber a
forall a r.
SNumberRepr a =>
a -> (forall (n :: Integer). SNumber a n -> r) -> r
withSNumber a
x forall a (n :: Integer). SNumber a n -> SomeSNumber a
forall (n :: Integer). SNumber a n -> SomeSNumber a
SomeSNumber

-- | Like 'someSNumberVal', but in quantified CPS style rather than GADT style.
withSNumber :: SNumberRepr a => a -> (forall n. SNumber a n -> r) -> r
withSNumber :: a -> (forall (n :: Integer). SNumber a n -> r) -> r
withSNumber a
x forall (n :: Integer). SNumber a n -> r
r = SNumber a Any -> r
forall (n :: Integer). SNumber a n -> r
r (a -> SNumber a Any
forall (n :: Integer) a. a -> SNumber a n
N# a
x)

-- | Arithmetic ops with overflow detection.
--
-- Laws:
--
-- * @overflowAdd x y = (False, xy) =>
--      toInteger xy === toInteger x + toInteger y@
-- * @overflowSub x y = (False, xy) =>
--      toInteger xy === toInteger x - toInteger y@
-- * @overflowMul x y = (False, xy) =>
--      toInteger xy === toInteger x * toInteger y@
--
-- This is used for arithmetic on 'SNumber' runtime values, so creating
-- incorrect instances is type-unsafe.
class Integral a => OverflowArith a where
  overflowAdd :: a -> a -> (Bool, a)
  overflowSub :: a -> a -> (Bool, a)
  overflowMul :: a -> a -> (Bool, a)

instance OverflowArith Word where
  overflowAdd :: Word -> Word -> (Bool, Word)
overflowAdd (W# Word#
x) (W# Word#
y) =
    case Word# -> Word# -> (# Word#, Int# #)
addWordC# Word#
x Word#
y of (# Word#
xy, Int#
ovf #) -> (Int# -> Int
I# Int#
ovf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0, Word# -> Word
W# Word#
xy)
  overflowSub :: Word -> Word -> (Bool, Word)
overflowSub (W# Word#
x) (W# Word#
y) =
    case Word# -> Word# -> (# Word#, Int# #)
subWordC# Word#
x Word#
y of (# Word#
xy, Int#
ovf #) -> (Int# -> Int
I# Int#
ovf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0, Word# -> Word
W# Word#
xy)
  overflowMul :: Word -> Word -> (Bool, Word)
overflowMul (W# Word#
x) (W# Word#
y) =
    case Word# -> Word# -> (# Word#, Word# #)
timesWord2# Word#
x Word#
y of (# Word#
hi, Word#
lo #) -> (Word# -> Word
W# Word#
hi Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
0, Word# -> Word
W# Word#
lo)

instance OverflowArith Int where
  overflowAdd :: Int -> Int -> (Bool, Int)
overflowAdd (I# Int#
x) (I# Int#
y) =
    case Int# -> Int# -> (# Int#, Int# #)
addIntC# Int#
x Int#
y of (# Int#
xy, Int#
ovf #) -> (Int# -> Int
I# Int#
ovf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0, Int# -> Int
I# Int#
xy)
  overflowSub :: Int -> Int -> (Bool, Int)
overflowSub (I# Int#
x) (I# Int#
y) =
    case Int# -> Int# -> (# Int#, Int# #)
subIntC# Int#
x Int#
y of (# Int#
xy, Int#
ovf #) -> (Int# -> Int
I# Int#
ovf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0, Int# -> Int
I# Int#
xy)
  overflowMul :: Int -> Int -> (Bool, Int)
overflowMul (I# Int#
x) (I# Int#
y) =
    -- TODO(awpr): Newer versions of base have 'timesInt2#'; consider using CPP
    -- to use that when available.
    let xy :: Int
xy = Int# -> Int
I# (Int#
x Int# -> Int# -> Int#
*# Int#
y)
    in  case Int# -> Int# -> Int#
mulIntMayOflo# Int#
x Int#
y of
          Int#
ovf -> if Int# -> Int
I# Int#
ovf Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0
            then (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
xy Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# Int#
x) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int# -> Int
I# Int#
y), Int
xy)
            else (Bool
False, Int# -> Int
I# (Int#
x Int# -> Int# -> Int#
*# Int#
y))

instance OverflowArith Natural where
  overflowAdd :: Natural -> Natural -> (Bool, Natural)
overflowAdd Natural
x Natural
y = (Bool
False, Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
y)
  overflowSub :: Natural -> Natural -> (Bool, Natural)
overflowSub Natural
x Natural
y = (Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
y, Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
y)
  overflowMul :: Natural -> Natural -> (Bool, Natural)
overflowMul Natural
x Natural
y = (Bool
False, Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
y)

instance OverflowArith Integer where
  overflowAdd :: Integer -> Integer -> (Bool, Integer)
overflowAdd Integer
x Integer
y = (Bool
False, Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)
  overflowSub :: Integer -> Integer -> (Bool, Integer)
overflowSub Integer
x Integer
y = (Bool
False, Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  overflowMul :: Integer -> Integer -> (Bool, Integer)
overflowMul Integer
x Integer
y = (Bool
False, Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y)

-- Note: this internal helper function will make any SNumber result you want,
-- thus "unsafe".
unsafeMkTry
  :: (a -> a -> (Bool, a)) -> SNumber a n -> SNumber a m -> Maybe (SNumber a o)
unsafeMkTry :: (a -> a -> (Bool, a))
-> SNumber a n -> SNumber a m -> Maybe (SNumber a o)
unsafeMkTry a -> a -> (Bool, a)
f (N# a
x) (N# a
y) = case a -> a -> (Bool, a)
f a
x a
y of
  (Bool
True, a
_) -> Maybe (SNumber a o)
forall a. Maybe a
Nothing
  (Bool
False, a
xy) -> SNumber a o -> Maybe (SNumber a o)
forall a. a -> Maybe a
Just (a -> SNumber a o
forall (n :: Integer) a. a -> SNumber a n
N# a
xy)

-- | Compute a runtime witness of @m + n@, or 'Nothing'.
tryAdd
  :: (SNumberRepr a, OverflowArith a)
  => SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n))
tryAdd :: SNumber a m -> SNumber a n -> Maybe (SNumber a (m + n))
tryAdd = (a -> a -> (Bool, a))
-> SNumber a m -> SNumber a n -> Maybe (SNumber a (AddInteger m n))
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(a -> a -> (Bool, a))
-> SNumber a n -> SNumber a m -> Maybe (SNumber a o)
unsafeMkTry a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowAdd

-- | Compute a runtime witness of @m - n@, or 'Nothing'.
trySub
  :: (SNumberRepr a, OverflowArith a)
  => SNumber a m -> SNumber a n -> Maybe (SNumber a (m - n))
trySub :: SNumber a m -> SNumber a n -> Maybe (SNumber a (m - n))
trySub = (a -> a -> (Bool, a))
-> SNumber a m -> SNumber a n -> Maybe (SNumber a (SubInteger m n))
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(a -> a -> (Bool, a))
-> SNumber a n -> SNumber a m -> Maybe (SNumber a o)
unsafeMkTry a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowSub

-- | Compute a runtime witness of @m * n@, or 'Nothing'.
tryMul
  :: (SNumberRepr a, OverflowArith a)
  => SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n))
tryMul :: SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n))
tryMul = (a -> a -> (Bool, a))
-> SNumber a m -> SNumber a n -> Maybe (SNumber a (MulInteger m n))
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(a -> a -> (Bool, a))
-> SNumber a n -> SNumber a m -> Maybe (SNumber a o)
unsafeMkTry a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowMul

-- | An exception for overflows in checked 'SNumber' arithmetic.
data UnrepresentableSNumber = UnrepresentableSNumber String Integer Integer
  deriving Int -> UnrepresentableSNumber -> ShowS
[UnrepresentableSNumber] -> ShowS
UnrepresentableSNumber -> String
(Int -> UnrepresentableSNumber -> ShowS)
-> (UnrepresentableSNumber -> String)
-> ([UnrepresentableSNumber] -> ShowS)
-> Show UnrepresentableSNumber
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnrepresentableSNumber] -> ShowS
$cshowList :: [UnrepresentableSNumber] -> ShowS
show :: UnrepresentableSNumber -> String
$cshow :: UnrepresentableSNumber -> String
showsPrec :: Int -> UnrepresentableSNumber -> ShowS
$cshowsPrec :: Int -> UnrepresentableSNumber -> ShowS
Show

instance Exception UnrepresentableSNumber

-- Note: this internal helper function will make any SNumber result you want,
-- thus "unsafe".
unsafeMkChk
  :: (HasCallStack, Integral a)
  => String
  -> (a -> a -> (Bool, a)) -> SNumber a n -> SNumber a m -> SNumber a o
unsafeMkChk :: String
-> (a -> a -> (Bool, a))
-> SNumber a n
-> SNumber a m
-> SNumber a o
unsafeMkChk String
s a -> a -> (Bool, a)
f (N# a
x) (N# a
y) = case a -> a -> (Bool, a)
f a
x a
y of
  (Bool
True, a
_) -> UnrepresentableSNumber -> SNumber a o
forall a e. Exception e => e -> a
throw (String -> Integer -> Integer -> UnrepresentableSNumber
UnrepresentableSNumber String
s (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
y))
  (Bool
False, a
xy) -> a -> SNumber a o
forall (n :: Integer) a. a -> SNumber a n
N# a
xy

-- | Compute a runtime witness of @m + n@, or throw.
chkAdd
  :: (SNumberRepr a, OverflowArith a, HasCallStack)
  => SNumber a m -> SNumber a n -> SNumber a (m + n)
chkAdd :: SNumber a m -> SNumber a n -> SNumber a (m + n)
chkAdd = (HasCallStack =>
 String
 -> (a -> a -> (Bool, a))
 -> SNumber a m
 -> SNumber a n
 -> SNumber a (AddInteger m n))
-> String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (AddInteger m n)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (AddInteger m n)
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(HasCallStack, Integral a) =>
String
-> (a -> a -> (Bool, a))
-> SNumber a n
-> SNumber a m
-> SNumber a o
unsafeMkChk String
"+" a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowAdd

-- | Compute a runtime witness of @m - n@, or throw.
chkSub
  :: (SNumberRepr a, OverflowArith a, HasCallStack)
  => SNumber a m -> SNumber a n -> SNumber a (m - n)
chkSub :: SNumber a m -> SNumber a n -> SNumber a (m - n)
chkSub = (HasCallStack =>
 String
 -> (a -> a -> (Bool, a))
 -> SNumber a m
 -> SNumber a n
 -> SNumber a (SubInteger m n))
-> String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (SubInteger m n)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (SubInteger m n)
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(HasCallStack, Integral a) =>
String
-> (a -> a -> (Bool, a))
-> SNumber a n
-> SNumber a m
-> SNumber a o
unsafeMkChk String
"-" a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowSub

-- | Compute a runtime witness of @m * n@, or throw.
chkMul
  :: (SNumberRepr a, OverflowArith a, HasCallStack)
  => SNumber a m -> SNumber a n -> SNumber a (m * n)
chkMul :: SNumber a m -> SNumber a n -> SNumber a (m * n)
chkMul = (HasCallStack =>
 String
 -> (a -> a -> (Bool, a))
 -> SNumber a m
 -> SNumber a n
 -> SNumber a (MulInteger m n))
-> String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (MulInteger m n)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack HasCallStack =>
String
-> (a -> a -> (Bool, a))
-> SNumber a m
-> SNumber a n
-> SNumber a (MulInteger m n)
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(HasCallStack, Integral a) =>
String
-> (a -> a -> (Bool, a))
-> SNumber a n
-> SNumber a m
-> SNumber a o
unsafeMkChk String
"*" a -> a -> (Bool, a)
forall a. OverflowArith a => a -> a -> (Bool, a)
overflowMul

-- | Compute a runtime witness of exact division.
--
-- We could provide division in terms of 'GHC.TypeNats.Div' instead, but
-- "Kinds.Integer" doesn't currently have division.
divExact :: SNumberRepr a => SNumber a (m * n) -> SNumber a n -> SNumber a m
divExact :: SNumber a (m * n) -> SNumber a n -> SNumber a m
divExact = String
-> (a -> a -> (Bool, a))
-> SNumber a (MulInteger m n)
-> SNumber a n
-> SNumber a m
forall a (n :: Integer) (m :: Integer) (o :: Integer).
(HasCallStack, Integral a) =>
String
-> (a -> a -> (Bool, a))
-> SNumber a n
-> SNumber a m
-> SNumber a o
unsafeMkChk String
"/" (\a
x a
y -> (Bool
False, a
x a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
y))