{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.Payloaded where

import           Data.Binary                      (Binary)
import           Data.Function                    (const, ($), (.))
import           Data.Functor.Rep                 (Rep, Representable)
import           Data.Proxy                       (Proxy (..))
import           Data.Tuple                       (snd)
import           GHC.Generics                     (U1 (..))

import           ZkFold.Base.Control.HApplicative (hunit)
import           ZkFold.Symbolic.Class            (Symbolic (..))
import           ZkFold.Symbolic.Data.Bool        (true)
import           ZkFold.Symbolic.Data.Class       (SymbolicData (..))
import           ZkFold.Symbolic.Data.Input       (SymbolicInput (..))

newtype Payloaded f c = Payloaded { forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
Payloaded f c -> f (WitnessField c)
runPayloaded :: f (WitnessField c) }

instance (Symbolic c, Representable f) => SymbolicData (Payloaded f c) where
  type Context (Payloaded f c) = c
  type Support (Payloaded f c) = Proxy c
  type Layout (Payloaded f c) = U1
  type Payload (Payloaded f c) = f

  arithmetize :: Payloaded f c
-> Support (Payloaded f c)
-> Context (Payloaded f c) (Layout (Payloaded f c))
arithmetize Payloaded f c
_ Support (Payloaded f c)
_ = c U1
Context (Payloaded f c) (Layout (Payloaded f c))
forall {k} (c :: (k -> Type) -> Type). HApplicative c => c U1
hunit
  payload :: Payloaded f c
-> Support (Payloaded f c)
-> Payload (Payloaded f c) (WitnessField (Context (Payloaded f c)))
payload = f (WitnessField c) -> Proxy c -> f (WitnessField c)
forall a b. a -> b -> a
const (f (WitnessField c) -> Proxy c -> f (WitnessField c))
-> (Payloaded f c -> f (WitnessField c))
-> Payloaded f c
-> Proxy c
-> f (WitnessField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Payloaded f c -> f (WitnessField c)
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
Payloaded f c -> f (WitnessField c)
runPayloaded
  restore :: forall (c :: (Type -> Type) -> Type).
(Context (Payloaded f c) ~ c) =>
(Support (Payloaded f c)
 -> (c (Layout (Payloaded f c)),
     Payload (Payloaded f c) (WitnessField c)))
-> Payloaded f c
restore = f (WitnessField c) -> Payloaded f c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded (f (WitnessField c) -> Payloaded f c)
-> ((Proxy c -> (c U1, f (WitnessField c))) -> f (WitnessField c))
-> (Proxy c -> (c U1, f (WitnessField c)))
-> Payloaded f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c U1, f (WitnessField c)) -> f (WitnessField c)
forall a b. (a, b) -> b
snd ((c U1, f (WitnessField c)) -> f (WitnessField c))
-> ((Proxy c -> (c U1, f (WitnessField c)))
    -> (c U1, f (WitnessField c)))
-> (Proxy c -> (c U1, f (WitnessField c)))
-> f (WitnessField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Proxy c -> (c U1, f (WitnessField c)))
-> Proxy c -> (c U1, f (WitnessField c))
forall a b. (a -> b) -> a -> b
$ Proxy c
forall {k} (t :: k). Proxy t
Proxy)

instance (Symbolic c, Representable f, Binary (Rep f)) =>
    SymbolicInput (Payloaded f c) where
  isValid :: Payloaded f c -> Bool (Context (Payloaded f c))
isValid = Bool c -> Payloaded f c -> Bool c
forall a b. a -> b -> a
const Bool c
forall b. BoolType b => b
true