Safe Haskell | None |
---|---|
Language | Haskell98 |
- type Candidates = [(Term, Type)]
- initialIFSCandidates :: TCM Candidates
- initializeIFSMeta :: String -> Type -> TCM Term
- findInScope :: MetaId -> Candidates -> TCM ()
- findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
- checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates
- applyDroppingParameters :: Term -> Args -> TCM Term
- solveIrrelevantMetas :: TCM ()
- solveMetaIfIrrelevant :: MetaId -> TCM ()
Documentation
type Candidates = [(Term, Type)] Source
A candidate solution for an instance meta is a term with its type.
initializeIFSMeta :: String -> Type -> TCM Term Source
initializeIFSMeta s t
generates an instance meta of type t
with suggested name s
.
findInScope :: MetaId -> Candidates -> TCM () Source
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.
findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates) Source
Result says whether we need to add constraint, and if so, the set of remaining candidates.
checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates Source
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 Source
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.
solveIrrelevantMetas :: TCM () Source
Attempt to solve irrelevant metas by instance search.
solveMetaIfIrrelevant :: MetaId -> TCM () Source