{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
#if !defined(__HLINT__)
{-# LANGUAGE StandaloneDeriving #-}
#endif
module DependentLiterals.Int
(
HasIntLiterals(..), valueOf
, HasBasicLiterals, AllowsIntLiteral, IntLiteral
, StockLit(..)
, SNum(..), Satisfying(..), SNumLit(..)
, type (-#), CMaybe(..)
, lit#, match#
, NoAssertion
) where
import Data.Functor.Const (Const(..))
import Data.Functor.Identity (Identity(..))
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy(..))
import Data.Ratio (Ratio)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Semigroup (Sum(..), Product(..), Min(..), Max(..))
import Data.Type.Equality ((:~:)(..))
import Foreign.C.Types
( CChar, CSChar, CUChar, CWchar
, CShort, CUShort, CInt, CUInt, CLong, CULong, CLLong, CULLong
, CPtrdiff, CSize, CSigAtomic, CBool
, CIntPtr, CUIntPtr, CIntMax, CUIntMax
, CClock, CTime, CUSeconds, CSUSeconds
)
import GHC.TypeLits (TypeError, ErrorMessage(..))
import GHC.TypeNats (Nat)
import Numeric.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)
import Data.Tagged (Tagged(..))
import Data.SInt (SInt(SI#, unSInt))
import Data.SNumber (SafeSNumber, SNumber(N#), sameSNumber, unsafeMkSNumber)
import Kinds.Integer (type (-#), KnownInteger(..), pattern Pos)
import Kinds.Num (type (>=), type (<), Cmp, ToInteger)
import qualified Kinds.Integer as K (Integer)
import Data.Fin.Int (Fin, finToInt, unsafeFin)
import DependentLiterals.Bounds
( CheckAtLeastMinBound, CheckLessThanMaxBound
, AssertEq, OutOfRangeMsg, ShowTypedNum
)
data Satisfying c t = forall x. c x => Satisfying (t x)
data CMaybe c = c => CJust | CNothing
class SNum a where
type SNumRepr a :: Type
type SNumConstraint a :: K.Integer -> Constraint
fromSNum :: Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a
intoSNum :: a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))
instance SNum (SInt n) where
type SNumRepr (SInt n) = Int
#if !defined(__HLINT__)
type SNumConstraint (SInt n) = (~) ('Pos n)
#endif
fromSNum :: Satisfying (SNumConstraint (SInt n)) (SNumber (SNumRepr (SInt n)))
-> SInt n
fromSNum (Satisfying (N# x)) = Int -> SInt n
forall (n :: Nat). Int -> SInt n
SI# Int
x
intoSNum :: SInt n
-> Satisfying
(SNumConstraint (SInt n)) (SNumber (SNumRepr (SInt n)))
intoSNum SInt n
x = SNumber Int ('Pos n) -> Satisfying ((~) ('Pos n)) (SNumber Int)
forall k (c :: k -> Constraint) (t :: k -> *) (x :: k).
c x =>
t x -> Satisfying c t
Satisfying (Int -> SNumber Int ('Pos n)
forall (n :: Integer) a. a -> SNumber a n
N# @('Pos n) (SInt n -> Int
forall (n :: Nat). SInt n -> Int
unSInt SInt n
x))
instance SNum (SNumber a n) where
type SNumRepr (SNumber a n) = a
#if !defined(__HLINT__)
type SNumConstraint (SNumber a n) = (~) n
#endif
fromSNum :: Satisfying
(SNumConstraint (SNumber a n)) (SNumber (SNumRepr (SNumber a n)))
-> SNumber a n
fromSNum (Satisfying SNumber (SNumRepr (SNumber a n)) x
x) = SNumber a n
SNumber (SNumRepr (SNumber a n)) x
x
intoSNum :: SNumber a n
-> Satisfying
(SNumConstraint (SNumber a n)) (SNumber (SNumRepr (SNumber a n)))
intoSNum = SNumber a n
-> Satisfying
(SNumConstraint (SNumber a n)) (SNumber (SNumRepr (SNumber a n)))
forall k (c :: k -> Constraint) (t :: k -> *) (x :: k).
c x =>
t x -> Satisfying c t
Satisfying
class (Cmp n ('Pos m) ~ 'LT, n >= 'Pos 0)
=> FinInBounds (m :: Nat) (n :: K.Integer)
instance (Cmp n ('Pos m) ~ 'LT, n >= 'Pos 0) => FinInBounds m n
instance SNum (Fin n) where
type SNumRepr (Fin n) = Int
type SNumConstraint (Fin n) = FinInBounds n
fromSNum :: Satisfying (SNumConstraint (Fin n)) (SNumber (SNumRepr (Fin n)))
-> Fin n
fromSNum (Satisfying (N# x)) = Int -> Fin n
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin Int
x
intoSNum :: Fin n
-> Satisfying (SNumConstraint (Fin n)) (SNumber (SNumRepr (Fin n)))
intoSNum Fin n
x = Satisfying NoConstraint (SNumber Int)
-> Satisfying (FinInBounds n) (SNumber Int)
forall a b. a -> b
unsafeCoerce (SNumber Int Any -> Satisfying NoConstraint (SNumber Int)
forall k (c :: k -> Constraint) (t :: k -> *) (x :: k).
c x =>
t x -> Satisfying c t
Satisfying @NoConstraint (Int -> SNumber Int Any
forall (n :: Integer) a. a -> SNumber a n
N# (Fin n -> Int
forall (n :: Nat). Fin n -> Int
finToInt Fin n
x)))
class HasIntLiterals a where
type ReprAssertion a :: Type -> K.Integer -> Constraint
type LitConstraint a :: K.Integer -> Constraint
type LitAssertion a :: Type -> K.Integer -> Constraint
unsafeFromInteger
:: forall n b
. (LitAssertion a b n, ReprAssertion a b n)
=> Proxy b -> Tagged n Integer -> a
unsafeMatchInteger
:: forall n b
. ReprAssertion a b n
=> Proxy b -> Tagged n Integer -> a -> CMaybe (LitConstraint a n)
type HasBasicLiterals a =
( HasIntLiterals a
, LitAssertion a ~ NoAssertion
, ReprAssertion a ~ NoAssertion
)
type AllowsIntLiteral n a =
( LitAssertion a a (ToInteger n)
, ReprAssertion a a (ToInteger n)
)
type IntLiteral n a = (HasIntLiterals a, AllowsIntLiteral n a)
lit#
:: forall n a
. (HasIntLiterals a, ReprAssertion a a n, LitAssertion a a n)
=> (Num a => a) -> Integer -> a
lit# :: (Num a => a) -> Integer -> a
lit# Num a => a
_ = Proxy a -> Tagged n Integer -> a
forall a (n :: Integer) b.
(HasIntLiterals a, LitAssertion a b n, ReprAssertion a b n) =>
Proxy b -> Tagged n Integer -> a
unsafeFromInteger (Proxy a
forall k (t :: k). Proxy t
Proxy @a) (Tagged n Integer -> a)
-> (Integer -> Tagged n Integer) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. b -> Tagged n b
forall k (s :: k) b. b -> Tagged s b
Tagged @n
match#
:: forall n a
. (HasIntLiterals a, ReprAssertion a a n)
=> (Num a => a) -> Integer -> a -> CMaybe (LitConstraint a n)
match# :: (Num a => a) -> Integer -> a -> CMaybe (LitConstraint a n)
match# Num a => a
_ = Proxy a -> Tagged n Integer -> a -> CMaybe (LitConstraint a n)
forall a (n :: Integer) b.
(HasIntLiterals a, ReprAssertion a b n) =>
Proxy b -> Tagged n Integer -> a -> CMaybe (LitConstraint a n)
unsafeMatchInteger (Proxy a
forall k (t :: k). Proxy t
Proxy @a) (Tagged n Integer -> a -> CMaybe (LitConstraint a n))
-> (Integer -> Tagged n Integer)
-> Integer
-> a
-> CMaybe (LitConstraint a n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. b -> Tagged n b
forall k (s :: k) b. b -> Tagged s b
Tagged @n
valueOf' :: forall n a. (IntLiteral n a, KnownInteger n) => a
valueOf' :: a
valueOf' = Proxy a -> Tagged n Integer -> a
forall a (n :: Integer) b.
(HasIntLiterals a, LitAssertion a b n, ReprAssertion a b n) =>
Proxy b -> Tagged n Integer -> a
unsafeFromInteger (Proxy a
forall k (t :: k). Proxy t
Proxy @a) (forall b. b -> Tagged n b
forall k (s :: k) b. b -> Tagged s b
Tagged @n (Integer -> Tagged n Integer) -> Integer -> Tagged n Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ KnownInteger n => Integer
forall (n :: Integer). KnownInteger n => Integer
integerVal @n)
valueOf
:: forall n a
. (IntLiteral (ToInteger n) a, KnownInteger (ToInteger n))
=> a
valueOf :: a
valueOf = forall a.
(IntLiteral (ToInteger n) a, KnownInteger (ToInteger n)) =>
a
forall (n :: Integer) a. (IntLiteral n a, KnownInteger n) => a
valueOf' @(ToInteger n)
newtype SNumLit (c :: Type -> K.Integer -> Constraint) a = SNumLit a
class SNumConstraint a n => SNumLitAssertion c a b n
#if !defined(__HLINT__)
instance (c b n, cc ~ SNumConstraint a, forall m. c b m => cc m)
=> SNumLitAssertion c a b n
#endif
class SafeSNumber repr n => SNumReprAssertion repr b n
instance SafeSNumber repr n => SNumReprAssertion repr b n
instance (Eq (SNumRepr a), Num (SNumRepr a), SNum a)
=> HasIntLiterals (SNumLit c a) where
type ReprAssertion (SNumLit c a) = SNumReprAssertion (SNumRepr a)
type LitAssertion (SNumLit c a) = SNumLitAssertion c a
type LitConstraint (SNumLit c a) = SNumConstraint a
unsafeFromInteger :: Proxy b -> Tagged n Integer -> SNumLit c a
unsafeFromInteger (Proxy b
_ :: Proxy b) (Tagged Integer
n :: Tagged n Integer) =
a -> SNumLit c a
forall (c :: * -> Integer -> Constraint) a. a -> SNumLit c a
SNumLit (a -> SNumLit c a) -> a -> SNumLit c a
forall a b. (a -> b) -> a -> b
$ Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a
forall a.
SNum a =>
Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a
fromSNum (Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a)
-> Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a
forall a b. (a -> b) -> a -> b
$ SNumber (SNumRepr a) n
-> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))
forall k (c :: k -> Constraint) (t :: k -> *) (x :: k).
c x =>
t x -> Satisfying c t
Satisfying (SNumRepr a -> SNumber (SNumRepr a) n
forall (n :: Integer) a. SafeSNumber a n => a -> SNumber a n
unsafeMkSNumber @n (Integer -> SNumRepr a
forall a. Num a => Integer -> a
fromInteger Integer
n))
unsafeMatchInteger :: Proxy b
-> Tagged n Integer
-> SNumLit c a
-> CMaybe (LitConstraint (SNumLit c a) n)
unsafeMatchInteger (Proxy b
_ :: Proxy b) (Tagged Integer
n :: Tagged n Integer) (SNumLit a
a) =
case a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))
forall a.
SNum a =>
a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))
intoSNum a
a of
Satisfying SNumber (SNumRepr a) x
m ->
case SNumber (SNumRepr a) n -> SNumber (SNumRepr a) x -> Maybe (n :~: x)
forall a (m :: Integer) (n :: Integer).
Eq a =>
SNumber a m -> SNumber a n -> Maybe (m :~: n)
sameSNumber (SNumRepr a -> SNumber (SNumRepr a) n
forall (n :: Integer) a. SafeSNumber a n => a -> SNumber a n
unsafeMkSNumber @n (Integer -> SNumRepr a
forall a. Num a => Integer -> a
fromInteger Integer
n)) SNumber (SNumRepr a) x
m of
Just n :~: x
Refl -> CMaybe (LitConstraint (SNumLit c a) n)
forall (c :: Constraint). c => CMaybe c
CJust
Maybe (n :~: x)
Nothing -> CMaybe (LitConstraint (SNumLit c a) n)
forall (c :: Constraint). CMaybe c
CNothing
newtype StockLit a = StockLit a
class NoConstraint (a :: k)
instance NoConstraint a
class NoAssertion (a :: Type) (n :: K.Integer)
instance NoAssertion a n
instance (Eq a, Num a) => HasIntLiterals (StockLit a) where
type ReprAssertion (StockLit a) = NoAssertion
type LitConstraint (StockLit a) = NoConstraint
type LitAssertion (StockLit a) = NoAssertion
unsafeFromInteger :: Proxy b -> Tagged n Integer -> StockLit a
unsafeFromInteger Proxy b
_ (Tagged Integer
n) = a -> StockLit a
forall a. a -> StockLit a
StockLit (Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
n)
unsafeMatchInteger :: Proxy b
-> Tagged n Integer
-> StockLit a
-> CMaybe (LitConstraint (StockLit a) n)
unsafeMatchInteger Proxy b
_ (Tagged Integer
n) (StockLit a
a) = if Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
then CMaybe (LitConstraint (StockLit a) n)
forall (c :: Constraint). c => CMaybe c
CJust
else CMaybe (LitConstraint (StockLit a) n)
forall (c :: Constraint). CMaybe c
CNothing
class n ~ m => SIntLitAssertion (m :: K.Integer) (a :: Type) (n :: K.Integer)
instance AssertEq
(TypeError
('Text "SInt literal value does not match " ':<>:
'Text "expected type index:" ':$$:
'Text " " ':<>: ShowTypedNum a n))
n
m
=> SIntLitAssertion m a n
class (n >= 'Pos 0, n < 'Pos m) => FinLitAssertion m a n
instance ( CheckLessThanMaxBound
(OutOfRangeMsg ('Pos 0) ('Pos m) a n)
('Pos m)
a
n
, CheckAtLeastMinBound
(OutOfRangeMsg ('Pos 0) ('Pos m) a n)
('Pos 0)
a
n
)
=> FinLitAssertion m a n
#if !defined(__HLINT__)
deriving via SNumLit (SIntLitAssertion ('Pos n)) (SInt n)
instance HasIntLiterals (SInt n)
deriving via SNumLit (SIntLitAssertion n) (SNumber a n)
instance (Eq a, Num a) => HasIntLiterals (SNumber a n)
deriving via SNumLit (FinLitAssertion n) (Fin n) instance HasIntLiterals (Fin n)
deriving via StockLit Integer instance HasIntLiterals Integer
deriving via StockLit Natural instance HasIntLiterals Natural
deriving via StockLit (Ratio a) instance Integral a => HasIntLiterals (Ratio a)
deriving via StockLit Int instance HasIntLiterals Int
deriving via StockLit Int8 instance HasIntLiterals Int8
deriving via StockLit Int16 instance HasIntLiterals Int16
deriving via StockLit Int32 instance HasIntLiterals Int32
deriving via StockLit Int64 instance HasIntLiterals Int64
deriving via StockLit Word instance HasIntLiterals Word
deriving via StockLit Word8 instance HasIntLiterals Word8
deriving via StockLit Word16 instance HasIntLiterals Word16
deriving via StockLit Word32 instance HasIntLiterals Word32
deriving via StockLit Word64 instance HasIntLiterals Word64
deriving via StockLit Float instance HasIntLiterals Float
deriving via StockLit Double instance HasIntLiterals Double
deriving via StockLit (Sum a)
instance (Eq a, Num a) => HasIntLiterals (Sum a)
deriving via StockLit (Product a)
instance (Eq a, Num a) => HasIntLiterals (Product a)
deriving via StockLit (Min a)
instance (Eq a, Num a) => HasIntLiterals (Min a)
deriving via StockLit (Max a)
instance (Eq a, Num a) => HasIntLiterals (Max a)
deriving via StockLit (Const a b)
instance (Eq a, Num a) => HasIntLiterals (Const a b)
deriving via StockLit (Identity a)
instance (Eq a, Num a) => HasIntLiterals (Identity a)
deriving via StockLit CChar instance HasIntLiterals CChar
deriving via StockLit CSChar instance HasIntLiterals CSChar
deriving via StockLit CUChar instance HasIntLiterals CUChar
deriving via StockLit CShort instance HasIntLiterals CShort
deriving via StockLit CUShort instance HasIntLiterals CUShort
deriving via StockLit CInt instance HasIntLiterals CInt
deriving via StockLit CUInt instance HasIntLiterals CUInt
deriving via StockLit CLong instance HasIntLiterals CLong
deriving via StockLit CULong instance HasIntLiterals CULong
deriving via StockLit CPtrdiff instance HasIntLiterals CPtrdiff
deriving via StockLit CSize instance HasIntLiterals CSize
deriving via StockLit CWchar instance HasIntLiterals CWchar
deriving via StockLit CSigAtomic instance HasIntLiterals CSigAtomic
deriving via StockLit CLLong instance HasIntLiterals CLLong
deriving via StockLit CULLong instance HasIntLiterals CULLong
deriving via StockLit CBool instance HasIntLiterals CBool
deriving via StockLit CIntPtr instance HasIntLiterals CIntPtr
deriving via StockLit CUIntPtr instance HasIntLiterals CUIntPtr
deriving via StockLit CIntMax instance HasIntLiterals CIntMax
deriving via StockLit CUIntMax instance HasIntLiterals CUIntMax
deriving via StockLit CClock instance HasIntLiterals CClock
deriving via StockLit CTime instance HasIntLiterals CTime
deriving via StockLit CUSeconds instance HasIntLiterals CUSeconds
deriving via StockLit CSUSeconds instance HasIntLiterals CSUSeconds
#endif