| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.SizedTypes
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
- 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
- oldSolveSizeConstraints :: TCM ()
- oldSolver :: [(MetaId, Int)] -> [OldSizeConstraint] -> TCM Bool
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
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 :: (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 #
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
| Eq OldSizeExpr Source # | |
Defined in Agda.TypeChecking.SizedTypes | |
| Show OldSizeExpr Source # | |
Defined in Agda.TypeChecking.SizedTypes Methods showsPrec :: Int -> OldSizeExpr -> ShowS # show :: OldSizeExpr -> String # showList :: [OldSizeExpr] -> ShowS # | |
| Pretty OldSizeExpr Source # | |
Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeExpr -> Doc Source # prettyPrec :: Int -> OldSizeExpr -> Doc Source # prettyList :: [OldSizeExpr] -> Doc Source # | |
data OldSizeConstraint Source #
Size constraints we can solve.
Constructors
| Leq OldSizeExpr Int OldSizeExpr |
|
Instances
| Show OldSizeConstraint Source # | |
Defined in Agda.TypeChecking.SizedTypes Methods showsPrec :: Int -> OldSizeConstraint -> ShowS # show :: OldSizeConstraint -> String # showList :: [OldSizeConstraint] -> ShowS # | |
| Pretty OldSizeConstraint Source # | |
Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeConstraint -> Doc Source # prettyPrec :: Int -> OldSizeConstraint -> Doc Source # prettyList :: [OldSizeConstraint] -> Doc 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.
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.
oldSolveSizeConstraints :: TCM () Source #
Main function.
Uses the old solver for size constraints using Agda.Utils.Warshall.
This solver does not smartly use size hypotheses j : Size< i.
It only checks that its computed solution is compatible
Arguments
| :: [(MetaId, Int)] | Size metas and their arity. |
| -> [OldSizeConstraint] | Size constraints (in preprocessed form). |
| -> TCM Bool | Returns |
Old solver for size constraints using Agda.Utils.Warshall.
This solver does not smartly use size hypotheses j : Size< i.