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.
This involves migrating from de Bruijn indices to de Bruijn levels.
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 level 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.
 Doublecheck whether the constraints are solved.
 solveSizeConstraints :: 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
solveSizeConstraints :: 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 0,1,..,n1
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.
data NamedRigid Source
Identifiers for rigid variables.
NamedRigid  

Eq NamedRigid Source  
Ord NamedRigid Source  
Show NamedRigid Source  
Subst SizeConstraint Source  
PrettyTCM SizeConstraint Source  Assumes we are in the right context. 
Plus NamedRigid Int NamedRigid Source  
Subst (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. 
Subst SizeConstraint Source  
Subst SizeMeta Source  
PrettyTCM SizeConstraint Source  Assumes we are in the right context. 
PrettyTCM SizeMeta Source  
Flexs SizeMeta HypSizeConstraint Source  
Subst (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.
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.