Safe Haskell  None 

Language  Haskell2010 
Synopsis
 checkSizeLtSat :: Term > TCM ()
 checkSizeNeverZero :: Term > TCM Bool
 checkSizeVarNeverZero :: Int > TCM Bool
 isBounded :: (MonadReduce m, MonadTCEnv m, HasBuiltins m) => Nat > 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 :: Term > TCM DeepSizeView
 sizeMaxView :: (MonadReduce m, HasBuiltins 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 [Closure Constraint]
 getSizeConstraints :: (Comparison > Bool) > TCM [Closure Constraint]
 getSizeMetas :: Bool > TCM [(MetaId, Type, Telescope)]
 data OldSizeExpr
 data OldSizeConstraint = Leq OldSizeExpr Int OldSizeExpr
 oldComputeSizeConstraints :: [Closure Constraint] > TCM [OldSizeConstraint]
 oldComputeSizeConstraint :: Constraint > TCM (Maybe OldSizeConstraint)
 oldSizeExpr :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins 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 nonempty.
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 :: (MonadReduce m, MonadTCEnv m, HasBuiltins 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.
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.
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 :: Term > TCM DeepSizeView Source #
Compute the deep size view of a term. Precondition: sized types are enabled.
sizeMaxView :: (MonadReduce m, HasBuiltins 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 #
:: (Type > Bool)  Test for being a sized type 
> (Comparison > Bool)  Restriction to these directions. 
> Closure Constraint  
> Bool 
takeSizeConstraints :: (Comparison > Bool) > TCM [Closure Constraint] Source #
Take out all size constraints of the given direction (DANGER!).
getSizeConstraints :: (Comparison > Bool) > TCM [Closure Constraint] 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.
Instances
Eq OldSizeExpr Source #  
Defined in Agda.TypeChecking.SizedTypes (==) :: OldSizeExpr > OldSizeExpr > Bool # (/=) :: OldSizeExpr > OldSizeExpr > Bool #  
Show OldSizeExpr Source #  
Defined in Agda.TypeChecking.SizedTypes showsPrec :: Int > OldSizeExpr > ShowS # show :: OldSizeExpr > String # showList :: [OldSizeExpr] > ShowS #  
Pretty OldSizeExpr Source #  
Defined in Agda.TypeChecking.SizedTypes pretty :: OldSizeExpr > Doc Source # prettyPrec :: Int > OldSizeExpr > Doc Source # prettyList :: [OldSizeExpr] > Doc Source # 
data OldSizeConstraint Source #
Size constraints we can solve.
Leq OldSizeExpr Int OldSizeExpr 

Instances
Show OldSizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes showsPrec :: Int > OldSizeConstraint > ShowS # show :: OldSizeConstraint > String # showList :: [OldSizeConstraint] > ShowS #  
Pretty OldSizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes pretty :: OldSizeConstraint > Doc Source # prettyPrec :: Int > OldSizeConstraint > Doc Source # prettyList :: [OldSizeConstraint] > Doc Source # 
oldComputeSizeConstraints :: [Closure Constraint] > 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 :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins 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,..,n1
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
:: [(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
.