{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.Singletons (
Sing(SLambda, applySing), (@@),
SingI(..), SingKind(..),
KindOf, SameKind,
SingInstance(..), SomeSing(..),
singInstance, pattern Sing, withSingI,
withSomeSing, pattern FromSing,
singByProxy, demote,
singByProxy#,
withSing, singThat,
TyFun, type (~>),
TyCon1, TyCon2, TyCon3, TyCon4, TyCon5, TyCon6, TyCon7, TyCon8,
TyCon, Apply, type (@@),
singFun1, singFun2, singFun3, singFun4, singFun5, singFun6, singFun7,
singFun8,
unSingFun1, unSingFun2, unSingFun3, unSingFun4, unSingFun5,
unSingFun6, unSingFun7, unSingFun8,
pattern SLambda2, pattern SLambda3, pattern SLambda4, pattern SLambda5,
pattern SLambda6, pattern SLambda7, pattern SLambda8,
SingFunction1, SingFunction2, SingFunction3, SingFunction4, SingFunction5,
SingFunction6, SingFunction7, SingFunction8,
Proxy(..),
DemoteSym0, DemoteSym1,
SameKindSym0, SameKindSym1, SameKindSym2,
KindOfSym0, KindOfSym1,
type (~>@#@$), type (~>@#@$$), type (~>@#@$$$),
ApplySym0, ApplySym1, ApplySym2,
type (@@@#@$), type (@@@#@$$), type (@@@#@$$$)
) where
import Data.Singletons.Internal
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Monoid
import Data.Singletons.Prelude.Num
import Data.Singletons.Prelude.Ord
import Data.Singletons.Prelude.Semigroup
import Data.Singletons.Promote
import Data.Singletons.ShowSing
instance SEq k => Eq (SomeSing k) where
SomeSing a == SomeSing b = fromSing (a %== b)
SomeSing a /= SomeSing b = fromSing (a %/= b)
instance SOrd k => Ord (SomeSing k) where
SomeSing a `compare` SomeSing b = fromSing (a `sCompare` b)
SomeSing a < SomeSing b = fromSing (a %< b)
SomeSing a <= SomeSing b = fromSing (a %<= b)
SomeSing a > SomeSing b = fromSing (a %> b)
SomeSing a >= SomeSing b = fromSing (a %>= b)
instance SBounded k => Bounded (SomeSing k) where
minBound = SomeSing sMinBound
maxBound = SomeSing sMaxBound
instance (SEnum k, SingKind k) => Enum (SomeSing k) where
succ (SomeSing a) = SomeSing (sSucc a)
pred (SomeSing a) = SomeSing (sPred a)
toEnum n = withSomeSing (fromIntegral n) (SomeSing . sToEnum)
fromEnum (SomeSing a) = fromIntegral (fromSing (sFromEnum a))
enumFromTo (SomeSing from) (SomeSing to) =
map toSing (fromSing (sEnumFromTo from to))
enumFromThenTo (SomeSing from) (SomeSing then_) (SomeSing to) =
map toSing (fromSing (sEnumFromThenTo from then_ to))
instance SNum k => Num (SomeSing k) where
SomeSing a + SomeSing b = SomeSing (a %+ b)
SomeSing a - SomeSing b = SomeSing (a %- b)
SomeSing a * SomeSing b = SomeSing (a %* b)
negate (SomeSing a) = SomeSing (sNegate a)
abs (SomeSing a) = SomeSing (sAbs a)
signum (SomeSing a) = SomeSing (sSignum a)
fromInteger n = withSomeSing (fromIntegral n) (SomeSing . sFromInteger)
deriving instance ShowSing k => Show (SomeSing k)
instance SSemigroup k => Semigroup (SomeSing k) where
SomeSing a <> SomeSing b = SomeSing (a %<> b)
instance SMonoid k => Monoid (SomeSing k) where
mempty = SomeSing sMempty
$(genDefunSymbols [''Demote, ''SameKind, ''KindOf, ''(~>), ''Apply, ''(@@)])