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))