Module MenhirLib.LinearizedArray

This module offers support for linearizing an array of arrays (of possibly different lengths). All of the data is placed in a single data array, which is constructed by concatenating all of the little arrays. An entry array, which contains offsets into the data array, is also constructed.

make a turns the array of arrays a into a linearized array.

read la i j reads the linearized array la at indices i and j. Thus, read (make a) i j is equivalent to a.(i).(j).

write la i j v writes the value v into the linearized array la at indices i and j.

length la is the number of rows of the array la. Thus, length (make a) is equivalent to Array.length a.

row_length la i is the length of the row at index i in the linearized array la. Thus, row_length (make a) i is equivalent to Array.length a.(i).

read_row la i reads the row at index i, producing a list. Thus, read_row (make a) i is equivalent to Array.to_list a.(i).

Provided the accessor functions get_data and get_entry offers read access to the data and entry arrays of the linearized array la, read_row_via get_data get_entry i reads a row at index i in the linearized array la.