Agda.TypeChecking.Conversion

Documentation

tryConversion :: TCM () -> TCM Bool

Try whether a computation runs without errors or new constraints (may create new metas, though). Restores state upon failure.

tryConversion' :: TCM a -> TCM (Maybe a)

Try whether a computation runs without errors or new constraints (may create new metas, though). Return Just the result upon success. Return Nothing and restore state upon failure.

sameVars :: Elims -> Elims -> Bool

Check if to lists of arguments are the same (and all variables). Precondition: the lists have the same length.

intersectVars :: Elims -> Elims -> Maybe [Bool]

intersectVars us vs checks whether all relevant elements in us and vs are variables, and if yes, returns a prune list which says True for arguments which are different and can be pruned.

equalTerm :: Type -> Term -> Term -> TCM ()

equalAtom :: Type -> Term -> Term -> TCM ()

equalType :: Type -> Type -> TCM ()

convError :: TypeError -> TCM ()

Ignore errors in irrelevant context.

compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()

Type directed equality on values.

assignE :: CompareDirection -> MetaId -> Elims -> Term -> (Term -> Term -> TCM ()) -> TCM ()

Try to assign meta. If meta is projected, try to eta-expand and run conversion check again.

compareTermDir :: CompareDirection -> Type -> Term -> Term -> TCM ()

compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()

compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()

compareTel t1 t2 cmp tel1 tel1 checks whether pointwise tel1 `cmp` tel2 and complains that t2 `cmp` t1 failed if not.

etaInequal :: Comparison -> Type -> Term -> Term -> TCM ()

Raise UnequalTerms if there is no hope that by meta solving and subsequent eta-contraction these terms could become equal. Precondition: the terms are in reduced form (with no top-level pointer) and failed to be equal in the compareAtom check.

By eta-contraction, a lambda or a record constructor term can become anything.

compareAtomDir :: CompareDirection -> Type -> Term -> Term -> TCM ()

computeElimHeadType :: QName -> Elims -> Elims -> TCM Type

Compute the head type of an elimination. For projection-like functions this requires inferring the type of the principal argument.

compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()

Syntax directed equality on atomic values

compareDom

Arguments

:: Free c

=> Comparison

cmp The comparison direction

-> Dom Type

a1 The smaller domain.

-> Dom Type

a2 The other domain.

-> Abs b

b1 The smaller codomain.

-> Abs c

b2 The bigger codomain.

-> TCM ()

Continuation if mismatch in Hiding.

-> TCM ()

Continuation if mismatch in Relevance.

-> TCM ()

Continuation if comparison is successful.

-> TCM ()

Check whether a1 cmp a2 and continue in context extended by a1.

compareRelevance :: Comparison -> Relevance -> Relevance -> Bool

antiUnify :: ProblemId -> Type -> Term -> Term -> TCM Term

When comparing argument spines (in compareElims) where the first arguments don't match, we keep going, substituting the anti-unification of the two terms in the telescope. More precisely:

@ (u = v : A)[pid] w = antiUnify pid A u v us = vs : Δ[w/x] ------------------------------------------------------------- u us = v vs : (x : A) Δ @

The simplest case of anti-unification is to return a fresh metavariable (created by blockTermOnProblem), but if there's shared structure between the two terms we can expose that.

This is really a crutch that lets us get away with things that otherwise would require heterogenous conversion checking. See for instance issue #2384.

antiUnifyType :: ProblemId -> Type -> Type -> TCM Type

antiUnifyElims :: ProblemId -> Type -> Term -> Elims -> Elims -> TCM Term

compareElims :: [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()

compareElims pols a v els1 els2 performs type-directed equality on eliminator spines. t is the type of the head v.

compareIrrelevant :: Type -> Term -> Term -> TCM ()

Compare two terms in irrelevant position. This always succeeds. However, we can dig for solutions of irrelevant metas in the terms we compare. (Certainly not the systematic solution, that'd be proof search...)

compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()

polFromCmp :: Comparison -> Polarity

compareArgs :: [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> TCM ()

Type-directed equality on argument lists

Types

compareType :: Comparison -> Type -> Type -> TCM ()

Equality on Types

leqType :: Type -> Type -> TCM ()

coerce :: Comparison -> Term -> Type -> Type -> TCM Term

coerce v a b coerces v : a to type b, returning a v' : b with maybe extra hidden applications or hidden abstractions.

In principle, this function can host coercive subtyping, but currently it only tries to fix problems with hidden function types.

Precondition: a and b are reduced.

coerceSize :: (Type -> Type -> TCM ()) -> Term -> Type -> Type -> TCM ()

Account for situations like k : (Size< j) <= (Size< k + 1)

Actually, the semantics is (Size<= k) ∩ (Size< j) ⊆ rhs which gives a disjunctive constraint. Mmmh, looks like stuff TODO.

For now, we do a cheap heuristics.

Precondition: types are reduced.

Sorts and levels

compareLevel :: Comparison -> Level -> Level -> TCM ()

compareSort :: Comparison -> Sort -> Sort -> TCM ()

leqSort :: Sort -> Sort -> TCM ()

Check that the first sort is less or equal to the second.

We can put SizeUniv below Inf, but otherwise, it is unrelated to the other universes.

leqLevel :: Level -> Level -> TCM ()

equalLevel :: Level -> Level -> TCM ()

equalLevel' :: Level -> Level -> TCM ()

Precondition: levels are normalised.

equalSort :: Sort -> Sort -> TCM ()

Check that the first sort equal to the second.

forallFaceMaps :: Term -> (Map Int Bool -> MetaId -> Term -> TCM a) -> (Substitution -> TCM a) -> TCM [a]

compareInterval :: Comparison -> Type -> Term -> Term -> TCM ()

type Conj = (Map Int (Set Bool), [Term])

isCanonical :: [Conj] -> Bool

leqInterval :: [Conj] -> [Conj] -> TCM Bool

leqInterval r q = r ≤ q in the I lattice. (∨ r_i) ≤ (∨ q_j) iff ∀ i. ∃ j. r_i ≤ q_j

leqConj :: Conj -> Conj -> TCM Bool

leqConj r q = r ≤ q in the I lattice, when r and q are conjuctions. ' (∧ r_i) ≤ (∧ q_j) iff ' (∧ r_i) ∧ (∧ q_j) = (∧ r_i) iff ' {r_i | i} ∪ {q_j | j} = {r_i | i} iff ' {q_j | j} ⊆ {r_i | i}

equalTermOnFace :: Term -> Type -> Term -> Term -> TCM ()

equalTermOnFace φ A u v = _ , φ ⊢ u = v : A

compareTermOnFace :: Comparison -> Term -> Type -> Term -> Term -> TCM ()

compareTermOnFace' :: (Comparison -> Type -> Term -> Term -> TCM ()) -> Comparison -> Term -> Type -> Term -> Term -> TCM ()

Definitions

bothAbsurd :: QName -> QName -> TCM Bool