Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




deepSizeView :: Term -> TCM DeepSizeViewSource

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

trySizeUniv :: Comparison -> Type -> Term -> Term -> QName -> [Elim] -> QName -> [Elim] -> TCM ()Source

Account for subtyping Size< i =< Size Preconditions: m = x els1, n = y els2, m and n are not equal.

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

Compare two sizes. Only with --sized-types.

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

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

isSizeProblem :: ProblemId -> TCM BoolSource

Test whether a problem consists only of size constraints.

isSizeConstraint :: Closure Constraint -> TCM BoolSource

Test is a constraint speaks about sizes.

getSizeConstraints :: TCM [Closure Constraint]Source

Find the size constraints.

data SizeExpr Source

Atomic size expressions.


SizeMeta MetaId [Int]

A size meta applied to de Bruijn levels.

Rigid Int

A de Bruijn level.


data SizeConstraint Source

Size constraints we can solve.


Leq SizeExpr Int SizeExpr

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


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

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)Source

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

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

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])]Source

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

canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraintSource

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.