{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.Payloaded where

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

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Control.HApplicative (hunit)
import           ZkFold.Symbolic.Class            (Symbolic (..))
import           ZkFold.Symbolic.Data.Bool        (Bool (..), true)
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Conditional (Conditional (..))
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, PayloadFunctor 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, PayloadFunctor 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

instance (Symbolic c, PayloadFunctor f) => Conditional (Bool c) (Payloaded f c) where
  bool :: Payloaded f c -> Payloaded f c -> Bool c -> Payloaded f c
bool (Payloaded f (WitnessField c)
onFalse) (Payloaded f (WitnessField c)
onTrue) (Bool (c Par1 -> Par1 (WitnessField c)
forall (f :: Type -> Type). Functor f => c f -> f (WitnessField c)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
c f -> f (WitnessField c)
witnessF -> Par1 WitnessField c
b)) =
    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)
-> f (WitnessField c) -> Payloaded f c
forall a b. (a -> b) -> a -> b
$ (WitnessField c -> WitnessField c -> WitnessField c)
-> f (WitnessField c) -> f (WitnessField c) -> f (WitnessField c)
forall (f :: Type -> Type) a b c.
Representable f =>
(a -> b -> c) -> f a -> f b -> f c
mzipWithRep (\WitnessField c
f WitnessField c
t -> WitnessField c
t WitnessField c -> WitnessField c -> WitnessField c
forall a. MultiplicativeSemigroup a => a -> a -> a
* WitnessField c
b WitnessField c -> WitnessField c -> WitnessField c
forall a. AdditiveSemigroup a => a -> a -> a
+ (WitnessField c
forall a. MultiplicativeMonoid a => a
one WitnessField c -> WitnessField c -> WitnessField c
forall a. AdditiveGroup a => a -> a -> a
- WitnessField c
b) WitnessField c -> WitnessField c -> WitnessField c
forall a. MultiplicativeSemigroup a => a -> a -> a
* WitnessField c
f) f (WitnessField c)
onFalse f (WitnessField c)
onTrue