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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.SizedTypes

Contents

- SIZELT stuff
- Size views that `reduce`.
- Size comparison that might add constraints.
- Size constraints.
- Size constraint solving.

Synopsis

- checkSizeLtSat :: Term -> TCM ()
- checkSizeNeverZero :: Term -> TCM Bool
- checkSizeVarNeverZero :: Int -> TCM Bool
- isBounded :: PureTCM m => Nat -> m BoundedSize
- isBoundedProjVar :: (MonadCheckInternal m, PureTCM m) => ProjectedVar -> m BoundedSize
- isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
- boundedSizeMetaHook :: (MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m, HasOptions m, HasBuiltins m) => Term -> Telescope -> Type -> m ()
- trySizeUniv :: MonadConversion m => Comparison -> CompareAs -> Term -> Term -> QName -> Elims -> QName -> Elims -> m ()
- deepSizeView :: (PureTCM m, MonadTCError m) => Term -> m DeepSizeView
- sizeMaxView :: PureTCM m => Term -> m SizeMaxView
- compareSizes :: MonadConversion m => Comparison -> Term -> Term -> m ()
- compareMaxViews :: MonadConversion m => Comparison -> SizeMaxView -> SizeMaxView -> m ()
- compareBelowMax :: MonadConversion m => DeepSizeView -> SizeMaxView -> m ()
- compareSizeViews :: MonadConversion m => Comparison -> DeepSizeView -> DeepSizeView -> m ()
- giveUp :: MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
- trivial :: MonadConversion m => Term -> Term -> m Bool
- isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
- isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool
- mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
- isSizeConstraint_ :: (Type -> Bool) -> (Comparison -> Bool) -> Closure Constraint -> Bool
- takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
- getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
- getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
- data OldSizeExpr
  - = SizeMeta MetaId [Int]
  - | Rigid Int
- data OldSizeConstraint = Leq OldSizeExpr Int OldSizeExpr
- oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
- oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
- oldSizeExpr :: (PureTCM m, MonadBlock m) => Term -> m (OldSizeExpr, Int)
- flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
- oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint

# SIZELT stuff

checkSizeLtSat :: Term -> 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 :: PureTCM m => Nat -> m BoundedSize Source #

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

isBoundedProjVar :: (MonadCheckInternal m, PureTCM m) => ProjectedVar -> m BoundedSize Source #

isBoundedSizeType :: PureTCM m => Type -> m BoundedSize Source #

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

Whenever we create a bounded size meta, add a constraint expressing the bound. First argument is the new meta and must be a `MetaV{}`. In `boundedSizeMetaHook v tel a`, `tel` includes the current context.

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

`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 :: (PureTCM m, MonadTCError m) => Term -> m DeepSizeView Source #

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

sizeMaxView :: PureTCM m => Term -> m SizeMaxView Source #

# Size comparison that might add constraints.

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

Compare two sizes.

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

Compare two sizes in max view.

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

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

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

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

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

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

# Size constraints.

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

Test whether a problem consists only of size constraints.

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

Test whether a constraint speaks about sizes.

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

isSizeConstraint_ Source #

Arguments

:: (Type -> Bool) | Test for being a sized type
-> (Comparison -> Bool) | Restriction to these directions.
-> Closure Constraint |
-> Bool |

takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint] Source #

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

getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint] Source #

Find the size constraints of the matching direction.

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

Return a list of size metas and their context.

# Size constraint solving.

data OldSizeExpr Source #

Atomic size expressions.

Constructors

SizeMeta MetaId [Int] | A size meta applied to de Bruijn indices.
Rigid Int | A de Bruijn index.

#### Instances

Instances details

Pretty OldSizeExpr Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeExpr -> Doc Source # prettyPrec :: Int -> OldSizeExpr -> Doc Source # prettyList :: [OldSizeExpr] -> Doc Source #
Show OldSizeExpr Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods showsPrec :: Int -> OldSizeExpr -> ShowS Source # show :: OldSizeExpr -> String Source # showList :: [OldSizeExpr] -> ShowS Source #
Eq OldSizeExpr Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods (==) :: OldSizeExpr -> OldSizeExpr -> Bool Source # (/=) :: OldSizeExpr -> OldSizeExpr -> Bool Source #

data OldSizeConstraint Source #

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

Instances details

Pretty OldSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeConstraint -> Doc Source # prettyPrec :: Int -> OldSizeConstraint -> Doc Source # prettyList :: [OldSizeConstraint] -> Doc Source #
Show OldSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods showsPrec :: Int -> OldSizeConstraint -> ShowS Source # show :: OldSizeConstraint -> String Source # showList :: [OldSizeConstraint] -> ShowS Source #

oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint] 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.

cf. `simplifyLevelConstraint`

oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint) Source #

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

oldSizeExpr :: (PureTCM m, MonadBlock m) => Term -> m (OldSizeExpr, Int) Source #

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])] Source #

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

oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint Source #

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.