Module Waksman

Function apply_switching_network_bool


pub  fn apply_switching_network_bool
[
N : Nat,
@D
]
(   x : list[bool[N] $post @D] $pre @public,
   netDesc : list[uint[18446744073709551616] $pre @public] $pre @public,
   switches : list[bool[N] $post @D] $pre @public
) 
-> list[bool[N] $post @D] $pre @public

where

  Field[N]

The result of the permutation obtained by giving the switches in the third argument (in the format produced by switches_of_perm) as input to the network in the second argument (in the format produced by make_waksman_network) when applied to the list of booleans in the first argument.

Function apply_switching_network_generic


pub  fn apply_switching_network_generic
[
T : Qualified,
N : Nat,
@D
]
(   x : list[T] $pre @public,
   netDesc : list[uint[18446744073709551616] $pre @public] $pre @public,
   switches : list[bool[N] $post @D] $pre @public,
   interface : ApplySwitchingNetworkInterface[T, N, @D] $pre @public
) 
-> list[T] $pre @public

The generic result of the permutation obtained by giving the switches in the third argument (in the format produced by switches_of_perm) as input to the network in the second argument (in the format produced by make_waksman_network) when applied to the list in the first argument. Generic context is provided by the ApplySwitchingNetworkInterface object in the fourth argument.

Function apply_switching_network_uint


pub  fn apply_switching_network_uint
[
N : Nat,
@D
]
(   x : list[uint[N] $post @D] $pre @public,
   netDesc : list[uint[18446744073709551616] $pre @public] $pre @public,
   switches : list[bool[N] $post @D] $pre @public
) 
-> list[uint[N] $post @D] $pre @public

The result of the permutation obtained by giving the switches in the third argument (in the format produced by switches_of_perm) as input to the network in the second argument (in the format produced by make_waksman_network) when applied to the list of integers in the first argument.

Function get_switches_for_sorting


pub  fn get_switches_for_sorting
[
N : Nat,
@D
]
(   x : list[uint[N] $pre @D] $pre @public
) 
-> list[bool[N] $post @D] $pre @public

where

  Field[N],

  Vectorization

The list of switches on wires that, if given as input to the Waksman network of appropriate order, produces a permutation that sorts the given input list. Integrity is not checked.

Function make_waksman_network


pub  fn make_waksman_network
(   n : uint[18446744073709551616] $pre @public
) 
-> list[uint[18446744073709551616] $pre @public] $pre @public

Constructing a Waksman permutation network of the given order. A synonym of the builtin function __make_waksman_network.

Function switches_of_perm


pub  fn switches_of_perm
[
N : Nat,
@D
]
(   template : list[uint[18446744073709551616] $pre @D] $pre @public
) 
-> list[bool[N] $pre @D] $pre @public

The list of switches which, if given as input to the Waksman network of the order of the length of the given permutation, leads to the given permutation. Unlike in the case of the builtin function __permutation_switches, the switches are returned as booleans.