Library
Module
Module type
Parameter
Class
Class type
This module provides an abstract data type of implicit, finite sequences. An implicit sequence is not explicitly represented in memory as an actual sequence of elements: instead, it is described by a data structure which contains enough information to produce an arbitrary element upon request. This design decision imposes some constraints on the operations that can be efficiently supported: for instance, filter
is not supported.
include FeatCore.IFSeqSig.IFSEQ_EXTENDED with type index = Num.t
include FeatCore.IFSeqSig.IFSEQ_BASIC with type index = Num.t
Constructors.
val empty : 'a seq
empty
is a sequence of length zero.
val zero : 'a seq
zero
is a synonym for empty
.
val singleton : 'a -> 'a seq
singleton x
is a sequence of length one whose single element is x
.
val one : 'a -> 'a seq
one
is a synonym for singleton
.
product s1 s2
is the Cartesian product of the sequences s1
and s2
. Its length is the product of the lengths of s1
and s2
. The first pair component is considered most significant.
map phi s
is the image of the sequence s
through the function phi
. If the user wishes to work with sequences of pairwise distinct elements, then phi
should be injective. If furthermore the user wishes to work with sequences that enumerate all elements of a type, then phi
should be surjective.
val up : int -> int -> int seq
up i j
is the sequence of the integers from i
included up to j
excluded.
type index = Num.t
The type index
is the type of integers used to represent indices and lengths.
get s i
is the i
-th element of the sequence s
. The index i
must be comprised between zero included and length s
excluded.
val foreach : 'a seq -> ('a -> unit) -> unit
foreach s k
iterates over all elements of the sequence s
. Each element in turn is passed to the loop body k
.
sample m s k
is an explicit sequence of at most m
elements extracted out of the implicit sequence s
, prepended in front of the existing sequence k
. If length s
is at most m
, then all elements of s
are produced. Otherwise, a random sample of m
elements extracted out of s
is produced.