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

Agda.TypeChecking.MetaVars

Synopsis

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.

class HasMeta t where

Methods

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

metaVariable :: MetaId -> Args -> t

Instances

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

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

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

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

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.

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.

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.

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