Flatten telescope: (Γ : Tel) -> [Type Γ].

flattenTel is lazy in both the spine and values of the resulting list.

Flatten telescope: (Γ : Tel) -> [Type Γ] into a reversed list.

flattenRevTel is lazy in both the spine and values of the resulting list.

Turn a context into a flat telescope: all entries live in the whole context. (Γ : Context) -> [Type Γ]

Order a flattened telescope in the correct dependency order: Γ -> Permutation (Γ -> Γ~)

Since reorderTel tel uses free variable analysis of type in tel, the telescope should be normalised.

Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.

A variant of unflattenTel which takes the size of the last argument as an argument.

Rename the variables in the telescope to the given names Precondition: size xs == size tel.

Get the suggested names from a telescope

Convert a telescope to a list of Arg in left-to-right order:

teleArgs ((a : A) (b : B a) {c : C}) = [a, b, {c}] = [2, 1, {0}]

Convert a telescope to a list of Dom in left-to-right order:

teleDoms ((a : A) (b : B a) {c : C}) = [a, b, {c}] = [2, 1, {0}]

A variant of teleNamedArgs which takes the argument names (and the argument info) from the first telescope and the variable names from the second telescope.

Precondition: the two telescopes have the same length.

Split the telescope at the specified position.

Take the first n elements off of a telescope.

Drop the last n elements off of a telescope.

This is strict in the spine of the telescope.

Permute telescope: permutes or drops the types in the telescope according to the given permutation (on de Bruijn _levels_). Assumes that the permutation preserves the dependencies in the telescope.

For example (Andreas, 2016-12-18, issue #2344): tel = (A : Type) (X : _18 A) (i : Fin (_m_23 A X)) tel (de Bruijn) = 2:Type, 1:_18 0, 0:Fin(_m_23 1 0) flattenTel tel = 2:Type, 1:_18 0, 0:Fin(_m_23 1 0) |- [ Type, _18 2, Fin (_m_23 2 1) ] perm = 0,1,2 -> 0,1 (picks the first two) renaming _ perm = [var 0, var 1, error] -- THE WRONG RENAMING! (levels) renaming _ (reverseP perm) = [error, var 0, var 1] -- The correct renaming! (indices) apply to flattened tel = ... |- [ Type, _18 1, Fin (_m_23 1 0) ] permute perm it = ... |- [ Type, _18 1 ] unflatten (de Bruijn) = 1:Type, 0: _18 0 unflatten = (A : Type) (X : _18 A)

Like permuteTel, but start with a context.

Recursively computes dependencies of a set of variables in a given telescope. Any dependencies outside of the telescope are ignored.

Note that varDependencies considers a variable to depend on itself.

Computes the set of variables in a telescope whose type depend on one of the variables in the given set (including recursive dependencies). Any dependencies outside of the telescope are ignored.

Unlike varDependencies, a variable is *not* considered to depend on itself.

A telescope split in two.

Split a telescope into the part that defines the given variables and the part that doesn't.

See prop_splitTelescope.

As splitTelescope, but fails if any additional variables or reordering would be needed to make the first part well-typed.

Try to instantiate one variable in the telescope (given by its de Bruijn level) with the given value, returning the new telescope and a substitution to the old one. Returns Nothing if the given value depends (directly or indirectly) on the variable.

Try to eta-expand one variable in the telescope (given by its de Bruijn level)

Gather leading Πs of a type in a telescope.

telViewUpTo n t takes off the first n function types of t. Takes off all if n < 0.

telViewUpTo' n p t takes off $t$ the first n (or arbitrary many if n < 0) function domains as long as they satify p.

telViewUpToPath n t takes off t the first n (or arbitrary many if n < 0) function domains or Path types.

telViewUpToPath n t = fst $ telViewUpToPathBoundary' n t

Boundary conditions [[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]. For instance, if p : Path A a b, then p i has boundary condition (i,(a,b)). We call i the dimension and (x,y) its boundary.

Usually, the dimensions of a boundary condition are interval variables, represented by a de Bruijn index Int.

Substitution formally creates dimensions that are interval expressions, represented by a Term. However, in practice these terms should be of the form var i.

Turn dimension variables i into dimension expressions var i.

Turn dimension expressions into dimension variables. Formally this is a partial operation, but should only be called when the precondition is met.

Precondition: the dimension terms in the boundary are all of the form var i.

Like telViewUpToPath but also returns the Boundary expected by the Path types encountered. The boundary terms live in the telescope given by the TelView. Each point of the boundary has the type of the codomain of the Path type it got taken from, see fullBoundary.

 (TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary' n a
 Input:  Δ ⊢ a
 Output: Δ.Γ ⊢ b
         Δ.Γ ⊢ T is the codomain of the PathP at variable i
         Δ.Γ ⊢ i : I
         Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T

Useful to reconstruct IApplyP patterns after teleNamedArgs Γ.

(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary n a Input: Δ ⊢ a Output: ΔΓ ⊢ b ΔΓ ⊢ i : I ΔΓ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : b

teleElimsB args bs = es Input: Δ.Γ ⊢ args : Γ Δ.Γ ⊢ T is the codomain of the PathP at variable i Δ.Γ ⊢ i : I Δ.Γ ⊢ bs = [ (i=0) -> t_i; (i=1) -> u_i ] : T Output: Δ.Γ | PiPath Γ bs A ⊢ es : A

Reduces Type.

Reduces Type.

Returns Left (a,b) in case the type is Pi a b or PathP b _ _. Assumes the Type is in whnf.

Assumes Type is in whnf.

Decomposing a function type.

If the given type is a Pi, pass its parts to the first continuation. If not (or blocked), pass the reduced type to the second continuation.

If the given type is a Pi, pass its parts to the first continuation. If not (or blocked), pass the reduced type to the second continuation.

If the given type is blocked or not a Pi, pass it reduced to the first continuation. If it is a Pi, pass its parts to the second continuation.

If the given type is blocked or not a Pi, pass it reduced to the first continuation. If it is a Pi, pass its parts to the second continuation.

Instantiate a Type with a sequence of arguments, possibly reducing if the type is not manifestly a Pi.

This is a safe variant of piApply.

A class for things (Arg, etc) that can be turned into a sequence of arguments for piApplyM'.

A version of piApplyM'' generalised over the arguments to instantiate with.

A version of piApplyM'' generalised over the arguments to instantiate with, throwing an __IMPOSSIBLE__ error if there are leftover arguments and the type can not be reduced to a Pi type.

Compute type arity

Fold a telescope into a monadic computation, adding variables to the context at each step.

Instantiate a Teletype with some Args, attempting to produce a Type.

Takes continuations for whether we ran out of arguments with leftover quantification, or out of quantifiers with leftover arguments. Note that, unlike teleView, the Type given to the "out of arguments" continuation may include leading Pis.

Instantiate a Teletype with some Args, handling leftover arguments by attempting reduction.

Leftover quantifiers are turned into dependent binders (Abs), as per telePi_.

Instantiate a Teletype with some Args. Leftover quantifiers are turned into dependent binders (Abs), as per telePi_.

INVARIANT: the length of the arguments must not exceed the explicit quantification in the teletype. If this is not known, use the monadic teleApplyM instead.

View a Teletype as a TelView, continuing into the "core" type if necessary.

Unlike unpackTeletype, this function will also move quantification in the "core" of the Teletype into the Telescope returned, as per telView.

Quantify a Type over a Telescope, producing a Teletype.

If the type is a literal function type (as per telView'), these extra quantifiers are also moved into the Teletype.

Add a binding to the front of a Teletype.

View a Teletype as a TelView, continuing into the "core" type if necessary, returning the expected boundaries of any path encountered along the way; a Teletype version of telViewUpToPathBoundary.

The Int parameter, n, controls the number of quantifiers that may be returned in the TelView. This means that if n is less than the size of the teletype, any quantifiers will be moved into the type part of the TelView.

This function is lazy in the Boundary, so it can be used even if computing the boundary is not necessary.