Abstract

Permutations. Permutations can be constructed using the id and mk constructors and manipulated using a series of other constructors, which all guarantee that compositions are safe. The only way to inspect a permutation is to apply it, using the permute function.

Synopsis

local module type perm = {
type t [n]
val id: (n: i64) -> t [n]
val add [m] [n]: t [m] -> t [n] -> t [m + n]
val swap [n]: t [n] -> i64 -> i64 -> t [n]
val compose [n]: t [n] -> t [n] -> t [n]
val inv [n]: t [n] -> t [n]
val mk [n]: [n]i64 -> t [n]
val permute 'a [n]: t [n] -> [n]a -> [n]a
val rev [n]: t [n] -> t [n]
}
module perm: perm

Description

↑local module type perm
↑type t [n]

Type of permutations

↑val id: (n: i64) -> t [n]

The identity permutation of size n.

↑val add [m] [n]: t [m] -> t [n] -> t [m + n]

Parallel composition of permutations

↑val swap [n]: t [n] -> i64 -> i64 -> t [n]

Build a permutation from another permutation and a swap. It is checked that the two indices are in-bound.

↑val compose [n]: t [n] -> t [n] -> t [n]

Composition of two permutations. We have permute (compose f g) a = permute f (permute g a).

↑val inv [n]: t [n] -> t [n]

The inverse permutation. We have permute (inv p) (permute p a) = a for any p and any a of compatible sizes.

↑val mk [n]: [n]i64 -> t [n]

Build a permutation from a vector of indices indicating their position. We have permute (mk is) a = map (\i -> a[i]) is. It is checked that is indeed is a permutation.

↑val permute 'a [n]: t [n] -> [n]a -> [n]a

Perform a permutation on a vector.

↑val rev [n]: t [n] -> t [n]

Reverse a permutation.

↑module perm