Safe Haskell  None 

Language  Haskell2010 
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.
 Doublecheck whether the constraints are solved.
Synopsis
 type CC = Closure Constraint
 data DefaultToInfty
 solveSizeConstraints :: DefaultToInfty > TCM ()
 castConstraintToCurrentContext' :: Closure Constraint > MaybeT TCM Constraint
 castConstraintToCurrentContext :: Closure Constraint > MaybeT TCM Constraint
 solveSizeConstraints_ :: DefaultToInfty > [CC] > TCM (Set MetaId)
 solveCluster :: DefaultToInfty > NonemptyList (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 {}
 computeSizeConstraint :: Closure Constraint > TCM (Maybe HypSizeConstraint)
 sizeExpr :: Term > TCM (Maybe DBSizeExpr)
 unSizeExpr :: DBSizeExpr > TCM Term
Documentation
type CC = Closure Constraint Source #
data DefaultToInfty Source #
Flag to control the behavior of size solver.
DefaultToInfty  Instantiate all unconstrained size variables to ∞. 
DontDefaultToInfty  Leave unconstrained size variables unsolved. 
Instances
Eq DefaultToInfty Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve (==) :: DefaultToInfty > DefaultToInfty > Bool # (/=) :: DefaultToInfty > DefaultToInfty > Bool #  
Ord DefaultToInfty Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve 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 Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve showsPrec :: Int > DefaultToInfty > ShowS # show :: DefaultToInfty > String # showList :: [DefaultToInfty] > ShowS # 
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 :: Closure Constraint > MaybeT TCM Constraint 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 > NonemptyList (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 n1,...,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  

Instances
Size metas in size expressions.
SizeMeta  

Instances
Eq SizeMeta Source #  An equality which ignores the meta arguments. 
Ord SizeMeta Source #  An order which ignores the meta arguments. 
Defined in Agda.TypeChecking.SizedTypes.Solve  
Show SizeMeta Source #  
Pretty SizeMeta Source #  
PrettyTCM SizeConstraint Source #  Assumes we are in the right context. 
Defined in Agda.TypeChecking.SizedTypes.Solve  
PrettyTCM SizeMeta Source #  
Flexs SizeMeta HypSizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve  
Subst Term SizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve  
Subst Term SizeMeta Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve applySubst :: Substitution' Term > SizeMeta > SizeMeta Source #  
Subst Term (SizeExpr' NamedRigid SizeMeta) Source #  Only for 
Defined in Agda.TypeChecking.SizedTypes.Solve 
type DBSizeExpr = SizeExpr' NamedRigid SizeMeta Source #
Size expression with de Bruijn indices.
data HypSizeConstraint Source #
Size constraint with de Bruijn indices.
HypSizeConstraint  

Instances
PrettyTCM HypSizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve  
Flexs SizeMeta HypSizeConstraint Source #  
Defined in Agda.TypeChecking.SizedTypes.Solve 
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.