Agda.TypeChecking.Telescope

Documentation

flattenTel :: Telescope -> [Dom Type]

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

reorderTel :: [Dom Type] -> Maybe Permutation

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

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

reorderTel_ :: [Dom Type] -> Permutation

unflattenTel :: [ArgName] -> [Dom Type] -> Telescope

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

teleNames :: Telescope -> [ArgName]

Get the suggested names from a telescope

teleArgNames :: Telescope -> [Arg ArgName]

teleArgs :: DeBruijn a => Telescope -> [Arg a]

withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]

teleNamedArgs :: DeBruijn a => Telescope -> [NamedArg a]

tele2NamedArgs :: DeBruijn a => Telescope -> Telescope -> [NamedArg a]

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.

splitTelescopeAt :: Int -> Telescope -> (Telescope, Telescope)

Split the telescope at the specified position.

permuteTel :: Permutation -> Telescope -> Telescope

Permute telescope: permutes or drops the types in the telescope according to the given permutation. Assumes that the permutation preserves the dependencies in the telescope.

For example (Andreas, 2016-12-18, issue #2344): tel = (A : Set) (X : _18 A) (i : Fin (_m_23 A X)) tel (de Bruijn) = 2:Set, 1:_18 0, 0:Fin(_m_23 1 0) flattenTel tel = 2:Set, 1:_18 0, 0:Fin(_m_23 1 0) |- [ Set, _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! renaming _ (flipP perm) = [error, var 1, var 0] -- The correct renaming! apply to flattened tel = ... |- [ Set, _18 1, Fin (_m_23 1 0) ] permute perm it = ... |- [ Set, _18 1 ] unflatten (de Bruijn) = 1:Set, 0: _18 0 unflatten = (A : Set) (X : _18 A)

varDependencies :: Telescope -> IntSet -> IntSet

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

data SplitTel

A telescope split in two.

Constructors

SplitTel

Fields

• firstPart :: Telescope
• secondPart :: Telescope
• splitPerm :: Permutation

  The permutation takes us from the original telescope to firstPart ++ secondPart.

splitTelescope

Arguments

:: VarSet

A set of de Bruijn indices.

-> Telescope

Original telescope.

-> SplitTel

firstPart mentions the given variables, secondPart not.

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

See prop_splitTelescope.

splitTelescopeExact

Arguments

:: [Int]

A list of de Bruijn indices

-> Telescope

The telescope to split

-> Maybe SplitTel

firstPart mentions the given variables in the given order, secondPart contains all other variables

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

instantiateTelescope

Arguments

:: Telescope

⊢ Γ

-> Int

Γ ⊢ var k : A

-> Term

Γ ⊢ u : A

-> Maybe (Telescope, PatternSubstitution, Permutation)

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.

expandTelescopeVar :: Telescope -> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)

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

telView :: Type -> TCM TelView

Gather leading Πs of a type in a telescope.

telViewUpTo :: Int -> Type -> TCM TelView

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

telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView

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

mustBePi :: MonadTCM tcm => Type -> tcm (Dom Type, Abs Type)

Decomposing a function type.

ifPi :: MonadTCM tcm => Term -> (Dom Type -> Abs Type -> tcm a) -> (Term -> tcm a) -> tcm a

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.

ifPiType :: MonadTCM tcm => Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a

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.

ifNotPi :: MonadTCM tcm => Term -> (Term -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a

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.

ifNotPiType :: MonadTCM tcm => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a

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.

piApplyM :: Type -> Args -> TCM Type

A safe variant of piApply.

piApply1 :: MonadTCM tcm => Type -> Term -> tcm Type

typeArity :: Type -> TCM Nat

Compute type arity

Instance definitions

data OutputTypeName

Constructors

OutputTypeName QName

OutputTypeVar

OutputTypeNameNotYetKnown

NoOutputTypeName

getOutputTypeName :: Type -> TCM OutputTypeName

Strips all Pi's and return the head definition name, if possible.

addTypedInstance :: QName -> Type -> TCM ()

resolveUnknownInstanceDefs :: TCM ()

getInstanceDefs :: TCM InstanceTable

Try to solve the instance definitions whose type is not yet known, report an error if it doesn't work and return the instance table otherwise.