Safe Haskell | None |
---|---|

Language | Haskell98 |

- checkSizeLtSat :: Type -> TCM ()
- checkSizeNeverZero :: Term -> TCM Bool
- checkSizeVarNeverZero :: Int -> TCM Bool
- isBounded :: MonadTCM tcm => Nat -> tcm BoundedSize
- boundedSizeMetaHook :: Term -> Telescope -> Type -> TCM ()
- trySizeUniv :: Comparison -> Type -> Term -> Term -> QName -> Elims -> QName -> Elims -> TCM ()
- deepSizeView :: Term -> TCM DeepSizeView
- sizeMaxView :: Term -> TCM SizeMaxView
- compareSizes :: Comparison -> Term -> Term -> TCM ()
- compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()
- compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
- compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
- trivial :: Term -> Term -> TCM Bool
- isSizeProblem :: ProblemId -> TCM Bool
- isSizeConstraint :: Closure Constraint -> TCM Bool
- getSizeConstraints :: TCM [Closure Constraint]
- getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
- data SizeExpr
- data SizeConstraint = Leq SizeExpr Int SizeExpr
- computeSizeConstraints :: [Closure Constraint] -> TCM [SizeConstraint]
- computeSizeConstraint :: Constraint -> TCM (Maybe SizeConstraint)
- sizeExpr :: Term -> TCM (SizeExpr, Int)
- flexibleVariables :: SizeConstraint -> [(MetaId, [Int])]
- canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
- solveSizeConstraints :: TCM ()
- oldSolver :: [(MetaId, Int)] -> [SizeConstraint] -> TCM Bool

# SIZELT stuff

checkSizeLtSat :: Type -> TCM () Source

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

checkSizeNeverZero :: Term -> TCM Bool Source

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

if undecided

checkSizeVarNeverZero :: Int -> TCM Bool Source

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 :: MonadTCM tcm => Nat -> tcm BoundedSize Source

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

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

`trySizeUniv cmp t m n x els1 y els2`

is called as a last resort when conversion checking `m `

failed for definitions `cmp`

n : t`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 Source

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

sizeMaxView :: Term -> TCM SizeMaxView Source

# Size comparison that might add constraints.

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

Compare two sizes.

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

Compare two sizes in max view.

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

`compareBelowMax u vs`

checks `u <= max vs`

. Precondition: `size vs >= 2`

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

trivial :: Term -> Term -> TCM Bool Source

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

).

# Size constraints.

isSizeProblem :: ProblemId -> TCM Bool Source

Test whether a problem consists only of size constraints.

isSizeConstraint :: Closure Constraint -> TCM Bool Source

Test is a constraint speaks about sizes.

getSizeConstraints :: TCM [Closure Constraint] Source

Find the size constraints.

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

Return a list of size metas and their context.

# Size constraint solving.

Atomic size expressions.

data SizeConstraint Source

Size constraints we can solve.

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.

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

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

Main function.

:: [(MetaId, Int)] | Size metas and their arity. |

-> [SizeConstraint] | Size constraints (in preprocessed form). |

-> TCM Bool | Returns |

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