Agda.TypeChecking.SizedTypes

SIZELT stuff

isBounded :: MonadTCM tcm => Nat -> tcm BoundedSize

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

boundedSizeMetaHook :: Term -> Telescope -> Type -> TCM ()

Whenever we create a bounded size meta, add a constraint expressing the bound. In boundedSizeMetaHook v tel a, tel includes the current context.

trySizeUniv :: Comparison -> Type -> Term -> Term -> QName -> Elims -> QName -> Elims -> TCM ()

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.

Size views that reduce.

deepSizeView :: Term -> TCM DeepSizeView

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

sizeMaxView :: Term -> TCM SizeMaxView

Size comparison that might add constraints.

compareSizes :: Comparison -> Term -> Term -> TCM ()

Compare two sizes.

compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()

Compare two sizes in max view.

compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()

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

compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()

trivial :: Term -> Term -> TCM Bool

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

Size constraints.

isSizeProblem :: ProblemId -> TCM Bool

Test whether a problem consists only of size constraints.

isSizeConstraint :: Closure Constraint -> TCM Bool

Test is a constraint speaks about sizes.

getSizeConstraints :: TCM [Closure Constraint]

Find the size constraints.

getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]

Return a list of size metas and their context.

Size constraint solving.

data SizeExpr

Atomic size expressions.

Constructors

SizeMeta MetaId [Int]

A size meta applied to de Bruijn levels.

Rigid Int

A de Bruijn level.

Instances

Eq SizeExpr

Show SizeExpr

data SizeConstraint

Size constraints we can solve.

Constructors

Leq SizeExpr Int SizeExpr

Leq a +n b represents a =< b + n. Leq a -n b represents a + n =< b.

Instances

Show SizeConstraint

computeSizeConstraints :: [Closure Constraint] -> TCM [SizeConstraint]

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

computeSizeConstraint :: Constraint -> TCM (Maybe SizeConstraint)

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

sizeExpr :: Term -> TCM (SizeExpr, Int)

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

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

flexibleVariables :: SizeConstraint -> [(MetaId, [Int])]

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

canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint

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

X[σ] <= t beomes 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.

solveSizeConstraints :: TCM ()

Main function.

oldSolver

Arguments

:: [(MetaId, Int)]

Size metas and their arity.

-> [SizeConstraint]

Size constraints (in preprocessed form).

-> TCM Bool

Returns False if solver fails.

Old solver for size constraints using Agda.Utils.Warshall.