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

Safe Haskell | None

Agda.TypeChecking.Irrelevance

Contents

- Operations on `Dom`.
- Operations on `Context`.
- Tests

Description

Irrelevant function types.

Synopsis

- 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

irrelevantOrUnused :: Relevance -> Bool

data `Relevance` see `Common`

unusableRelevance :: Relevance -> Bool

`unusableRelevance rel == True` iff we cannot use a variable of `rel`.

composeRelevance :: Relevance -> Relevance -> Relevance

`Relevance` composition. `Irrelevant` is dominant, `Relevant` is neutral.

inverseComposeRelevance :: Relevance -> Relevance -> Relevance

`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

For comparing `Relevance` ignoring `Forced` and `UnusedArg`.

irrToNonStrict :: Relevance -> Relevance

Irrelevant function arguments may appear non-strictly in the codomain type.

nonStrictToIrr :: Relevance -> Relevance

# Operations on `Dom`.

hideAndRelParams :: Dom a -> Dom a

Prepare parts of a parameter telescope for abstraction in constructors and projections.

inverseApplyRelevance :: Relevance -> Dom a -> Dom a

Used to modify context when going into a `rel` argument.

applyRelevance :: Relevance -> Dom a -> Dom a

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

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

Call me if --experimental-irrelevance is set.

workOnTypes' :: Bool -> TCM a -> TCM a

Internal workhorse, expects value of --experimental-irrelevance flag as argument.

applyRelevanceToContext :: Relevance -> TCM a -> TCM a

(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

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.

# Tests

prop_galois :: Relevance -> Relevance -> Relevance -> Bool

tests :: IO Bool