Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




type Candidate = (Term, Type) Source

A candidate solution for an instance meta is a term with its type.

initialIFSCandidates :: Type -> TCM (Maybe Candidates) Source

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 Source

initializeIFSMeta s t generates an instance meta of type t with suggested name s.

findInScope :: MetaId -> Maybe Candidates -> TCM () Source

findInScope m (v,a)s tries to instantiate on of the types as of the candidate terms vs 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) Source

Result says whether we need to add constraint, and if so, the set of remaining candidates.

rigidlyConstrainedMetas :: TCM [MetaId] Source

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 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.