{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.List where

import           Control.Monad                    (return)
import           Data.Distributive                (Distributive (..))
import           Data.Function                    (const)
import           Data.Functor                     (Functor)
import           Data.Functor.Rep                 (Representable, distributeRep, pureRep, tabulate)
import           Data.List.Infinite               (Infinite (..))
import           Data.Proxy                       (Proxy (..))
import           Data.Traversable                 (traverse)
import           Data.Tuple                       (snd)
import           GHC.Generics                     (Generic, Generic1, Par1 (..), (:*:) (..), (:.:) (..))
import           Prelude                          (fmap, fst, type (~), undefined, ($), (.), (<$>))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Data.Functor.Rep     ()
import           ZkFold.Base.Data.HFunctor        (hmap)
import           ZkFold.Base.Data.List.Infinite   ()
import           ZkFold.Base.Data.Product         (fstP, sndP)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool        (Bool (..))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (Payloaded))
import           ZkFold.Symbolic.Data.UInt        (UInt)
import           ZkFold.Symbolic.MonadCircuit

data ListItem x a = ListItem
  { forall x a. ListItem x a -> Layout x a
tailHash    :: Layout x a
  , forall x a. ListItem x a -> Layout x a
headLayout  :: Layout x a
  , forall x a. ListItem x a -> Payload x a
headPayload :: Payload x a
  }
  deriving ((forall a. ListItem x a -> Rep1 (ListItem x) a)
-> (forall a. Rep1 (ListItem x) a -> ListItem x a)
-> Generic1 (ListItem x)
forall a. Rep1 (ListItem x) a -> ListItem x a
forall a. ListItem x a -> Rep1 (ListItem x) a
forall x a. Rep1 (ListItem x) a -> ListItem x a
forall x a. ListItem x a -> Rep1 (ListItem x) a
forall k (f :: k -> Type).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall x a. ListItem x a -> Rep1 (ListItem x) a
from1 :: forall a. ListItem x a -> Rep1 (ListItem x) a
$cto1 :: forall x a. Rep1 (ListItem x) a -> ListItem x a
to1 :: forall a. Rep1 (ListItem x) a -> ListItem x a
Generic1)

deriving instance
  (Functor (Layout x), Functor (Payload x)) =>
  Functor (ListItem x)

instance
    (Representable (Layout x), Representable (Payload x)) =>
    Distributive (ListItem x) where
  distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (ListItem x a) -> ListItem x (f a)
distribute = f (ListItem x a) -> ListItem x (f a)
forall (f :: Type -> Type) (w :: Type -> Type) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep

instance
  (Representable (Layout x), Representable (Payload x)) =>
  Representable (ListItem x)

data List c x = List
  { forall (c :: (Type -> Type) -> Type) x. List c x -> c (Layout x)
lHash    :: c (Layout x)
  , forall (c :: (Type -> Type) -> Type) x. List c x -> c Par1
lSize    :: c Par1
  , forall (c :: (Type -> Type) -> Type) x.
List c x -> Payloaded (Infinite :.: ListItem x) c
lWitness :: Payloaded (Infinite :.: ListItem x) c
  }
  deriving ((forall x. List c x -> Rep (List c x) x)
-> (forall x. Rep (List c x) x -> List c x) -> Generic (List c x)
forall x. Rep (List c x) x -> List c x
forall x. List c x -> Rep (List c x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (c :: (Type -> Type) -> Type) x x.
Rep (List c x) x -> List c x
forall (c :: (Type -> Type) -> Type) x x.
List c x -> Rep (List c x) x
$cfrom :: forall (c :: (Type -> Type) -> Type) x x.
List c x -> Rep (List c x) x
from :: forall x. List c x -> Rep (List c x) x
$cto :: forall (c :: (Type -> Type) -> Type) x x.
Rep (List c x) x -> List c x
to :: forall x. Rep (List c x) x -> List c x
Generic)

instance (SymbolicData x, c ~ Context x) => SymbolicData (List c x)
-- | TODO: Maybe some 'isValid' check for Lists?..
instance (SymbolicInput x, c ~ Context x) => SymbolicInput (List c x)

-- | TODO: A proof-of-concept where hash == id.
-- Replace id with a proper hash if we need lists to be cryptographically secure.
--
emptyList
    :: forall context x
    .  SymbolicData x
    => Context x ~ context
    => List context x
emptyList :: forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList = context (Layout x)
-> context Par1
-> Payloaded (Infinite :.: ListItem x) context
-> List context x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1 -> Payloaded (Infinite :.: ListItem x) c -> List c 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 (f :: Type -> Type) a. Representable f => a -> f a
pureRep 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) (Payloaded (Infinite :.: ListItem x) context -> List context x)
-> Payloaded (Infinite :.: ListItem x) context -> List context x
forall a b. (a -> b) -> a -> b
$ (:.:) Infinite (ListItem x) (WitnessField context)
-> Payloaded (Infinite :.: ListItem x) context
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded ((:.:) Infinite (ListItem x) (WitnessField context)
 -> Payloaded (Infinite :.: ListItem x) context)
-> (:.:) Infinite (ListItem x) (WitnessField context)
-> Payloaded (Infinite :.: ListItem x) context
forall a b. (a -> b) -> a -> b
$ (Rep (Infinite :.: ListItem x) -> WitnessField context)
-> (:.:) Infinite (ListItem x) (WitnessField context)
forall a.
(Rep (Infinite :.: ListItem x) -> a)
-> (:.:) Infinite (ListItem x) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (WitnessField context
-> (Natural,
    Either
      (WrappedRep (Layout x))
      (Either (WrappedRep (Layout x)) (WrappedRep (Payload x))))
-> WitnessField context
forall a b. a -> b -> a
const WitnessField context
forall a. AdditiveMonoid a => a
zero)

-- | A list is empty if it's size is 0, in which case the first element of @runInvert@ is @one@.
--
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)
Payloaded (Infinite :.: ListItem x) context
lHash :: forall (c :: (Type -> Type) -> Type) x. List c x -> c (Layout x)
lSize :: forall (c :: (Type -> Type) -> Type) x. List c x -> c Par1
lWitness :: forall (c :: (Type -> Type) -> Type) x.
List c x -> Payloaded (Infinite :.: ListItem x) c
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: Payloaded (Infinite :.: ListItem x) context
..} = context Par1 -> Bool context
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (context Par1 -> CircuitFun '[Par1] Par1 context -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun '[f] g context -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g 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 w (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a w m, Representable f, Traversable f) =>
f i -> m (f i, f i)
runInvert))

infixr 5 .:
(.:)
    :: forall context x
    .  SymbolicOutput x
    => Context x ~ context
    => x
    -> List context x
    -> List context x
x
x .: :: forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x -> List context x
.: List{context Par1
context (Layout x)
Payloaded (Infinite :.: ListItem x) context
lHash :: forall (c :: (Type -> Type) -> Type) x. List c x -> c (Layout x)
lSize :: forall (c :: (Type -> Type) -> Type) x. List c x -> c Par1
lWitness :: forall (c :: (Type -> Type) -> Type) x.
List c x -> Payloaded (Infinite :.: ListItem x) c
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: Payloaded (Infinite :.: ListItem x) context
..} = context (Layout x)
-> context Par1
-> Payloaded (Infinite :.: ListItem x) context
-> List context x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1 -> Payloaded (Infinite :.: ListItem x) c -> List c x
List context (Layout x)
incSum context Par1
incSize ((context (Layout x) -> Layout x (WitnessField context)
forall (f :: Type -> Type).
Functor f =>
context f -> f (WitnessField context)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
c f -> f (WitnessField c)
witnessF context (Layout x)
lHash, context (Layout x) -> Layout x (WitnessField context)
forall (f :: Type -> Type).
Functor f =>
context f -> f (WitnessField context)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
c f -> f (WitnessField c)
witnessF (x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy), x -> Support x -> Payload x (WitnessField (Context x))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy)(Layout x (WitnessField context), Layout x (WitnessField context),
 Payload x (WitnessField context))
-> Payloaded (Infinite :.: ListItem x) context
-> Payloaded (Infinite :.: ListItem x) context
forall {c :: (Type -> Type) -> Type} {c :: (Type -> Type) -> Type}
       {x}.
(WitnessField c ~ WitnessField c) =>
(Layout x (WitnessField c), Layout x (WitnessField c),
 Payload x (WitnessField c))
-> Payloaded (Infinite :.: ListItem x) c
-> Payloaded (Infinite :.: ListItem x) c
<:<Payloaded (Infinite :.: ListItem x) context
lWitness)
    where
        (Layout x (WitnessField c)
a, Layout x (WitnessField c)
b, Payload x (WitnessField c)
c) <:< :: (Layout x (WitnessField c), Layout x (WitnessField c),
 Payload x (WitnessField c))
-> Payloaded (Infinite :.: ListItem x) c
-> Payloaded (Infinite :.: ListItem x) c
<:< Payloaded (Comp1 Infinite (ListItem x (WitnessField c))
l) = (:.:) Infinite (ListItem x) (WitnessField c)
-> Payloaded (Infinite :.: ListItem x) c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded ((:.:) Infinite (ListItem x) (WitnessField c)
 -> Payloaded (Infinite :.: ListItem x) c)
-> (:.:) Infinite (ListItem x) (WitnessField c)
-> Payloaded (Infinite :.: ListItem x) c
forall a b. (a -> b) -> a -> b
$ Infinite (ListItem x (WitnessField c))
-> (:.:) Infinite (ListItem x) (WitnessField c)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (Layout x (WitnessField c)
-> Layout x (WitnessField c)
-> Payload x (WitnessField c)
-> ListItem x (WitnessField c)
forall x a. Layout x a -> Layout x a -> Payload x a -> ListItem x a
ListItem Layout x (WitnessField c)
Layout x (WitnessField c)
a Layout x (WitnessField c)
Layout x (WitnessField c)
b Payload x (WitnessField c)
Payload x (WitnessField c)
c ListItem x (WitnessField c)
-> Infinite (ListItem x (WitnessField c))
-> Infinite (ListItem x (WitnessField c))
forall a. a -> Infinite a -> Infinite a
:< Infinite (ListItem x (WitnessField c))
l)

        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)
arithmetize x
x (forall {k} (t :: k). Proxy t
forall (t :: (Type -> Type) -> Type). Proxy t
Proxy @context)

        incSize :: context Par1
        incSize :: context Par1
incSize = context Par1 -> CircuitFun '[Par1] Par1 context -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun '[f] g context -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g 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 w (m :: Type -> Type).
MonadCircuit var a w 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))

        incSum :: context (Layout x)
        incSum :: context (Layout x)
incSum = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit i (BaseField context) (WitnessField context) m) =>
    FunBody '[Layout x, Layout x, Par1] (Layout x) i m)
-> 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 -> CircuitFun '[f, g, h] k c -> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
incSize ((forall {i} {m :: Type -> Type}.
  (NFData i,
   MonadCircuit i (BaseField context) (WitnessField context) m) =>
  FunBody '[Layout x, Layout x, Par1] (Layout x) i m)
 -> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit i (BaseField context) (WitnessField context) m) =>
    FunBody '[Layout x, Layout x, Par1] (Layout x) i m)
-> 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.
(Representable f, Traversable f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
mzipWithMRep (i -> i -> i -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
i -> i -> i -> m i
hashFun i
s) Layout x i
vHash Layout x i
vRepr

hashFun :: MonadCircuit i a w m => i -> i -> i -> m i
hashFun :: forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
i -> i -> i -> m i
hashFun i
s i
h i
t = ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
h) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
t) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
s))

uncons ::
  forall c x.
  SymbolicOutput x =>
  Context x ~ c =>
  List c x -> (x, List c x)
uncons :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
List c x -> (x, List c x)
uncons List{c Par1
c (Layout x)
Payloaded (Infinite :.: ListItem x) c
lHash :: forall (c :: (Type -> Type) -> Type) x. List c x -> c (Layout x)
lSize :: forall (c :: (Type -> Type) -> Type) x. List c x -> c Par1
lWitness :: forall (c :: (Type -> Type) -> Type) x.
List c x -> Payloaded (Infinite :.: ListItem x) c
lHash :: c (Layout x)
lSize :: c Par1
lWitness :: Payloaded (Infinite :.: ListItem x) c
..} = case Payloaded (Infinite :.: ListItem x) c
lWitness of
  Payloaded (Comp1 (ListItem {Layout x (WitnessField c)
Payload x (WitnessField c)
tailHash :: forall x a. ListItem x a -> Layout x a
headLayout :: forall x a. ListItem x a -> Layout x a
headPayload :: forall x a. ListItem x a -> Payload x a
tailHash :: Layout x (WitnessField c)
headLayout :: Layout x (WitnessField c)
headPayload :: Payload x (WitnessField c)
..} :< Infinite (ListItem x (WitnessField c))
tWitness)) ->
    ( (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
restore ((Support x -> (c (Layout x), Payload x (WitnessField c))) -> x)
-> (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall a b. (a -> b) -> a -> b
$ (c (Layout x), Payload x (WitnessField c))
-> Proxy c -> (c (Layout x), Payload x (WitnessField c))
forall a b. a -> b -> a
const ((forall a. (:*:) (Layout x) (Layout x) a -> Layout x a)
-> c (Layout x :*: Layout x) -> c (Layout x)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:) (Layout x) (Layout x) a -> Layout x a
forall a. (:*:) (Layout x) (Layout x) a -> Layout x a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP c (Layout x :*: Layout x)
preimage, Payload x (WitnessField c)
headPayload)
    , c (Layout x)
-> c Par1 -> Payloaded (Infinite :.: ListItem x) c -> List c x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1 -> Payloaded (Infinite :.: ListItem x) c -> List c x
List ((forall a. (:*:) (Layout x) (Layout x) a -> Layout x a)
-> c (Layout x :*: Layout x) -> c (Layout x)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:) (Layout x) (Layout x) a -> Layout x a
forall a. (:*:) (Layout x) (Layout x) a -> Layout x a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP c (Layout x :*: Layout x)
preimage) c Par1
decSize (Payloaded (Infinite :.: ListItem x) c -> List c x)
-> Payloaded (Infinite :.: ListItem x) c -> List c x
forall a b. (a -> b) -> a -> b
$ (:.:) Infinite (ListItem x) (WitnessField c)
-> Payloaded (Infinite :.: ListItem x) c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded (Infinite (ListItem x (WitnessField c))
-> (:.:) Infinite (ListItem x) (WitnessField c)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 Infinite (ListItem x (WitnessField c))
tWitness))
    where
      decSize :: c Par1
decSize = c Par1 -> CircuitFun '[Par1] Par1 c -> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF c Par1
lSize (CircuitFun '[Par1] Par1 c -> c Par1)
-> CircuitFun '[Par1] Par1 c -> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) ->
        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 c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)

      preimage :: c (Layout x :*: Layout x)
      preimage :: c (Layout x :*: Layout x)
preimage = c Par1
-> c (Layout x)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Layout x] (Layout x :*: Layout x) i m)
-> c (Layout x :*: Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
lSize c (Layout x)
lHash ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Layout x] (Layout x :*: Layout x) i m)
 -> c (Layout x :*: Layout x))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Layout x] (Layout x :*: Layout x) i m)
-> c (Layout x :*: Layout x)
forall a b. (a -> b) -> a -> b
$ \(Par1 i
s) Layout x i
y -> do
        Layout x i
tH :*: Layout x i
hH <- (WitnessField c -> m i)
-> (:*:) (Layout x) (Layout x) (WitnessField c)
-> m ((:*:) (Layout x) (Layout x) i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> (:*:) (Layout x) (Layout x) a
-> f ((:*:) (Layout x) (Layout x) b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained (Layout x (WitnessField c)
tailHash Layout x (WitnessField c)
-> Layout x (WitnessField c)
-> (:*:) (Layout x) (Layout x) (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Layout x (WitnessField c)
headLayout)
        Layout x i
hash <- (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Representable f, Traversable f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
mzipWithMRep (i -> i -> i -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
i -> i -> i -> m i
hashFun i
s) Layout x i
hH Layout x i
tH
        Layout x ()
_ <- (i -> i -> m ()) -> Layout x i -> Layout x i -> m (Layout x ())
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Representable f, Traversable f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
mzipWithMRep (\i
i i
j -> ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
j))) Layout x i
hash Layout x i
y
        (:*:) (Layout x) (Layout x) i -> m ((:*:) (Layout x) (Layout x) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Layout x i
hH Layout x i -> Layout x i -> (:*:) (Layout x) (Layout x) i
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Layout x i
tH)

-- | TODO: Is there really a nicer way to handle empty lists?
--
head ::
  SymbolicOutput x =>
  Context x ~ c =>
  List c x -> x
head :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c) =>
List c x -> x
head = (x, List c x) -> x
forall a b. (a, b) -> a
fst ((x, List c x) -> x)
-> (List c x -> (x, List c x)) -> List c x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List c x -> (x, List c x)
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
List c x -> (x, List c x)
uncons

tail ::
  SymbolicOutput x =>
  Context x ~ c =>
  List c x -> List c x
tail :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c) =>
List c x -> List c x
tail = (x, List c x) -> List c x
forall a b. (a, b) -> b
snd ((x, List c x) -> List c x)
-> (List c x -> (x, List c x)) -> List c x -> List c x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List c x -> (x, List c x)
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
List c x -> (x, List c x)
uncons

{-- TODO: Foldable relies on Haskell types such as Bool (i.e. null = foldr (\_ _ -> False) True)
   I am not sure this is suitable for Symbolic interface

reverse :: forall context x . Foldable (List context) => List context x -> List context x
reverse = foldl (flip (.:)) emptyList

init :: forall context x . Foldable (List context) => List context x -> List context x
init = reverse . tail . reverse

last :: forall context x . Foldable (List context) => List context x -> x
last = head . reverse
--}
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

singleton
    :: forall context x
    .  SymbolicOutput x
    => Context x ~ context
    => x
    -> List context x
singleton :: forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x
singleton x
x = x
x x -> List context x -> List context x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x -> List context x
.: List context x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList

(!!) :: List context x -> UInt n Auto context -> x
!! :: forall (context :: (Type -> Type) -> Type) x (n :: Natural).
List context x -> UInt n 'Auto context -> x
(!!) = List context x -> UInt n 'Auto context -> x
forall a. HasCallStack => a
undefined

concat :: List context (List context x) -> List context x
concat :: forall (context :: (Type -> Type) -> Type) x.
List context (List context x) -> List context x
concat = List context (List context x) -> List context x
forall a. HasCallStack => a
undefined