Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Telescope

Contents

Instance definitions

Synopsis

flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
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
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
type Boundary = Boundary' (Term, Term)
type Boundary' a = [(Term, a)]
telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
fullBoundary :: Telescope -> Boundary -> Boundary
telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP :: PureTCM m => Int -> Type -> m (TelView, Boundary)
telViewPathBoundaryP :: PureTCM m => Type -> m (TelView, Boundary)
teleElims :: DeBruijn a => Telescope -> Boundary' (a, 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
data OutputTypeName
- = OutputTypeName QName
- | OutputTypeVar
- | OutputTypeVisiblePi
- | OutputTypeNameNotYetKnown Blocker
- | NoOutputTypeName
getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance' :: Bool -> QName -> Type -> TCM ()
resolveUnknownInstanceDefs :: TCM ()
getInstanceDefs :: TCM InstanceTable

Documentation

flattenTel :: TermSubst 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 normalised.

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:_180, 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, _181 ] 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.

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

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

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

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

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.

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

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

Instance definitions

data OutputTypeName Source #

Constructors

OutputTypeName QName
OutputTypeVar
OutputTypeVisiblePi
OutputTypeNameNotYetKnown Blocker
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 Source #

Arguments

:: QName	Name of instance.
-> Type	Type of instance.
-> TCM ()

Register the definition with the given type as an instance. Issue warnings if instance is unusable.

addTypedInstance' Source #

Arguments

:: Bool	Should we print warnings for unusable instance declarations?
-> QName	Name of instance.
-> Type	Type of instance.
-> TCM ()

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.