Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

Documentation

data Occurrence Source

Subterm occurrences for positivity checking. The constructors are listed in increasing information they provide: Mixed <= JustPos <= StrictPos <= GuardPos <= Unused Mixed <= JustNeg <= Unused.

Constructors

Mixed	Arbitrary occurrence (positive and negative).
JustNeg	Negative occurrence.
JustPos	Positive occurrence, but not strictly positive.
StrictPos	Strictly positive occurrence.
GuardPos	Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records.
Unused

Instances

Bounded Occurrence Source
Enum Occurrence Source
Eq Occurrence Source
Ord Occurrence Source
Show Occurrence Source
NFData Occurrence Source
StarSemiRing Occurrence Source
SemiRing Occurrence Source	`Occurrence` is a complete lattice with least element `Mixed` and greatest element `Unused`. It forms a commutative semiring where `oplus` is meet (glb) and `otimes` is composition. Both operations are idempotent. For `oplus`, `Unused` is neutral (zero) and `Mixed` is dominant. For `otimes`, `StrictPos` is neutral (one) and `Unused` is dominant.
CoArbitrary Occurrence Source
Arbitrary Occurrence Source
Null Occurrence Source
KillRange Occurrence Source
PrettyTCM Occurrence Source
Abstract [Occurrence] Source
Apply [Occurrence] Source
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source

boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)] Source

The map contains bindings of the form bound |-> es, satisfying the following property: for every non-empty list w, foldr1 otimes w <= bound iff or [ all every w && any some w | (every, some) <- ess ].

productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e Source

productOfEdgesInBoundedWalk occ g u v bound returns Just e iff there is a walk c (a list of edges) in g, from u to v, for which the product foldr1 otimes (map occ c) <= bound. In this case the returned value e is the product foldr1 otimes c for one such walk.

Preconditions: u and v must belong to g, and bound must belong to the domain of boundToEverySome.

tests :: IO Bool Source

Tests.