{-# LANGUAGE DerivingStrategies #-}

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness where

import           Control.Applicative             (Applicative (..))
import           Control.DeepSeq                 (NFData (..), rwhnf)
import           Control.Monad                   (Monad (..), ap)
import           Data.Function                   ((.))
import           Data.Functor                    (Functor)
import           Numeric.Natural                 (Natural)
import           Prelude                         (Integer)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Symbolic.MonadCircuit    (ResidueField)

type IsWitness a n w = (Scale a w, FromConstant a w, ResidueField n w)

newtype WitnessF a v = WitnessF { forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF :: forall n w. IsWitness a n w => (v -> w) -> w }
  deriving ((forall a b. (a -> b) -> WitnessF a a -> WitnessF a b)
-> (forall a b. a -> WitnessF a b -> WitnessF a a)
-> Functor (WitnessF a)
forall a b. a -> WitnessF a b -> WitnessF a a
forall a b. (a -> b) -> WitnessF a a -> WitnessF a b
forall a a b. a -> WitnessF a b -> WitnessF a a
forall a a b. (a -> b) -> WitnessF a a -> WitnessF a b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> WitnessF a a -> WitnessF a b
fmap :: forall a b. (a -> b) -> WitnessF a a -> WitnessF a b
$c<$ :: forall a a b. a -> WitnessF a b -> WitnessF a a
<$ :: forall a b. a -> WitnessF a b -> WitnessF a a
Functor)

instance NFData (WitnessF a v) where
  -- From instance NFData (a -> b):
  -- This instance is for convenience and consistency with seq.
  -- This assumes that WHNF is equivalent to NF for functions.
  rnf :: WitnessF a v -> ()
rnf = WitnessF a v -> ()
forall a. a -> ()
rwhnf

instance Applicative (WitnessF a) where
  pure :: forall a. a -> WitnessF a a
pure a
v = (forall n w. IsWitness a n w => (a -> w) -> w) -> WitnessF a a
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (\a -> w
x -> a -> w
x a
v)
  <*> :: forall a b. WitnessF a (a -> b) -> WitnessF a a -> WitnessF a b
(<*>) = WitnessF a (a -> b) -> WitnessF a a -> WitnessF a b
forall (m :: Type -> Type) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad (WitnessF a) where
  WitnessF forall n w. IsWitness a n w => (a -> w) -> w
f >>= :: forall a b. WitnessF a a -> (a -> WitnessF a b) -> WitnessF a b
>>= a -> WitnessF a b
k = (forall n w. IsWitness a n w => (b -> w) -> w) -> WitnessF a b
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (\b -> w
x -> (a -> w) -> w
forall n w. IsWitness a n w => (a -> w) -> w
f (\a
a -> WitnessF a b -> forall n w. IsWitness a n w => (b -> w) -> w
forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF (a -> WitnessF a b
k a
a) b -> w
x))

instance FromConstant Natural (WitnessF a v) where fromConstant :: Natural -> WitnessF a v
fromConstant Natural
x = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (Natural -> (v -> w) -> w
forall a b. FromConstant a b => a -> b
fromConstant Natural
x)
instance FromConstant Integer (WitnessF a v) where fromConstant :: Integer -> WitnessF a v
fromConstant Integer
x = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (Integer -> (v -> w) -> w
forall a b. FromConstant a b => a -> b
fromConstant Integer
x)
instance {-# INCOHERENT #-} FromConstant a (WitnessF a v) where fromConstant :: a -> WitnessF a v
fromConstant a
x = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (a -> (v -> w) -> w
forall a b. FromConstant a b => a -> b
fromConstant a
x)
instance Scale Natural (WitnessF a v) where scale :: Natural -> WitnessF a v -> WitnessF a v
scale Natural
k (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (Natural -> ((v -> w) -> w) -> (v -> w) -> w
forall b a. Scale b a => b -> a -> a
scale Natural
k (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
instance Scale Integer (WitnessF a v) where scale :: Integer -> WitnessF a v -> WitnessF a v
scale Integer
k (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (Integer -> ((v -> w) -> w) -> (v -> w) -> w
forall b a. Scale b a => b -> a -> a
scale Integer
k (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
instance Scale a (WitnessF a v) where scale :: a -> WitnessF a v -> WitnessF a v
scale a
k (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (a -> w -> w
forall b a. Scale b a => b -> a -> a
scale a
k (w -> w) -> ((v -> w) -> w) -> (v -> w) -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
instance Exponent (WitnessF a v) Natural where WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f ^ :: WitnessF a v -> Natural -> WitnessF a v
^ Natural
p = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f ((v -> w) -> w) -> Natural -> (v -> w) -> w
forall a b. Exponent a b => a -> b -> a
^ Natural
p)
instance Exponent (WitnessF a v) Integer where WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f ^ :: WitnessF a v -> Integer -> WitnessF a v
^ Integer
p = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f ((v -> w) -> w) -> Integer -> (v -> w) -> w
forall a b. Exponent a b => a -> b -> a
^ Integer
p)
instance AdditiveSemigroup (WitnessF a v) where WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f + :: WitnessF a v -> WitnessF a v -> WitnessF a v
+ WitnessF forall n w. IsWitness a n w => (v -> w) -> w
g = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f ((v -> w) -> w) -> ((v -> w) -> w) -> (v -> w) -> w
forall a. AdditiveSemigroup a => a -> a -> a
+ (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
g)
instance AdditiveMonoid (WitnessF a v) where zero :: WitnessF a v
zero = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (v -> w) -> w
forall a. AdditiveMonoid a => a
forall n w. IsWitness a n w => (v -> w) -> w
zero
instance AdditiveGroup (WitnessF a v) where
  negate :: WitnessF a v -> WitnessF a v
negate (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (((v -> w) -> w) -> (v -> w) -> w
forall a. AdditiveGroup a => a -> a
negate (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
  WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f - :: WitnessF a v -> WitnessF a v -> WitnessF a v
- WitnessF forall n w. IsWitness a n w => (v -> w) -> w
g = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f ((v -> w) -> w) -> ((v -> w) -> w) -> (v -> w) -> w
forall a. AdditiveGroup a => a -> a -> a
- (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
g)
instance MultiplicativeSemigroup (WitnessF a v) where WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f * :: WitnessF a v -> WitnessF a v -> WitnessF a v
* WitnessF forall n w. IsWitness a n w => (v -> w) -> w
g = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f ((v -> w) -> w) -> ((v -> w) -> w) -> (v -> w) -> w
forall a. MultiplicativeSemigroup a => a -> a -> a
* (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
g)
instance MultiplicativeMonoid (WitnessF a v) where one :: WitnessF a v
one = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (v -> w) -> w
forall a. MultiplicativeMonoid a => a
forall n w. IsWitness a n w => (v -> w) -> w
one
instance Semiring (WitnessF a v)
instance Ring (WitnessF a v)
instance Field (WitnessF a v) where
  finv :: WitnessF a v -> WitnessF a v
finv (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (w -> w
forall a. Field a => a -> a
finv (w -> w) -> ((v -> w) -> w) -> (v -> w) -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
  WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f // :: WitnessF a v -> WitnessF a v -> WitnessF a v
// WitnessF forall n w. IsWitness a n w => (v -> w) -> w
g = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (\v -> w
x -> (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f v -> w
x w -> w -> w
forall a. Field a => a -> a -> a
// (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
g v -> w
x)
instance ToConstant (WitnessF a v) where
  type Const (WitnessF a v) = EuclideanF a v
  toConstant :: WitnessF a v -> Const (WitnessF a v)
toConstant (WitnessF forall n w. IsWitness a n w => (v -> w) -> w
f) = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (w -> n
w -> Const w
forall a. ToConstant a => a -> Const a
toConstant (w -> n) -> ((v -> w) -> w) -> (v -> w) -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> w) -> w
forall n w. IsWitness a n w => (v -> w) -> w
f)
instance FromConstant (EuclideanF a v) (WitnessF a v) where fromConstant :: EuclideanF a v -> WitnessF a v
fromConstant (EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f) = (forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (n -> w
forall a b. FromConstant a b => a -> b
fromConstant (n -> w) -> ((v -> w) -> n) -> (v -> w) -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f)
instance Finite a => Finite (WitnessF a v) where type Order (WitnessF a v) = Order a

newtype EuclideanF a v = EuclideanF { forall a v.
EuclideanF a v -> forall n w. IsWitness a n w => (v -> w) -> n
euclideanF :: forall n w. IsWitness a n w => (v -> w) -> n }

instance FromConstant Natural (EuclideanF a v) where fromConstant :: Natural -> EuclideanF a v
fromConstant Natural
x = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (Natural -> (v -> w) -> n
forall a b. FromConstant a b => a -> b
fromConstant Natural
x)
instance Scale Natural (EuclideanF a v) where scale :: Natural -> EuclideanF a v -> EuclideanF a v
scale Natural
k (EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f) = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (Natural -> ((v -> w) -> n) -> (v -> w) -> n
forall b a. Scale b a => b -> a -> a
scale Natural
k (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f)
instance Exponent (EuclideanF a v) Natural where EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f ^ :: EuclideanF a v -> Natural -> EuclideanF a v
^ Natural
p = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF ((v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f ((v -> w) -> n) -> Natural -> (v -> w) -> n
forall a b. Exponent a b => a -> b -> a
^ Natural
p)
instance AdditiveSemigroup (EuclideanF a v) where EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f + :: EuclideanF a v -> EuclideanF a v -> EuclideanF a v
+ EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
g = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF ((v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f ((v -> w) -> n) -> ((v -> w) -> n) -> (v -> w) -> n
forall a. AdditiveSemigroup a => a -> a -> a
+ (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
g)
instance AdditiveMonoid (EuclideanF a v) where zero :: EuclideanF a v
zero = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (v -> w) -> n
forall a. AdditiveMonoid a => a
forall n w. IsWitness a n w => (v -> w) -> n
zero
instance MultiplicativeSemigroup (EuclideanF a v) where EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f * :: EuclideanF a v -> EuclideanF a v -> EuclideanF a v
* EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
g = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF ((v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f ((v -> w) -> n) -> ((v -> w) -> n) -> (v -> w) -> n
forall a. MultiplicativeSemigroup a => a -> a -> a
* (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
g)
instance MultiplicativeMonoid (EuclideanF a v) where one :: EuclideanF a v
one = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (v -> w) -> n
forall a. MultiplicativeMonoid a => a
forall n w. IsWitness a n w => (v -> w) -> n
one
instance Semiring (EuclideanF a v)
instance SemiEuclidean (EuclideanF a v) where
  EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f div :: EuclideanF a v -> EuclideanF a v -> EuclideanF a v
`div` EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
g = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (\v -> w
x -> (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f v -> w
x n -> n -> n
forall a. SemiEuclidean a => a -> a -> a
`div` (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
g v -> w
x)
  EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
f mod :: EuclideanF a v -> EuclideanF a v -> EuclideanF a v
`mod` EuclideanF forall n w. IsWitness a n w => (v -> w) -> n
g = (forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> n) -> EuclideanF a v
EuclideanF (\v -> w
x -> (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
f v -> w
x n -> n -> n
forall a. SemiEuclidean a => a -> a -> a
`mod` (v -> w) -> n
forall n w. IsWitness a n w => (v -> w) -> n
g v -> w
x)