Module MenhirLib.RowDisplacementDecode

Row displacement aims to compress a two-dimensional table where some values are considered insignificant.

type displacement = int

A displacement is a nonnegative integer, which, once decoded in a certain way, represents a possibly negative offset into a data array.

val get : ('displacement -> int -> displacement) -> ('data -> int -> 'a) -> ('displacement * 'data) -> int -> int -> 'a

A compressed table is represented as a pair of a displacement array and a data array. If the functions get_displacement and get_data offer read access to these arrays, then get get_displacement get_data i j returns the value found at indices i and j in the compressed table. This call is permitted only if the value found at indices i and j in the original table is significant.

val decode : displacement -> int

The auxiliary function decode is part of the implementation of get. It is exposed because it is used by the specialized versions of get that the table back-end generates. See TableUtils.