| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.MetaVars

Synopsis

findIdx :: Eq a => [a] -> a -> Maybe Int
isBlockedTerm :: 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
postponeTypeCheckingProblem_ :: MonadTCM tcm => Expr -> Type -> tcm Term
postponeTypeCheckingProblem :: MonadTCM tcm => Expr -> Type -> TCM Bool -> tcm Term
etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()
etaExpandMeta :: MonadTCM tcm => MetaId -> tcm ()
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
checkArgs :: MonadTCM tcm => MetaId -> Args -> tcm [Arg Nat]
validParameters :: Monad m => Args -> 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 Int | Source

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 Bool | Source

Check whether a meta variable is a place holder for a blocked term.

class HasMeta t where | Source

Methods

metaInstance :: MonadTCM tcm => t -> tcm MetaInstantiation | Source

metaVariable :: MetaId -> Args -> t | Source

Instances

HasMeta Sort
HasMeta Term

(=:=) :: 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 Sort | Source

newSortMetaCtx :: MonadTCM tcm => Args -> tcm Sort | Source

newTypeMeta :: MonadTCM tcm => Sort -> tcm Type | Source

newTypeMeta_ :: MonadTCM tcm => tcm Type | Source

newValueMeta :: MonadTCM tcm => Type -> tcm Term | Source

Create a new metavariable, possibly -expanding in the process.

newValueMetaCtx :: MonadTCM tcm => Type -> Args -> tcm Term | Source

newValueMeta' :: MonadTCM tcm => Type -> tcm Term | Source

Create a new value meta without -expanding.

newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm Term | Source

Create a new value meta with specific dependencies.

newTelMeta :: MonadTCM tcm => Telescope -> tcm Args | Source

newArgsMeta :: MonadTCM tcm => Type -> tcm Args | Source

newArgsMetaCtx :: MonadTCM tcm => Type -> Telescope -> Args -> tcm Args | Source

newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm Term | Source

Create a metavariable of record type. This is actually one metavariable for each field.

newRecordMetaCtx :: MonadTCM tcm => QName -> Args -> Telescope -> Args -> tcm Term | Source

newQuestionMark :: MonadTCM tcm => Type -> tcm Term | Source

blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm Term | Source

Construct a blocked constant if there are constraints.

postponeTypeCheckingProblem_ :: MonadTCM tcm => Expr -> Type -> tcm Term | Source

postponeTypeCheckingProblem :: MonadTCM tcm => Expr -> Type -> TCM Bool -> tcm Term | Source

etaExpandListeners :: MonadTCM tcm => MetaId -> tcm () | Source

Eta expand metavariables listening on the current meta.

etaExpandMeta :: MonadTCM tcm => MetaId -> tcm () | Source

Eta expand a metavariable.

abortAssign :: MonadTCM tcm => tcm a | Source

handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm a | Source

assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm Constraints | Source

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 Constraints | Source

checkArgs :: MonadTCM tcm => MetaId -> Args -> tcm [Arg Nat] | Source

Check that arguments to a metavar are in pattern fragment. Assumes all arguments already in whnf. Parameters are represented as `Var`s so `checkArgs` really checks that all args are unique `Var`s 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 -> m [Arg Nat] | Source

Check that the parameters to a meta variable are distinct variables.

isVar :: Arg Term -> Bool | Source

updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm () | Source

Produced by Haddock version 2.4.2