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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.MetaVars

Contents

- Performing the assignment
- Creating meta variables.
- Solve constraint `x vs = v`.

Synopsis

- findIdx :: Eq a => [a] -> a -> Maybe Int
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
- assignTerm :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- newSortMetaBelowInf :: TCM Sort
- newSortMeta :: TCM Sort
- newSortMetaCtx :: Args -> TCM Sort
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term)
- newInstanceMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM (MetaId, Term)
- newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term)
- newNamedValueMeta' :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term)
- newValueMeta :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term)
- newValueMetaCtx :: Frozen -> RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
- newValueMeta' :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term)
- newValueMetaCtx' :: Frozen -> RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
- newTelMeta :: Telescope -> TCM Args
- type Condition = Dom Type -> Abs Type -> Bool
- trueCondition :: Condition
- newArgsMeta :: Type -> TCM Args
- newArgsMeta' :: Condition -> Type -> TCM Args
- newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
- newArgsMetaCtx' :: Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args
- newRecordMeta :: QName -> Args -> TCM Term
- newRecordMetaCtx :: Frozen -> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
- newQuestionMark :: InteractionId -> Type -> TCM (MetaId, Term)
- newQuestionMark' :: (Type -> TCM (MetaId, Term)) -> InteractionId -> Type -> TCM (MetaId, Term)
- blockTerm :: Type -> TCM Term -> TCM Term
- blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
- blockTypeOnProblem :: Type -> ProblemId -> TCM Type
- unblockedTester :: Type -> TCM Bool
- postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
- postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term
- problemType :: TypeCheckingProblem -> Type
- etaExpandListeners :: MetaId -> TCM ()
- wakeupListener :: Listener -> TCM ()
- etaExpandMetaSafe :: MetaId -> TCM ()
- data MetaKind
  - = Records
  - | SingletonRecords
  - | Levels
- allMetaKinds :: [MetaKind]
- etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
- etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
- assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
- assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
- assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
- assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
- assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
- subtypingForSizeLt :: CompareDirection -> MetaId -> MetaVariable -> Type -> Args -> Term -> (Term -> TCM ()) -> TCM ()
- expandProjectedVars :: (Show a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, Subst Term b) => a -> b -> (a -> b -> TCM c) -> TCM c
- etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
- class NoProjectedVar a where
  - noProjectedVar :: a -> Either ProjVarExc ()
- data ProjVarExc = ProjVarExc Int [(ProjOrigin, QName)]
- class (TermLike a, Subst Term a, Reduce a) => ReduceAndEtaContract a where
  - reduceAndEtaContract :: a -> TCM a
- type FVs = VarSet
- type SubstCand = [(Int, Term)]
- checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
- type Res = [(Arg Nat, Term)]
- data InvertExcept
  - = CantInvert
  - | NeutralArg
  - | ProjectedVar Int [(ProjOrigin, QName)]
- inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
- openMetasToPostulates :: 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 :: MetaId -> TCM Bool Source #

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

isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool Source #

# Performing the assignment

assignTerm :: MetaId -> [Arg ArgName] -> Term -> TCM () Source #

Performing the meta variable assignment.

The instantiation should not be an `InstV` and the `MetaId` should point to something `Open` or a `BlockedConst`. Further, the meta variable may not be `Frozen`.

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source #

Skip frozen check. Used for eta expanding frozen metas.

# Creating meta variables.

newSortMetaBelowInf :: TCM Sort Source #

Create a sort meta that cannot be instantiated with `Inf` (Setω).

newSortMeta :: TCM Sort Source #

Create a sort meta that may be instantiated with `Inf` (Setω).

newSortMetaCtx :: Args -> TCM Sort Source #

Create a sort meta that may be instantiated with `Inf` (Setω).

newTypeMeta :: Sort -> TCM Type Source #

newTypeMeta_ :: TCM Type Source #

newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term) Source #

`newInstanceMeta s t cands` creates a new instance metavariable of type the output type of `t` with name suggestion `s`.

newInstanceMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM (MetaId, Term) Source #

newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term) Source #

Create a new value meta with specific dependencies, possibly η-expanding in the process.

newNamedValueMeta' :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM (MetaId, Term) Source #

Create a new value meta with specific dependencies without η-expanding.

newValueMeta :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term) Source #

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

newValueMetaCtx :: Frozen -> RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term) Source #

newValueMeta' :: RunMetaOccursCheck -> Type -> TCM (MetaId, Term) Source #

Create a new value meta without η-expanding.

newValueMetaCtx' :: Frozen -> RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term) Source #

Create a new value meta with specific dependencies.

newTelMeta :: Telescope -> TCM Args Source #

type Condition = Dom Type -> Abs Type -> Bool Source #

trueCondition :: Condition Source #

newArgsMeta :: Type -> TCM Args Source #

newArgsMeta' :: Condition -> Type -> TCM Args Source #

newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args Source #

newArgsMetaCtx' :: Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args Source #

newRecordMeta :: QName -> Args -> TCM Term Source #

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

newRecordMetaCtx Source #

Arguments

:: Frozen | Should the meta be created frozen?
-> QName | Name of record type
-> Args | Parameters of record type.
-> Telescope |
-> Permutation |
-> Args |
-> TCM Term |

newQuestionMark :: InteractionId -> Type -> TCM (MetaId, Term) Source #

newQuestionMark' :: (Type -> TCM (MetaId, Term)) -> InteractionId -> Type -> TCM (MetaId, Term) Source #

blockTerm :: Type -> TCM Term -> TCM Term Source #

Construct a blocked constant if there are constraints.

blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term Source #

blockTypeOnProblem :: Type -> ProblemId -> TCM Type Source #

unblockedTester :: Type -> TCM Bool Source #

`unblockedTester t` returns `False` if `t` is a meta or a blocked term.

Auxiliary function to create a postponed type checking problem.

postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term Source #

Create a postponed type checking problem `e : t` that waits for type `t` to unblock (become instantiated or its constraints resolved).

postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term Source #

Create a postponed type checking problem `e : t` that waits for conditon `unblock`. A new meta is created in the current context that has as instantiation the postponed type checking problem. An `UnBlock` constraint is added for this meta, which links to this meta.

problemType :: TypeCheckingProblem -> Type Source #

Type of the term that is produced by solving the `TypeCheckingProblem`.

etaExpandListeners :: MetaId -> TCM () Source #

Eta expand metavariables listening on the current meta.

wakeupListener :: Listener -> TCM () Source #

Wake up a meta listener and let it do its thing

etaExpandMetaSafe :: MetaId -> TCM () Source #

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

data MetaKind Source #

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 Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods minBound :: MetaKind Source # maxBound :: MetaKind Source #
Enum MetaKind Source # |

Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

succ :: MetaKind -> MetaKind Source #

pred :: MetaKind -> MetaKind Source #

toEnum :: Int -> MetaKind Source #

fromEnum :: MetaKind -> Int Source #

enumFrom :: MetaKind -> [MetaKind] Source #

enumFromThen :: MetaKind -> MetaKind -> [MetaKind] Source #

enumFromTo :: MetaKind -> MetaKind -> [MetaKind] Source #

enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind] Source #

Eq MetaKind Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods (==) :: MetaKind -> MetaKind -> Bool Source # (/=) :: MetaKind -> MetaKind -> Bool Source #
Show MetaKind Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods showsPrec :: Int -> MetaKind -> ShowS Source # show :: MetaKind -> String Source # showList :: [MetaKind] -> ShowS Source #

allMetaKinds :: [MetaKind] Source #

All possible metavariable kinds.

etaExpandMeta :: [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 :: Reduce t => Blocked t -> TCM (Blocked t) Source #

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

# Solve constraint `x vs = v`.

assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM () Source #

Assign to an open metavar which may not be frozen. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

Assignment is aborted by throwing a `PatternErr` via a call to `patternViolation`. This error is caught by `catchConstraint` during equality checking (`compareAtom`) and leads to restoration of the original constraints.

assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM () Source #

assign :: CompareDirection -> MetaId -> Args -> Term -> TCM () Source #

Miller pattern unification:

`assign x vs v` solves problem `x vs = v` for meta `x` if `vs` are distinct variables (linearity check) and `v` depends only on these variables and does not contain `x` itself (occurs check).

This is the basic story, but we have added some features:

1. Pruning.
2. Benign cases of non-linearity.
3. `vs` may contain record patterns.

For a reference to some of these extensions, read Andreas Abel and Brigitte Pientka's TLCA 2011 paper.

assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM () Source #

`assignMeta m x t ids u` solves `x ids = u` for meta `x` of type `t`, where term `u` lives in a context of length `m`. Precondition: `ids` is linear.

assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM () Source #

`assignMeta' m x t ids u` solves `x = [ids]u` for meta `x` of type `t`, where term `u` lives in a context of length `m`, and `ids` is a partial substitution.

subtypingForSizeLt Source #

Arguments

:: CompareDirection

    dir

-> MetaId | The meta variable `x`.
-> MetaVariable | Its associated information `mvar <- lookupMeta x`.
-> Type | Its type `t = jMetaType $ mvJudgement mvar`
-> Args | Its arguments.
-> Term | Its to-be-assigned value `v`, such that `x args `dir` v`.
-> (Term -> TCM ()) | Continuation taking its possibly assigned value.
-> TCM () |

Turn the assignment problem `_X args <= SizeLt u` into `_X args = SizeLt (_Y args)` and constraint `_Y args <= u`.

expandProjectedVars Source #

Arguments

:: (Show a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, Subst Term b) |
=> a | Meta variable arguments.
-> b | Right hand side.
-> (a -> b -> TCM c) |
-> TCM c |

Eta-expand bound variables like `z` in `X (fst z)`.

etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c Source #

Eta-expand a de Bruijn index of record type in context and passed term(s).

class NoProjectedVar a where Source #

Check whether one of the meta args is a projected var.

Methods

noProjectedVar :: a -> Either ProjVarExc () Source #

Instances

NoProjectedVar Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjVarExc () Source #
NoProjectedVar a => NoProjectedVar [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: [a] -> Either ProjVarExc () Source #
NoProjectedVar a => NoProjectedVar (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Arg a -> Either ProjVarExc () Source #

data ProjVarExc Source #

Constructors

ProjVarExc Int [(ProjOrigin, QName)] |

class (TermLike a, Subst Term a, Reduce a) => ReduceAndEtaContract a where Source #

Normalize just far enough to be able to eta-contract maximally.

Minimal complete definition

Nothing

Methods

reduceAndEtaContract :: a -> TCM a Source #

reduceAndEtaContract :: (Traversable f, TermLike b, Subst Term b, Reduce b, ReduceAndEtaContract b, f b ~ a) => a -> TCM a Source #

Instances

ReduceAndEtaContract Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term Source #
ReduceAndEtaContract a => ReduceAndEtaContract [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: [a] -> TCM [a] Source #
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Arg a -> TCM (Arg a) Source #

type FVs = VarSet Source #

type SubstCand Source #

Arguments

= [(Int, Term)] | a possibly non-deterministic substitution

checkLinearity :: SubstCand -> ExceptT () TCM SubstCand Source #

Turn non-det substitution into proper substitution, if possible. Otherwise, raise the error.

type Res = [(Arg Nat, Term)] Source #

data InvertExcept Source #

Exceptions raised when substitution cannot be inverted.

Constructors

CantInvert | Cannot recover.
NeutralArg | A potentially neutral arg: can't invert, but can try pruning.
ProjectedVar Int [(ProjOrigin, QName)] | Try to eta-expand var to remove projs.

inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand Source #

Check that arguments `args` to a metavar are in pattern fragment. Assumes all arguments already in whnf and eta-reduced. Parameters are represented as `Var`s so `checkArgs` really checks that all args are `Var`s and returns the "substitution" to be applied to the rhs of the equation to solve. (If `args` is considered a substitution, its inverse is returned.)

The returned list might not be ordered. Linearity, i.e., whether the substitution is deterministic, has to be checked separately.

openMetasToPostulates :: TCM () Source #

Turn open metas into postulates.

Preconditions:

1. We are `inTopContext`.
2. `envCurrentModule` is set to the top-level module.