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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Telescope

Contents

- Instance definitions

Synopsis

- flattenTel :: Subst t a => Tele (Dom a) -> [Dom a]
- reorderTel :: [Dom Type] -> Maybe Permutation
- reorderTel_ :: [Dom Type] -> Permutation
- unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
- teleNames :: Telescope -> [ArgName]
- teleArgNames :: Telescope -> [Arg ArgName]
- teleArgs :: DeBruijn a => Tele (Dom t) -> [Arg a]
- withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
- teleNamedArgs :: DeBruijn a => Telescope -> [NamedArg a]
- tele2NamedArgs :: DeBruijn a => Telescope -> Telescope -> [NamedArg a]
- splitTelescopeAt :: Int -> Telescope -> (Telescope, Telescope)
- permuteTel :: Permutation -> Telescope -> Telescope
- varDependencies :: Telescope -> IntSet -> IntSet
- data SplitTel = SplitTel {
  - firstPart :: Telescope
  - secondPart :: Telescope
  - splitPerm :: Permutation
  }
- splitTelescope :: VarSet -> Telescope -> SplitTel
- splitTelescopeExact :: [Int] -> Telescope -> Maybe SplitTel
- instantiateTelescopeN :: Telescope -> [(Int, Term)] -> Maybe (Telescope, Substitution)
- instantiateTelescope :: Telescope -> Int -> Term -> Maybe (Telescope, PatternSubstitution, Permutation)
- expandTelescopeVar :: Telescope -> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
- telView :: Type -> TCM TelView
- telViewUpTo :: Int -> Type -> TCM TelView
- telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView
- telViewPath :: Type -> TCM TelView
- telViewUpToPath :: Int -> Type -> TCM TelView
- type Boundary = Boundary' (Term, Term)
- type Boundary' a = [(Term, a)]
- telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView, Boundary)
- fullBoundary :: Telescope -> Boundary -> Boundary
- telViewUpToPathBoundary :: Int -> Type -> TCM (TelView, Boundary)
- telViewUpToPathBoundaryP :: Int -> Type -> TCM (TelView, Boundary)
- telViewPathBoundaryP :: Type -> TCM (TelView, Boundary)
- teleElims :: DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
- pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type)
- pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term, Term)) Type)
- pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
- piOrPath :: Type -> TCM (Either (Dom Type, Abs Type) Type)
- telView'UpToPath :: Int -> Type -> TCM TelView
- telView'Path :: Type -> TCM TelView
- isPath :: Type -> TCM (Maybe (Dom Type, Abs Type))
- telePatterns :: (DeBruijn a, DeBruijn (Pattern' a)) => Telescope -> Boundary -> [NamedArg (Pattern' a)]
- telePatterns' :: (DeBruijn a, DeBruijn (Pattern' a)) => (forall a. DeBruijn a => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
- mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type)
- ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
- ifPiType :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
- ifNotPi :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
- ifNotPiType :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
- ifNotPiOrPathType :: (MonadReduce tcm, MonadTCM tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
- class PiApplyM a where
  - piApplyM :: MonadReduce m => Type -> a -> m Type
- typeArity :: Type -> TCM Nat
- data OutputTypeName
  - = OutputTypeName QName
  - | OutputTypeVar
  - | OutputTypeVisiblePi
  - | OutputTypeNameNotYetKnown
  - | NoOutputTypeName
- getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
- addTypedInstance :: QName -> Type -> TCM ()
- resolveUnknownInstanceDefs :: TCM ()
- getInstanceDefs :: TCM InstanceTable

# Documentation

flattenTel :: Subst t a => Tele (Dom a) -> [Dom a] 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 `normalise`d.

reorderTel_ :: [Dom Type] -> Permutation Source #

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

teleArgNames :: Telescope -> [Arg ArgName] Source #

teleArgs :: DeBruijn a => Tele (Dom t) -> [Arg a] Source #

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

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

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.

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

Split the telescope at the specified position.

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.

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

instantiateTelescopeN Source #

Arguments

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

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)

telView :: Type -> TCM TelView Source #

Gather leading Πs of a type in a telescope.

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`.

telViewPath :: Type -> TCM TelView Source #

telViewUpToPath :: Int -> Type -> TCM TelView Source #

`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 #

telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView, Boundary) 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`.

fullBoundary :: Telescope -> Boundary -> Boundary Source #

telViewUpToPathBoundary :: Int -> Type -> TCM (TelView, Boundary) Source #

`(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

telViewUpToPathBoundaryP :: Int -> Type -> TCM (TelView, Boundary) Source #

`(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 Γ.

telViewPathBoundaryP :: Type -> TCM (TelView, Boundary) Source #

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

pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type) Source #

pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term, Term)) Type) Source #

pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type) Source #

piOrPath :: Type -> TCM (Either (Dom Type, Abs Type) Type) Source #

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

telView'UpToPath :: Int -> Type -> TCM TelView Source #

telView'Path :: Type -> TCM TelView Source #

isPath :: Type -> TCM (Maybe (Dom Type, Abs Type)) Source #

telePatterns :: (DeBruijn a, DeBruijn (Pattern' a)) => Telescope -> Boundary -> [NamedArg (Pattern' a)] Source #

telePatterns' :: (DeBruijn a, DeBruijn (Pattern' a)) => (forall a. DeBruijn a => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)] Source #

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

PiApplyM Term Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Term -> m Type Source #
PiApplyM a => PiApplyM [a] Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> [a] -> m Type Source #
PiApplyM a => PiApplyM (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Arg a -> m Type Source #
PiApplyM a => PiApplyM (Named n a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Named n a -> m Type Source #

typeArity :: Type -> TCM Nat Source #

Compute type arity

# Instance definitions

data OutputTypeName Source #

Constructors

OutputTypeName QName |
OutputTypeVar |
OutputTypeVisiblePi |
OutputTypeNameNotYetKnown |
NoOutputTypeName |

getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName) Source #

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

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

Register the definition with the given type as an instance

resolveUnknownInstanceDefs :: TCM () Source #

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.