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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Telescope

Synopsis

- flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
- flattenContext :: Context -> [ContextEntry]
- reorderTel :: [Dom Type] -> Maybe Permutation
- reorderTel_ :: [Dom Type] -> Permutation
- unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
- unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Telescope
- renameTel :: [Maybe ArgName] -> Telescope -> Telescope
- teleNames :: Telescope -> [ArgName]
- teleArgNames :: Telescope -> [Arg ArgName]
- teleArgs :: DeBruijn a => Tele (Dom t) -> [Arg a]
- teleDoms :: DeBruijn a => Tele (Dom t) -> [Dom a]
- teleNamedArgs :: DeBruijn a => Tele (Dom t) -> [NamedArg a]
- tele2NamedArgs :: DeBruijn a => Telescope -> Telescope -> [NamedArg a]
- splitTelescopeAt :: Int -> Telescope -> (Telescope, Telescope)
- permuteTel :: Permutation -> Telescope -> Telescope
- permuteContext :: Permutation -> Context -> Telescope
- varDependencies :: Telescope -> IntSet -> IntSet
- varDependents :: Telescope -> IntSet -> IntSet
- data SplitTel = SplitTel {
  - firstPart :: Telescope
  - secondPart :: Telescope
  - splitPerm :: Permutation
  }
- splitTelescope :: VarSet -> Telescope -> SplitTel
- splitTelescopeExact :: [Int] -> Telescope -> Maybe SplitTel
- instantiateTelescope :: Telescope -> Int -> DeBruijnPattern -> Maybe (Telescope, PatternSubstitution, Permutation)
- expandTelescopeVar :: Telescope -> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
- telView :: (MonadReduce m, MonadAddContext m) => Type -> m TelView
- telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
- telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
- telViewPath :: PureTCM m => Type -> m TelView
- telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
- newtype Boundary' x a = Boundary {
  - theBoundary :: [(x, (a, a))]
  }
- type Boundary = Boundary' Int Term
- type TmBoundary = Boundary' Term Term
- tmBoundary :: Boundary' Int a -> Boundary' Term a
- varBoundary :: Boundary' Term a -> Boundary' Int a
- telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
- fullBoundary :: Telescope -> Boundary -> Boundary
- telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (TelView, Boundary)
- telViewPathBoundary :: PureTCM m => Type -> m (TelView, Boundary)
- teleElims :: DeBruijn a => Telescope -> Boundary' Int a -> [Elim' a]
- pathViewAsPi :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type)
- pathViewAsPi' :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
- pathViewAsPi'whnf :: HasBuiltins m => m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
- piOrPath :: HasBuiltins m => Type -> m (Either (Dom Type, Abs Type) Type)
- telView'UpToPath :: Int -> Type -> TCM TelView
- telView'Path :: Type -> TCM TelView
- isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
- ifPath :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
- ifPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
- ifNotPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
- ifPiOrPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
- ifNotPiOrPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
- telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
- telePatterns' :: DeBruijn a => (forall a1. DeBruijn a1 => Telescope -> [NamedArg a1]) -> 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
- ifPiB :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
- ifPiTypeB :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> 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, HasBuiltins tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
- shouldBePath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
- shouldBePi :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
- shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
- class PiApplyM a where
  - piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type
  - piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type
- typeArity :: Type -> TCM Nat
- foldrTelescopeM :: MonadAddContext m => (Dom (ArgName, Type) -> m b -> m b) -> m b -> Telescope -> m b

# Documentation

flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a] Source #

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

flattenContext :: Context -> [ContextEntry] Source #

Turn a context into a flat telescope: all entries live in the whole context. `(Γ : Context) -> [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.

unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Telescope Source #

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

renameTel :: [Maybe ArgName] -> Telescope -> Telescope Source #

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

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 #

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

teleNamedArgs :: DeBruijn a => Tele (Dom t) -> [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)`

permuteContext :: Permutation -> Context -> Telescope Source #

Like `permuteTel`, but start with a context.

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.

varDependents :: Telescope -> IntSet -> IntSet Source #

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.

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 de Bruijn _level_
-> DeBruijnPattern | Γ ⊢ 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 :: (MonadReduce m, MonadAddContext m) => Type -> m TelView Source #

Gather leading Πs of a type in a telescope.

telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView Source #

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

telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m 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 :: PureTCM m => Type -> m TelView Source #

telViewUpToPath :: PureTCM m => Int -> Type -> m TelView Source #

`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

newtype Boundary' x a Source #

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.

Constructors

Boundary |

Fields

- theBoundary :: [(x, (a, a))]

#### Instances

Instances details

Subst Boundary Source # | Substitution into a `Boundary` a priori creates a `TmBoundary` which we convert back via `varBoundary`. A priori, this is a partial operation.

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg Boundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg Boundary = Term

Methods

applySubst :: Substitution' (SubstArg Boundary) -> Boundary -> Boundary Source #

Subst TmBoundary Source # |

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg TmBoundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg TmBoundary = Term

Methods

applySubst :: Substitution' (SubstArg TmBoundary) -> TmBoundary -> TmBoundary Source #

(Pretty x, Pretty a) => Pretty (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods pretty :: Boundary' x a -> Doc Source # prettyPrec :: Int -> Boundary' x a -> Doc Source # prettyList :: [Boundary' x a] -> Doc Source #
(ComputeOccurrences x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Boundary' x a -> OccM OccurrencesBuilder Source #
(PrettyTCM x, PrettyTCM a) => PrettyTCM (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Boundary' x a -> m Doc Source #
Null (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods empty :: Boundary' x a Source # null :: Boundary' x a -> Bool Source #
(Show x, Show a) => Show (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods showsPrec :: Int -> Boundary' x a -> ShowS Source # show :: Boundary' x a -> String Source # showList :: [Boundary' x a] -> ShowS Source #
type SubstArg Boundary Source # |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg Boundary = Term
type SubstArg TmBoundary Source # |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg TmBoundary = Term

type Boundary = Boundary' Int Term Source #

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

type TmBoundary = Boundary' Term Term Source #

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

tmBoundary :: Boundary' Int a -> Boundary' Term a Source #

Turn dimension variables `i` into dimension expressions ``var` i`.

varBoundary :: Boundary' Term a -> Boundary' Int a Source #

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

telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (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`.

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

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

telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (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

telViewPathBoundary :: PureTCM m => Type -> m (TelView, Boundary) Source #

teleElims :: DeBruijn a => Telescope -> Boundary' Int 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 :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type) Source #

Reduces `Type`.

pathViewAsPi' :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type) Source #

Reduces `Type`.

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

piOrPath :: HasBuiltins m => Type -> m (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 #

Assumes `Type` is in whnf.

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

isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type)) Source #

ifPath :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a Source #

ifPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a Source #

ifNotPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a Source #

ifPiOrPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a Source #

ifNotPiOrPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a Source #

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

telePatterns' :: DeBruijn a => (forall a1. DeBruijn a1 => Telescope -> [NamedArg a1]) -> 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.

ifPiB :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a Source #

ifPiTypeB :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a Source #

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, HasBuiltins tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a Source #

shouldBePath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type) Source #

shouldBePi :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type) Source #

shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type) Source #

class PiApplyM a where Source #

A safe variant of `piApply`.

Minimal complete definition

piApplyM'

Methods

piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type Source #

piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type Source #

#### Instances

Instances details

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

typeArity :: Type -> TCM Nat Source #

Compute type arity

foldrTelescopeM :: MonadAddContext m => (Dom (ArgName, Type) -> m b -> m b) -> m b -> Telescope -> m b Source #

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