Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Solving size constraints under hypotheses.

The size solver proceeds as follows:

  1. 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.

  1. 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.

  1. 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.

  1. Convert the constraints into a constraint graph.

Here we need to convert MetaVs into flexible variables.

  1. Run the solver
  2. Convert the solution into meta instantiations.
  3. Double-check whether the constraints are solved.



solveSizeConstraints :: TCM () Source

Solve size constraints involving hypotheses.

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,..,n-1 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.




rigidName :: String

Name for printing in debug messages.

rigidIndex :: Int

De Bruijn index.

data SizeMeta Source

Size metas in size expressions.




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 raise.

type DBSizeExpr = SizeExpr' NamedRigid SizeMeta Source

Size expression 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.