{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.Class (
        SymbolicData (..),
        SymbolicOutput,
        GSymbolicData (..),
    ) where

import           Control.Applicative              ((<*>))
import           Data.Bifunctor                   (bimap)
import           Data.Function                    (flip, (.))
import           Data.Functor                     ((<$>))
import           Data.Functor.Rep                 (Representable (..))
import           Data.Kind                        (Type)
import           Data.Traversable                 (Traversable)
import           Data.Tuple                       (fst)
import           Data.Type.Equality               (type (~))
import           Data.Typeable                    (Proxy (..))
import           GHC.Generics                     (U1 (..), (:*:) (..), (:.:) (..))
import qualified GHC.Generics                     as G

import           ZkFold.Base.Algebra.Basic.Number (KnownNat)
import           ZkFold.Base.Control.HApplicative (HApplicative, hliftA2, hpure)
import           ZkFold.Base.Data.HFunctor        (hmap)
import           ZkFold.Base.Data.Package         (Package, pack)
import           ZkFold.Base.Data.Product         (fstP, sndP)
import           ZkFold.Base.Data.Vector          (Vector)
import           ZkFold.Symbolic.Class            (Symbolic (WitnessField))

-- | A class for Symbolic data types.
class
    ( Symbolic (Context x)
    , Traversable (Layout x)
    , Representable (Layout x)
    , Representable (Payload x)
    ) => SymbolicData x where

    type Context x :: (Type -> Type) -> Type
    type Context x = GContext (G.Rep x)

    type Support x :: Type
    type Support x = GSupport (G.Rep x)

    type Layout x :: Type -> Type
    type Layout x = GLayout (G.Rep x)

    type Payload x :: Type -> Type
    type Payload x = GPayload (G.Rep x)

    -- | Returns the circuit that makes up `x`.
    arithmetize :: x -> Support x -> Context x (Layout x)
    default arithmetize
      :: ( G.Generic x
         , GSymbolicData (G.Rep x)
         , Context x ~ GContext (G.Rep x)
         , Support x ~ GSupport (G.Rep x)
         , Layout x ~ GLayout (G.Rep x)
         )
      => x -> Support x -> Context x (Layout x)
    arithmetize x
x = Rep x Any -> GSupport (Rep x) -> GContext (Rep x) (GLayout (Rep x))
forall x.
Rep x x -> GSupport (Rep x) -> GContext (Rep x) (GLayout (Rep x))
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GContext u (GLayout u)
garithmetize (x -> Rep x Any
forall x. x -> Rep x x
forall a x. Generic a => a -> Rep a x
G.from x
x)

    payload :: x -> Support x -> Payload x (WitnessField (Context x))
    default payload
      :: ( G.Generic x
         , GSymbolicData (G.Rep x)
         , Context x ~ GContext (G.Rep x)
         , Support x ~ GSupport (G.Rep x)
         , Payload x ~ GPayload (G.Rep x)
         )
      => x -> Support x -> Payload x (WitnessField (Context x))
    payload x
x = Rep x Any
-> GSupport (Rep x)
-> GPayload (Rep x) (WitnessField (GContext (Rep x)))
forall x.
Rep x x
-> GSupport (Rep x)
-> GPayload (Rep x) (WitnessField (GContext (Rep x)))
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GPayload u (WitnessField (GContext u))
gpayload (x -> Rep x Any
forall x. x -> Rep x x
forall a x. Generic a => a -> Rep a x
G.from x
x)

    -- | Restores `x` from the circuit's outputs.
    restore ::
      Context x ~ c =>
      (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
    default restore ::
      ( Context x ~ c, G.Generic x, GSymbolicData (G.Rep x)
      , Context x ~ GContext (G.Rep x)
      , Support x ~ GSupport (G.Rep x)
      , Layout x ~ GLayout (G.Rep x)
      , Payload x ~ GPayload (G.Rep x)) =>
      (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
    restore Support x -> (c (Layout x), Payload x (WitnessField c))
f = Rep x Any -> x
forall a x. Generic a => Rep a x -> a
forall x. Rep x x -> x
G.to ((GSupport (Rep x)
 -> (c (GLayout (Rep x)), GPayload (Rep x) (WitnessField c)))
-> Rep x Any
forall {k} (u :: k -> Type) (c :: (Type -> Type) -> Type) (x :: k).
(GSymbolicData u, GContext u ~ c) =>
(GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
forall (c :: (Type -> Type) -> Type) x.
(GContext (Rep x) ~ c) =>
(GSupport (Rep x)
 -> (c (GLayout (Rep x)), GPayload (Rep x) (WitnessField c)))
-> Rep x x
grestore GSupport (Rep x)
-> (c (GLayout (Rep x)), GPayload (Rep x) (WitnessField c))
Support x -> (c (Layout x), Payload x (WitnessField c))
f)

type SymbolicOutput x = (SymbolicData x, Support x ~ Proxy (Context x))

instance
    ( Symbolic c
    , Representable f
    , Traversable f
    ) => SymbolicData (c (f :: Type -> Type)) where

    type Context (c f) = c
    type Support (c f) = Proxy c
    type Layout (c f) = f
    type Payload (c f) = U1

    arithmetize :: c f -> Support (c f) -> Context (c f) (Layout (c f))
arithmetize c f
x Support (c f)
_ = c f
Context (c f) (Layout (c f))
x
    payload :: c f
-> Support (c f) -> Payload (c f) (WitnessField (Context (c f)))
payload c f
_ Support (c f)
_ = U1 (WitnessField c)
Payload (c f) (WitnessField (Context (c f)))
forall k (p :: k). U1 p
U1
    restore :: forall (c :: (Type -> Type) -> Type).
(Context (c f) ~ c) =>
(Support (c f)
 -> (c (Layout (c f)), Payload (c f) (WitnessField c)))
-> c f
restore Support (c f) -> (c (Layout (c f)), Payload (c f) (WitnessField c))
f = (c f, U1 (WitnessField c)) -> c f
forall a b. (a, b) -> a
fst (Support (c f) -> (c (Layout (c f)), Payload (c f) (WitnessField c))
f Proxy c
Support (c f)
forall {k} (t :: k). Proxy t
Proxy)

instance Symbolic c => SymbolicData (Proxy (c :: (Type -> Type) -> Type)) where
    type Context (Proxy c) = c
    type Support (Proxy c) = Proxy c
    type Layout (Proxy c) = U1
    type Payload (Proxy c) = U1

    arithmetize :: Proxy c
-> Support (Proxy c) -> Context (Proxy c) (Layout (Proxy c))
arithmetize Proxy c
_ Support (Proxy c)
_ = (forall a. U1 a) -> c U1
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type).
HApplicative c =>
(forall (a :: k). f a) -> c f
forall (f :: Type -> Type). (forall a. f a) -> c f
hpure U1 a
forall a. U1 a
forall k (p :: k). U1 p
U1
    payload :: Proxy c
-> Support (Proxy c)
-> Payload (Proxy c) (WitnessField (Context (Proxy c)))
payload Proxy c
_ Support (Proxy c)
_ = U1 (WitnessField c)
Payload (Proxy c) (WitnessField (Context (Proxy c)))
forall k (p :: k). U1 p
U1
    restore :: forall (c :: (Type -> Type) -> Type).
(Context (Proxy c) ~ c) =>
(Support (Proxy c)
 -> (c (Layout (Proxy c)), Payload (Proxy c) (WitnessField c)))
-> Proxy c
restore Support (Proxy c)
-> (c (Layout (Proxy c)), Payload (Proxy c) (WitnessField c))
_ = Proxy c
forall {k} (t :: k). Proxy t
Proxy

instance
    ( SymbolicData x
    , SymbolicData y
    , HApplicative (Context x)
    , Context x ~ Context y
    , Support x ~ Support y
    ) => SymbolicData (x, y) where

instance
    ( SymbolicData x
    , SymbolicData y
    , SymbolicData z
    , HApplicative (Context x)
    , Context x ~ Context y
    , Context y ~ Context z
    , Support x ~ Support y
    , Support y ~ Support z
    ) => SymbolicData (x, y, z) where

instance
    ( SymbolicData w
    , SymbolicData x
    , SymbolicData y
    , SymbolicData z
    , HApplicative (Context x)
    , Context w ~ Context x
    , Context x ~ Context y
    , Context y ~ Context z
    , Support w ~ Support x
    , Support x ~ Support y
    , Support y ~ Support z
    ) => SymbolicData (w, x, y, z) where

instance
    ( SymbolicData v
    , SymbolicData w
    , SymbolicData x
    , SymbolicData y
    , SymbolicData z
    , HApplicative (Context x)
    , Context v ~ Context w
    , Context w ~ Context x
    , Context x ~ Context y
    , Context y ~ Context z
    , Support v ~ Support w
    , Support w ~ Support x
    , Support x ~ Support y
    , Support y ~ Support z
    ) => SymbolicData (v, w, x, y, z) where

instance
    ( SymbolicData x
    , Package (Context x)
    , KnownNat n
    ) => SymbolicData (Vector n x) where

    type Context (Vector n x) = Context x
    type Support (Vector n x) = Support x
    type Layout (Vector n x) = Vector n :.: Layout x
    type Payload (Vector n x) = Vector n :.: Payload x

    arithmetize :: Vector n x
-> Support (Vector n x)
-> Context (Vector n x) (Layout (Vector n x))
arithmetize Vector n x
xs Support (Vector n x)
s = Vector n (Context x (Layout x))
-> Context x (Vector n :.: Layout x)
forall {k1} (c :: (k1 -> Type) -> Type) (f :: Type -> Type)
       (g :: k1 -> Type).
(Package c, Foldable f, Functor f) =>
f (c g) -> c (f :.: g)
forall (f :: Type -> Type) (g :: Type -> Type).
(Foldable f, Functor f) =>
f (Context x g) -> Context x (f :.: g)
pack ((x -> Support x -> Context x (Layout x))
-> Support x -> x -> Context x (Layout x)
forall a b c. (a -> b -> c) -> b -> a -> c
flip x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize Support x
Support (Vector n x)
s (x -> Context x (Layout x))
-> Vector n x -> Vector n (Context x (Layout x))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector n x
xs)
    payload :: Vector n x
-> Support (Vector n x)
-> Payload (Vector n x) (WitnessField (Context (Vector n x)))
payload Vector n x
xs Support (Vector n x)
s = Vector n (Payload x (WitnessField (Context x)))
-> (:.:) (Vector n) (Payload x) (WitnessField (Context x))
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ((x -> Support x -> Payload x (WitnessField (Context x)))
-> Support x -> x -> Payload x (WitnessField (Context x))
forall a b c. (a -> b -> c) -> b -> a -> c
flip x -> Support x -> Payload x (WitnessField (Context x))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload Support x
Support (Vector n x)
s (x -> Payload x (WitnessField (Context x)))
-> Vector n x -> Vector n (Payload x (WitnessField (Context x)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector n x
xs)
    restore :: forall (c :: (Type -> Type) -> Type).
(Context (Vector n x) ~ c) =>
(Support (Vector n x)
 -> (c (Layout (Vector n x)),
     Payload (Vector n x) (WitnessField c)))
-> Vector n x
restore Support (Vector n x)
-> (c (Layout (Vector n x)), Payload (Vector n x) (WitnessField c))
f = (Rep (Vector n) -> x) -> Vector n x
forall a. (Rep (Vector n) -> a) -> Vector n a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (\Rep (Vector n)
i -> (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
restore ((c (Vector n :.: Layout x) -> c (Layout x))
-> ((:.:) (Vector n) (Payload x) (WitnessField c)
    -> Payload x (WitnessField c))
-> (c (Vector n :.: Layout x),
    (:.:) (Vector n) (Payload x) (WitnessField c))
-> (c (Layout x), Payload x (WitnessField c))
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall a. (:.:) (Vector n) (Layout x) a -> Layout x a)
-> c (Vector n :.: Layout x) -> c (Layout x)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (Rep (Vector n) -> (:.:) (Vector n) (Layout x) a -> Layout x a
forall {k1} {f :: Type -> Type} {g :: k1 -> Type} {p :: k1}.
Representable f =>
Rep f -> (:.:) f g p -> g p
ix Rep (Vector n)
i)) (Rep (Vector n)
-> (:.:) (Vector n) (Payload x) (WitnessField c)
-> Payload x (WitnessField c)
forall {k1} {f :: Type -> Type} {g :: k1 -> Type} {p :: k1}.
Representable f =>
Rep f -> (:.:) f g p -> g p
ix Rep (Vector n)
i) ((c (Vector n :.: Layout x),
  (:.:) (Vector n) (Payload x) (WitnessField c))
 -> (c (Layout x), Payload x (WitnessField c)))
-> (Support x
    -> (c (Vector n :.: Layout x),
        (:.:) (Vector n) (Payload x) (WitnessField c)))
-> Support x
-> (c (Layout x), Payload x (WitnessField c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Support x
-> (c (Vector n :.: Layout x),
    (:.:) (Vector n) (Payload x) (WitnessField c))
Support (Vector n x)
-> (c (Layout (Vector n x)), Payload (Vector n x) (WitnessField c))
f))
      where ix :: Rep f -> (:.:) f g p -> g p
ix Rep f
i = (f (g p) -> Rep f -> g p) -> Rep f -> f (g p) -> g p
forall a b c. (a -> b -> c) -> b -> a -> c
flip f (g p) -> Rep f -> g p
forall a. f a -> Rep f -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index Rep f
i (f (g p) -> g p) -> ((:.:) f g p -> f (g p)) -> (:.:) f g p -> g p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) f g p -> f (g p)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1

instance SymbolicData f => SymbolicData (x -> f) where
    type Context (x -> f) = Context f
    type Support (x -> f) = (x, Support f)
    type Layout (x -> f) = Layout f
    type Payload (x -> f) = Payload f

    arithmetize :: (x -> f) -> Support (x -> f) -> Context (x -> f) (Layout (x -> f))
arithmetize x -> f
f (x
x, Support f
i) = f -> Support f -> Context f (Layout f)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (x -> f
f x
x) Support f
i
    payload :: (x -> f)
-> Support (x -> f)
-> Payload (x -> f) (WitnessField (Context (x -> f)))
payload x -> f
f (x
x, Support f
i) = f -> Support f -> Payload f (WitnessField (Context f))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload (x -> f
f x
x) Support f
i
    restore :: forall (c :: (Type -> Type) -> Type).
(Context (x -> f) ~ c) =>
(Support (x -> f)
 -> (c (Layout (x -> f)), Payload (x -> f) (WitnessField c)))
-> x -> f
restore Support (x -> f)
-> (c (Layout (x -> f)), Payload (x -> f) (WitnessField c))
f x
x = (Support f -> (c (Layout f), Payload f (WitnessField c))) -> f
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context f ~ c) =>
(Support f -> (c (Layout f), Payload f (WitnessField c))) -> f
restore ((x, Support f) -> (c (Layout f), Payload f (WitnessField c))
Support (x -> f)
-> (c (Layout (x -> f)), Payload (x -> f) (WitnessField c))
f ((x, Support f) -> (c (Layout f), Payload f (WitnessField c)))
-> (Support f -> (x, Support f))
-> Support f
-> (c (Layout f), Payload f (WitnessField c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x
x,))

class
    ( Symbolic (GContext u)
    , Traversable (GLayout u)
    , Representable (GLayout u)
    , Representable (GPayload u)
    ) => GSymbolicData u where
    type GContext u :: (Type -> Type) -> Type
    type GSupport u :: Type
    type GLayout u :: Type -> Type
    type GPayload u :: Type -> Type

    garithmetize :: u x -> GSupport u -> GContext u (GLayout u)
    gpayload :: u x -> GSupport u -> GPayload u (WitnessField (GContext u))
    grestore ::
      GContext u ~ c =>
      (GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x

instance
    ( GSymbolicData u
    , GSymbolicData v
    , HApplicative (GContext u)
    , GContext u ~ GContext v
    , GSupport u ~ GSupport v
    ) => GSymbolicData (u :*: v) where

    type GContext (u :*: v) = GContext u
    type GSupport (u :*: v) = GSupport u
    type GLayout (u :*: v) = GLayout u :*: GLayout v
    type GPayload (u :*: v) = GPayload u :*: GPayload v

    garithmetize :: forall (x :: k).
(:*:) u v x
-> GSupport (u :*: v) -> GContext (u :*: v) (GLayout (u :*: v))
garithmetize (u x
a :*: v x
b) = (forall a.
 GLayout u a -> GLayout v a -> (:*:) (GLayout u) (GLayout v) a)
-> GContext v (GLayout u)
-> GContext v (GLayout v)
-> GContext v (GLayout u :*: GLayout v)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type) (h :: k -> Type).
HApplicative c =>
(forall (a :: k). f a -> g a -> h a) -> c f -> c g -> c h
forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type).
(forall a. f a -> g a -> h a)
-> GContext v f -> GContext v g -> GContext v h
hliftA2 GLayout u a -> GLayout v a -> (:*:) (GLayout u) (GLayout v) a
forall a.
GLayout u a -> GLayout v a -> (:*:) (GLayout u) (GLayout v) a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (GContext v (GLayout u)
 -> GContext v (GLayout v) -> GContext v (GLayout u :*: GLayout v))
-> (GSupport v -> GContext v (GLayout u))
-> GSupport v
-> GContext v (GLayout v)
-> GContext v (GLayout u :*: GLayout v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> u x -> GSupport u -> GContext u (GLayout u)
forall (x :: k). u x -> GSupport u -> GContext u (GLayout u)
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GContext u (GLayout u)
garithmetize u x
a (GSupport v
 -> GContext v (GLayout v) -> GContext v (GLayout u :*: GLayout v))
-> (GSupport v -> GContext v (GLayout v))
-> GSupport v
-> GContext v (GLayout u :*: GLayout v)
forall a b.
(GSupport v -> a -> b) -> (GSupport v -> a) -> GSupport v -> b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> v x -> GSupport v -> GContext v (GLayout v)
forall (x :: k). v x -> GSupport v -> GContext v (GLayout v)
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GContext u (GLayout u)
garithmetize v x
b
    gpayload :: forall (x :: k).
(:*:) u v x
-> GSupport (u :*: v)
-> GPayload (u :*: v) (WitnessField (GContext (u :*: v)))
gpayload (u x
a :*: v x
b) = GPayload u (WitnessField (GContext v))
-> GPayload v (WitnessField (GContext v))
-> (:*:) (GPayload u) (GPayload v) (WitnessField (GContext v))
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (GPayload u (WitnessField (GContext v))
 -> GPayload v (WitnessField (GContext v))
 -> (:*:) (GPayload u) (GPayload v) (WitnessField (GContext v)))
-> (GSupport v -> GPayload u (WitnessField (GContext v)))
-> GSupport v
-> GPayload v (WitnessField (GContext v))
-> (:*:) (GPayload u) (GPayload v) (WitnessField (GContext v))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> u x -> GSupport u -> GPayload u (WitnessField (GContext u))
forall (x :: k).
u x -> GSupport u -> GPayload u (WitnessField (GContext u))
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GPayload u (WitnessField (GContext u))
gpayload u x
a (GSupport v
 -> GPayload v (WitnessField (GContext v))
 -> (:*:) (GPayload u) (GPayload v) (WitnessField (GContext v)))
-> (GSupport v -> GPayload v (WitnessField (GContext v)))
-> GSupport v
-> (:*:) (GPayload u) (GPayload v) (WitnessField (GContext v))
forall a b.
(GSupport v -> a -> b) -> (GSupport v -> a) -> GSupport v -> b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> v x -> GSupport v -> GPayload v (WitnessField (GContext v))
forall (x :: k).
v x -> GSupport v -> GPayload v (WitnessField (GContext v))
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GPayload u (WitnessField (GContext u))
gpayload v x
b
    grestore :: forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext (u :*: v) ~ c) =>
(GSupport (u :*: v)
 -> (c (GLayout (u :*: v)), GPayload (u :*: v) (WitnessField c)))
-> (:*:) u v x
grestore GSupport (u :*: v)
-> (c (GLayout (u :*: v)), GPayload (u :*: v) (WitnessField c))
f =
      (GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
forall {k} (u :: k -> Type) (c :: (Type -> Type) -> Type) (x :: k).
(GSymbolicData u, GContext u ~ c) =>
(GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext u ~ c) =>
(GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
grestore ((c (GLayout u :*: GLayout v) -> c (GLayout u))
-> ((:*:) (GPayload u) (GPayload v) (WitnessField c)
    -> GPayload u (WitnessField c))
-> (c (GLayout u :*: GLayout v),
    (:*:) (GPayload u) (GPayload v) (WitnessField c))
-> (c (GLayout u), GPayload u (WitnessField c))
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall a. (:*:) (GLayout u) (GLayout v) a -> GLayout u a)
-> c (GLayout u :*: GLayout v) -> c (GLayout u)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:) (GLayout u) (GLayout v) a -> GLayout u a
forall a. (:*:) (GLayout u) (GLayout v) a -> GLayout u a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP) (:*:) (GPayload u) (GPayload v) (WitnessField c)
-> GPayload u (WitnessField c)
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP ((c (GLayout u :*: GLayout v),
  (:*:) (GPayload u) (GPayload v) (WitnessField c))
 -> (c (GLayout u), GPayload u (WitnessField c)))
-> (GSupport v
    -> (c (GLayout u :*: GLayout v),
        (:*:) (GPayload u) (GPayload v) (WitnessField c)))
-> GSupport v
-> (c (GLayout u), GPayload u (WitnessField c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GSupport v
-> (c (GLayout u :*: GLayout v),
    (:*:) (GPayload u) (GPayload v) (WitnessField c))
GSupport (u :*: v)
-> (c (GLayout (u :*: v)), GPayload (u :*: v) (WitnessField c))
f)
      u x -> v x -> (:*:) u v x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (GSupport v -> (c (GLayout v), GPayload v (WitnessField c))) -> v x
forall {k} (u :: k -> Type) (c :: (Type -> Type) -> Type) (x :: k).
(GSymbolicData u, GContext u ~ c) =>
(GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext v ~ c) =>
(GSupport v -> (c (GLayout v), GPayload v (WitnessField c))) -> v x
grestore ((c (GLayout u :*: GLayout v) -> c (GLayout v))
-> ((:*:) (GPayload u) (GPayload v) (WitnessField c)
    -> GPayload v (WitnessField c))
-> (c (GLayout u :*: GLayout v),
    (:*:) (GPayload u) (GPayload v) (WitnessField c))
-> (c (GLayout v), GPayload v (WitnessField c))
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall a. (:*:) (GLayout u) (GLayout v) a -> GLayout v a)
-> c (GLayout u :*: GLayout v) -> c (GLayout v)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:) (GLayout u) (GLayout v) a -> GLayout v a
forall a. (:*:) (GLayout u) (GLayout v) a -> GLayout v a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP) (:*:) (GPayload u) (GPayload v) (WitnessField c)
-> GPayload v (WitnessField c)
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP ((c (GLayout u :*: GLayout v),
  (:*:) (GPayload u) (GPayload v) (WitnessField c))
 -> (c (GLayout v), GPayload v (WitnessField c)))
-> (GSupport v
    -> (c (GLayout u :*: GLayout v),
        (:*:) (GPayload u) (GPayload v) (WitnessField c)))
-> GSupport v
-> (c (GLayout v), GPayload v (WitnessField c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GSupport v
-> (c (GLayout u :*: GLayout v),
    (:*:) (GPayload u) (GPayload v) (WitnessField c))
GSupport (u :*: v)
-> (c (GLayout (u :*: v)), GPayload (u :*: v) (WitnessField c))
f)

instance GSymbolicData f => GSymbolicData (G.M1 i c f) where
    type GContext (G.M1 i c f) = GContext f
    type GSupport (G.M1 i c f) = GSupport f
    type GLayout (G.M1 i c f) = GLayout f
    type GPayload (G.M1 i c f) = GPayload f
    garithmetize :: forall (x :: k).
M1 i c f x
-> GSupport (M1 i c f) -> GContext (M1 i c f) (GLayout (M1 i c f))
garithmetize (G.M1 f x
a) = f x -> GSupport f -> GContext f (GLayout f)
forall (x :: k). f x -> GSupport f -> GContext f (GLayout f)
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GContext u (GLayout u)
garithmetize f x
a
    gpayload :: forall (x :: k).
M1 i c f x
-> GSupport (M1 i c f)
-> GPayload (M1 i c f) (WitnessField (GContext (M1 i c f)))
gpayload (G.M1 f x
a) = f x -> GSupport f -> GPayload f (WitnessField (GContext f))
forall (x :: k).
f x -> GSupport f -> GPayload f (WitnessField (GContext f))
forall {k} (u :: k -> Type) (x :: k).
GSymbolicData u =>
u x -> GSupport u -> GPayload u (WitnessField (GContext u))
gpayload f x
a
    grestore :: forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext (M1 i c f) ~ c) =>
(GSupport (M1 i c f)
 -> (c (GLayout (M1 i c f)), GPayload (M1 i c f) (WitnessField c)))
-> M1 i c f x
grestore GSupport (M1 i c f)
-> (c (GLayout (M1 i c f)), GPayload (M1 i c f) (WitnessField c))
f = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
G.M1 ((GSupport f -> (c (GLayout f), GPayload f (WitnessField c))) -> f x
forall {k} (u :: k -> Type) (c :: (Type -> Type) -> Type) (x :: k).
(GSymbolicData u, GContext u ~ c) =>
(GSupport u -> (c (GLayout u), GPayload u (WitnessField c))) -> u x
forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext f ~ c) =>
(GSupport f -> (c (GLayout f), GPayload f (WitnessField c))) -> f x
grestore GSupport f -> (c (GLayout f), GPayload f (WitnessField c))
GSupport (M1 i c f)
-> (c (GLayout (M1 i c f)), GPayload (M1 i c f) (WitnessField c))
f)

instance SymbolicData x => GSymbolicData (G.Rec0 x) where
    type GContext (G.Rec0 x) = Context x
    type GSupport (G.Rec0 x) = Support x
    type GLayout (G.Rec0 x) = Layout x
    type GPayload (G.Rec0 x) = Payload x
    garithmetize :: forall (x :: k).
Rec0 x x
-> GSupport (Rec0 x) -> GContext (Rec0 x) (GLayout (Rec0 x))
garithmetize (G.K1 x
x) = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize x
x
    gpayload :: forall (x :: k).
Rec0 x x
-> GSupport (Rec0 x)
-> GPayload (Rec0 x) (WitnessField (GContext (Rec0 x)))
gpayload (G.K1 x
x) = x -> Support x -> Payload x (WitnessField (Context x))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload x
x
    grestore :: forall (c :: (Type -> Type) -> Type) (x :: k).
(GContext (Rec0 x) ~ c) =>
(GSupport (Rec0 x)
 -> (c (GLayout (Rec0 x)), GPayload (Rec0 x) (WitnessField c)))
-> Rec0 x x
grestore GSupport (Rec0 x)
-> (c (GLayout (Rec0 x)), GPayload (Rec0 x) (WitnessField c))
f = x -> K1 R x x
forall k i c (p :: k). c -> K1 i c p
G.K1 ((Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
restore GSupport (Rec0 x)
-> (c (GLayout (Rec0 x)), GPayload (Rec0 x) (WitnessField c))
Support x -> (c (Layout x), Payload x (WitnessField c))
f)