Safe Haskell | None |
---|---|
Language | Haskell98 |
Solving size constraints under hypotheses.
The size solver proceeds as follows:
- Get size constraints, cluster into connected components.
All size constraints that mention the same metas go into the same cluster. Each cluster can be solved by itself.
Constraints that do not fit our format are ignored. We check whether our computed solution fulfills them as well in the last step.
- Find a joint context for each cluster.
Each constraint comes with its own typing context, which
contains size hypotheses j : Size< i
. We need to find a
common super context in which all constraints of a cluster live,
and raise all constraints to this context.
There might not be a common super context. Then we are screwed, since our solver is not ready to deal with such a situation. We will blatantly refuse to solve this cluster and blame it on the user.
- Convert the joint context into a hypothesis graph.
This is straightforward. Each de Bruijn index becomes a
rigid variable, each typing assumption j : Size< i
becomes an
arc.
- Convert the constraints into a constraint graph.
Here we need to convert MetaV
s into flexible variables.
- Run the solver
- Convert the solution into meta instantiations.
- Double-check whether the constraints are solved.
- data DefaultToInfty
- solveSizeConstraints :: DefaultToInfty -> TCM ()
- solveSizeConstraints_ :: [Closure Constraint] -> TCM ()
- solveCluster :: [HypSizeConstraint] -> TCM ()
- getSizeHypotheses :: Context -> TCM [(CtxId, SizeConstraint)]
- canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
- data NamedRigid = NamedRigid {
- rigidName :: String
- rigidIndex :: Int
- data SizeMeta = SizeMeta {
- sizeMetaId :: MetaId
- sizeMetaArgs :: [Int]
- type DBSizeExpr = SizeExpr' NamedRigid SizeMeta
- type SizeConstraint = Constraint' NamedRigid SizeMeta
- data HypSizeConstraint = HypSizeConstraint {}
- computeSizeConstraint :: Closure Constraint -> TCM (Maybe HypSizeConstraint)
- sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
- unSizeExpr :: DBSizeExpr -> TCM Term
Documentation
data DefaultToInfty Source
Flag to control the behavior of size solver.
DefaultToInfty | Instantiate all unconstrained size variables to ∞. |
DontDefaultToInfty | Leave unconstrained size variables unsolved. |
solveSizeConstraints :: DefaultToInfty -> TCM () Source
Solve size constraints involving hypotheses.
solveSizeConstraints_ :: [Closure Constraint] -> TCM () Source
solveCluster :: [HypSizeConstraint] -> TCM () Source
getSizeHypotheses :: Context -> TCM [(CtxId, SizeConstraint)] Source
Collect constraints from a typing context, looking for SIZELT hypotheses.
canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint Source
Convert size constraint into form where each meta is applied
to indices n-1,...,1,0
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.
Cf. SizedTypes.oldCanonicalizeSizeConstraint
.
Fixes (the rather artificial) issue 300. But it is unsound when pruned metas occur and triggers issue 1914. Thus we deactivate it. This needs to be properly implemented, possibly using the metaPermuatation of each meta variable.
data NamedRigid Source
Identifiers for rigid variables.
NamedRigid | |
|
Eq NamedRigid Source | |
Ord NamedRigid Source | |
Show NamedRigid Source | |
PrettyTCM SizeConstraint Source | Assumes we are in the right context. |
Subst Term SizeConstraint Source | |
Plus NamedRigid Int NamedRigid Source | |
Subst Term (SizeExpr' NamedRigid SizeMeta) Source | Only for |
Size metas in size expressions.
SizeMeta | |
|
Eq SizeMeta Source | An equality which ignores the meta arguments. |
Ord SizeMeta Source | An order which ignores the meta arguments. |
Show SizeMeta Source | |
PrettyTCM SizeConstraint Source | Assumes we are in the right context. |
PrettyTCM SizeMeta Source | |
Flexs SizeMeta HypSizeConstraint Source | |
Subst Term SizeConstraint Source | |
Subst Term SizeMeta Source | |
Subst Term (SizeExpr' NamedRigid SizeMeta) Source | Only for |
type DBSizeExpr = SizeExpr' NamedRigid SizeMeta Source
Size expression with de Bruijn indices.
data HypSizeConstraint Source
Size constraint with de Bruijn indices.
HypSizeConstraint | |
|
computeSizeConstraint :: Closure Constraint -> TCM (Maybe HypSizeConstraint) Source
Turn a constraint over de Bruijn indices into a size constraint.
sizeExpr :: Term -> TCM (Maybe DBSizeExpr) Source
Turn a term into a size expression.
Returns Nothing
if the term isn't a proper size expression.
unSizeExpr :: DBSizeExpr -> TCM Term Source
Turn a de size expression into a term.