Safe Haskell | None |
---|
Agda.TypeChecking.SizedTypes
- builtinSizeHook :: String -> QName -> Term -> Type -> TCM ()
- deepSizeView :: Term -> TCM DeepSizeView
- sizeMaxView :: Term -> TCM SizeMaxView
- trySizeUniv :: Comparison -> Type -> Term -> Term -> QName -> [Elim] -> QName -> [Elim] -> TCM ()
- compareSizes :: Comparison -> Term -> Term -> TCM ()
- compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()
- compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
- compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
- isBounded :: Nat -> TCM BoundedSize
- trivial :: Term -> Term -> TCM Bool
- boundedSizeMetaHook :: Term -> Telescope -> Type -> TCM ()
- isSizeProblem :: ProblemId -> TCM Bool
- isSizeConstraint :: Closure Constraint -> TCM Bool
- getSizeConstraints :: TCM [Closure Constraint]
- getSizeMetas :: TCM [(MetaId, Int)]
- 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])]
- haveSizedTypes :: TCM Bool
- canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
- solveSizeConstraints :: TCM ()
Documentation
deepSizeView :: Term -> TCM DeepSizeView
Compute the deep size view of a term. Precondition: sized types are enabled.
sizeMaxView :: Term -> TCM SizeMaxView
trySizeUniv :: Comparison -> Type -> Term -> Term -> QName -> [Elim] -> QName -> [Elim] -> TCM ()
Account for subtyping Size< i =< Size
Preconditions:
m = x els1
, n = y els2
, m
and n
are not equal.
compareSizes :: Comparison -> Term -> Term -> TCM ()
Compare two sizes. Only with --sized-types.
compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()
compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
compareBelowMax u vs
checks u = max vs@. Precondition: @size vs = 2
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
isBounded :: Nat -> TCM BoundedSize
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.
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 :: TCM [(MetaId, Int)]
data SizeExpr
Atomic size expressions.
data SizeConstraint
Size constraints we can solve.
Constructors
Leq SizeExpr Int SizeExpr |
|
Instances
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.
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.