{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module GHC.TypeLits.Singletons.Internal (
Sing,
Natural, TL.Symbol, Char,
TN.SNat, pattern TN.SNat,
TL.SSymbol, pattern TL.SSymbol, pattern SSym,
TL.SChar, pattern TL.SChar,
TN.withKnownNat, TL.withKnownSymbol, TL.withKnownChar,
Error, sError,
ErrorWithoutStackTrace, sErrorWithoutStackTrace,
Undefined, sUndefined,
TL.KnownNat, TN.natVal, TL.KnownSymbol, TL.symbolVal, TL.KnownChar, TL.charVal,
type (TN.^), (%^),
type (TN.<=?), (%<=?),
ErrorSym0, ErrorSym1,
ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
UndefinedSym0,
type (^@#@$), type (^@#@$$), type (^@#@$$$),
type (<=?@#@$), type (<=?@#@$$), type (<=?@#@$$$)
) where
import Data.Bool.Singletons
import Data.Eq.Singletons
import Data.Ord.Singletons as O
import Data.Semigroup.Singletons.Internal.Classes
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import Data.Type.Equality (TestEquality(..))
import GHC.Stack (HasCallStack)
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
import Numeric.Natural (Natural)
import Unsafe.Coerce
import qualified Data.Text as T
import Data.Text ( Text )
type instance Sing = TN.SNat
instance TN.KnownNat n => SingI n where
sing :: Sing n
sing = Sing n
SNat n
forall (n :: Nat). KnownNat n => SNat n
TN.natSing
instance SingKind Natural where
type Demote Natural = Natural
fromSing :: forall (a :: Nat). Sing a -> Demote Nat
fromSing = Sing a -> Demote Nat
SNat a -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat
toSing :: Demote Nat -> SomeSing Nat
toSing Demote Nat
n = Nat -> (forall (n :: Nat). SNat n -> SomeSing Nat) -> SomeSing Nat
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat Nat
Demote Nat
n Sing n -> SomeSing Nat
SNat n -> SomeSing Nat
forall (n :: Nat). SNat n -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing
type instance Sing = TL.SSymbol
pattern SSym :: forall s. () => TL.KnownSymbol s => TL.SSymbol s
pattern $mSSym :: forall {r} {s :: Symbol}.
SSymbol s -> (KnownSymbol s => r) -> ((# #) -> r) -> r
$bSSym :: forall (s :: Symbol). KnownSymbol s => SSymbol s
SSym = TL.SSymbol
{-# COMPLETE SSym #-}
instance TL.KnownSymbol n => SingI n where
sing :: Sing n
sing = Sing n
SSymbol n
forall (s :: Symbol). KnownSymbol s => SSymbol s
TL.symbolSing
instance SingKind TL.Symbol where
type Demote TL.Symbol = Text
fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol
fromSing = String -> Text
T.pack (String -> Text) -> (SSymbol a -> String) -> SSymbol a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SSymbol a -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol
toSing :: Demote Symbol -> SomeSing Symbol
toSing Demote Symbol
s = String
-> (forall (s :: Symbol). SSymbol s -> SomeSing Symbol)
-> SomeSing Symbol
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
TL.withSomeSSymbol (Text -> String
T.unpack Demote Symbol
Text
s) Sing s -> SomeSing Symbol
SSymbol s -> SomeSing Symbol
forall k (a :: k). Sing a -> SomeSing k
forall (s :: Symbol). SSymbol s -> SomeSing Symbol
SomeSing
type instance Sing = TL.SChar
instance TL.KnownChar c => SingI c where
sing :: Sing c
sing = Sing c
SChar c
forall (n :: Char). KnownChar n => SChar n
TL.charSing
instance SingKind Char where
type Demote Char = Char
fromSing :: forall (a :: Char). Sing a -> Demote Char
fromSing = Sing a -> Demote Char
SChar a -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar
toSing :: Demote Char -> SomeSing Char
toSing Demote Char
c = Char
-> (forall (c :: Char). SChar c -> SomeSing Char) -> SomeSing Char
forall r. Char -> (forall (c :: Char). SChar c -> r) -> r
TL.withSomeSChar Char
Demote Char
c Sing c -> SomeSing Char
SChar c -> SomeSing Char
forall (c :: Char). SChar c -> SomeSing Char
forall k (a :: k). Sing a -> SomeSing k
SomeSing
instance SDecide Natural where
Sing a
sn %~ :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
| Just a :~: b
r <- SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing a
SNat a
sn Sing b
SNat b
sm
= (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
| Bool
otherwise
= Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
where errStr :: String
errStr = String
"Broken Natural singletons"
instance SDecide TL.Symbol where
Sing a
sn %~ :: forall (a :: Symbol) (b :: Symbol).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
| Just a :~: b
r <- SSymbol a -> SSymbol b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality Sing a
SSymbol a
sn Sing b
SSymbol b
sm
= (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
| Bool
otherwise
= Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
where errStr :: String
errStr = String
"Broken TL.Symbol singletons"
instance SDecide Char where
Sing a
sn %~ :: forall (a :: Char) (b :: Char).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
sm
| Just a :~: b
r <- SChar a -> SChar b -> Maybe (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing a
SChar a
sn Sing b
SChar b
sm
= (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: b
r
| Bool
otherwise
= Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
errStr)
where errStr :: String
errStr = String
"Broken Char singletons"
instance PEq Natural where
type x == y = DefaultEq x y
instance PEq TL.Symbol where
type x == y = DefaultEq x y
instance PEq Char where
type x == y = DefaultEq x y
instance SEq Natural where
Sing t1
sn %== :: forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
= case SNat t1 -> SNat t2 -> Maybe (t1 :~: t2)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing t1
SNat t1
sn Sing t2
SNat t2
sm of
Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
Maybe (t1 :~: t2)
Nothing -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
instance SEq TL.Symbol where
Sing t1
sn %== :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
= case SSymbol t1 -> SSymbol t2 -> Maybe (t1 :~: t2)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality Sing t1
SSymbol t1
sn Sing t2
SSymbol t2
sm of
Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
Maybe (t1 :~: t2)
Nothing -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
instance SEq Char where
Sing t1
sn %== :: forall (t1 :: Char) (t2 :: Char).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sm
= case SChar t1 -> SChar t2 -> Maybe (t1 :~: t2)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Sing t1
SChar t1
sn Sing t2
SChar t2
sm of
Just t1 :~: t2
Refl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
Maybe (t1 :~: t2)
Nothing -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
instance POrd Natural where
type (a :: Natural) `Compare` (b :: Natural) = a `TN.CmpNat` b
instance POrd TL.Symbol where
type (a :: TL.Symbol) `Compare` (b :: TL.Symbol) = a `TL.CmpSymbol` b
instance POrd Char where
type (a :: Char) `Compare` (b :: Char) = a `TL.CmpChar` b
instance SOrd Natural where
Sing t1
a sCompare :: forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t1
a Demote Nat -> Demote Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t2
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
instance SOrd TL.Symbol where
Sing t1
a sCompare :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t1
a Demote Symbol -> Demote Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t2
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpSymbol t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
instance SOrd Char where
Sing t1
a sCompare :: forall (t1 :: Char) (t2 :: Char).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing t2
b = case Sing t1 -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t1
a Demote Char -> Demote Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t2 -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t2
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpChar t1 t2)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
instance PSemigroup TL.Symbol where
type a <> b = TL.AppendSymbol a b
instance SSemigroup TL.Symbol where
Sing t1
sa %<> :: forall (t1 :: Symbol) (t2 :: Symbol).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<>@#@$) t1) t2)
%<> Sing t2
sb =
let a :: Demote Symbol
a = Sing t1 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t1
sa
b :: Demote Symbol
b = Sing t2 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t2
sb
in String
-> (forall (s :: Symbol).
SSymbol s -> SSymbol (AppendSymbol t1 t2))
-> SSymbol (AppendSymbol t1 t2)
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
TL.withSomeSSymbol (Text -> String
T.unpack (Demote Symbol
Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Demote Symbol
Text
b)) SSymbol s -> SSymbol (AppendSymbol t1 t2)
forall a b. a -> b
forall (s :: Symbol). SSymbol s -> SSymbol (AppendSymbol t1 t2)
unsafeCoerce
type Error :: TL.Symbol -> a
type family Error (str :: TL.Symbol) :: a where {}
$(genDefunSymbols [''Error])
instance SingI (ErrorSym0 :: TL.Symbol ~> a) where
sing :: Sing ErrorSym0
sing = SingFunction1 ErrorSym0 -> Sing ErrorSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Apply ErrorSym0 t)
Sing t -> Sing (Error t)
SingFunction1 ErrorSym0
forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError
sError :: HasCallStack => Sing (str :: TL.Symbol) -> a
sError :: forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError Sing str
sstr = String -> a
forall a. HasCallStack => String -> a
error (Text -> String
T.unpack (Sing str -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing str
sstr))
type ErrorWithoutStackTrace :: TL.Symbol -> a
type family ErrorWithoutStackTrace (str :: TL.Symbol) :: a where {}
$(genDefunSymbols [''ErrorWithoutStackTrace])
instance SingI (ErrorWithoutStackTraceSym0 :: TL.Symbol ~> a) where
sing :: Sing ErrorWithoutStackTraceSym0
sing = SingFunction1 ErrorWithoutStackTraceSym0
-> Sing ErrorWithoutStackTraceSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Apply ErrorWithoutStackTraceSym0 t)
Sing t -> Sing (ErrorWithoutStackTrace t)
SingFunction1 ErrorWithoutStackTraceSym0
forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace
sErrorWithoutStackTrace :: Sing (str :: TL.Symbol) -> a
sErrorWithoutStackTrace :: forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace Sing str
sstr = String -> a
forall a. String -> a
errorWithoutStackTrace (Text -> String
T.unpack (Sing str -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing str
sstr))
type Undefined :: a
type family Undefined :: a where {}
$(genDefunSymbols [''Undefined])
sUndefined :: HasCallStack => a
sUndefined :: forall a. HasCallStack => a
sUndefined = a
forall a. HasCallStack => a
undefined
(%^) :: Sing a -> Sing b -> Sing (a TN.^ b)
Sing a
sa %^ :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
%^ Sing b
sb =
let a :: Demote Nat
a = Sing a -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa
b :: Demote Nat
b = Sing b -> Demote Nat
forall (a :: Nat). Sing a -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing b
sb
in Nat -> (forall (n :: Nat). SNat n -> SNat (a ^ b)) -> SNat (a ^ b)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat (Nat
Demote Nat
a Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Nat
Demote Nat
b) SNat n -> SNat (a ^ b)
forall (n :: Nat). SNat n -> SNat (a ^ b)
forall a b. a -> b
unsafeCoerce
infixr 8 %^
$(genDefunSymbols [''(TN.^)])
instance SingI (^@#@$) where
sing :: Sing (^@#@$)
sing = SingFunction2 (^@#@$) -> Sing (^@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (t1 ^ t2)
Sing t1 -> Sing t2 -> Sing (Apply (Apply (^@#@$) t1) t2)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
SingFunction2 (^@#@$)
(%^)
instance SingI x => SingI ((^@#@$$) x) where
sing :: Sing ((^@#@$$) x)
sing = SingFunction1 ((^@#@$$) x) -> Sing ((^@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x %^)
instance SingI1 (^@#@$$) where
liftSing :: forall (x :: Nat). Sing x -> Sing ((^@#@$$) x)
liftSing Sing x
s = SingFunction1 ((^@#@$$) x) -> Sing ((^@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s %^)
(%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a TN.<=? b)
Sing a
sa %<=? :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=? Sing b
sb = SBool (a <= b) -> SBool (OrdCond (CmpNat a b) 'True 'True 'False)
forall a b. a -> b
unsafeCoerce (Sing a
sa Sing a -> Sing b -> Sing (Apply (Apply (<=@#@$) a) b)
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)
%<= Sing b
sb)
infix 4 %<=?
$(genDefunSymbols [''(TN.<=?)])
instance SingI ((<=?@#@$) @Natural) where
sing :: Sing (<=?@#@$)
sing = SingFunction2 (<=?@#@$) -> Sing (<=?@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=?@#@$) t1) t2)
Sing t1 -> Sing t2 -> Sing (t1 <=? t2)
SingFunction2 (<=?@#@$)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
(%<=?)
instance SingI x => SingI ((<=?@#@$$) @Natural x) where
sing :: Sing ((<=?@#@$$) x)
sing = SingFunction1 ((<=?@#@$$) x) -> Sing ((<=?@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x %<=?)
instance SingI1 ((<=?@#@$$) @Natural) where
liftSing :: forall (x :: Nat). Sing x -> Sing ((<=?@#@$$) x)
liftSing Sing x
s = SingFunction1 ((<=?@#@$$) x) -> Sing ((<=?@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s %<=?)