Fix.Indexing
This module offers a safe API for manipulating indices into fixed-size arrays.
It provides support for constructing finite sets at the type level and for encoding the inhabitants of these sets as runtime integers. These runtime integers are statically branded with the name of the set that they inhabit, so two inhabitants of two distinct sets cannot be inadvertently confused.
If n
is a type-level name for a finite set, then a value of type n cardinal
is a runtime integer that represents the cardinal of the set n
.
In the following, the functor Gensym
allows creating open-ended sets, which can grow over time. If n
is such a set, then a value of type n cardinal
can be thought of as the as-yet-undetermined cardinal of the set.
val cardinal : 'n cardinal -> int
If n
is the cardinal of the set n
, then cardinal n
returns the cardinal of this set, as a concrete integer.
In the following, the functor Gensym
allows creating open-ended sets, which can grow over time. If n
is such a set, then calling cardinal n
has the side-effect of freezing this set, thereby fixing its cardinal: thereafter, calling fresh
becomes forbidden, so no new elements can be added.
val is_fixed : 'n cardinal -> bool
is_fixed n
determines whether the cardinal n
is (or has been) fixed.
The equality type.
equal n m
tests whether the cardinals n
and m
are equal, and if so, produces a type-level equality between the types 'n
and 'm
. If the cardinals n
or m
are not yet fixed, then, as a side effect of this call, they become fixed.
assert_equal n m
checks that the cardinals n
and m
are equal, and produces a type-level equality between the types 'n
and 'm
. If the cardinals n
or m
are not yet fixed, then, as a side effect of this call, they become fixed.
If n
is a type-level name for a finite set, then a value i
of type n index
is an integer value that is guaranteed to inhabit the set n
.
If n
has type n cardinal
, then 0 <= i < cardinal n
must hold.
The main reason why elements of a finite set are called "indices" is that their main purpose is to serve as indices in fixed-size vectors. See the submodule Vector
below.
module type CARDINAL = sig ... end
A new type-level set is created by an application of the functors Const
, Gensym
, and Sum
below. Each functor application creates a fresh type name n
. More precisely, each functor application returns a module whose signature is CARDINAL
: it contains both a fresh abstract type n
and a value n
of type n cardinal
that represents the cardinal of the newly-created set.
Const(struct let cardinal = c end)
creates a fresh type-level name for a set whose cardinal is c
. c
must be nonnegative.
val const : int -> (module CARDINAL)
module Gensym () : sig ... end
Gensym()
creates an open-ended type-level set, whose cardinality is not known a priori. As long as the cardinal of the set has not been observed by invoking cardinal
, new elements can be added to the set by invoking fresh
.
The type ('l, 'r) either
represents the disjoint sum of the types 'l
and 'r
. It is isomorphic to the type either
found in Stdlib.Either
in OCaml 4.12.0.
module type SUM = sig ... end
The signature SUM
extends CARDINAL
with an explicit isomorphism between the set n
and the disjoint sum l + r
. The functions inj_l
and inj_r
convert an index into l
or an index into r
into an index into n
. Conversely, the function prj
converts an index into r
into either an index into l
or an index into r
.
Sum(L)(R)
creates a new type-level set, which is the disjoint sums of the sets L
and R
. The functor application Sum(L)(R)
involves a call to cardinal L.n
, thereby fixing the cardinal of the set L
, if it was an open-ended set. The cardinal of the set R
is not fixed: if R
is an open-ended set, then the new set is open-ended as well, and it is still permitted to add new elements to R
by calling R.fresh()
. Fixing the cardinal of the new set fixes the cardinal of R
.
A vector of type (n, a) vector
is a (fixed-size) array whose indices lie in the type-level set n
and whose elements have type a
.