{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module PgSchema.Utils.Instances where

import Data.Kind (Type)
import Data.Singletons
import Data.Text as T
import GHC.TypeLits


-- * Bool singletons (avoid "Data.Bool.Singletons" from singletons-base)

data SBool :: Bool -> Type where
  SFalse :: SBool 'False
  STrue :: SBool 'True

type instance Sing @Bool = SBool

instance SingKind Bool where
  type Demote Bool = Bool
  fromSing :: forall (a :: Bool). Sing a -> Demote Bool
fromSing Sing a
SBool a
SFalse = Bool
Demote Bool
False
  fromSing Sing a
SBool a
STrue = Bool
Demote Bool
True
  toSing :: Demote Bool -> SomeSing Bool
toSing Bool
Demote Bool
False = Sing 'False -> SomeSing Bool
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'False
SBool 'False
SFalse
  toSing Bool
Demote Bool
True = Sing 'True -> SomeSing Bool
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'True
SBool 'True
STrue

instance SingI 'False where sing :: Sing 'False
sing = Sing 'False
SBool 'False
SFalse

instance SingI 'True where sing :: Sing 'True
sing = Sing 'True
SBool 'True
STrue

-- * Maybe singletons (avoid "Data.Maybe.Singletons" from singletons-base)

data SMaybe :: Maybe k -> Type where
  SNothing :: SMaybe 'Nothing
  SJust :: Sing x -> SMaybe ('Just x)

type instance Sing @(Maybe k) = SMaybe

instance SingKind k => SingKind (Maybe k) where
  type Demote (Maybe k) = Maybe (Demote k)
  fromSing :: forall (a :: Maybe k). Sing a -> Demote (Maybe k)
fromSing Sing a
SMaybe a
SNothing = Maybe (Demote k)
Demote (Maybe k)
forall a. Maybe a
Nothing
  fromSing (SJust Sing x
sx) = Demote k -> Maybe (Demote k)
forall a. a -> Maybe a
Just (Sing x -> Demote k
forall (a :: k). Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx)
  toSing :: Demote (Maybe k) -> SomeSing (Maybe k)
toSing Maybe (Demote k)
Demote (Maybe k)
Nothing = Sing 'Nothing -> SomeSing (Maybe k)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'Nothing
SMaybe 'Nothing
forall {k}. SMaybe 'Nothing
SNothing
  toSing (Just Demote k
x) = case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
x of
    SomeSing Sing a
sx -> Sing ('Just a) -> SomeSing (Maybe k)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> SMaybe ('Just a)
forall {k} (x :: k). Sing x -> SMaybe ('Just x)
SJust Sing a
sx)

instance SingI 'Nothing where
  sing :: Sing 'Nothing
sing = Sing 'Nothing
SMaybe 'Nothing
forall {k}. SMaybe 'Nothing
SNothing

instance SingI x => SingI ('Just x) where
  sing :: Sing ('Just x)
sing = Sing x -> SMaybe ('Just x)
forall {k} (x :: k). Sing x -> SMaybe ('Just x)
SJust Sing x
forall {k} (a :: k). SingI a => Sing a
sing

-- * @Symbol@ singletons (@Demote Symbol = Text@, as in @pg-schema@)

type instance Sing @Symbol = SSymbol

instance SingKind Symbol where
  type Demote Symbol = Text
  fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol
fromSing (SSymbol a
SSymbol :: SSymbol n) = String -> Text
T.pack (Proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @n))
  toSing :: Demote Symbol -> SomeSing Symbol
toSing Demote Symbol
t = case String -> SomeSymbol
someSymbolVal (Text -> String
T.unpack Text
Demote Symbol
t) of
    SomeSymbol (Proxy n
_ :: Proxy n) -> Sing n -> SomeSing Symbol
forall k (a :: k). Sing a -> SomeSing k
SomeSing (forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol @n)

instance KnownSymbol n => SingI n where
  sing :: Sing n
sing = SSymbol n
Sing n
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol

-- * List singletons

data SList :: [k] -> Type where
  SNil :: SList '[]
  SCons :: Sing x -> Sing xs -> SList (x ': xs)

type instance Sing @[k] = SList

instance SingKind k => SingKind [k] where
  type Demote [k] = [Demote k]
  fromSing :: forall (a :: [k]). Sing a -> Demote [k]
fromSing Sing a
SList a
SNil = []
  fromSing (SCons Sing x
sx Sing xs
sxs) = Sing x -> Demote k
forall (a :: k). Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx Demote k -> [Demote k] -> [Demote k]
forall a. a -> [a] -> [a]
: Sing xs -> Demote [k]
forall (a :: [k]). Sing a -> Demote [k]
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing xs
sxs
  toSing :: Demote [k] -> SomeSing [k]
toSing [] = Sing '[] -> SomeSing [k]
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing '[]
SList '[]
forall {k}. SList '[]
SNil
  toSing (Demote k
x : [Demote k]
xs) = case (Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
x, Demote [k] -> SomeSing [k]
forall k. SingKind k => Demote k -> SomeSing k
toSing [Demote k]
Demote [k]
xs) of
    (SomeSing Sing a
sx, SomeSing Sing a
sxs) -> Sing (a : a) -> SomeSing [k]
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing a -> SList (a : a)
forall {k} (x :: k) (y :: [k]). Sing x -> Sing y -> SList (x : y)
SCons Sing a
sx Sing a
sxs)

instance SingI '[] where
  sing :: Sing '[]
sing = Sing '[]
SList '[]
forall {k}. SList '[]
SNil

instance (SingI x, SingI xs) => SingI (x ': xs) where
  sing :: Sing (x : xs)
sing = Sing x -> Sing xs -> SList (x : xs)
forall {k} (x :: k) (y :: [k]). Sing x -> Sing y -> SList (x : y)
SCons Sing x
forall {k} (a :: k). SingI a => Sing a
sing Sing xs
forall {k} (a :: k). SingI a => Sing a
sing

-- * Pair singletons

data STuple2 :: (a, b) -> Type where
  STuple2 :: Sing x -> Sing y -> STuple2 '(x, y)

type instance Sing @(a, b) = STuple2

instance (SingKind a, SingKind b) => SingKind (a, b) where
  type Demote (a, b) = (Demote a, Demote b)
  fromSing :: forall (a :: (a, b)). Sing a -> Demote (a, b)
fromSing (STuple2 Sing x
sx Sing y
sy) = (Sing x -> Demote a
forall (a :: a). Sing a -> Demote a
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx, Sing y -> Demote b
forall (a :: b). Sing a -> Demote b
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy)
  toSing :: Demote (a, b) -> SomeSing (a, b)
toSing (Demote a
x, Demote b
y) = case (Demote a -> SomeSing a
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote a
x, Demote b -> SomeSing b
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote b
y) of
    (SomeSing Sing a
sx, SomeSing Sing a
sy) -> Sing '(a, a) -> SomeSing (a, b)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing a -> STuple2 '(a, a)
forall {k} {k} (x :: k) (y :: k).
Sing x -> Sing y -> STuple2 '(x, y)
STuple2 Sing a
sx Sing a
sy)

instance (SingI a, SingI b) => SingI '(a, b) where
  sing :: Sing '(a, b)
sing = Sing a -> Sing b -> STuple2 '(a, b)
forall {k} {k} (x :: k) (y :: k).
Sing x -> Sing y -> STuple2 '(x, y)
STuple2 Sing a
forall {k} (a :: k). SingI a => Sing a
sing Sing b
forall {k} (a :: k). SingI a => Sing a
sing