{-# LANGUAGE TypeOperators #-}
module ZkFold.Symbolic.Data.List where
import Control.Applicative (Applicative)
import Data.Functor.Rep (Representable)
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Data.Traversable (Traversable)
import Data.Zip (Zip)
import GHC.Generics (Par1 (..))
import Prelude (fmap, fst, pure, type (~), undefined, ($), (.), (<$>))
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Data.Utils (zipWithM)
import ZkFold.Symbolic.Class
import ZkFold.Symbolic.Data.Bool (Bool (..))
import ZkFold.Symbolic.Data.Class
import ZkFold.Symbolic.Data.Combinators
import ZkFold.Symbolic.Data.Conditional
import ZkFold.Symbolic.MonadCircuit
data List (context :: (Type -> Type) -> Type) x
= List
{ forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lHash :: (context (Layout x))
, forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lSize :: (context Par1)
, forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lWitness :: [x]
}
emptyList
:: forall context x
. Symbolic context
=> Applicative (Layout x)
=> List context x
emptyList :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x)) =>
List context x
emptyList = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List (Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero) (Par1 (BaseField context) -> context Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Par1 (BaseField context) -> context Par1)
-> Par1 (BaseField context) -> context Par1
forall a b. (a -> b) -> a -> b
$ BaseField context -> Par1 (BaseField context)
forall p. p -> Par1 p
Par1 BaseField context
forall a. AdditiveMonoid a => a
zero) []
null
:: forall context x
. Symbolic context
=> List context x
-> Bool context
null :: forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = context Par1 -> Bool context
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (((Par1 i, Par1 i) -> Par1 i) -> m (Par1 i, Par1 i) -> m (Par1 i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Par1 i, Par1 i) -> Par1 i
forall a b. (a, b) -> a
fst (m (Par1 i, Par1 i) -> m (Par1 i))
-> (Par1 i -> m (Par1 i, Par1 i)) -> Par1 i -> m (Par1 i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 i -> m (Par1 i, Par1 i)
forall i a (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a m, Representable f, Traversable f) =>
f i -> m (f i, f i)
runInvert))
infixr 5 .:
(.:)
:: forall context x
. Symbolic context
=> Traversable (Layout x)
=> Zip (Layout x)
=> SymbolicData x
=> Context x ~ context
=> Support x ~ Proxy context
=> x
-> List context x
-> List context x
x
x .: :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Traversable (Layout x), Zip (Layout x),
SymbolicData x, Context x ~ context, Support x ~ Proxy context) =>
x -> List context x -> List context x
.: List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List context (Layout x)
incSum context Par1
incSize (x
xx -> [x] -> [x]
forall a. a -> [a] -> [a]
:[x]
lWitness)
where
xRepr :: context (Layout x)
xRepr :: context (Layout x)
xRepr = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x (forall {k} (t :: k). Proxy t
forall (t :: (Type -> Type) -> Type). Proxy t
Proxy @context)
incSum :: context (Layout x)
incSum :: context (Layout x)
incSum = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
\Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
h x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
r x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))) Layout x i
vHash Layout x i
vRepr
incSize :: context Par1
incSize :: context Par1
incSize = context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (\(Par1 i
s) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))
uncons
:: forall context x
. Symbolic context
=> SymbolicData x
=> Applicative (Layout x)
=> Traversable (Layout x)
=> Representable (Layout x)
=> Zip (Layout x)
=> SymbolicData (List context x)
=> Representable (Layout (List context x))
=> Traversable (Layout (List context x))
=> Context x ~ context
=> Context (List context x) ~ context
=> Support x ~ Proxy context
=> List context x
-> (x, List context x)
uncons :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, SymbolicData x, Applicative (Layout x),
Traversable (Layout x), Representable (Layout x), Zip (Layout x),
SymbolicData (List context x),
Representable (Layout (List context x)),
Traversable (Layout (List context x)), Context x ~ context,
Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> (x, List context x)
uncons List context x
l = (List context x -> x
forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
Representable (Layout x), Zip (Layout x), SymbolicData x,
Context x ~ context, Support x ~ Proxy context) =>
List context x -> x
head List context x
l, List context x -> List context x
forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
Zip (Layout x), SymbolicData x, SymbolicData (List context x),
Representable (Layout (List context x)),
Traversable (Layout (List context x)), Context x ~ context,
Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> List context x
tail List context x
l)
head
:: forall context x
. Symbolic context
=> Applicative (Layout x)
=> Traversable (Layout x)
=> Representable (Layout x)
=> Zip (Layout x)
=> SymbolicData x
=> Context x ~ context
=> Support x ~ Proxy context
=> List context x -> x
head :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
Representable (Layout x), Zip (Layout x), SymbolicData x,
Context x ~ context, Support x ~ Proxy context) =>
List context x -> x
head xs :: List context x
xs@List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = x -> x -> Bool context -> x
forall b a. Conditional b a => a -> a -> b -> a
bool ((Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore ((Support x -> Context x (Layout x)) -> x)
-> (Support x -> Context x (Layout x)) -> x
forall a b. (a -> b) -> a -> b
$ \Support x
_ -> context (Layout x)
Context x (Layout x)
unsafeHead) ((Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore ((Support x -> Context x (Layout x)) -> x)
-> (Support x -> Context x (Layout x)) -> x
forall a b. (a -> b) -> a -> b
$ \Support x
_ -> Layout x (BaseField (Context x)) -> Context x (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField (Context x)) -> Context x (Layout x))
-> Layout x (BaseField (Context x)) -> Context x (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero) (List context x -> Bool context
forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List context x
xs)
where
xRepr :: context (Layout x)
xRepr :: context (Layout x)
xRepr = case [x]
lWitness of
(x
x:[x]
_) -> x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy
[x]
_ -> Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero
unsafeHead :: context (Layout x)
unsafeHead :: context (Layout x)
unsafeHead = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
\Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> NewConstraint i (BaseField context)
-> Witness i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
NewConstraint var a -> Witness var a -> m var
newConstrained (\i -> x
p i
v -> i -> x
p i
h x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
v x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one)) ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
r)) Layout x i
vHash Layout x i
vRepr
tail
:: forall context x
. Symbolic context
=> Applicative (Layout x)
=> Traversable (Layout x)
=> Zip (Layout x)
=> SymbolicData x
=> SymbolicData (List context x)
=> Representable (Layout (List context x))
=> Traversable (Layout (List context x))
=> Context x ~ context
=> Context (List context x) ~ context
=> Support x ~ Proxy context
=> List context x
-> List context x
tail :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
Zip (Layout x), SymbolicData x, SymbolicData (List context x),
Representable (Layout (List context x)),
Traversable (Layout (List context x)), Context x ~ context,
Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> List context x
tail xs :: List context x
xs@List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = List context x -> List context x -> Bool context -> List context x
forall b a. Conditional b a => a -> a -> b -> a
bool List context x
unsafeTail List context x
xs (List context x -> Bool context
forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List context x
xs)
where
tailId :: [a] -> [a]
tailId :: forall a. [a] -> [a]
tailId [] = []
tailId (a
_:[a]
xs') = [a]
xs'
unsafeTail :: List context x
unsafeTail :: List context x
unsafeTail = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List context (Layout x)
decSum context Par1
decSize ([x] -> [x]
forall a. [a] -> [a]
tailId [x]
lWitness)
xRepr :: context (Layout x)
xRepr :: context (Layout x)
xRepr = case [x]
lWitness of
(x
x:[x]
_) -> x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy
[x]
_ -> Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero
decSum :: context (Layout x)
decSum :: context (Layout x)
decSum = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField context) m =>
Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
\Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
h x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
r x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
s)) Layout x i
vHash Layout x i
vRepr
decSize :: context Par1
decSize :: context Par1
decSize = context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (\(Par1 i
s) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
s x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
forall a. MultiplicativeMonoid a => a
one))
last :: List context x -> x
last :: forall (context :: (Type -> Type) -> Type) x. List context x -> x
last = List context x -> x
forall a. HasCallStack => a
undefined
(++) :: List context x -> List context x -> List context x
List context x
_ ++ :: forall (context :: (Type -> Type) -> Type) x.
List context x -> List context x -> List context x
++ List context x
_ = List context x
forall a. HasCallStack => a
undefined
filter ::
(x -> Bool context)
-> List context x
-> List context x
filter :: forall x (context :: (Type -> Type) -> Type).
(x -> Bool context) -> List context x -> List context x
filter = (x -> Bool context) -> List context x -> List context x
forall a. HasCallStack => a
undefined
delete :: x -> List context x -> List context x
delete :: forall x (context :: (Type -> Type) -> Type).
x -> List context x -> List context x
delete = x -> List context x -> List context x
forall a. HasCallStack => a
undefined
(\\) :: List context x -> List context x -> List context x
List context x
_ \\ :: forall (context :: (Type -> Type) -> Type) x.
List context x -> List context x -> List context x
\\ List context x
_ = List context x
forall a. HasCallStack => a
undefined