Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.MetaVars
Synopsis
findIdx :: Eq a => [a] -> a -> Maybe Int
isBlockedTerm :: MonadTCM tcm => MetaId -> tcm Bool
isEtaExpandable :: MonadTCM tcm => MetaId -> tcm Bool
class HasMeta t where
metaInstance :: MonadTCM tcm => t -> tcm MetaInstantiation
metaVariable :: MetaId -> Args -> t
(=:=) :: MonadTCM tcm => MetaId -> Term -> tcm ()
(=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()
assignTerm :: MonadTCM tcm => MetaId -> Term -> tcm ()
assignSort :: MonadTCM tcm => MetaId -> Sort -> tcm ()
newSortMeta :: MonadTCM tcm => tcm Sort
newSortMetaCtx :: MonadTCM tcm => Args -> tcm Sort
newTypeMeta :: MonadTCM tcm => Sort -> tcm Type
newTypeMeta_ :: MonadTCM tcm => tcm Type
newValueMeta :: MonadTCM tcm => Type -> tcm Term
newValueMetaCtx :: MonadTCM tcm => Type -> Args -> tcm Term
newValueMeta' :: MonadTCM tcm => Type -> tcm Term
newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm Term
newTelMeta :: MonadTCM tcm => Telescope -> tcm Args
newArgsMeta :: MonadTCM tcm => Type -> tcm Args
newArgsMetaCtx :: MonadTCM tcm => Type -> Telescope -> Args -> tcm Args
newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm Term
newRecordMetaCtx :: MonadTCM tcm => QName -> Args -> Telescope -> Args -> tcm Term
newQuestionMark :: MonadTCM tcm => Type -> tcm Term
blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm Term
unblockedTester :: MonadTCM tcm => Type -> tcm Bool
postponeTypeCheckingProblem_ :: MonadTCM tcm => Expr -> Type -> tcm Term
postponeTypeCheckingProblem :: MonadTCM tcm => Expr -> Type -> TCM Bool -> tcm Term
etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()
etaExpandMetaSafe :: MonadTCM tcm => MetaId -> tcm ()
data MetaKind
= Records
| SingletonRecords
| Levels
allMetaKinds :: [MetaKind]
etaExpandMeta :: MonadTCM tcm => [MetaKind] -> MetaId -> tcm ()
etaExpandBlocked :: (MonadTCM tcm, Reduce t) => Blocked t -> tcm (Blocked t)
abortAssign :: MonadTCM tcm => tcm a
handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm a
assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm Constraints
assignS :: MonadTCM tcm => MetaId -> Args -> Sort -> tcm Constraints
type FVs = Set Nat
checkArgs :: MonadTCM tcm => MetaId -> Args -> FVs -> tcm [Arg Nat]
validParameters :: Monad m => Args -> FVs -> m [Arg Nat]
isVar :: Arg Term -> Bool
updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm ()
Documentation
findIdx :: Eq a => [a] -> a -> Maybe IntSource

Find position of a value in a list. Used to change metavar argument indices during assignment.

reverse is necessary because we are directly abstracting over the list.

isBlockedTerm :: MonadTCM tcm => MetaId -> tcm BoolSource
Check whether a meta variable is a place holder for a blocked term.
isEtaExpandable :: MonadTCM tcm => MetaId -> tcm BoolSource
class HasMeta t whereSource
Methods
metaInstance :: MonadTCM tcm => t -> tcm MetaInstantiationSource
metaVariable :: MetaId -> Args -> tSource
(=:=) :: MonadTCM tcm => MetaId -> Term -> tcm ()Source
(=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()Source
The instantiation should not be an InstV or InstS and the MetaId should point to something Open or a BlockedConst.
assignTerm :: MonadTCM tcm => MetaId -> Term -> tcm ()Source
assignSort :: MonadTCM tcm => MetaId -> Sort -> tcm ()Source
newSortMeta :: MonadTCM tcm => tcm SortSource
newSortMetaCtx :: MonadTCM tcm => Args -> tcm SortSource
newTypeMeta :: MonadTCM tcm => Sort -> tcm TypeSource
newTypeMeta_ :: MonadTCM tcm => tcm TypeSource
newValueMeta :: MonadTCM tcm => Type -> tcm TermSource
Create a new metavariable, possibly -expanding in the process.
newValueMetaCtx :: MonadTCM tcm => Type -> Args -> tcm TermSource
newValueMeta' :: MonadTCM tcm => Type -> tcm TermSource
Create a new value meta without -expanding.
newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm TermSource
Create a new value meta with specific dependencies.
newTelMeta :: MonadTCM tcm => Telescope -> tcm ArgsSource
newArgsMeta :: MonadTCM tcm => Type -> tcm ArgsSource
newArgsMetaCtx :: MonadTCM tcm => Type -> Telescope -> Args -> tcm ArgsSource
newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm TermSource
Create a metavariable of record type. This is actually one metavariable for each field.
newRecordMetaCtx :: MonadTCM tcm => QName -> Args -> Telescope -> Args -> tcm TermSource
newQuestionMark :: MonadTCM tcm => Type -> tcm TermSource
blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm TermSource
Construct a blocked constant if there are constraints.
unblockedTester :: MonadTCM tcm => Type -> tcm BoolSource
Auxiliary function to create a postponed type checking problem.
postponeTypeCheckingProblem_ :: MonadTCM tcm => Expr -> Type -> tcm TermSource
postponeTypeCheckingProblem :: MonadTCM tcm => Expr -> Type -> TCM Bool -> tcm TermSource
etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()Source
Eta expand metavariables listening on the current meta.
etaExpandMetaSafe :: MonadTCM tcm => MetaId -> tcm ()Source
Do safe eta-expansions for meta (SingletonRecords,Levels).
data MetaKind Source
Various kinds of metavariables.
Constructors
RecordsMeta variables of record type.
SingletonRecordsMeta variables of "hereditarily singleton" record type.
LevelsMeta variables of level type, if type-in-type is activated.
allMetaKinds :: [MetaKind]Source
All possible metavariable kinds.
etaExpandMeta :: MonadTCM tcm => [MetaKind] -> MetaId -> tcm ()Source
Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.
etaExpandBlocked :: (MonadTCM tcm, Reduce t) => Blocked t -> tcm (Blocked t)Source
Eta expand blocking metavariables of record type, and reduce the blocked thing.
abortAssign :: MonadTCM tcm => tcm aSource
handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm aSource
assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm ConstraintsSource
Assign to an open metavar. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.
assignS :: MonadTCM tcm => MetaId -> Args -> Sort -> tcm ConstraintsSource
type FVs = Set NatSource
checkArgs :: MonadTCM tcm => MetaId -> Args -> FVs -> tcm [Arg Nat]Source

Check that arguments to a metavar are in pattern fragment. Assumes all arguments already in whnf. Parameters are represented as Vars so checkArgs really checks that all args are unique Vars and returns the list of corresponding indices for each arg-- done to not define equality on Term.

reverse is necessary because we are directly abstracting over this list ids.

validParameters :: Monad m => Args -> FVs -> m [Arg Nat]Source
Check that the parameters to a meta variable are distinct variables. Andreas, 2010-09-24: Allow non-linear variables that do not appear in FVs.
isVar :: Arg Term -> BoolSource
updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm ()Source
Produced by Haddock version 2.6.1