Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Data.List

Synopsis

data List (context :: (Type -> Type) -> Type) x = List {
- lHash :: context (Layout x)
- lSize :: context Par1
- lWitness :: [x]
}
emptyList :: forall context x. Symbolic context => Applicative (Layout x) => List context x
null :: forall context x. Symbolic context => List context x -> Bool context
(.:) :: 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
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)
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
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
last :: List context x -> x
(++) :: List context x -> List context x -> List context x
filter :: (x -> Bool context) -> List context x -> List context x
delete :: x -> List context x -> List context x
(\\) :: List context x -> List context x -> List context x

Documentation

data List (context :: (Type -> Type) -> Type) x Source #

Constructors

List
Fields lHash :: context (Layout x) lSize :: context Par1 lWitness :: [x] TODO: As the name suggests, this is only needed in witness cinstruction in uncons. This list is never used in circuit itlest. Think of a better solution for carrying witnesses. Besides, List is not an instance of SymbolicData while this list is present

emptyList :: forall context x. Symbolic context => Applicative (Layout x) => List context x Source #

TODO: A proof-of-concept where hash == id. Replace id with a proper hash if we need lists to be cryptographically secure.

null :: forall context x. Symbolic context => List context x -> Bool context Source #

A list is empty if it's size is 0, in which case the first element of runInvert is one.

(.:) :: 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 infixr 5 Source #

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

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 Source #

TODO: Is there really a nicer way to handle empty lists?

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 Source #

last :: List context x -> x Source #

(++) :: List context x -> List context x -> List context x Source #

filter :: (x -> Bool context) -> List context x -> List context x Source #

delete :: x -> List context x -> List context x Source #

(\\) :: List context x -> List context x -> List context x Source #