module Generics.Kind.Unexported where

import Generics.Kind hiding (SubstRep)


class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where
  type family SubstRep f x :: LoT k -> *
  substRep   :: f (x ':&&: xs) -> SubstRep f x xs
  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)

instance SubstRep' U1 x xs where
  type SubstRep U1 x = U1
  substRep :: U1 (x ':&&: xs) -> SubstRep U1 x xs
substRep   U1 = SubstRep U1 x xs
forall k (p :: k). U1 p
U1
  unsubstRep :: SubstRep U1 x xs -> U1 (x ':&&: xs)
unsubstRep U1 = U1 (x ':&&: xs)
forall k (p :: k). U1 p
U1

instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where
  type SubstRep (f :+: g)  x = (SubstRep f x) :+: (SubstRep g x)
  substRep :: (:+:) f g (x ':&&: xs) -> SubstRep (f :+: g) x xs
substRep   (L1 x :: f (x ':&&: xs)
x) = SubstRep f x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  substRep   (R1 x :: g (x ':&&: xs)
x) = SubstRep g x xs -> (:+:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g (x ':&&: xs) -> SubstRep g x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   g (x ':&&: xs)
x)
  unsubstRep :: SubstRep (f :+: g) x xs -> (:+:) f g (x ':&&: xs)
unsubstRep (L1 x) = f (x ':&&: xs) -> (:+:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)
  unsubstRep (R1 x) = g (x ':&&: xs) -> (:+:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (SubstRep g x xs -> g (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep g x xs
x)

instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where
  type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x)
  substRep :: (:*:) f g (x ':&&: xs) -> SubstRep (f :*: g) x xs
substRep   (x :: f (x ':&&: xs)
x :*: y :: g (x ':&&: xs)
y) = f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x SubstRep f x xs
-> SubstRep g x xs -> (:*:) (SubstRep f x) (SubstRep g x) xs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g (x ':&&: xs) -> SubstRep g x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   g (x ':&&: xs)
y
  unsubstRep :: SubstRep (f :*: g) x xs -> (:*:) f g (x ':&&: xs)
unsubstRep (x :*: y) = SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x f (x ':&&: xs) -> g (x ':&&: xs) -> (:*:) f g (x ':&&: xs)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: SubstRep g x xs -> g (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep g x xs
y

instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where
  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)
  substRep :: M1 i c f (x ':&&: xs) -> SubstRep (M1 i c f) x xs
substRep   (M1 x :: f (x ':&&: xs)
x) = SubstRep f x xs -> M1 i c (SubstRep f x) xs
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  unsubstRep :: SubstRep (M1 i c f) x xs -> M1 i c f (x ':&&: xs)
unsubstRep (M1 x) = f (x ':&&: xs) -> M1 i c f (x ':&&: xs)
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)

instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)
         => SubstRep' (c :=>: f) x xs where
  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)
  substRep :: (:=>:) c f (x ':&&: xs) -> SubstRep (c :=>: f) x xs
substRep   (SuchThat x :: f (x ':&&: xs)
x) = SubstRep f x xs -> (:=>:) (SubstAtom c x) (SubstRep f x) xs
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (f (x ':&&: xs) -> SubstRep f x xs
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
f (x ':&&: xs) -> SubstRep f x xs
substRep   f (x ':&&: xs)
x)
  unsubstRep :: SubstRep (c :=>: f) x xs -> (:=>:) c f (x ':&&: xs)
unsubstRep (SuchThat x) = f (x ':&&: xs) -> (:=>:) c f (x ':&&: xs)
forall d (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (SubstRep f x xs -> f (x ':&&: xs)
forall t k (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k).
SubstRep' f x xs =>
SubstRep f x xs -> f (x ':&&: xs)
unsubstRep SubstRep f x xs
x)

instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs))
         => SubstRep' (Field t) x xs where
  type SubstRep (Field t) x = Field (SubstAtom t x)
  substRep :: Field t (x ':&&: xs) -> SubstRep (Field t) x xs
substRep   (Field x :: Interpret t (x ':&&: xs)
x) = Interpret (SubstAtom t x) xs -> Field (SubstAtom t x) xs
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (SubstAtom t x) xs
Interpret t (x ':&&: xs)
x
  unsubstRep :: SubstRep (Field t) x xs -> Field t (x ':&&: xs)
unsubstRep (Field x) = Interpret t (x ':&&: xs) -> Field t (x ':&&: xs)
forall d (t :: Atom d *) (x :: LoT d). Interpret t x -> Field t x
Field Interpret (SubstAtom t x) xs
Interpret t (x ':&&: xs)
x

type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where
  SubstAtom ('Var 'VZ)     x = 'Kon x
  SubstAtom ('Var ('VS v)) x = 'Var v
  SubstAtom ('Kon t)       x = 'Kon t
  SubstAtom (t1 ':@: t2)   x = (SubstAtom t1 x) ':@: (SubstAtom t2 x)
  SubstAtom (t1 ':&: t2)   x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)