{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, FlexibleInstances,
UndecidableInstances, ScopedTypeVariables, RankNTypes,
GADTs, FlexibleContexts, TypeOperators, ConstraintKinds,
TemplateHaskell, TypeApplications, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module GHC.TypeLits.Singletons.Internal (
Sing,
Nat, Symbol,
SNat(..), SSymbol(..), withKnownNat, withKnownSymbol,
Error, sError,
ErrorWithoutStackTrace, sErrorWithoutStackTrace,
Undefined, sUndefined,
KnownNat, TN.natVal, KnownSymbol, symbolVal,
type (^), (%^),
type (<=?), (%<=?),
ErrorSym0, ErrorSym1,
ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
UndefinedSym0,
type (^@#@$), type (^@#@$$), type (^@#@$$$),
type (<=?@#@$), type (<=?@#@$$), type (<=?@#@$$$)
) where
import Data.Bool.Singletons
import Data.Eq.Singletons
import Data.Kind
import Data.Ord.Singletons as O
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import GHC.Show (appPrec, appPrec1)
import GHC.Stack (HasCallStack)
import 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 SNat :: Nat -> Type
data SNat (n :: Nat) = KnownNat n => SNat
type instance Sing = SNat
instance KnownNat n => SingI n where
sing :: Sing n
sing = Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat
instance SingKind Nat where
type Demote Nat = Natural
fromSing :: forall (a :: Nat). Sing a -> Demote Nat
fromSing (Sing a
SNat a
SNat :: Sing n) = Proxy a -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
TN.natVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
toSing :: Demote Nat -> SomeSing Nat
toSing Demote Nat
n = case Natural -> SomeNat
TN.someNatVal Natural
Demote Nat
n of
SomeNat (Proxy n
_ :: Proxy n) -> Sing n -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing n)
type SSymbol :: Symbol -> Type
data SSymbol (n :: Symbol) = KnownSymbol n => SSym
type instance Sing = SSymbol
instance KnownSymbol n => SingI n where
sing :: Sing n
sing = Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym
instance SingKind Symbol where
type Demote Symbol = Text
fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol
fromSing (Sing a
SSymbol a
SSym :: Sing n) = String -> Text
T.pack (Proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
toSing :: Demote Symbol -> SomeSing Symbol
toSing Demote Symbol
s = case String -> SomeSymbol
someSymbolVal (Text -> String
T.unpack Demote Symbol
Text
s) of
SomeSymbol (Proxy n
_ :: Proxy n) -> Sing n -> SomeSing Symbol
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing n)
instance SDecide Nat where
(Sing a
SNat a
SNat :: Sing n) %~ :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing b
SNat b
SNat :: Sing m)
| Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
TN.sameNat (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
= (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 Nat singletons"
instance SDecide Symbol where
(Sing a
SSymbol a
SSym :: Sing n) %~ :: forall (a :: Symbol) (b :: Symbol).
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing b
SSymbol b
SSym :: Sing m)
| Just a :~: b
r <- Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
(proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
= (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 Symbol singletons"
instance PEq Nat where
type x == y = DefaultEq x y
instance PEq Symbol where
type x == y = DefaultEq x y
instance SEq Nat where
(Sing t
SNat t
SNat :: Sing n) %== :: forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== (Sing t
SNat t
SNat :: Sing m)
= case Proxy t -> Proxy t -> Maybe (t :~: t)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy m) of
Just t :~: t
Refl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
Maybe (t :~: t)
Nothing -> SBool 'False -> SBool (DefaultEq t t)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
instance SEq Symbol where
(Sing t
SSymbol t
SSym :: Sing n) %== :: forall (t :: Symbol) (t :: Symbol).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== (Sing t
SSymbol t
SSym :: Sing m)
= case Proxy t -> Proxy t -> Maybe (t :~: t)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
(proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy m) of
Just t :~: t
Refl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
Maybe (t :~: t)
Nothing -> SBool 'False -> SBool (DefaultEq t t)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
instance POrd Nat where
type (a :: Nat) `Compare` (b :: Nat) = a `TN.CmpNat` b
instance POrd Symbol where
type (a :: Symbol) `Compare` (b :: Symbol) = a `TL.CmpSymbol` b
instance SOrd Nat where
Sing t
a sCompare :: forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
`sCompare` Sing t
b = case Sing t -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
a Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat t t)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
instance SOrd Symbol where
Sing t
a sCompare :: forall (t :: Symbol) (t :: Symbol).
Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
`sCompare` Sing t
b = case Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
a Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
b of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpSymbol t t)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpSymbol t t)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpSymbol t t)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
SGT
instance Show (SNat n) where
showsPrec :: Int -> SNat n -> ShowS
showsPrec Int
p n :: SNat n
n@SNat n
SNat
= Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
( String -> ShowS
showString String
"SNat @"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
TN.natVal SNat n
n)
)
instance Show (SSymbol s) where
showsPrec :: Int -> SSymbol s -> ShowS
showsPrec Int
p s :: SSymbol s
s@SSymbol s
SSym
= Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
( String -> ShowS
showString String
"SSym @"
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (SSymbol s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol s
s)
)
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
SNat n
SNat KnownNat n => r
f = r
KnownNat n => r
f
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol :: forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing n
SSymbol n
SSym KnownSymbol n => r
f = r
KnownSymbol n => r
f
type Error :: k0 -> k
type family Error (str :: k0) :: k where {}
$(genDefunSymbols [''Error])
instance SingI (ErrorSym0 :: Symbol ~> a) where
sing :: Sing ErrorSym0
sing = SingFunction1 ErrorSym0 -> Sing ErrorSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ErrorSym0
forall (str :: Symbol) a. HasCallStack => Sing str -> a
sError
sError :: HasCallStack => Sing (str :: 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
fromSing Sing str
sstr))
type ErrorWithoutStackTrace :: k0 -> k
type family ErrorWithoutStackTrace (str :: k0) :: k where {}
$(genDefunSymbols [''ErrorWithoutStackTrace])
instance SingI (ErrorWithoutStackTraceSym0 :: Symbol ~> a) where
sing :: Sing ErrorWithoutStackTraceSym0
sing = SingFunction1 ErrorWithoutStackTraceSym0
-> Sing ErrorWithoutStackTraceSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ErrorWithoutStackTraceSym0
forall (str :: Symbol) a. Sing str -> a
sErrorWithoutStackTrace
sErrorWithoutStackTrace :: Sing (str :: 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
fromSing Sing str
sstr))
type Undefined :: k
type family Undefined :: k where {}
$(genDefunSymbols [''Undefined])
sUndefined :: HasCallStack => a
sUndefined :: forall a. HasCallStack => a
sUndefined = a
forall a. HasCallStack => a
undefined
(%^) :: Sing a -> Sing b -> Sing (a ^ 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 k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa
b :: Demote Nat
b = Sing b -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing b
sb
ex :: SomeNat
ex = Natural -> SomeNat
TN.someNatVal (Natural
Demote Nat
a Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
Demote Nat
b)
in
case SomeNat
ex of
SomeNat (Proxy n
_ :: Proxy ab) -> SNat n -> SNat (a ^ b)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat :: Sing ab)
infixr 8 %^
$(genDefunSymbols [''(^)])
instance SingI (^@#@$) where
sing :: Sing (^@#@$)
sing = SingFunction2 (^@#@$) -> Sing (^@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 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 {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x ^ t)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
%^)
(%<=?) :: Sing a -> Sing b -> Sing (a <=? b)
Sing a
sa %<=? :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=? Sing b
sb = SBool (Case_6989586621679170817 a b (CmpNat a b))
-> SBool (a <=? b)
forall a b. a -> b
unsafeCoerce (Sing a
sa Sing a -> Sing b -> Sing (Apply (Apply (<=@#@$) a) b)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)
%<= Sing b
sb)
infix 4 %<=?
$(genDefunSymbols [''(<=?)])
instance SingI (<=?@#@$) where
sing :: Sing (<=?@#@$)
sing = SingFunction2 (<=?@#@$) -> Sing (<=?@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 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 {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x <=? t)
forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
%<=?)