Safe Haskell	None
Language	GHC2021

Protocols.Vec

Description

Utility functions for working with Vecs of Circuits.

Synopsis

vecCircuits :: forall (n :: Nat) a b. KnownNat n => Vec n (Circuit a b) -> Circuit (Vec n a) (Vec n b)
append :: forall (n0 :: Nat) circuit (n1 :: Nat). KnownNat n0 => Circuit (Vec n0 circuit, Vec n1 circuit) (Vec (n0 + n1) circuit)
append3 :: forall (n0 :: Nat) (n1 :: Nat) (n2 :: Nat) circuit. (KnownNat n0, KnownNat n1, KnownNat n2) => Circuit (Vec n0 circuit, Vec n1 circuit, Vec n2 circuit) (Vec ((n0 + n1) + n2) circuit)
split :: forall (n0 :: Nat) (n1 :: Natural) circuit. KnownNat n0 => Circuit (Vec (n0 + n1) circuit) (Vec n0 circuit, Vec n1 circuit)
split3 :: forall (n0 :: Nat) (n1 :: Nat) (n2 :: Nat) circuit. (KnownNat n0, KnownNat n1, KnownNat n2) => Circuit (Vec ((n0 + n1) + n2) circuit) (Vec n0 circuit, Vec n1 circuit, Vec n2 circuit)
zip :: forall (n :: Nat) a b. KnownNat n => Circuit (Vec n a, Vec n b) (Vec n (a, b))
zip3 :: forall (n :: Nat) a b c. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c) (Vec n (a, b, c))
zip4 :: forall (n :: Nat) a b c d. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c, Vec n d) (Vec n (a, b, c, d))
zip5 :: forall (n :: Nat) a b c d e. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e) (Vec n (a, b, c, d, e))
unzip :: forall (n :: Nat) a b. KnownNat n => Circuit (Vec n (a, b)) (Vec n a, Vec n b)
unzip3 :: forall (n :: Nat) a b c. KnownNat n => Circuit (Vec n (a, b, c)) (Vec n a, Vec n b, Vec n c)
unzip4 :: forall (n :: Nat) a b c d. KnownNat n => Circuit (Vec n (a, b, c, d)) (Vec n a, Vec n b, Vec n c, Vec n d)
unzip5 :: forall (n :: Nat) a b c d e. KnownNat n => Circuit (Vec n (a, b, c, d, e)) (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
concat :: forall (n0 :: Nat) (n1 :: Nat) circuit. (KnownNat n0, KnownNat n1) => Circuit (Vec n0 (Vec n1 circuit)) (Vec (n0 * n1) circuit)
unconcat :: forall (n :: Nat) (m :: Nat) circuit. (KnownNat n, KnownNat m) => SNat m -> Circuit (Vec (n * m) circuit) (Vec n (Vec m circuit))

Documentation

vecCircuits :: forall (n :: Nat) a b. KnownNat n => Vec n (Circuit a b) -> Circuit (Vec n a) (Vec n b) Source #

Bundle together a Vec of Circuits into a Circuit with Vec input and output. The Circuits all run in parallel.

A general inverse of vecCircuits cannot exist, because we cannot guarantee that the nth output circuit depends only on the nth input circuit.

append :: forall (n0 :: Nat) circuit (n1 :: Nat). KnownNat n0 => Circuit (Vec n0 circuit, Vec n1 circuit) (Vec (n0 + n1) circuit) Source #

Append two separate vectors of the same circuits into one vector of circuits

append3 :: forall (n0 :: Nat) (n1 :: Nat) (n2 :: Nat) circuit. (KnownNat n0, KnownNat n1, KnownNat n2) => Circuit (Vec n0 circuit, Vec n1 circuit, Vec n2 circuit) (Vec ((n0 + n1) + n2) circuit) Source #

Append three separate vectors of the same circuits into one vector of circuits

split :: forall (n0 :: Nat) (n1 :: Natural) circuit. KnownNat n0 => Circuit (Vec (n0 + n1) circuit) (Vec n0 circuit, Vec n1 circuit) Source #

Split a vector of circuits into two vectors of circuits.

split3 :: forall (n0 :: Nat) (n1 :: Nat) (n2 :: Nat) circuit. (KnownNat n0, KnownNat n1, KnownNat n2) => Circuit (Vec ((n0 + n1) + n2) circuit) (Vec n0 circuit, Vec n1 circuit, Vec n2 circuit) Source #

Split a vector of circuits into three vectors of circuits.

zip :: forall (n :: Nat) a b. KnownNat n => Circuit (Vec n a, Vec n b) (Vec n (a, b)) Source #

Transforms two vectors of circuits into a vector of tuples of circuits. Only works if the two vectors have the same length.

zip3 :: forall (n :: Nat) a b c. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c) (Vec n (a, b, c)) Source #

Transforms three vectors of circuits into a vector of tuples of circuits. Only works if the three vectors have the same length.

zip4 :: forall (n :: Nat) a b c d. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c, Vec n d) (Vec n (a, b, c, d)) Source #

Transforms four vectors of circuits into a vector of tuples of circuits. Only works if the four vectors have the same length.

zip5 :: forall (n :: Nat) a b c d e. KnownNat n => Circuit (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e) (Vec n (a, b, c, d, e)) Source #

Transforms five vectors of circuits into a vector of tuples of circuits. Only works if the five vectors have the same length.

unzip :: forall (n :: Nat) a b. KnownNat n => Circuit (Vec n (a, b)) (Vec n a, Vec n b) Source #

Unzip a vector of tuples of circuits into a tuple of vectors of circuits.

unzip3 :: forall (n :: Nat) a b c. KnownNat n => Circuit (Vec n (a, b, c)) (Vec n a, Vec n b, Vec n c) Source #

Unzip a vector of 3-tuples of circuits into a 3-tuple of vectors of circuits.

unzip4 :: forall (n :: Nat) a b c d. KnownNat n => Circuit (Vec n (a, b, c, d)) (Vec n a, Vec n b, Vec n c, Vec n d) Source #

Unzip a vector of 4-tuples of circuits into a 4-tuple of vectors of circuits.

unzip5 :: forall (n :: Nat) a b c d e. KnownNat n => Circuit (Vec n (a, b, c, d, e)) (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e) Source #

Unzip a vector of 5-tuples of circuits into a 5-tuple of vectors of circuits.

concat :: forall (n0 :: Nat) (n1 :: Nat) circuit. (KnownNat n0, KnownNat n1) => Circuit (Vec n0 (Vec n1 circuit)) (Vec (n0 * n1) circuit) Source #

Transform a vector of vectors of circuits into a vector of circuits.

unconcat :: forall (n :: Nat) (m :: Nat) circuit. (KnownNat n, KnownNat m) => SNat m -> Circuit (Vec (n * m) circuit) (Vec n (Vec m circuit)) Source #

Transform a vector of circuits into a vector of vectors of circuits.