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

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