Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Telescope

Contents

Synopsis

Documentation

getOutputTypeName :: Type -> TCM OutputTypeName Source

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

renameP :: Subst t a => Permutation -> a -> a Source

The permutation should permute the corresponding telescope. (left-to-right list)

renaming :: forall a. DeBruijn a => Permutation -> Substitution' a Source

If permute π : [a]Γ -> [a]Δ, then applySubst (renaming π) : Term Γ -> Term Δ

renamingR :: DeBruijn a => Permutation -> Substitution' a Source

If permute π : [a]Γ -> [a]Δ, then applySubst (renamingR π) : Term Δ -> Term Γ

flattenTel :: Telescope -> [Dom Type] Source

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

reorderTel :: [Dom Type] -> Maybe Permutation Source

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.

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

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

teleNames :: Telescope -> [ArgName] Source

Get the suggested names from a telescope

permuteTel :: Permutation -> Telescope -> Telescope Source

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.

varDependencies :: Telescope -> IntSet -> IntSet Source

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

data SplitTel Source

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 Source

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 Source

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 Source

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) Source

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

telViewUpTo :: Int -> Type -> TCM TelView Source

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 Source

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) Source

Decomposing a function type.

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

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 Source

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 Source

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 Source

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 Source

A safe variant of piApply.

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

intro1 :: MonadTCM tcm => Type -> (Type -> tcm a) -> tcm a Source

Given a function type, introduce its domain into the context and continue with its codomain.

Instance definitions

getInstanceDefs :: TCM InstanceTable Source

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.