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

Agda.TypeChecking.Telescope

Contents

Synopsis

Documentation

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

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.

Get the suggested names from a telescope

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

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.

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)

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 FieldsfirstPart :: Telescope secondPart :: Telescope splitPerm :: PermutationThe permutation takes us from the original telescope to firstPart ++ secondPart.

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.

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.

Arguments

 :: Telescope ⊢ Γ -> [(Int, Term)] Γ ⊢ var k_i : A_i ascending order, Γ ⊢ u_i : A_i -> Maybe (Telescope, Substitution)

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.

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' :: 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.

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

type Boundary = Boundary' (Term, Term) Source #

[ (i,(x,y))
] = [(i=0) -> x, (i=1) -> y]

type Boundary' a = [(Term, a)] Source #

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 ΔΓ ⊢ i : I ΔΓ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : b

(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundaryP 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 Γ.

teleElims :: DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a] Source #

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

returns Left (a,b) in case the type is Pi a b or PathP b _ _ assumes the type is in whnf.

mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type) Source #

Decomposing a function type.

ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m 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 :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m 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 :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m 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 :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m 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.

ifNotPiOrPathType :: (MonadReduce tcm, MonadTCM tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a Source #

class PiApplyM a where Source #

A safe variant of piApply.

Methods

piApplyM :: MonadReduce m => Type -> a -> m Type Source #

Instances
 Source # Instance detailsDefined in Agda.TypeChecking.Telescope MethodspiApplyM :: MonadReduce m => Type -> Term -> m Type Source # PiApplyM a => PiApplyM [a] Source # Instance detailsDefined in Agda.TypeChecking.Telescope MethodspiApplyM :: MonadReduce m => Type -> [a] -> m Type Source # PiApplyM a => PiApplyM (Arg a) Source # Instance detailsDefined in Agda.TypeChecking.Telescope MethodspiApplyM :: MonadReduce m => Type -> Arg a -> m Type Source # PiApplyM a => PiApplyM (Named n a) Source # Instance detailsDefined in Agda.TypeChecking.Telescope MethodspiApplyM :: MonadReduce m => Type -> Named n a -> m Type Source #

Compute type arity

Instance definitions

Strips all hidden and instance Pi's and return the argument telescope and head definition name, if possible.

Register the definition with the given type as an instance

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.