Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.SizedTypes.Solve

Description

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 `MetaV`s into flexible variables.

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

Synopsis

- type CC = ProblemConstraint
- data DefaultToInfty
  - = DefaultToInfty
  - | DontDefaultToInfty
- solveSizeConstraints :: DefaultToInfty -> TCM ()
- castConstraintToCurrentContext' :: Closure Constraint -> MaybeT TCM Constraint
- castConstraintToCurrentContext :: ProblemConstraint -> MaybeT TCM ProblemConstraint
- solveSizeConstraints_ :: DefaultToInfty -> [CC] -> TCM (Set MetaId)
- solveCluster :: DefaultToInfty -> List1 (CC, HypSizeConstraint) -> TCM ()
- getSizeHypotheses :: Context -> TCM [(Nat, 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 {
  - sizeContext :: Context
  - sizeHypIds :: [Nat]
  - sizeHypotheses :: [SizeConstraint]
  - sizeConstraint :: SizeConstraint
  }
- computeSizeConstraint :: ProblemConstraint -> TCM (Maybe HypSizeConstraint)
- sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
- unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term

# Documentation

type CC = ProblemConstraint Source #

data DefaultToInfty Source #

Flag to control the behavior of size solver.

Constructors

DefaultToInfty | Instantiate all unconstrained size variables to ∞.
DontDefaultToInfty | Leave unconstrained size variables unsolved.

#### Instances

Instances details

Show DefaultToInfty Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods showsPrec :: Int -> DefaultToInfty -> ShowS Source # show :: DefaultToInfty -> String Source # showList :: [DefaultToInfty] -> ShowS Source #
Eq DefaultToInfty Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods (==) :: DefaultToInfty -> DefaultToInfty -> Bool Source # (/=) :: DefaultToInfty -> DefaultToInfty -> Bool Source #
Ord DefaultToInfty Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

compare :: DefaultToInfty -> DefaultToInfty -> Ordering Source #

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

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

(>) :: DefaultToInfty -> DefaultToInfty -> Bool Source #

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

max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty Source #

min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty Source #

solveSizeConstraints :: DefaultToInfty -> TCM () Source #

Solve size constraints involving hypotheses.

castConstraintToCurrentContext' :: Closure Constraint -> MaybeT TCM Constraint Source #

TODO: this does not actually work!

We would like to use a constraint `c` created in context `Δ` from module `N` in the current context `Γ` and current module `M`.

`Δ` is module tel `Δ₁` of `N` extended by some local bindings `Δ₂`. `Γ` is the current context. The module parameter substitution from current `M` to `N` be `Γ ⊢ σ : Δ₁`.

If `M == N`, we do not need the parameter substitution. We try raising.

We first strengthen `Δ ⊢ c` to live in `Δ₁` and obtain `c₁ = strengthen Δ₂ c`. We then transport `c₁` to `Γ` and obtain `c₂ = applySubst σ c₁`.

This works for different modules, but if `M == N` we should not strengthen and then weaken, because strengthening is a partial operation. We should rather lift the substitution `σ` by `Δ₂` and then raise by `Γ₂ - Δ₂`. This "raising" might be a strengthening if `Γ₂` is shorter than `Δ₂`.

(TODO: If the module substitution does not exist, because `N` is not a parent of `M`, we cannot use the constraint, as it has been created in an unrelated context.)

castConstraintToCurrentContext :: ProblemConstraint -> MaybeT TCM ProblemConstraint Source #

A hazardous hack, may the Gods have mercy on us.

To cast to the current context, we match the context of the given constraint by `CtxId`, and as fallback, by variable name (douh!).

This hack lets issue 2046 go through.

solveSizeConstraints_ :: DefaultToInfty -> [CC] -> TCM (Set MetaId) Source #

Return the size metas occurring in the simplified constraints. A constraint like `↑ _j =< ∞ : Size` simplifies to nothing, so `_j` would not be in this set.

solveCluster :: DefaultToInfty -> List1 (CC, HypSizeConstraint) -> TCM () Source #

Solve a cluster of constraints sharing some metas.

getSizeHypotheses :: Context -> TCM [(Nat, 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.

Constructors

NamedRigid |

Fields

- rigidName :: String

  Name for printing in debug messages.

- rigidIndex :: Int

  De Bruijn index.

#### Instances

Instances details

PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
Subst SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg SizeConstraint Source # Methods applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #
Pretty NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods pretty :: NamedRigid -> Doc Source # prettyPrec :: Int -> NamedRigid -> Doc Source # prettyList :: [NamedRigid] -> Doc Source #
Show NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods showsPrec :: Int -> NamedRigid -> ShowS Source # show :: NamedRigid -> String Source # showList :: [NamedRigid] -> ShowS Source #
Eq NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods (==) :: NamedRigid -> NamedRigid -> Bool Source # (/=) :: NamedRigid -> NamedRigid -> Bool Source #
Ord NamedRigid Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

compare :: NamedRigid -> NamedRigid -> Ordering Source #

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

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

(>) :: NamedRigid -> NamedRigid -> Bool Source #

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

max :: NamedRigid -> NamedRigid -> NamedRigid Source #

min :: NamedRigid -> NamedRigid -> NamedRigid Source #

Plus NamedRigid Int NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods plus :: NamedRigid -> Int -> NamedRigid Source #
Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # Methods applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
type SubstArg SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term
type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

data SizeMeta Source #

Size metas in size expressions.

Constructors

SizeMeta |

Fields

- sizeMetaId :: MetaId
- sizeMetaArgs :: [Int]

  De Bruijn indices.

#### Instances

Instances details

PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
PrettyTCM SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #
Subst SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg SizeConstraint Source # Methods applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #
Subst SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg SizeMeta Source # Methods applySubst :: Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta Source #
Pretty SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods pretty :: SizeMeta -> Doc Source # prettyPrec :: Int -> SizeMeta -> Doc Source # prettyList :: [SizeMeta] -> Doc Source #
Show SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods showsPrec :: Int -> SizeMeta -> ShowS Source # show :: SizeMeta -> String Source # showList :: [SizeMeta] -> ShowS Source #
Eq SizeMeta Source # | An equality which ignores the meta arguments.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods (==) :: SizeMeta -> SizeMeta -> Bool Source # (/=) :: SizeMeta -> SizeMeta -> Bool Source #
Ord SizeMeta Source # | An order which ignores the meta arguments.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

compare :: SizeMeta -> SizeMeta -> Ordering Source #

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

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

(>) :: SizeMeta -> SizeMeta -> Bool Source #

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

max :: SizeMeta -> SizeMeta -> SizeMeta Source #

min :: SizeMeta -> SizeMeta -> SizeMeta Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # Methods applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
type SubstArg SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term
type SubstArg SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeMeta = Term
type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

type DBSizeExpr = SizeExpr' NamedRigid SizeMeta Source #

Size expression with de Bruijn indices.

type SizeConstraint = Constraint' NamedRigid SizeMeta Source #

data HypSizeConstraint Source #

Size constraint with de Bruijn indices.

Constructors

HypSizeConstraint |

Fields

- sizeContext :: Context
- sizeHypIds :: [Nat]

  DeBruijn indices

- sizeHypotheses :: [SizeConstraint]

  Living in `Context`.

- sizeConstraint :: SizeConstraint

  Living in `Context`.

#### Instances

Instances details

PrettyTCM HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #
Flexs HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type FlexOf HypSizeConstraint Source # Methods flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint) Source #
type FlexOf HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type FlexOf HypSizeConstraint = SizeMeta

computeSizeConstraint :: ProblemConstraint -> 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 :: HasBuiltins m => DBSizeExpr -> m Term Source #

Turn a de size expression into a term.