package segmap

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module SegmapSource

This library offers an implementation of segment maps. A segment map represents a thinning, an increasing function of the natural numbers to the natural numbers.

Sourcetype index = int

An index is a member of the domain or codomain of the function that we wish to represent. In other words, it is a coordinate along the horizontal or vertical axis.

Sourcetype gap = int

A gap is a vertical displacement. It measures a move towards the north. It can be positive, zero, or negative.

Sourcetype len = int

A length is the length of a diagonal segment. It measures a move towards the northeast (that is, towards the north and towards the east). It is nonnegative.

Sourcetype delta = len

A delta is a horizontal displacement. It measures a move towards the west. It is nonnegative.

Sourcetype map

A segment map, or map, is an immutable data structure, which represents a thinning. A thinning is an increasing function of the natural integers to the natural integers. Visually, it can be understood as a succession of finite diagonal line segments, followed with an infinite diagonal half-line.

The weight of a map is the number of segments in this map. The extent of a map is the start index of the half-line. It is also the total length of the segments in this map. Because every segment has length at least one, the weight of a map is less than or equal to its extent.

Construction

Sourceval identity : map

The map identity represents the identity function. Thus, get identity i is i.

Sourceval north : gap -> map -> map

The map north gap m is the map m, moved by gap units towards the north. Thus, get (north gap m) x is get m x + gap.

The caller must guarantee 0 <= get m 0 + gap.

Complexity: O(1).

Sourceval northeast : len -> map -> map

The map northeast len m is the map m, moved by len units towards the northeast, and extended with a new diagonal segment of length len, beginning at the origin. Thus, get (northeast len m) x is if x < len then x else get m (x - len) + len.

The caller must guarantee 0 <= len.

Complexity: O(1).

Sourceval east : gap -> len -> map -> map

The map east gap len m is the map m, moved by len units towards the east, and extended with a new diagonal segment of length len, beginning at (0, gap). Thus, get (east gap len m) x is if x < len then gap + x else get m (x - len).

The caller must guarantee 0 <= gap && 0 <= len && gap + len <= get m 0.

Complexity: O(1).

Sourceval west : delta -> map -> map

The map west delta m is the map m, moved by delta units towards the west. The information contained in m on the semi-open interval [0, delta) is lost. Thus, get (west delta m) x is get m (x + delta).

The caller must guarantee 0 <= delta.

Complexity: O(min(delta, log W)), where W is the weight of the map m.

Sourceval compose : map -> map -> map

compose m1 m2 is the sequential composition of the maps m1 and m2, in left-to-right order. Thus get (compose m1 m2) x is get m2 (get m1 x).

Two complexity bounds can be given. First, the cost of composition is O(W1+W2), where W1 and W2 are the weights of the maps m1 and m2. Second, the cost of composition is also O(min(W1, W2).log(max(W1, W2)) + min(W1+W2, E1, E2)), which means that if one of the two maps has extent O(1) then the cost is logarithmic in the weight of the other map. In short, provided that one of its arguments is small, composition is very fast.

Observation

Sourceval get : map -> index -> index

get m x is the image of the index x through the map m.

The caller must guarantee 0 <= x.

Complexity: O(min(x, log W)), where W is the weight of the map m.

Sourceval head : map -> index

head m is a synonym for get m 0, and is slightly faster than get m 0.

Complexity: O(1).

Sourceval invert : map -> index -> index

invert m y returns the the lowest index x such that y <= get m x holds. Thus, unless x is zero, get m (x - 1) < y holds.

Complexity: O(min(y, log W)), where W is the weight of the map m.

Sourceval is_identity : map -> bool

is_identity m determines whether m is the identity map, that is, whether, for every index x, get m x is x.

Complexity: O(1).

Sourceval is_identity_below : delta -> map -> bool

is_identity_below m determines whether m is the identity map below index delta, that is, whether, for every index x such that x < delta holds, get m x is x.

The caller must guarantee 0 <= delta.

Complexity: O(1).

Sourceval equal : map -> map -> bool

equal m1 m2 determines whether the maps m1 and m2 are equal, that is, whether, for every index x, get m1 x = get m2 x holds.

Complexity: O(1) if the maps m1 and m2 have different weights; O(W) if they have a common weight W.

Sourcetype view =
  1. | VId of gap
  2. | VSeg of gap * len * map
Sourceval view : map -> view

view m is a view of the first segment of the map m, if it exists.

If view m is VId gap, then, for every index x, get m x is gap + x. Then 0 <= gap must hold.

If view m is VSeg gap len m', then, for every index x, get m x is if x < len then gap + x else get m' (x - len). Then 0 <= gap && 0 < len must hold.

view can be understood as a lazy variant of to_seglist. Instead of converting the entire map m to a segment list, view produces just the first segment, if it exists, together with a map m' that contains the remaining segments.

Complexity: O(1).

Conversion

Sourcetype seglist =
  1. | SId of gap
  2. | Seg of gap * len * seglist

A segment list is a simple description of a thinning. It is a finite list of diagonal segments, terminated with an infinite diagonal half-line. Each segment is described by a vertical gap gap and a length len, where 0 <= gap && 0 < len hold. The final half-line is described by a vertical gap gap, where 0 <= gap holds. A gap is absolute, not relative to the previous segment. Thus, every gap measures an altitude above the horizontal axis. Because a thinning is an increasing function, and because two consecutive segments can never be fused to form a single segment, the starting point of each segment, and of the final half-line, lies strictly higher than the endpoint of the previous segment.

Sourceval to_seglist : map -> seglist

to_seglist m returns a representation of the map m as a segment list.

Complexity: O(W), where W is the weight of the map m.

Sourceval of_seglist : seglist -> map

of_seglist segs converts the segment list segs to a map.

The caller must guarantee that the segment list segs is well-formed.

Complexity: O(W), where W is the weight (the length) of the segment list segs.