Agda.TypeChecking.SizedTypes

SIZELT stuff

checkSizeLtSat :: Term -> TCM ()

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

checkSizeNeverZero :: Term -> TCM Bool

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

checkSizeVarNeverZero :: Int -> TCM Bool

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.

isBounded :: (MonadReduce m, MonadTCEnv m, HasBuiltins m) => Nat -> m BoundedSize

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

boundedSizeMetaHook :: (MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m, HasOptions m, HasBuiltins m) => Term -> Telescope -> Type -> m ()

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

trySizeUniv :: MonadConversion m => Comparison -> CompareAs -> Term -> Term -> QName -> Elims -> QName -> Elims -> m ()

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 :: (MonadReduce m, HasBuiltins m) => Term -> m SizeMaxView

Size comparison that might add constraints.

compareSizes :: MonadConversion m => Comparison -> Term -> Term -> m ()

Compare two sizes.

compareMaxViews :: MonadConversion m => Comparison -> SizeMaxView -> SizeMaxView -> m ()

Compare two sizes in max view.

compareBelowMax :: MonadConversion m => DeepSizeView -> SizeMaxView -> m ()

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

compareSizeViews :: MonadConversion m => Comparison -> DeepSizeView -> DeepSizeView -> m ()

giveUp :: MonadConversion m => Comparison -> Type -> Term -> Term -> m ()

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

trivial :: MonadConversion m => Term -> Term -> m Bool

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

Size constraints.

isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool

Test whether a problem consists only of size constraints.

isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool

Test whether a constraint speaks about sizes.

mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool

isSizeConstraint_

Arguments

:: (Type -> Bool)

Test for being a sized type

-> (Comparison -> Bool)

Restriction to these directions.

-> Closure Constraint

-> Bool

takeSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]

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

getSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]

Find the size constraints of the matching direction.

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

Return a list of size metas and their context.

Size constraint solving.

data OldSizeExpr

Atomic size expressions.

Constructors

SizeMeta MetaId [Int]

A size meta applied to de Bruijn indices.

Rigid Int

A de Bruijn index.

Instances

Eq OldSizeExpr

Defined in Agda.TypeChecking.SizedTypes

Methods

(==) :: OldSizeExpr -> OldSizeExpr -> Bool

(/=) :: OldSizeExpr -> OldSizeExpr -> Bool

Show OldSizeExpr

Defined in Agda.TypeChecking.SizedTypes

Methods

showsPrec :: Int -> OldSizeExpr -> ShowS

show :: OldSizeExpr -> String

showList :: [OldSizeExpr] -> ShowS

Pretty OldSizeExpr

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeExpr -> Doc

prettyPrec :: Int -> OldSizeExpr -> Doc

prettyList :: [OldSizeExpr] -> Doc

data OldSizeConstraint

Size constraints we can solve.

Constructors

Leq OldSizeExpr Int OldSizeExpr

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

Instances

Show OldSizeConstraint

Defined in Agda.TypeChecking.SizedTypes

Methods

showsPrec :: Int -> OldSizeConstraint -> ShowS

show :: OldSizeConstraint -> String

showList :: [OldSizeConstraint] -> ShowS

Pretty OldSizeConstraint

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeConstraint -> Doc

prettyPrec :: Int -> OldSizeConstraint -> Doc

prettyList :: [OldSizeConstraint] -> Doc

oldComputeSizeConstraints :: [Closure Constraint] -> TCM [OldSizeConstraint]

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

oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)

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

oldSizeExpr :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) => Term -> m (OldSizeExpr, Int)

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.

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

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

oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint

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.

oldSolveSizeConstraints :: TCM ()

Main function. Uses the old solver for size constraints using Agda.Utils.Warshall. This solver does not smartly use size hypotheses j : Size< i. It only checks that its computed solution is compatible

oldSolver

Arguments

:: [(MetaId, Int)]

Size metas and their arity.

-> [OldSizeConstraint]

Size constraints (in preprocessed form).

-> TCM Bool

Returns False if solver fails.

Old solver for size constraints using Agda.Utils.Warshall. This solver does not smartly use size hypotheses j : Size< i.