Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
package menhirGLR
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Module MenhirGLR.RowDisplacementDecodeSource
Row displacement aims to compress a two-dimensional table where some values are considered insignificant.
A displacement is a nonnegative integer, which, once decoded in a certain way, represents a possibly negative offset into a data array.
Source
val get :
('displacement -> int -> displacement) ->
('data -> int -> 'a) ->
('displacement * 'data) ->
int ->
int ->
'aA 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.
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.