Safe Haskell | None |
---|---|
Language | Haskell98 |
- modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
- initOccursCheck :: MetaVariable -> TCM ()
- defNeedsChecking :: QName -> TCM Bool
- tallyDef :: QName -> TCM ()
- data OccursCtx
- = Flex
- | Rigid
- | StronglyRigid
- | Top
- | Irrel
- data UnfoldStrategy
- defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
- unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
- leaveTop :: OccursCtx -> OccursCtx
- weakly :: OccursCtx -> OccursCtx
- strongly :: OccursCtx -> OccursCtx
- patternViolation' :: Int -> String -> TCM a
- abort :: OccursCtx -> TypeError -> TCM a
- type Vars = ([Nat], [Nat])
- goIrrelevant :: Vars -> Vars
- allowedVar :: Nat -> Vars -> Bool
- takeRelevant :: Vars -> [Nat]
- liftUnderAbs :: Vars -> Vars
- class Occurs t where
- occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t
- metaOccurs :: MetaId -> t -> TCM ()
- occursCheck :: MetaId -> Vars -> Term -> TCM Term
- prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
- hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool
- isNeutral :: MonadTCM tcm => QName -> Elims -> tcm Bool
- rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool
- data PruneResult
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> ([Arg Bool], Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()
Documentation
initOccursCheck :: MetaVariable -> TCM () Source
Set the names of definitions to be looked at to the defs in the current mutual block.
defNeedsChecking :: QName -> TCM Bool Source
Is a def in the list of stuff to be checked?
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 |
Top | we are at the term root (this turns into |
Irrel | we are in an irrelevant argument |
defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx Source
patternViolation' :: Int -> String -> TCM a Source
goIrrelevant :: Vars -> Vars Source
allowedVar :: Nat -> Vars -> Bool Source
takeRelevant :: Vars -> [Nat] Source
liftUnderAbs :: Vars -> Vars Source
Extended occurs check.
occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t Source
metaOccurs :: MetaId -> t -> TCM () Source
Occurs QName | |
Occurs Clause | |
Occurs LevelAtom | |
Occurs PlusLevel | |
Occurs Level | |
Occurs Sort | |
Occurs Type | |
Occurs Term | |
Occurs Defn | |
Occurs a => Occurs [a] | |
(Occurs a, Subst a) => Occurs (Abs a) | |
Occurs a => Occurs (Elim' a) | |
Occurs a => Occurs (Dom a) | |
Occurs a => Occurs (Arg a) | |
(Occurs a, Occurs b) => Occurs (a, b) |
occursCheck :: MetaId -> Vars -> Term -> TCM Term Source
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 PruneResult Source
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
.
Issue 1147:
If any of the meta args vs
is matchable, e.g., is a constructor term,
we cannot prune, because the offending variables could be removed by
reduction for a suitable instantiation of the meta variable.
hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool Source
hasBadRigid xs v = Just 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.
Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).
hasBadRigid xs v = Nothing
means that
we cannot prune at all as one of the meta args is matchable.
(See issue 1147.)
isNeutral :: MonadTCM tcm => QName -> Elims -> tcm Bool Source
Check whether a term Def f es
is finally stuck.
Currently, we give only a crude approximation.
rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool Source
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 PruneResult Source
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 :: [(Dom (ArgName, Type), Bool)] -> Type -> ([Arg Bool], Type) Source
killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')
(ignoring Dom
). 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
.