Source file `RowDisplacementDecode.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
(******************************************************************************)
(*                                                                            *)
(*                                    Menhir                                  *)
(*                                                                            *)
(*   Copyright Inria. All rights reserved. This file is distributed under     *)
(*   the terms of the GNU Library General Public License version 2, with a    *)
(*   special exception on linking, as described in the file LICENSE.          *)
(*                                                                            *)
(******************************************************************************)

(* -------------------------------------------------------------------------- *)

(**A displacement is a nonnegative integer, which, once decoded in a certain
   way, represents a possibly negative offset into a data array. *)
type displacement =
  int

(* A compressed table is represented as a pair of a displacement array and a
   data array. The displacement array is an array of (encoded) offsets into
   the data array. *)

(* -------------------------------------------------------------------------- *)

(* In order to avoid producing negative displacements, we encode displacements
   by moving to the sign bit to the least significant position. This decoding
   function undoes this. *)

let[@inline] decode (displacement : displacement) : int =
  if displacement land 1 = 0 then
    displacement lsr 1
  else
    -(displacement lsr 1)

(* -------------------------------------------------------------------------- *)

(* [get ct i j] returns the value found at indices [i] and [j] in the
   compressed table [ct]. This call is permitted only if the value found at
   indices [i] and [j] in the original table is significant. *)

(* Together, [compress] and [get] have the property that, if the value found
   at indices [i] and [j] in an uncompressed table [t] is significant, then
   [get (compress t) i j] is equal to that value. *)

(* Unused:

let get (displacement, data) i j =
  assert (0 <= i && i < Array.length displacement);
  let k = decode displacement.(i) in
  assert (0 <= k + j && k + j < Array.length data);
    (* Failure of the above assertion indicates an attempt to access an
       insignificant element that happens to be mapped out of the bounds
       of the [data] array. *)
  data.(k + j)

 *)

(* -------------------------------------------------------------------------- *)

(* This variant of [get] requires read access, via accessors, to the two
   components of the table. It is otherwise identical to [get] above. *)

let[@inline] get get_displacement get_data (displacement, data) i j =
  let k = decode (get_displacement displacement i) in
  get_data data (k + j)

(* Specialized copies of [get] are generated by the table back-end.
   See [TableUtils]. *)