Agda.TypeChecking.SizedTypes.Solve

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.

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

Documentation

data DefaultToInfty

Flag to control the behavior of size solver.

Constructors

DefaultToInfty

Instantiate all unconstrained size variables to ∞.

DontDefaultToInfty

Leave unconstrained size variables unsolved.

Instances

Eq DefaultToInfty

Methods

(==) :: DefaultToInfty -> DefaultToInfty -> Bool

(/=) :: DefaultToInfty -> DefaultToInfty -> Bool

Ord DefaultToInfty

Methods

compare :: DefaultToInfty -> DefaultToInfty -> Ordering

(<) :: DefaultToInfty -> DefaultToInfty -> Bool

(<=) :: DefaultToInfty -> DefaultToInfty -> Bool

(>) :: DefaultToInfty -> DefaultToInfty -> Bool

(>=) :: DefaultToInfty -> DefaultToInfty -> Bool

max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty

min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty

Show DefaultToInfty

Methods

showsPrec :: Int -> DefaultToInfty -> ShowS

show :: DefaultToInfty -> String

showList :: [DefaultToInfty] -> ShowS

solveSizeConstraints :: DefaultToInfty -> TCM ()

Solve size constraints involving hypotheses.

solveSizeConstraints_ :: [Closure Constraint] -> TCM ()

solveCluster :: [HypSizeConstraint] -> TCM ()

getSizeHypotheses :: Context -> TCM [(CtxId, SizeConstraint)]

Collect constraints from a typing context, looking for SIZELT hypotheses.

canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint

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

Identifiers for rigid variables.

Constructors

NamedRigid

Fields

• rigidName :: String

  Name for printing in debug messages.

• rigidIndex :: Int

  De Bruijn index.

Instances

Eq NamedRigid

Methods

(==) :: NamedRigid -> NamedRigid -> Bool

(/=) :: NamedRigid -> NamedRigid -> Bool

Ord NamedRigid

Methods

compare :: NamedRigid -> NamedRigid -> Ordering

(<) :: NamedRigid -> NamedRigid -> Bool

(<=) :: NamedRigid -> NamedRigid -> Bool

(>) :: NamedRigid -> NamedRigid -> Bool

(>=) :: NamedRigid -> NamedRigid -> Bool

max :: NamedRigid -> NamedRigid -> NamedRigid

min :: NamedRigid -> NamedRigid -> NamedRigid

Show NamedRigid

Methods

showsPrec :: Int -> NamedRigid -> ShowS

show :: NamedRigid -> String

showList :: [NamedRigid] -> ShowS

PrettyTCM SizeConstraint

Assumes we are in the right context.

Methods

prettyTCM :: SizeConstraint -> TCM Doc

Subst Term SizeConstraint

Methods

applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint

Plus NamedRigid Int NamedRigid

Methods

plus :: NamedRigid -> Int -> NamedRigid

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Methods

applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

data SizeMeta

Size metas in size expressions.

Constructors

SizeMeta

Fields

• sizeMetaId :: MetaId
• sizeMetaArgs :: [Int]

  De Bruijn indices.

Instances

Eq SizeMeta

An equality which ignores the meta arguments.

Methods

(==) :: SizeMeta -> SizeMeta -> Bool

(/=) :: SizeMeta -> SizeMeta -> Bool

Ord SizeMeta

An order which ignores the meta arguments.

Methods

compare :: SizeMeta -> SizeMeta -> Ordering

(<) :: SizeMeta -> SizeMeta -> Bool

(<=) :: SizeMeta -> SizeMeta -> Bool

(>) :: SizeMeta -> SizeMeta -> Bool

(>=) :: SizeMeta -> SizeMeta -> Bool

max :: SizeMeta -> SizeMeta -> SizeMeta

min :: SizeMeta -> SizeMeta -> SizeMeta

Show SizeMeta

Methods

showsPrec :: Int -> SizeMeta -> ShowS

show :: SizeMeta -> String

showList :: [SizeMeta] -> ShowS

PrettyTCM SizeConstraint

Assumes we are in the right context.

Methods

prettyTCM :: SizeConstraint -> TCM Doc

PrettyTCM SizeMeta

Methods

prettyTCM :: SizeMeta -> TCM Doc

Flexs SizeMeta HypSizeConstraint

Methods

flexs :: HypSizeConstraint -> Set SizeMeta

Subst Term SizeConstraint

Methods

applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint

Subst Term SizeMeta

Methods

applySubst :: Substitution' Term -> SizeMeta -> SizeMeta

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Methods

applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

type DBSizeExpr = SizeExpr' NamedRigid SizeMeta

Size expression with de Bruijn indices.

type SizeConstraint = Constraint' NamedRigid SizeMeta

data HypSizeConstraint

Size constraint with de Bruijn indices.

Constructors

HypSizeConstraint

Fields

• sizeContext :: Context
• sizeHypIds :: [CtxId]
• sizeHypotheses :: [SizeConstraint]

  Living in Context.

• sizeConstraint :: SizeConstraint

  Living in Context.

Instances

PrettyTCM HypSizeConstraint

Methods

prettyTCM :: HypSizeConstraint -> TCM Doc

Flexs SizeMeta HypSizeConstraint

Methods

flexs :: HypSizeConstraint -> Set SizeMeta

computeSizeConstraint :: Closure Constraint -> TCM (Maybe HypSizeConstraint)

Turn a constraint over de Bruijn indices into a size constraint.

sizeExpr :: Term -> TCM (Maybe DBSizeExpr)

Turn a term into a size expression.

Returns Nothing if the term isn't a proper size expression.

unSizeExpr :: DBSizeExpr -> TCM Term

Turn a de size expression into a term.