Safe Haskell | None |
---|---|
Language | Haskell98 |
Irrelevant function types.
- irrelevantOrUnused :: Relevance -> Bool
- unusableRelevance :: Relevance -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- ignoreForced :: Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- hideAndRelParams :: Dom a -> Dom a
- inverseApplyRelevance :: Relevance -> Dom a -> Dom a
- applyRelevance :: Relevance -> Dom a -> Dom a
- workOnTypes :: TCM a -> TCM a
- doWorkOnTypes :: TCM a -> TCM a
- workOnTypes' :: Bool -> TCM a -> TCM a
- applyRelevanceToContext :: Relevance -> TCM a -> TCM a
- wakeIrrelevantVars :: TCM a -> TCM a
- prop_galois :: Relevance -> Relevance -> Relevance -> Bool
- tests :: IO Bool
Documentation
unusableRelevance :: Relevance -> Bool Source
unusableRelevance rel == True
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance Source
Relevance
composition.
Irrelevant
is dominant, Relevant
is neutral.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source
inverseComposeRelevance r x
returns the most irrelevant y
such that forall x
, y
we have
x `moreRelevant` (r `composeRelevance` y)
iff
(r `inverseComposeRelevance` x) `moreRelevant` y
(Galois connection).
ignoreForced :: Relevance -> Relevance Source
For comparing Relevance
ignoring Forced
and UnusedArg
.
irrToNonStrict :: Relevance -> Relevance Source
Irrelevant function arguments may appear non-strictly in the codomain type.
Operations on Dom
.
hideAndRelParams :: Dom a -> Dom a Source
Prepare parts of a parameter telescope for abstraction in constructors and projections.
inverseApplyRelevance :: Relevance -> Dom a -> Dom a Source
Used to modify context when going into a rel
argument.
applyRelevance :: Relevance -> Dom a -> Dom a Source
Compose two relevance flags.
This function is used to update the relevance information
on pattern variables a
after a match against something rel
.
Operations on Context
.
workOnTypes :: TCM a -> TCM a Source
Modify the context whenever going from the l.h.s. (term side) of the typing judgement to the r.h.s. (type side).
doWorkOnTypes :: TCM a -> TCM a Source
Call me if --experimental-irrelevance is set.
workOnTypes' :: Bool -> TCM a -> TCM a Source
Internal workhorse, expects value of --experimental-irrelevance flag as argument.
applyRelevanceToContext :: Relevance -> TCM a -> TCM a Source
(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
wakeIrrelevantVars :: TCM a -> TCM a Source
Wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.