Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.TypeChecking.InstanceArguments
- type Candidate = (Term, Type)
- type Candidates = [Candidate]
- initialIFSCandidates :: Type -> TCM (Maybe Candidates)
- initializeIFSMeta :: String -> Type -> TCM Term
- findInScope :: MetaId -> Maybe Candidates -> TCM ()
- findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
- rigidlyConstrainedMetas :: TCM [MetaId]
- checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates
- applyDroppingParameters :: Term -> Args -> TCM Term
Documentation
type Candidates = [Candidate]
initialIFSCandidates :: Type -> TCM (Maybe Candidates)
Compute a list of instance candidates.
Nothing
if type is a meta, error if type is not eligible
for instance search.
initializeIFSMeta :: String -> Type -> TCM Term
initializeIFSMeta s t
generates an instance meta of type t
with suggested name s
.
findInScope :: MetaId -> Maybe Candidates -> TCM ()
findInScope m (v,a)s
tries to instantiate on of the types a
s
of the candidate terms v
s to the type t
of the metavariable m
.
If successful, meta m
is solved with the instantiation of v
.
If unsuccessful, the constraint is regenerated, with possibly reduced
candidate set.
The list of candidates is equal to Nothing
when the type of the meta
wasn't known when the constraint was generated. In that case, try to find
its type again.
findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
Result says whether we need to add constraint, and if so, the set of remaining candidates.
rigidlyConstrainedMetas :: TCM [MetaId]
A meta _M is rigidly constrained if there is a constraint _M us == D vs, for inert D. Such metas can safely be instantiated by recursive instance search, since the constraint limits the solution space.
checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates
Given a meta m
of type t
and a list of candidates cands
,
checkCandidates m t cands
returns a refined list of valid candidates.
applyDroppingParameters :: Term -> Args -> TCM Term
To preserve the invariant that a constructor is not applied to its
parameter arguments, we explicitly check whether function term
we are applying to arguments is a unapplied constructor.
In this case we drop the first conPars
arguments.
See Issue670a.
Andreas, 2013-11-07 Also do this for projections, see Issue670b.