Safe Haskell | Safe-Infered |
---|
- data OccursCtx
- = Flex
- | Rigid
- | StronglyRigid
- | Irrel
- data UnfoldStrategy
- defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
- unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
- weakly :: OccursCtx -> OccursCtx
- strongly :: OccursCtx -> OccursCtx
- abort :: OccursCtx -> TypeError -> TCM ()
- type Vars = ([Nat], [Nat])
- goIrrelevant :: Vars -> Vars
- allowedVar :: Nat -> Vars -> Bool
- takeRelevant :: Vars -> [Nat]
- underAbs :: Vars -> Vars
- class Occurs t where
- occursCheck :: MetaId -> Vars -> Term -> TCM Term
- prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
- hasBadRigid :: [Nat] -> Term -> Bool
- data PruneResult
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()
Documentation
Flex | we are in arguments of a meta |
Rigid | we are not in arguments of a meta but a bound var |
StronglyRigid | we are at the start or in the arguments of a constructor |
Irrel | we are in an irrelevant argument |
defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtxSource
goIrrelevant :: Vars -> VarsSource
allowedVar :: Nat -> Vars -> BoolSource
takeRelevant :: Vars -> [Nat]Source
Extended occurs check.
occursCheck :: MetaId -> Vars -> Term -> TCM TermSource
When assigning m xs := v
, check that m
does not occur in v
and that the free variables of v
are contained in xs
.
Getting rid of flexible occurrences
prune :: MetaId -> Args -> [Nat] -> TCM PruneResultSource
prune m' vs xs
attempts to remove all arguments from vs
whose
free variables are not contained in xs
.
If successful, m'
is solved by the new, pruned meta variable and we
return True
else False
.
hasBadRigid :: [Nat] -> Term -> BoolSource
hasBadRigid xs v = True
iff one of the rigid variables in v
is not in xs
.
Actually we can only prune if a bad variable is in the head. See issue 458.
data PruneResult Source
NothingToPrune | the kill list is empty or only |
PrunedNothing | there is no possible kill (because of type dep.) |
PrunedSomething | managed to kill some args in the list |
PrunedEverything | all prescribed kills where performed |
killArgs :: [Bool] -> MetaId -> TCM PruneResultSource
killArgs [k1,...,kn] X
prunes argument i
from metavar X
if ki==True
.
Pruning is carried out whenever > 0 arguments can be pruned.
True
is only returned if all arguments could be pruned.
killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)Source
killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')
(ignoring Arg
). Let t' = (xs:as) -> b
.
Invariant: k'i == True
iff ki == True
and pruning the i
th argument from
type b
is possible without creating unbound variables.
t'
is type t
after pruning all k'i==True
.