A context that can be determined statically at compiler time.

Represents the size of a context.

Convert a context size to an Int.

The size of an empty context.

Increment the size to the next value.

Extend the size by a given difference.

The total size of two concatenated contexts.

Allows interpreting a size.

Project a size

Difference in number of elements between two contexts. The first context must be a sub-context of the other.

The identity difference. Identity element of Category instance.

The addition of differences. Flipped binary operation of Category instance.

Extend the difference to a sub-context of the right side.

A difference that can be automatically inferred at compile time.

Proof that r = l + app for some app

If l is a sub-context of r then extract out their "contextual difference", i.e., the app such that r = l + app

An index is a reference to a position with a particular type in a context.

Index for first element in context.

Increase context while staying at same index.

Return the last index of a element.

Return the index of a element one past the size.

Adapts an index in the left hand context of an append operation.

Adapts an index in the right hand context of an append operation.

Compute an Index into a context r from an Index into a sub-context l of r.

Compute an Index into an appended context from an Index into its suffix.

Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f is equivalent to v0 when n is zero, and f (forIndex (n-1) v0) n otherwise. Unlike the safe version, which starts from Index 0 and increments Index values, this version starts at Index (n-1) and decrements Index values to Index 0.

Given an index i, size n, a function f, value v, and a function f, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.

Return index at given integer or nothing if integer is out of bounds.

View of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.

Project an index

This represents a contiguous range of indices.

Return a range containing all indices in the context.

indexOfRange returns the only index in a range.

dropHeadRange r n drops the first n elements in r.

dropTailRange r n drops the last n elements in r.

An assignment is a sequence that maps each index with type tp to a value of type f tp.

This assignment implementation uses a binomial tree implementation that offers lookups and updates in time and space logarithmic with respect to the number of elements in the context.

Return number of elements in assignment.

replicate n make a context with different copies of the same polymorphic value.

Generate an assignment

Generate an assignment in an Applicative context

Return empty assignment

Modify the value of an assignment at a particular index.

Represent an assignment as either empty or an assignment with one appended.

View an assignment as either empty or an assignment with one appended.

Return value of assignment.

Return value of assignment, where the index is into an initial sequence of the assignment.

Create a single element context.

Convert the assignment to a vector.

Pattern synonym for extending an assignment on the right

Pattern synonym for the empty assignment

Return true if assignment is empty.

Return assignment with all but the last block.

Return the last element in the assignment.

View an assignment as either empty or an assignment with one appended.

Return the prefix of an appended Assignment

Return the suffix of an appended Assignment

'forIndexM sz f' calls f on indices '[0..sz-1]'.

Generate an assignment with some context type that is not known.

Generate an assignment with some context type that is not known.

Create an assignment from a list of values.

Visit each of the elements in an Assignment in order from left to right and collect the results using the provided Monoid.

Visit each of the elements in an Assignment in order from left to right, executing an action with each.

Utility function for testing if xs is an assignment with prefix as a prefix, and computing the tail of xs not in the prefix, if so.

This datastructure contains a proof that the first context is embeddable in the second. This is useful if we want to add extend an existing term under a larger context.

Prove that the prefix of an appended context is embeddable in it

Prove that the suffix of an appended context is embeddable in it

Constraint synonym used for getting an Index into a Ctx. n is the zero-based, left-counted index into the list of types ctx which has the type r.

Get a lens for an position in an Assignment by zero-based, left-to-right position. The position must be specified using TypeApplications for the n parameter.

Compute an Index value for a particular position in a Ctx. The TypeApplications extension will be needed to disambiguate the choice of the type n.

This version of natIndex is suitable for use without the TypeApplications extension.

This type family is used to define currying/uncurrying operations on assignments. It is best understood by seeing its evaluation on several examples:

CurryAssignment EmptyCtx f x = x
CurryAssignment (EmptyCtx ::> a) f x = f a -> x
CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x

This class implements two methods that witness the isomorphism between curried and uncurried functions.