module ZkFold.Base.Protocol.Plonkup.PlonkupConstraint where

import           Data.Functor.Rep                                    (Rep)
import           Prelude                                             hiding (Num (..), drop, length, replicate, sum,
                                                                      take, (!!), (/), (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Protocol.Plonkup.LookupConstraint       (LookupConstraint (..))
import           ZkFold.Base.Protocol.Plonkup.PlonkConstraint        (PlonkConstraint (..), toPlonkConstraint)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var      (toVar)

data PlonkupConstraint i a = ConsPlonk (PlonkConstraint i a) | ConsLookup (LookupConstraint i a) | ConsExtra

getPlonkConstraint :: (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint :: forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint (ConsPlonk PlonkConstraint i a
c) = PlonkConstraint i a
c
getPlonkConstraint PlonkupConstraint i a
_             = Poly a (Var a i) Natural -> PlonkConstraint i a
forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
Poly a (Var a i) Natural -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a i) Natural
forall a. AdditiveMonoid a => a
zero

isLookupConstraint :: FiniteField a => PlonkupConstraint i a -> a
isLookupConstraint :: forall a (i :: Type -> Type).
FiniteField a =>
PlonkupConstraint i a -> a
isLookupConstraint (ConsLookup LookupConstraint i a
_) = a
forall a. MultiplicativeMonoid a => a
one
isLookupConstraint PlonkupConstraint i a
_              = a
forall a. AdditiveMonoid a => a
zero

getA :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
getA :: forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
PlonkupConstraint i a -> Var a i
getA (ConsPlonk PlonkConstraint i a
c)  = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x1 PlonkConstraint i a
c
getA (ConsLookup LookupConstraint i a
c) = SysVar i -> Var a i
forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar (SysVar i -> Var a i) -> SysVar i -> Var a i
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar i
forall {k} (i :: Type -> Type) (a :: k).
LookupConstraint i a -> SysVar i
lkVar LookupConstraint i a
c
getA PlonkupConstraint i a
ConsExtra      = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x1 (Poly a (Var a i) Natural -> PlonkConstraint i a
forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
Poly a (Var a i) Natural -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a i) Natural
forall a. AdditiveMonoid a => a
zero)

getB :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
getB :: forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
PlonkupConstraint i a -> Var a i
getB (ConsPlonk PlonkConstraint i a
c)  = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x2 PlonkConstraint i a
c
getB (ConsLookup LookupConstraint i a
c) = SysVar i -> Var a i
forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar (SysVar i -> Var a i) -> SysVar i -> Var a i
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar i
forall {k} (i :: Type -> Type) (a :: k).
LookupConstraint i a -> SysVar i
lkVar LookupConstraint i a
c
getB PlonkupConstraint i a
ConsExtra      = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x2 (Poly a (Var a i) Natural -> PlonkConstraint i a
forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
Poly a (Var a i) Natural -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a i) Natural
forall a. AdditiveMonoid a => a
zero)

getC :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
getC :: forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
PlonkupConstraint i a -> Var a i
getC (ConsPlonk PlonkConstraint i a
c)  = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x3 PlonkConstraint i a
c
getC (ConsLookup LookupConstraint i a
c) = SysVar i -> Var a i
forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar (SysVar i -> Var a i) -> SysVar i -> Var a i
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar i
forall {k} (i :: Type -> Type) (a :: k).
LookupConstraint i a -> SysVar i
lkVar LookupConstraint i a
c
getC PlonkupConstraint i a
ConsExtra      = PlonkConstraint i a -> Var a i
forall (i :: Type -> Type) a. PlonkConstraint i a -> Var a i
x3 (Poly a (Var a i) Natural -> PlonkConstraint i a
forall a (i :: Type -> Type).
(Ord a, FiniteField a, Ord (Rep i)) =>
Poly a (Var a i) Natural -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a i) Natural
forall a. AdditiveMonoid a => a
zero)