module ZkFold.Base.Protocol.Plonkup.PlonkupConstraint where

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

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.Vector                             (Vector)
import           ZkFold.Base.Protocol.Plonkup.LookupConstraint       (LookupConstraint (..))
import           ZkFold.Base.Protocol.Plonkup.PlonkConstraint        (PlonkConstraint (..), toPlonkConstraint)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

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

getPlonkConstraint :: (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat 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 (Vector i)) Nat -> PlonkConstraint i a
forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero

isLookupConstraint :: FiniteField a => PlonkupConstraint i a -> a
isLookupConstraint :: forall a (i :: Nat). 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, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i)
getA :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getA (ConsPlonk PlonkConstraint i a
c)  = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x1 PlonkConstraint i a
c
getA (ConsLookup LookupConstraint i a
c) = SysVar (Vector i) -> Var a (Vector i)
forall a (i :: Type -> Type). SysVar i -> Var a i
SysVar (SysVar (Vector i) -> Var a (Vector i))
-> SysVar (Vector i) -> Var a (Vector i)
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar (Vector i)
forall {k} (i :: Nat) (a :: k).
LookupConstraint i a -> SysVar (Vector i)
lkVar LookupConstraint i a
c
getA PlonkupConstraint i a
ConsExtra      = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x1 (forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint @a Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero)

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

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