Agda.TypeChecking.MetaVars

Documentation

findIdx :: Eq a => [a] -> a -> Maybe Int

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

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

isEtaExpandable :: MonadTCM tcm => MetaId -> tcm Bool

class HasMeta t where

Methods

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

metaVariable :: MetaId -> Args -> t

Instances

HasMeta Sort

HasMeta Term

(=:=) :: MonadTCM tcm => MetaId -> Term -> tcm ()

(=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()

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

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

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

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

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

Create a new value meta without -expanding.

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

Create a new value meta with specific dependencies.

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

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

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

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

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

Construct a blocked constant if there are constraints.

unblockedTester :: MonadTCM tcm => Type -> tcm Bool

Auxiliary function to create a postponed type checking problem.

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

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

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

Eta expand metavariables listening on the current meta.

etaExpandMetaSafe :: MonadTCM tcm => MetaId -> tcm ()

Do safe eta-expansions for meta (SingletonRecords,Levels).

data MetaKind

Various kinds of metavariables.

Constructors

Records

Meta variables of record type.

SingletonRecords

Meta variables of "hereditarily singleton" record type.

Levels

Meta variables of level type, if type-in-type is activated.

Instances

Bounded MetaKind

Enum MetaKind

Eq MetaKind

allMetaKinds :: [MetaKind]

All possible metavariable kinds.

etaExpandMeta :: MonadTCM tcm => [MetaKind] -> MetaId -> tcm ()

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)

Eta expand blocking metavariables of record type, and reduce the blocked thing.

abortAssign :: MonadTCM tcm => tcm a

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

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

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

type FVs = Set Nat

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

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]

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

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