module Sqel.Uid where

import Sqel.Data.Dd (Dd, DdK, DdType, DdTypeSel, type (:>) ((:>)))
import Sqel.Data.Uid (Uid)
import Sqel.Merge (merge)
import Sqel.Names.Rename (Rename, rename)
import Sqel.Names.Set (SetTypeName)
import Sqel.Product (ProductSel (prodSel))
import qualified Sqel.Type as T
import Sqel.Type (type (*>), type (>))

type UidDd si sa =
  T.TypeSel (DdTypeSel sa) (T.Prod (Uid (DdType si) (DdType sa))) *> T.Name "id" si > T.Merge sa

type UidColumn :: Type -> Type -> DdK -> DdK -> DdK -> Constraint
class (
    DdType si ~ i,
    DdType sa ~ a
  ) => UidColumn i a si sa s | i a si sa -> s where
    uidColumn :: Dd si -> Dd sa -> Dd s

instance (
    DdType si ~ i,
    DdType sa ~ a,
    DdTypeSel sa ~ sel,
    ProductSel sel (Uid i a) (Dd si :> Dd (T.Merge sa)) s
  ) => UidColumn i a si sa s where
    uidColumn :: Dd si -> Dd sa -> Dd s
uidColumn Dd si
i Dd sa
a =
      forall {k} (sel :: k) a arg (s :: DdK).
ProductSel sel a arg s =>
arg -> Dd s
prodSel @sel @(Uid i a) (Dd si
i forall a b. a -> b -> a :> b
:> forall (s :: DdK). Dd s -> Dd (Merge s)
merge Dd sa
a)

uid ::
  ∀ (i :: Type) (a :: Type) (si :: DdK) (sa :: DdK) (s :: DdK) .
  UidColumn i a si sa s =>
  Dd si ->
  Dd sa ->
  Dd s
uid :: forall i a (si :: DdK) (sa :: DdK) (s :: DdK).
UidColumn i a si sa s =>
Dd si -> Dd sa -> Dd s
uid =
  forall i a (si :: DdK) (sa :: DdK) (s :: DdK).
UidColumn i a si sa s =>
Dd si -> Dd sa -> Dd s
uidColumn

uidAs ::
  ∀ (name :: Symbol) (i :: Type) (a :: Type) (si :: DdK) (sa :: DdK) (s :: DdK) .
  UidColumn i a si sa s =>
  Rename s (SetTypeName s name) =>
  Dd si ->
  Dd sa ->
  Dd (SetTypeName s name)
uidAs :: forall (name :: Symbol) i a (si :: DdK) (sa :: DdK) (s :: DdK).
(UidColumn i a si sa s, Rename s (SetTypeName s name)) =>
Dd si -> Dd sa -> Dd (SetTypeName s name)
uidAs Dd si
i Dd sa
a =
  forall (s0 :: DdK) (s1 :: DdK). Rename s0 s1 => Dd s0 -> Dd s1
rename (forall i a (si :: DdK) (sa :: DdK) (s :: DdK).
UidColumn i a si sa s =>
Dd si -> Dd sa -> Dd s
uidColumn Dd si
i Dd sa
a)