{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MagicHash                 #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE Trustworthy               #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

{-|
Module: Data.TypeNums.Ints
Copyright: (c) 2018-2021 Iris Ward
License: BSD3
Maintainer: aditu.venyhandottir@gmail.com
Stability: experimental

Type level integers can be used in the same way as type level naturals
from "GHC.TypeLits", for example @3@.  However, a minus sign is not
recognised in this context, so a negative type-level integer is instead
written as @'Neg' n@.
-}
module Data.TypeNums.Ints
  ( -- * Construction
    TInt(..)
    -- * Linking type and value level
  , KnownInt
  , intVal
  , intVal'
  , SomeInt(..)
  , someIntVal
  ) where

import Data.Bifunctor (first)
import Data.Proxy     (Proxy (..))
import GHC.Exts       (Proxy#, proxy#)
import GHC.TypeLits   (KnownNat, Nat, natVal')
import Unsafe.Coerce  (unsafeCoerce)

newtype SInt (n :: k) =
  SInt Integer

-- | (Kind) An integer that may be negative.
data TInt
  = Pos Nat
  | Neg Nat

-- | This class gives the (value-level) integer associated with a type-level
--   integer.  There are instances of this class for every concrete natural:
--   0, 1, 2, etc.  There are also instances of this class for every negated
--   natural, such as @'Neg' 1@.
class KnownInt (n :: k) where
  intSing :: SInt n

instance forall (n :: Nat). KnownNat n => KnownInt n where
  intSing :: SInt n
intSing = Integer -> SInt n
forall k (n :: k). Integer -> SInt n
SInt (Integer -> SInt n) -> Integer -> SInt n
forall a b. (a -> b) -> a -> b
$! Proxy# n -> Integer
forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n)

instance forall (n :: Nat). KnownNat n => KnownInt ('Pos n) where
  intSing :: SInt ('Pos n)
intSing = Integer -> SInt ('Pos n)
forall k (n :: k). Integer -> SInt n
SInt (Integer -> SInt ('Pos n)) -> Integer -> SInt ('Pos n)
forall a b. (a -> b) -> a -> b
$! Proxy# n -> Integer
forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n)

instance forall (n :: Nat). KnownNat n => KnownInt ('Neg n) where
  intSing :: SInt ('Neg n)
intSing = Integer -> SInt ('Neg n)
forall k (n :: k). Integer -> SInt n
SInt (Integer -> SInt ('Neg n)) -> Integer -> SInt ('Neg n)
forall a b. (a -> b) -> a -> b
$! Integer -> Integer
forall a. Num a => a -> a
negate (Proxy# n -> Integer
forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n))


-- | Get the value associated with a type-level integer
intVal ::
     forall n proxy. KnownInt n
  => proxy n
  -> Integer
intVal :: proxy n -> Integer
intVal proxy n
_ =
  case SInt n
forall k (n :: k). KnownInt n => SInt n
intSing :: SInt n of
    SInt Integer
x -> Integer
x

-- | Get the value associated with a type-level integer.  The difference
--   between this function and 'intVal' is that it takes a 'Proxy#' parameter,
--   which has zero runtime representation and so is entirely free.
intVal' ::
     forall n. KnownInt n
  => Proxy# n
  -> Integer
intVal' :: Proxy# n -> Integer
intVal' Proxy# n
_ =
  case SInt n
forall k (n :: k). KnownInt n => SInt n
intSing :: SInt n of
    SInt Integer
x -> Integer
x

-- | This type represents unknown type-level integers.
--
-- @since 0.1.1
data SomeInt =
  forall n. KnownInt n =>
            SomeInt (Proxy n)

instance Eq SomeInt where
  SomeInt Proxy n
x == :: SomeInt -> SomeInt -> Bool
== SomeInt Proxy n
y = Proxy n -> Integer
forall k (n :: k) (proxy :: k -> *).
KnownInt n =>
proxy n -> Integer
intVal Proxy n
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Integer
forall k (n :: k) (proxy :: k -> *).
KnownInt n =>
proxy n -> Integer
intVal Proxy n
y

instance Ord SomeInt where
  compare :: SomeInt -> SomeInt -> Ordering
compare (SomeInt Proxy n
x) (SomeInt Proxy n
y) = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Integer
forall k (n :: k) (proxy :: k -> *).
KnownInt n =>
proxy n -> Integer
intVal Proxy n
x) (Proxy n -> Integer
forall k (n :: k) (proxy :: k -> *).
KnownInt n =>
proxy n -> Integer
intVal Proxy n
y)

instance Show SomeInt where
  showsPrec :: Int -> SomeInt -> ShowS
showsPrec Int
p (SomeInt Proxy n
x) = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Integer
forall k (n :: k) (proxy :: k -> *).
KnownInt n =>
proxy n -> Integer
intVal Proxy n
x)

instance Read SomeInt where
  readsPrec :: Int -> ReadS SomeInt
readsPrec Int
p String
xs = (Integer -> SomeInt) -> (Integer, String) -> (SomeInt, String)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Integer -> SomeInt
someIntVal ((Integer, String) -> (SomeInt, String))
-> [(Integer, String)] -> [(SomeInt, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReadS Integer
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs

-- $impl
-- Implementation notes:
--   * A typeclass on a data constructor is represented internally as an extra
--     field on the data constructor containing the typeclass dictionary. This
--     field occurs before the other fields.
--   * A dictionary for the KnownInt typeclass is represented as just an SInt
--     value on its own, as there is only one member of the typeclass, and that
--     member is not a function.
--
-- someIntVal therefore constructs a datatype with the same representation as
-- the existentially qualified constructor SomeInt, then uses unsafeCoerce to
-- produce the SomeInt value.

data SomeIntWithDict =
  forall n. SomeIntWithDict (SInt n)
                            (Proxy n)

-- | Convert an integer into an unknown type-level integer.
--
-- @since 0.1.1
someIntVal :: Integer -> SomeInt
someIntVal :: Integer -> SomeInt
someIntVal Integer
x = SomeIntWithDict -> SomeInt
forall a b. a -> b
unsafeCoerce (SomeIntWithDict -> SomeInt) -> SomeIntWithDict -> SomeInt
forall a b. (a -> b) -> a -> b
$ SInt Any -> Proxy Any -> SomeIntWithDict
forall k (n :: k). SInt n -> Proxy n -> SomeIntWithDict
SomeIntWithDict (Integer -> SInt Any
forall k (n :: k). Integer -> SInt n
SInt Integer
x) Proxy Any
forall k (t :: k). Proxy t
Proxy