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 : tm = 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.