# package feat-core

Library

Module

Module type

Parameter

Class

Class type

This is the result signature of the functor `Enum.Make`

.

`module IFSeq : IFSeqSig.IFSEQ_EXTENDED`

This implementation of implicit finite sequences is used as a building block in the definition of the type `enum`

, which follows.

`type 'a enum = int -> 'a IFSeq.seq`

An enumeration of type `'a enum`

can be loosely thought of as a set of values of type `'a`

, equipped with a notion of size. More precisely, it is a function of a size `s`

to a subset of inhabitants of size `s`

, presented as a sequence.

We expose the fact that enumerations are functions, instead of making `enum`

an abstract type, because this allows the user to make recursive definitions. It is up to the user to ensure that recursion is well-founded; as a rule of thumb, every recursive call must appear under `pay`

. It is also up to the user to take precautions so that these functions have constant time complexity (beyond the cost of an initialization phase). This is typically achieved by using a memoizing fixed point combinator instead of an ordinary recursive definition.

`val empty : 'a enum`

`empty`

is the empty enumeration.

`val zero : 'a enum`

`zero`

is a synonym for `empty`

.

`val just : 'a -> 'a enum`

The enumeration `just x`

contains just the element `x`

, with size zero. `just x`

is equivalent to `finite [x]`

.

The enumeration `enum x`

contains the elements in the sequence `xs`

, with size zero.

The enumeration `pay e`

contains the same elements as `e`

, with a size that is increased by one with respect to `e`

.

`sum e1 e2`

is the union of the enumerations `e1`

and `e2`

. It is up to the user to ensure that the sets `e1`

and `e2`

are disjoint.

`exists xs e`

is the union of all enumerations of the form `e x`

, where `x`

is drawn from the list `xs`

. (This is an indexed sum.) It is up to the user to ensure that the sets `e1`

and `e2`

are disjoint.

`product e1 e2`

is the Cartesian product of the enumerations `e1`

and `e2`

.

`balanced_product e1 e2`

is a subset of the Cartesian product ```
product e1
e2
```

where the sizes of the left-hand and right-hand pair components must differ by at most one.

`map phi e`

is the image of the enumeration `e`

through the function `phi`

. It is up to the user to ensure that `phi`

is injective.

`val finite : 'a list -> 'a enum`

The enumeration `finite xs`

contains the elements in the list `xs`

, with size zero.

`val bool : bool enum`

`bool`

is equivalent to `finite [false; true]`

.

If `elem`

is an enumeration of the type `'a`

, then `list elem`

is an enumeration of the type `'a list`

. It is worth noting that every call to `list elem`

produces a fresh memoizing function, so (if possible) one should avoid applying `list`

twice to the same argument; that would be a waste of time and space.

Suppose we wish to enumerate lists of elements, where the validity of an element depends on which elements have appeared earlier in the list. For instance, we might wish to enumerate lists of instructions, where the set of permitted instructions at some point depends on the environment at this point, and each instruction produces an updated environment. If `fix`

is a suitable fixed point combinator and if the function `elem`

describes how elements depend on environments and how elements affect environments, then `dlist fix elem`

is such an enumeration. Each list node is considered to have size 1. Because the function `elem`

produces a list (as opposed to an enumeration), an element does not have a size.

The fixed point combinator `fix`

is typically of the form `curried fix`

, where `fix`

is a fixed point combinator for keys of type `'env * int`

. Memoization takes place at keys that are pairs of an environment and a size.

The function `elem`

receives an environment and must return a list of pairs of an element and an updated environment.

`val sample : int -> 'a enum -> int -> int -> 'a Stdlib.Seq.t -> 'a Stdlib.Seq.t`

`sample m e i j k`

is a sequence of at most `m`

elements of every size comprised between `i`

(included) and `j`

(excluded) extracted out of the enumeration `e`

, prepended in front of the existing sequence `k`

. At every size, if there are at most `m`

elements of this size, then all elements of this size are produced; otherwise, a random sample of `m`

elements of this size is produced.