{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE TypeOperators  #-}

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 (..), pureRep, tabulate)
import           Data.List.Infinite                (Infinite (..))
import           Data.Proxy                        (Proxy (..))
import           Data.Traversable                  (traverse)
import           Data.Tuple                        (fst, snd)
import           Data.Type.Equality                (type (~))
import           GHC.Generics                      (Generic, Generic1, Par1 (..), (:*:) (..), (:.:) (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number  (KnownNat)
import           ZkFold.Base.Data.HFunctor         (hmap)
import           ZkFold.Base.Data.List.Infinite    ()
import           ZkFold.Base.Data.Orphans          ()
import           ZkFold.Base.Data.Product          (fstP, sndP)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool         (Bool (..), BoolType (..))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Conditional  (Conditional, ifThenElse)
import           ZkFold.Symbolic.Data.Eq           (Eq (..))
import           ZkFold.Symbolic.Data.FieldElement (FieldElement (..))
import           ZkFold.Symbolic.Data.Input        (SymbolicInput (..))
import           ZkFold.Symbolic.Data.Morph        (MorphFrom, MorphTo (..), (@))
import           ZkFold.Symbolic.Data.Payloaded    (Payloaded (Payloaded, runPayloaded))
import           ZkFold.Symbolic.Data.Switch       (Switch (..))
import           ZkFold.Symbolic.Data.UInt         (UInt)
import           ZkFold.Symbolic.Fold
import           ZkFold.Symbolic.MonadCircuit

data ListItem l p a = ListItem
  { forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
tailHash    :: l a
  , forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headLayout  :: l a
  , forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> p a
headPayload :: p a
  }
  deriving ((forall a b. (a -> b) -> ListItem l p a -> ListItem l p b)
-> (forall a b. a -> ListItem l p b -> ListItem l p a)
-> Functor (ListItem l p)
forall a b. a -> ListItem l p b -> ListItem l p a
forall a b. (a -> b) -> ListItem l p a -> ListItem l p b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (l :: Type -> Type) (p :: Type -> Type) a b.
(Functor l, Functor p) =>
a -> ListItem l p b -> ListItem l p a
forall (l :: Type -> Type) (p :: Type -> Type) a b.
(Functor l, Functor p) =>
(a -> b) -> ListItem l p a -> ListItem l p b
$cfmap :: forall (l :: Type -> Type) (p :: Type -> Type) a b.
(Functor l, Functor p) =>
(a -> b) -> ListItem l p a -> ListItem l p b
fmap :: forall a b. (a -> b) -> ListItem l p a -> ListItem l p b
$c<$ :: forall (l :: Type -> Type) (p :: Type -> Type) a b.
(Functor l, Functor p) =>
a -> ListItem l p b -> ListItem l p a
<$ :: forall a b. a -> ListItem l p b -> ListItem l p a
Functor, (forall (a :: k). ListItem l p a -> Rep1 (ListItem l p) a)
-> (forall (a :: k). Rep1 (ListItem l p) a -> ListItem l p a)
-> Generic1 (ListItem l p)
forall (a :: k). Rep1 (ListItem l p) a -> ListItem l p a
forall (a :: k). ListItem l p a -> Rep1 (ListItem l p) a
forall k (f :: k -> Type).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall k (l :: k -> Type) (p :: k -> Type) (a :: k).
Rep1 (ListItem l p) a -> ListItem l p a
forall k (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> Rep1 (ListItem l p) a
$cfrom1 :: forall k (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> Rep1 (ListItem l p) a
from1 :: forall (a :: k). ListItem l p a -> Rep1 (ListItem l p) a
$cto1 :: forall k (l :: k -> Type) (p :: k -> Type) (a :: k).
Rep1 (ListItem l p) a -> ListItem l p a
to1 :: forall (a :: k). Rep1 (ListItem l p) a -> ListItem l p a
Generic1, Distributive (ListItem l p)
Distributive (ListItem l p) =>
(forall a. (Rep (ListItem l p) -> a) -> ListItem l p a)
-> (forall a. ListItem l p a -> Rep (ListItem l p) -> a)
-> Representable (ListItem l p)
forall a. ListItem l p a -> Rep (ListItem l p) -> a
forall a. (Rep (ListItem l p) -> a) -> ListItem l p a
forall (f :: Type -> Type).
Distributive f =>
(forall a. (Rep f -> a) -> f a)
-> (forall a. f a -> Rep f -> a) -> Representable f
forall (l :: Type -> Type) (p :: Type -> Type).
(Representable l, Representable p) =>
Distributive (ListItem l p)
forall (l :: Type -> Type) (p :: Type -> Type) a.
(Representable l, Representable p) =>
ListItem l p a -> Rep (ListItem l p) -> a
forall (l :: Type -> Type) (p :: Type -> Type) a.
(Representable l, Representable p) =>
(Rep (ListItem l p) -> a) -> ListItem l p a
$ctabulate :: forall (l :: Type -> Type) (p :: Type -> Type) a.
(Representable l, Representable p) =>
(Rep (ListItem l p) -> a) -> ListItem l p a
tabulate :: forall a. (Rep (ListItem l p) -> a) -> ListItem l p a
$cindex :: forall (l :: Type -> Type) (p :: Type -> Type) a.
(Representable l, Representable p) =>
ListItem l p a -> Rep (ListItem l p) -> a
index :: forall a. ListItem l p a -> Rep (ListItem l p) -> a
Representable)

instance (Distributive l, Distributive p) => Distributive (ListItem l p) where
  distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (ListItem l p a) -> ListItem l p (f a)
distribute f (ListItem l p a)
f = ListItem
    { tailHash :: l (f a)
tailHash = f (l a) -> l (f a)
forall (g :: Type -> Type) (f :: Type -> Type) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: Type -> Type) a. Functor f => f (l a) -> l (f a)
distribute (ListItem l p a -> l a
forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
tailHash (ListItem l p a -> l a) -> f (ListItem l p a) -> f (l a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (ListItem l p a)
f)
    , headLayout :: l (f a)
headLayout = f (l a) -> l (f a)
forall (g :: Type -> Type) (f :: Type -> Type) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: Type -> Type) a. Functor f => f (l a) -> l (f a)
distribute (ListItem l p a -> l a
forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headLayout (ListItem l p a -> l a) -> f (ListItem l p a) -> f (l a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (ListItem l p a)
f)
    , headPayload :: p (f a)
headPayload = f (p a) -> p (f a)
forall (g :: Type -> Type) (f :: Type -> Type) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: Type -> Type) a. Functor f => f (p a) -> p (f a)
distribute (ListItem l p a -> p a
forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> p a
headPayload (ListItem l p a -> p a) -> f (ListItem l p a) -> f (p a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (ListItem l p a)
f)
    }

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 (Layout x) (Payload x)) c
lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload 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)

instance (SymbolicData x, Symbolic c) => Conditional (Bool c) (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 (Layout x) (Payload x)) context
-> List context x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload 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) (FieldElement context -> context Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement FieldElement context
forall a. AdditiveMonoid a => a
zero) (Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
 -> List context x)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
-> List context x
forall a b. (a -> b) -> a -> b
$
    (:.:)
  Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded ((:.:)
   Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
 -> Payloaded
      (Infinite :.: ListItem (Layout x) (Payload x)) context)
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
forall a b. (a -> b) -> a -> b
$ (Rep (Infinite :.: ListItem (Layout x) (Payload x))
 -> WitnessField context)
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
forall a.
(Rep (Infinite :.: ListItem (Layout x) (Payload x)) -> a)
-> (:.:) Infinite (ListItem (Layout x) (Payload 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)

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 (Layout x) (Payload 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 (Layout x) (Payload x)) c
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
..} = context Par1 -> FieldElement context
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement context Par1
lSize FieldElement context -> FieldElement context -> Bool context
forall b a. Eq b a => a -> a -> b
== FieldElement context
forall a. AdditiveMonoid a => a
zero

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 (Layout x) (Payload 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 (Layout x) (Payload x)) c
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
..} = context (Layout x)
-> context Par1
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
-> List context x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
-> List c x
List context (Layout x)
incHash context Par1
incSize Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
incWitness
  where
    headL :: Context x (Layout x)
headL = 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
    headP :: Payload x (WitnessField (Context x))
headP = 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
    incHash :: context (Layout x)
incHash = context (Layout x)
-> context (Layout x)
-> context Par1
-> CircuitFun '[Layout x, Layout x, Par1] (Layout x) context
-> 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)
Context x (Layout x)
headL context Par1
incSize \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
    incSize :: context Par1
incSize = FieldElement context -> context Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement (context Par1 -> FieldElement context
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement context Par1
lSize FieldElement context
-> FieldElement context -> FieldElement context
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement context
forall a. MultiplicativeMonoid a => a
one)
    incItem :: ListItem (Layout x) (Payload x) (WitnessField context)
incItem = Layout x (WitnessField context)
-> Layout x (WitnessField context)
-> Payload x (WitnessField context)
-> ListItem (Layout x) (Payload x) (WitnessField context)
forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
l a -> l a -> p a -> ListItem l p a
ListItem (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 context (Layout x)
Context x (Layout x)
headL) Payload x (WitnessField context)
Payload x (WitnessField (Context x))
headP
    Payloaded (Comp1 Infinite (ListItem (Layout x) (Payload x) (WitnessField context))
srcWitness) = Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
lWitness
    incWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
incWitness = (:.:)
  Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded ((:.:)
   Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
 -> Payloaded
      (Infinite :.: ListItem (Layout x) (Payload x)) context)
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) context
forall a b. (a -> b) -> a -> b
$ Infinite (ListItem (Layout x) (Payload x) (WitnessField context))
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField context)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (ListItem (Layout x) (Payload x) (WitnessField context)
incItem ListItem (Layout x) (Payload x) (WitnessField context)
-> Infinite
     (ListItem (Layout x) (Payload x) (WitnessField context))
-> Infinite
     (ListItem (Layout x) (Payload x) (WitnessField context))
forall a. a -> Infinite a -> Infinite a
:< Infinite (ListItem (Layout x) (Payload x) (WitnessField context))
srcWitness)

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))

-- | TODO: Is there really a nicer way to handle empty lists?
--
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 (Layout x) (Payload 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 (Layout x) (Payload x)) c
lHash :: c (Layout x)
lSize :: c Par1
lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
..} = case Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
lWitness of
  Payloaded (Comp1 (ListItem {Layout x (WitnessField c)
Payload x (WitnessField c)
tailHash :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headLayout :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headPayload :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> p a
tailHash :: Layout x (WitnessField c)
headLayout :: Layout x (WitnessField c)
headPayload :: Payload x (WitnessField c)
..} :< Infinite (ListItem (Layout x) (Payload 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 (Layout x) (Payload x)) c
-> List c x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x)
-> c Par1
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload 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 (Layout x) (Payload x)) c
 -> List c x)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
-> List c x
forall a b. (a -> b) -> a -> b
$ (:.:) Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
-> Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded (Infinite (ListItem (Layout x) (Payload x) (WitnessField c))
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 Infinite (ListItem (Layout x) (Payload x) (WitnessField c))
tWitness))
    where
      decSize :: c Par1
decSize = FieldElement c -> c Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement (c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement c Par1
lSize FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveGroup a => a -> a -> a
- FieldElement c
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
decSize 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)

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

foldl ::
  forall x y c.
  ( SymbolicOutput x, Context x ~ c
  , SymbolicOutput y, Context y ~ c
  , SymbolicFold c
  ) =>
  MorphFrom c (y, x) y -> y -> List c x -> y
foldl :: forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl MorphFrom c (y, x) y
f y
y List {c Par1
c (Layout x)
Payloaded (Infinite :.: ListItem (Layout x) (Payload 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 (Layout x) (Payload x)) c
lHash :: c (Layout x)
lSize :: c Par1
lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
..} = (Support y -> (c (Layout y), Payload y (WitnessField c))) -> y
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 y ~ c) =>
(Support y -> (c (Layout y), Payload y (WitnessField c))) -> y
restore \Support y
s ->
  (forall (s :: (Type -> Type) -> Type).
 (SymbolicFold s, BaseField s ~ BaseField c) =>
 s (Layout y)
 -> Payload y (WitnessField s)
 -> s (Layout x :*: Payload x)
 -> (s (Layout y), Payload y (WitnessField s)))
-> c (Layout y)
-> Payload y (WitnessField c)
-> c (Layout x)
-> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c))
-> c Par1
-> (c (Layout y), Payload y (WitnessField c))
forall (f :: Type -> Type) (p :: Type -> Type) (g :: Type -> Type)
       (h :: Type -> Type) wc.
(Binary (Rep f), NFData (Rep f), Ord (Rep f),
 forall a. Binary a => Binary (f a), Representable f, NFData1 f,
 Traversable f, Binary (Rep p), Representable p, Binary (Rep g),
 NFData (Rep g), Ord (Rep g), Representable g,
 forall a. Binary a => Binary (h a), WitnessField c ~ wc) =>
(forall (s :: (Type -> Type) -> Type).
 (SymbolicFold s, BaseField s ~ BaseField c) =>
 s f -> p (WitnessField s) -> s g -> (s f, p (WitnessField s)))
-> c f -> p wc -> c h -> Infinite (g wc) -> c Par1 -> (c f, p wc)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (p :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type) wc.
(SymbolicFold c, Binary (Rep f), NFData (Rep f), Ord (Rep f),
 forall a. Binary a => Binary (f a), Representable f, NFData1 f,
 Traversable f, Binary (Rep p), Representable p, Binary (Rep g),
 NFData (Rep g), Ord (Rep g), Representable g,
 forall a. Binary a => Binary (h a), WitnessField c ~ wc) =>
(forall (s :: (Type -> Type) -> Type).
 (SymbolicFold s, BaseField s ~ BaseField c) =>
 s f -> p (WitnessField s) -> s g -> (s f, p (WitnessField s)))
-> c f -> p wc -> c h -> Infinite (g wc) -> c Par1 -> (c f, p wc)
sfoldl s (Layout y)
-> Payload y (WitnessField s)
-> s (Layout x :*: Payload x)
-> (s (Layout y), Payload y (WitnessField s))
forall (s :: (Type -> Type) -> Type).
(SymbolicFold s, BaseField s ~ BaseField c) =>
s (Layout y)
-> Payload y (WitnessField s)
-> s (Layout x :*: Payload x)
-> (s (Layout y), Payload y (WitnessField s))
foldOp (y -> Support y -> Context y (Layout y)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize y
y Support y
s) (y -> Support y -> Payload y (WitnessField (Context y))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload y
y Support y
s) c (Layout x)
lHash
    ((ListItem (Layout x) (Payload x) (WitnessField c)
 -> (:*:) (Layout x) (Payload x) (WitnessField c))
-> Infinite (ListItem (Layout x) (Payload x) (WitnessField c))
-> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c))
forall a b. (a -> b) -> Infinite a -> Infinite b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ListItem {Layout x (WitnessField c)
Payload x (WitnessField c)
tailHash :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headLayout :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> l a
headPayload :: forall {k} (l :: k -> Type) (p :: k -> Type) (a :: k).
ListItem l p a -> p a
tailHash :: Layout x (WitnessField c)
headLayout :: Layout x (WitnessField c)
headPayload :: Payload x (WitnessField c)
..} -> Layout x (WitnessField c)
headLayout Layout x (WitnessField c)
-> Payload x (WitnessField c)
-> (:*:) (Layout x) (Payload x) (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Payload x (WitnessField c)
headPayload)
      (Infinite (ListItem (Layout x) (Payload x) (WitnessField c))
 -> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c)))
-> ((:.:)
      Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
    -> Infinite (ListItem (Layout x) (Payload x) (WitnessField c)))
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
-> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
-> Infinite (ListItem (Layout x) (Payload x) (WitnessField c))
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1 ((:.:) Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
 -> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c)))
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
-> Infinite ((:*:) (Layout x) (Payload x) (WitnessField c))
forall a b. (a -> b) -> a -> b
$ Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
-> (:.:)
     Infinite (ListItem (Layout x) (Payload x)) (WitnessField c)
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
Payloaded f c -> f (WitnessField c)
runPayloaded Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c
lWitness
    ) c Par1
lSize
  where
    foldOp ::
      forall s.
      (SymbolicFold s, BaseField s ~ BaseField c) =>
      s (Layout y) -> Payload y (WitnessField s) ->
      s (Layout x :*: Payload x) ->
      (s (Layout y), Payload y (WitnessField s))
    foldOp :: forall (s :: (Type -> Type) -> Type).
(SymbolicFold s, BaseField s ~ BaseField c) =>
s (Layout y)
-> Payload y (WitnessField s)
-> s (Layout x :*: Payload x)
-> (s (Layout y), Payload y (WitnessField s))
foldOp s (Layout y)
yl Payload y (WitnessField s)
yp s (Layout x :*: Payload x)
il =
      let Switch {s (Layout y)
Payload y (WitnessField s)
sLayout :: s (Layout y)
sPayload :: Payload y (WitnessField s)
sLayout :: forall (c :: (Type -> Type) -> Type) x. Switch c x -> c (Layout x)
sPayload :: forall (c :: (Type -> Type) -> Type) x.
Switch c x -> Payload x (WitnessField c)
..} :: Switch s y = MorphTo s (y, x) y
MorphFrom c (y, x) y
f MorphTo s (y, x) y -> (Switch s y, Switch s x) -> Switch s y
forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@
                  ( s (Layout y) -> Payload y (WitnessField s) -> Switch s y
forall (c :: (Type -> Type) -> Type) x.
c (Layout x) -> Payload x (WitnessField c) -> Switch c x
Switch s (Layout y)
yl Payload y (WitnessField s)
yp :: Switch s y
                  , s (Layout x) -> Payload x (WitnessField s) -> Switch s x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x) -> Payload x (WitnessField c) -> Switch c x
Switch ((forall a. (:*:) (Layout x) (Payload x) a -> Layout x a)
-> s (Layout x :*: Payload x) -> s (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) -> s f -> s g
hmap (:*:) (Layout x) (Payload x) a -> Layout x a
forall a. (:*:) (Layout x) (Payload x) a -> Layout x a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP s (Layout x :*: Payload x)
il) (s (Payload x) -> Payload x (WitnessField s)
forall (f :: Type -> Type). Functor f => s f -> f (WitnessField s)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
c f -> f (WitnessField c)
witnessF ((forall a. (:*:) (Layout x) (Payload x) a -> Payload x a)
-> s (Layout x :*: Payload x) -> s (Payload 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) -> s f -> s g
hmap (:*:) (Layout x) (Payload x) a -> Payload x a
forall a. (:*:) (Layout x) (Payload x) a -> Payload x a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP s (Layout x :*: Payload x)
il))
                      :: Switch s x)
       in (s (Layout y)
sLayout, Payload y (WitnessField s)
sPayload)

revapp ::
  forall c x.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  List c x -> List c x -> List c x
-- | revapp xs ys = reverse xs ++ ys
revapp :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x -> List c x
revapp List c x
xs List c x
ys = MorphFrom c (List c x, x) (List c x)
-> List c x -> List c x -> List c x
forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl (((List c (Switch c x), Switch c x) -> List c (Switch c x))
-> MorphTo c (List c x, x) (List c x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(List c (Switch c x)
zs, Switch c x
x :: Switch s x) -> Switch c x
x Switch c x -> List c (Switch c x) -> List c (Switch c x)
forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x -> List context x
.: List c (Switch c x)
zs) List c x
ys List c x
xs

reverse ::
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) => List c x -> List c x
reverse :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse List c x
xs = List c x -> List c x -> List c x
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x -> List c x
revapp List c x
xs List c x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList

last :: (SymbolicOutput x, Context x ~ c, SymbolicFold c) => List c x -> x
last :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> x
last = List c x -> x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c) =>
List c x -> x
head (List c x -> x) -> (List c x -> List c x) -> List c x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse

init ::
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) => List c x -> List c x
init :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
init = List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse (List c x -> List c x)
-> (List c x -> List c x) -> List c x -> List c x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c) =>
List c x -> List c x
tail (List c x -> List c x)
-> (List c x -> List c x) -> List c x -> List c x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse

(++) ::
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  List c x -> List c x -> List c x
List c x
xs ++ :: forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x -> List c x
++ List c x
ys = List c x -> List c x -> List c x
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x -> List c x
revapp (List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse List c x
xs) List c x
ys

foldr ::
  forall c x y.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  (SymbolicOutput y, Context y ~ c) =>
  MorphFrom c (x, y) y -> y -> List c x -> y
foldr :: forall (c :: (Type -> Type) -> Type) x y.
(SymbolicOutput x, Context x ~ c, SymbolicFold c, SymbolicOutput y,
 Context y ~ c) =>
MorphFrom c (x, y) y -> y -> List c x -> y
foldr MorphFrom c (x, y) y
f y
s List c x
xs =
  MorphFrom c (y, x) y -> y -> List c x -> y
forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl (((Switch c y, Switch c x) -> Switch c y) -> MorphTo c (y, x) y
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(Switch c y
y :: Switch s y, Switch c x
x :: Switch s x) ->
                    MorphTo c (x, y) y
MorphFrom c (x, y) y
f MorphTo c (x, y) y -> (Switch c x, Switch c y) -> Switch c y
forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@ (Switch c x
x, Switch c y
y) :: Switch s y) y
s (List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse List c x
xs)

filter ::
  forall c x.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  MorphFrom c x (Bool c) -> List c x -> List c x
filter :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
MorphFrom c x (Bool c) -> List c x -> List c x
filter MorphFrom c x (Bool c)
pred = MorphFrom c (x, List c x) (List c x)
-> List c x -> List c x -> List c x
forall (c :: (Type -> Type) -> Type) x y.
(SymbolicOutput x, Context x ~ c, SymbolicFold c, SymbolicOutput y,
 Context y ~ c) =>
MorphFrom c (x, y) y -> y -> List c x -> y
foldr (((Switch c x, List c (Switch c x)) -> List c (Switch c x))
-> MorphTo c (x, List c x) (List c x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(Switch c x
x :: Switch s x, List c (Switch c x)
ys) ->
  Bool c
-> List c (Switch c x)
-> List c (Switch c x)
-> List c (Switch c x)
forall b a. Conditional b a => b -> a -> a -> a
ifThenElse (MorphTo c x (Bool c)
MorphFrom c x (Bool c)
pred MorphTo c x (Bool c) -> Switch c x -> Bool c
forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@ Switch c x
x :: Bool s) (Switch c x
x Switch c x -> List c (Switch c x) -> List c (Switch c x)
forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x -> List context x
.: List c (Switch c x)
ys) List c (Switch c x)
ys) List c x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList

delete ::
  forall c x.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  MorphFrom c (x, x) (Bool c) -> x -> List c x -> List c x
delete :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
MorphFrom c (x, x) (Bool c) -> x -> List c x -> List c x
delete MorphFrom c (x, x) (Bool c)
eq x
x List c x
xs =
  let (Bool c
_, x
_, List c x
result) =
        MorphFrom c (x, (Bool c, x, List c x)) (Bool c, x, List c x)
-> (Bool c, x, List c x) -> List c x -> (Bool c, x, List c x)
forall (c :: (Type -> Type) -> Type) x y.
(SymbolicOutput x, Context x ~ c, SymbolicFold c, SymbolicOutput y,
 Context y ~ c) =>
MorphFrom c (x, y) y -> y -> List c x -> y
foldr (((Switch c x, (Bool c, Switch c x, List c (Switch c x)))
 -> (Bool c, Switch c x, List c (Switch c x)))
-> MorphTo c (x, (Bool c, x, List c x)) (Bool c, x, List c x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(Switch c x
y :: Switch s x, (Bool c
ok :: Bool s, Switch c x
y0 :: Switch s x, List c (Switch c x)
ys)) ->
          let test :: Bool c
test = MorphTo c (x, x) (Bool c)
MorphFrom c (x, x) (Bool c)
eq MorphTo c (x, x) (Bool c) -> (Switch c x, Switch c x) -> Bool c
forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@ (Switch c x
y, Switch c x
y0)
           in (Bool c
ok Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
|| Bool c
test, Switch c x
y0, Bool c
-> List c (Switch c x)
-> List c (Switch c x)
-> List c (Switch c x)
forall b a. Conditional b a => b -> a -> a -> a
ifThenElse (Bool c
ok Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
|| Bool c -> Bool c
forall b. BoolType b => b -> b
not Bool c
test) (Switch c x
y Switch c x -> List c (Switch c x) -> List c (Switch c x)
forall (context :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ context) =>
x -> List context x -> List context x
.: List c (Switch c x)
ys) List c (Switch c x)
ys))
           (Bool c
forall b. BoolType b => b
false :: Bool c, x
x, List c x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList) List c x
xs
   in List c x
result

setminus ::
  forall c x.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  MorphFrom c (x, x) (Bool c) -> List c x -> List c x -> List c x
setminus :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
MorphFrom c (x, x) (Bool c) -> List c x -> List c x -> List c x
setminus MorphFrom c (x, x) (Bool c)
eq = MorphFrom c (List c x, x) (List c x)
-> List c x -> List c x -> List c x
forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl (MorphFrom c (List c x, x) (List c x)
 -> List c x -> List c x -> List c x)
-> MorphFrom c (List c x, x) (List c x)
-> List c x
-> List c x
-> List c x
forall a b. (a -> b) -> a -> b
$ ((List c (Switch c x), Switch c x) -> List c (Switch c x))
-> MorphTo c (List c x, x) (List c x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(List c (Switch c x)
xs, Switch c x
x :: Switch s x) ->
  MorphFrom c (Switch c x, Switch c x) (Bool c)
-> Switch c x -> List c (Switch c x) -> List c (Switch c x)
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
MorphFrom c (x, x) (Bool c) -> x -> List c x -> List c x
delete (((Switch c x, Switch c x) -> Bool c)
-> MorphTo c (Switch c x, Switch c x) (Bool c)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(Switch c x
y :: Switch s' x, Switch c x
z :: Switch s' x) ->
    MorphTo c (x, x) (Bool c)
MorphFrom c (x, x) (Bool c)
eq MorphTo c (x, x) (Bool c) -> (Switch c x, Switch c x) -> Bool c
forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@ (Switch c x
y, Switch c x
z) :: Bool s') Switch c x
x List c (Switch c x)
xs

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

(!!) ::
  forall x c n.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  (KnownNat n, KnownRegisters c n Auto) =>
  List c x -> UInt n Auto c -> x
List c x
xs !! :: forall x (c :: (Type -> Type) -> Type) (n :: Natural).
(SymbolicOutput x, Context x ~ c, SymbolicFold c, KnownNat n,
 KnownRegisters c n 'Auto) =>
List c x -> UInt n 'Auto c -> x
!! UInt n 'Auto c
n = (UInt n 'Auto c, x) -> x
forall a b. (a, b) -> b
snd ((UInt n 'Auto c, x) -> x) -> (UInt n 'Auto c, x) -> x
forall a b. (a -> b) -> a -> b
$ MorphFrom c ((UInt n 'Auto c, x), x) (UInt n 'Auto c, x)
-> (UInt n 'Auto c, x) -> List c x -> (UInt n 'Auto c, x)
forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl ((((UInt n 'Auto c, Switch c x), Switch c x)
 -> (UInt n 'Auto c, Switch c x))
-> MorphTo c ((UInt n 'Auto c, x), x) (UInt n 'Auto c, x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \((UInt n 'Auto c
m :: UInt n Auto s, Switch c x
y :: Switch s x), Switch c x
x) ->
  (UInt n 'Auto c
m UInt n 'Auto c -> UInt n 'Auto c -> UInt n 'Auto c
forall a. AdditiveGroup a => a -> a -> a
- UInt n 'Auto c
forall a. MultiplicativeMonoid a => a
one, Bool c -> Switch c x -> Switch c x -> Switch c x
forall b a. Conditional b a => b -> a -> a -> a
ifThenElse (UInt n 'Auto c
m UInt n 'Auto c -> UInt n 'Auto c -> Bool c
forall b a. Eq b a => a -> a -> b
== UInt n 'Auto c
forall a. AdditiveMonoid a => a
zero :: Bool s) Switch c x
x Switch c x
y))
  (UInt n 'Auto c
n, (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 (Layout x (BaseField c) -> c (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField c) -> c (Layout x))
-> Layout x (BaseField c) -> c (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField c -> Layout x (BaseField c)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep BaseField c
forall a. AdditiveMonoid a => a
zero, WitnessField c -> Payload x (WitnessField c)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep WitnessField c
forall a. AdditiveMonoid a => a
zero)) List c x
xs

concat ::
  forall c x.
  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
  List c (List c x) -> List c x
concat :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c (List c x) -> List c x
concat List c (List c x)
xs = List c x -> List c x
forall x (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x
reverse (List c x -> List c x) -> List c x -> List c x
forall a b. (a -> b) -> a -> b
$
  MorphFrom c (List c x, List c x) (List c x)
-> List c x -> List c (List c x) -> List c x
forall x y (c :: (Type -> Type) -> Type).
(SymbolicOutput x, Context x ~ c, SymbolicOutput y, Context y ~ c,
 SymbolicFold c) =>
MorphFrom c (y, x) y -> y -> List c x -> y
foldl (((List c (Switch c x), List c (Switch c x)) -> List c (Switch c x))
-> MorphTo c (List c x, List c x) (List c x)
forall (c :: (Type -> Type) -> Type) input output i o.
(Replica c input i, Replica c output o) =>
(i -> o) -> MorphTo c input output
Morph \(List c (Switch c x)
ys, List c (Switch c x)
x :: List s (Switch s x)) -> List c (Switch c x) -> List c (Switch c x) -> List c (Switch c x)
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
List c x -> List c x -> List c x
revapp List c (Switch c x)
x List c (Switch c x)
ys) List c x
forall (context :: (Type -> Type) -> Type) x.
(SymbolicData x, Context x ~ context) =>
List context x
emptyList List c (List c x)
xs