{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation where



import           Control.Applicative                            ()
import           Data.Functor.Rep                               (Rep)
import           GHC.Generics                                   (Generic)
import           GHC.Integer                                    (Integer)
import           GHC.Natural                                    (Natural)
import           Prelude                                        (Eq, Maybe (..), ($), (.), (==))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Data.ByteString                    ()
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var



data UVar a i
  = ConstUVar a
  | LinUVar a (SysVar i) a
  | More
  deriving (forall x. UVar a i -> Rep (UVar a i) x)
-> (forall x. Rep (UVar a i) x -> UVar a i) -> Generic (UVar a i)
forall x. Rep (UVar a i) x -> UVar a i
forall x. UVar a i -> Rep (UVar a i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (i :: Type -> Type) x. Rep (UVar a i) x -> UVar a i
forall a (i :: Type -> Type) x. UVar a i -> Rep (UVar a i) x
$cfrom :: forall a (i :: Type -> Type) x. UVar a i -> Rep (UVar a i) x
from :: forall x. UVar a i -> Rep (UVar a i) x
$cto :: forall a (i :: Type -> Type) x. Rep (UVar a i) x -> UVar a i
to :: forall x. Rep (UVar a i) x -> UVar a i
Generic

instance FromConstant a (UVar a i) where
    fromConstant :: a -> UVar a i
fromConstant = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar
instance FromConstant Natural a => FromConstant Natural (UVar a i) where fromConstant :: Natural -> UVar a i
fromConstant = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> (Natural -> a) -> Natural -> UVar a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant
instance FromConstant Integer a => FromConstant Integer (UVar a i) where fromConstant :: Integer -> UVar a i
fromConstant = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> (Integer -> a) -> Integer -> UVar a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance (Semiring a, Eq a) => Scale a (UVar a i) where
  scale :: a -> UVar a i -> UVar a i
scale a
k (ConstUVar a
c) = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
c
  scale a
k (LinUVar a
a SysVar i
x a
b) = if a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero
    then a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. AdditiveMonoid a => a
zero
    else a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar (a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
a) SysVar i
x (a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
b)
  scale a
k UVar a i
More = if a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero
    then a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. AdditiveMonoid a => a
zero
    else UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (Semiring a, Eq a) => Scale Natural (UVar a i) where scale :: Natural -> UVar a i -> UVar a i
scale Natural
k = a -> UVar a i -> UVar a i
forall b a. Scale b a => b -> a -> a
scale (Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant Natural
k :: a)
instance (Semiring a, Eq a, FromConstant Integer a) => Scale Integer (UVar a i) where scale :: Integer -> UVar a i -> UVar a i
scale Integer
k = a -> UVar a i -> UVar a i
forall b a. Scale b a => b -> a -> a
scale (Integer -> a
forall a b. FromConstant a b => a -> b
fromConstant Integer
k :: a)

instance MultiplicativeMonoid a => Exponent (UVar a i) Natural where
  (ConstUVar a
c) ^ :: UVar a i -> Natural -> UVar a i
^ Natural
n = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a
c a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Natural
n
  UVar a i
v ^ Natural
1             = UVar a i
v
  UVar a i
_ ^ Natural
0             = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. MultiplicativeMonoid a => a
one
  UVar a i
_ ^ Natural
_             = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (Exponent a Integer, MultiplicativeMonoid a) => Exponent (UVar a i) Integer where
  (ConstUVar a
c) ^ :: UVar a i -> Integer -> UVar a i
^ Integer
n   = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a
c a -> Integer -> a
forall a b. Exponent a b => a -> b -> a
^ Integer
n
  (LinUVar a
k SysVar i
x a
b) ^ Integer
1 = a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar a
k SysVar i
x a
b
  UVar a i
_ ^ Integer
0               = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. MultiplicativeMonoid a => a
one
  UVar a i
_ ^ Integer
_               = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (AdditiveMonoid a, Eq a, Eq (Rep i)) => AdditiveSemigroup (UVar a i) where
  ConstUVar a
c + :: UVar a i -> UVar a i -> UVar a i
+ UVar a i
x = a
c a -> UVar a i -> UVar a i
forall a (i :: Type -> Type).
AdditiveSemigroup a =>
a -> UVar a i -> UVar a i
.+ UVar a i
x
  UVar a i
x + ConstUVar a
c = a
c a -> UVar a i -> UVar a i
forall a (i :: Type -> Type).
AdditiveSemigroup a =>
a -> UVar a i -> UVar a i
.+ UVar a i
x
  LinUVar a
k1 SysVar i
x1 a
b1 + (LinUVar a
k2 SysVar i
x2 a
b2) = if SysVar i
x1 SysVar i -> SysVar i -> Bool
forall a. Eq a => a -> a -> Bool
== SysVar i
x2 then
    if a
k1 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
k2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero
      then a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a
b1 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
b2
      else a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar (a
k1 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
k2) SysVar i
x1 (a
b1 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
b2)
    else UVar a i
forall a (i :: Type -> Type). UVar a i
More
  UVar a i
_ + UVar a i
_ = UVar a i
forall a (i :: Type -> Type). UVar a i
More

(.+) :: AdditiveSemigroup a => a -> UVar a i -> UVar a i
a
c1 .+ :: forall a (i :: Type -> Type).
AdditiveSemigroup a =>
a -> UVar a i -> UVar a i
.+ ConstUVar a
c2 = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a
c1 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
c2
a
c .+ LinUVar a
k SysVar i
x a
b = a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar a
k SysVar i
x (a
b a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
c)
a
_ .+ UVar a i
More          = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (Semiring a, Eq a, Eq (Rep i)) => AdditiveMonoid (UVar a i) where
  zero :: UVar a i
zero = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. AdditiveMonoid a => a
zero

instance (Ring a, Eq a, Eq (Rep i)) => AdditiveGroup (UVar a i) where
  negate :: UVar a i -> UVar a i
negate (ConstUVar a
c)   = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> a
forall a. AdditiveGroup a => a -> a
negate a
c)
  negate (LinUVar a
k SysVar i
x a
b) = a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar (a -> a
forall a. AdditiveGroup a => a -> a
negate a
k) SysVar i
x (a -> a
forall a. AdditiveGroup a => a -> a
negate a
b)
  negate UVar a i
More            = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (Semiring a, Eq a) => MultiplicativeSemigroup (UVar a i) where
  ConstUVar a
c * :: UVar a i -> UVar a i -> UVar a i
* UVar a i
x = a -> UVar a i -> UVar a i
forall b a. Scale b a => b -> a -> a
scale a
c UVar a i
x
  UVar a i
x * ConstUVar a
c = a -> UVar a i -> UVar a i
forall b a. Scale b a => b -> a -> a
scale a
c UVar a i
x
  UVar a i
_ * UVar a i
_           = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance (Semiring a, Eq a) => MultiplicativeMonoid (UVar a i) where
  one :: UVar a i
one = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar a
forall a. MultiplicativeMonoid a => a
one

instance (Semiring a, Eq a, Eq (Rep i)) => Semiring (UVar a i)

instance (Ring a, Eq a, Eq (Rep i)) => Ring (UVar a i)

instance (Field a, Eq a, Eq (Rep i)) => Field (UVar a i) where
  finv :: UVar a i -> UVar a i
finv (ConstUVar a
c) = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Field a => a -> a
finv a
c
  finv UVar a i
_             = UVar a i
forall a (i :: Type -> Type). UVar a i
More

instance ToConstant a => ToConstant (UVar a i) where
  type Const (UVar a i) = Maybe (Const a)
  toConstant :: UVar a i -> Const (UVar a i)
toConstant (ConstUVar a
c) = Const a -> Maybe (Const a)
forall a. a -> Maybe a
Just (Const a -> Maybe (Const a)) -> Const a -> Maybe (Const a)
forall a b. (a -> b) -> a -> b
$ a -> Const a
forall a. ToConstant a => a -> Const a
toConstant a
c
  toConstant UVar a i
_             = Maybe (Const a)
Const (UVar a i)
forall a. Maybe a
Nothing

instance Finite a => Finite (UVar a i) where type Order (UVar a i) = Order a

instance FromConstant Natural a => FromConstant (Maybe Natural) (UVar a i) where
    fromConstant :: Maybe Natural -> UVar a i
fromConstant (Just Natural
c) = a -> UVar a i
forall a (i :: Type -> Type). a -> UVar a i
ConstUVar (a -> UVar a i) -> a -> UVar a i
forall a b. (a -> b) -> a -> b
$ Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant Natural
c
    fromConstant Maybe Natural
Nothing  = UVar a i
forall a (i :: Type -> Type). UVar a i
More