feat-core 20220407 (latest)

Parameters

module IFSeq : IFSeqSig.IFSEQ_EXTENDED

Signature

module IFSeq = IFSeq

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].

val enum : 'a IFSeq.seq -> 'a enum

The enumeration enum x contains the elements in the sequence xs, with size zero.

val pay : 'a enum -> 'a enum

The enumeration pay e contains the same elements as e, with a size that is increased by one with respect to e.

val sum : 'a enum -> 'a enum -> 'a enum

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.

val (++) : 'a enum -> 'a enum -> 'a enum

(++) is a synonym for sum.

val exists : 'a list -> ('a -> 'b enum) -> 'b enum

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.

val product : 'a enum -> 'b enum -> ('a * 'b) enum

product e1 e2 is the Cartesian product of the enumerations e1 and e2.

val (**) : 'a enum -> 'b enum -> ('a * 'b) enum

( ** ) is a synonym for product.

val balanced_product : 'a enum -> 'b enum -> ('a * 'b) enum

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.

val (*-*) : 'a enum -> 'b enum -> ('a * 'b) enum

( *-* ) is a synonym for balanced_product.

val map : ('a -> 'b) -> 'a enum -> 'b enum

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].

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

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.

val dlist : 
  ('env -> 'a list enum) Fix.fix ->
  ('env -> ('a * 'env) list) ->
  'env ->
  'a list enum

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 Seq.t -> 'a 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.

package feat-core

Parameters

Signature