Agda.TypeChecking.SizedTypes

Check whether a type is either not a SIZELT or a SIZELT that is non-empty.

Precondition: Term is reduced and not blocked. Throws a patternViolation if undecided

Checks that a size variable is ensured to be > 0. E.g. variable i cannot be zero in context (i : Size) (j : Size< ↑ ↑ i) (k : Size< j) (k' : Size< k). Throws a patternViolation if undecided.

Check whether a variable in the context is bounded by a size expression. If x : Size< a, then a is returned.

Whenever we create a bounded size meta, add a constraint expressing the bound. First argument is the new meta and must be a MetaV{}. In boundedSizeMetaHook v tel a, tel includes the current context.

trySizeUniv cmp t m n x els1 y els2 is called as a last resort when conversion checking m cmp n : t failed for definitions m = x els1 and n = y els2, where the heads x and y are not equal.

trySizeUniv accounts for subtyping between SIZELT and SIZE, like Size< i =< Size.

If it does not succeed it reports failure of conversion check.

Compute the deep size view of a term. Precondition: sized types are enabled.

Compare two sizes.

Compare two sizes in max view.

compareBelowMax u vs checks u <= max vs. Precondition: size vs >= 2

If envAssignMetas then postpone as constraint, otherwise, fail hard. Failing is required if we speculatively test several alternatives.

Checked whether a size constraint is trivial (like X <= X+1).

Test whether a problem consists only of size constraints.

Test whether a constraint speaks about sizes.

Take out all size constraints of the given direction (DANGER!).

Find the size constraints of the matching direction.

Return a list of size metas and their context.

Atomic size expressions.

Size constraints we can solve.

Compute a set of size constraints that all live in the same context from constraints over terms of type size that may live in different contexts.

cf. simplifyLevelConstraint

Turn a constraint over de Bruijn indices into a size constraint.

Turn a term with de Bruijn indices into a size expression with offset.

Throws a patternViolation if the term isn't a proper size expression.

Compute list of size metavariables with their arguments appearing in a constraint.

Convert size constraint into form where each meta is applied to indices 0,1,..,n-1 where n is the arity of that meta.

X[σ] <= t becomes X[id] <= t[σ^-1]

X[σ] ≤ Y[τ] becomes X[id] ≤ Y[τ[σ^-1]] or X[σ[τ^1]] ≤ Y[id] whichever is defined. If none is defined, we give up.