Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.SizedTypes

Synopsis

- 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
  - = SizeMeta MetaId [Int]
  - | Rigid Int
- 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

builtinSizeHook :: String -> QName -> Term -> Type -> TCM ()

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

trivial :: Term -> Term -> TCM Bool

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.

Constructors

SizeMeta MetaId [Int] | A size meta applied to de Bruijn levels.
Rigid Int | A de Bruijn level.

Instances

Eq SizeExpr |
Show SizeExpr |

data SizeConstraint

Size constraints we can solve.

Constructors

Leq SizeExpr Int SizeExpr | `Leq a +n b` represents `a =< b + n`. `Leq a -n b` represents `a + n =< b`.

Instances

Show SizeConstraint |

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.

cf. `simplifyLevelConstraint`

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.

haveSizedTypes :: TCM Bool

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.

solveSizeConstraints :: TCM ()