module Sqel.Names.Rename where

import qualified Generics.SOP as SOP
import Generics.SOP (AllZipN, HTrans (htrans), NP)

import Sqel.Data.Dd (CompInc (Merge), Dd (Dd), DdK (DdK), DdStruct (DdComp), Struct (Comp, Prim))
import Sqel.Data.Sel (
  Sel (SelAuto, SelSymbol, SelUnused),
  SelW (SelWAuto, SelWSymbol, SelWUnused),
  TSel (TSel),
  TSelW (TSelW),
  TypeName,
  )

type RenameSel :: Sel -> Sel -> Constraint
class RenameSel s0 s1 where
  renameSel :: SelW s0 -> SelW s1

instance {-# overlappable #-} (
    s0 ~ s1
  ) => RenameSel s0 s1 where
  renameSel :: SelW s0 -> SelW s1
renameSel = forall a. a -> a
id

instance (
    KnownSymbol name
  ) => RenameSel s0 ('SelSymbol name) where
  renameSel :: SelW s0 -> SelW ('SelSymbol name)
renameSel SelW s0
_ = forall (name :: Symbol).
KnownSymbol name =>
Proxy name -> SelW ('SelSymbol name)
SelWSymbol forall {k} (t :: k). Proxy t
Proxy

instance RenameSel s0 'SelUnused where
  renameSel :: SelW s0 -> SelW 'SelUnused
renameSel SelW s0
_ = SelW 'SelUnused
SelWUnused

instance RenameSel s0 'SelAuto where
  renameSel :: SelW s0 -> SelW 'SelAuto
renameSel SelW s0
_ = SelW 'SelAuto
SelWAuto

type RenameTSel :: TSel -> TSel -> Constraint
class RenameTSel s0 s1 where
  renameTSel :: TSelW s0 -> TSelW s1

instance {-# overlappable #-} (
    s0 ~ s1
  ) => RenameTSel s0 s1 where
  renameTSel :: TSelW s0 -> TSelW s1
renameTSel = forall a. a -> a
id

instance (
    TypeName prefix tpe name
  ) => RenameTSel s0 ('TSel prefix tpe) where
  renameTSel :: TSelW s0 -> TSelW ('TSel prefix tpe)
renameTSel TSelW s0
_ = forall (prefix :: SelPrefix) (tpe :: Symbol) (name :: Symbol).
TypeName prefix tpe name =>
Proxy '(tpe, name) -> TSelW ('TSel prefix tpe)
TSelW forall {k} (t :: k). Proxy t
Proxy

type Rename :: DdK -> DdK -> Constraint
class Rename s0 s1 where
  rename :: Dd s0 -> Dd s1

instance (
    RenameSel sel0 sel1
  ) => Rename ('DdK sel0 p t 'Prim) ('DdK sel1 p t 'Prim) where
  rename :: Dd ('DdK sel0 p t 'Prim) -> Dd ('DdK sel1 p t 'Prim)
rename (Dd SelW sel
sel Mods mods
p DdStruct s1
s) =
    forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd (forall (s0 :: Sel) (s1 :: Sel).
RenameSel s0 s1 =>
SelW s0 -> SelW s1
renameSel SelW sel
sel) Mods mods
p DdStruct s1
s

instance {-# overlappable #-} (
    RenameSel sel0 sel1,
    RenameTSel tsel0 tsel1
  ) => Rename ('DdK sel0 p t ('Comp tsel0 c i sub)) ('DdK sel1 p t ('Comp tsel1 c i sub)) where
    rename :: Dd ('DdK sel0 p t ('Comp tsel0 c i sub))
-> Dd ('DdK sel1 p t ('Comp tsel1 c i sub))
rename (Dd SelW sel
sel Mods mods
p (DdComp TSelW sel
tsel DdSort c
c DdInc i
i NP Dd sub
s)) =
      forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd (forall (s0 :: Sel) (s1 :: Sel).
RenameSel s0 s1 =>
SelW s0 -> SelW s1
renameSel SelW sel
sel) Mods mods
p (forall (sel :: TSel) (c :: Comp) (i :: CompInc) (sub :: [DdK]).
TSelW sel
-> DdSort c -> DdInc i -> NP Dd sub -> DdStruct ('Comp sel c i sub)
DdComp (forall (s0 :: TSel) (s1 :: TSel).
RenameTSel s0 s1 =>
TSelW s0 -> TSelW s1
renameTSel TSelW sel
tsel) DdSort c
c DdInc i
i NP Dd sub
s)

instance Rename ('DdK sel p t ('Comp tsel c 'Merge sub)) ('DdK sel p t ('Comp tsel c 'Merge sub)) where
    rename :: Dd ('DdK sel p t ('Comp tsel c 'Merge sub))
-> Dd ('DdK sel p t ('Comp tsel c 'Merge sub))
rename (Dd SelW sel
sel Mods mods
p (DdComp TSelW sel
tsel DdSort c
c DdInc i
i NP Dd sub
s)) =
      forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd SelW sel
sel Mods mods
p (forall (sel :: TSel) (c :: Comp) (i :: CompInc) (sub :: [DdK]).
TSelW sel
-> DdSort c -> DdInc i -> NP Dd sub -> DdStruct ('Comp sel c i sub)
DdComp TSelW sel
tsel DdSort c
c DdInc i
i NP Dd sub
s)

type RenameN :: ((DdK -> Type) -> k -> Type) -> k -> k -> Constraint
class RenameN h s0 s1 where
  renameN :: h Dd s0 -> h Dd s1

instance (
    HTrans h h,
    AllZipN (SOP.Prod h) Rename s0 s1
  ) => RenameN h s0 s1 where
  renameN :: h Dd s0 -> h Dd s1
renameN = forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *)
       (h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint)
       (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *)
       (f :: k1 -> *) (g :: k2 -> *).
(HTrans h1 h2, AllZipN (Prod h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
htrans (forall {k} (t :: k). Proxy t
Proxy @Rename) forall (s0 :: DdK) (s1 :: DdK). Rename s0 s1 => Dd s0 -> Dd s1
rename

type Rename2 :: DdK -> DdK -> Constraint
class Rename2 s0 s1 where
  rename2 :: Dd s0 -> Dd s1

instance (
    RenameSel sel0 sel1
  ) => Rename2 ('DdK sel0 p t 'Prim) ('DdK sel1 p t 'Prim) where
  rename2 :: Dd ('DdK sel0 p t 'Prim) -> Dd ('DdK sel1 p t 'Prim)
rename2 (Dd SelW sel
sel Mods mods
p DdStruct s1
s) = forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd (forall (s0 :: Sel) (s1 :: Sel).
RenameSel s0 s1 =>
SelW s0 -> SelW s1
renameSel SelW sel
sel) Mods mods
p DdStruct s1
s

instance (
    RenameSel sel0 sel1,
    RenameTSel tsel0 tsel1,
    RenameN NP s0 s1
  ) => Rename2 ('DdK sel0 p t ('Comp tsel0 c i s0)) ('DdK sel1 p t ('Comp tsel1 c i s1)) where
  rename2 :: Dd ('DdK sel0 p t ('Comp tsel0 c i s0))
-> Dd ('DdK sel1 p t ('Comp tsel1 c i s1))
rename2 (Dd SelW sel
sel Mods mods
p (DdComp TSelW sel
tsel DdSort c
c DdInc i
i NP Dd sub
sub)) = forall (sel :: Sel) (mods :: [*]) (s1 :: Struct) a.
SelW sel -> Mods mods -> DdStruct s1 -> Dd ('DdK sel mods a s1)
Dd (forall (s0 :: Sel) (s1 :: Sel).
RenameSel s0 s1 =>
SelW s0 -> SelW s1
renameSel SelW sel
sel) Mods mods
p (forall (sel :: TSel) (c :: Comp) (i :: CompInc) (sub :: [DdK]).
TSelW sel
-> DdSort c -> DdInc i -> NP Dd sub -> DdStruct ('Comp sel c i sub)
DdComp (forall (s0 :: TSel) (s1 :: TSel).
RenameTSel s0 s1 =>
TSelW s0 -> TSelW s1
renameTSel TSelW sel
tsel) DdSort c
c DdInc i
i (forall k (h :: (DdK -> *) -> k -> *) (s0 :: k) (s1 :: k).
RenameN h s0 s1 =>
h Dd s0 -> h Dd s1
renameN NP Dd sub
sub))