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 #
Methods minBound :: Occurrence # maxBound :: Occurrence #
Enum Occurrence Source #
Methods succ :: Occurrence -> Occurrence # pred :: Occurrence -> Occurrence # toEnum :: Int -> Occurrence # fromEnum :: Occurrence -> Int # enumFrom :: Occurrence -> [Occurrence] # enumFromThen :: Occurrence -> Occurrence -> [Occurrence] # enumFromTo :: Occurrence -> Occurrence -> [Occurrence] # enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence] #
Eq Occurrence Source #
Methods (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool #
Ord Occurrence Source #
Methods compare :: Occurrence -> Occurrence -> Ordering # (<) :: Occurrence -> Occurrence -> Bool # (<=) :: Occurrence -> Occurrence -> Bool # (>) :: Occurrence -> Occurrence -> Bool # (>=) :: Occurrence -> Occurrence -> Bool # max :: Occurrence -> Occurrence -> Occurrence # min :: Occurrence -> Occurrence -> Occurrence #
Show Occurrence Source #
Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS #
Arbitrary Occurrence Source #
Methods arbitrary :: Gen Occurrence # shrink :: Occurrence -> [Occurrence] #
CoArbitrary Occurrence Source #
Methods coarbitrary :: Occurrence -> Gen b -> Gen b #
NFData Occurrence Source #
Methods rnf :: Occurrence -> () #
StarSemiRing Occurrence Source #
Methods ostar :: Occurrence -> 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.
Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source #
Null Occurrence Source #
Methods empty :: Occurrence Source # null :: Occurrence -> Bool Source #
KillRange Occurrence Source #
Methods killRange :: KillRangeT Occurrence Source #
PrettyTCM Occurrence Source #
Methods prettyTCM :: Occurrence -> TCM Doc Source #
Abstract [Occurrence] Source #
Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Apply [Occurrence] Source #
Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source #
Methods prettyTCM :: WithNode n Occurrence -> TCM Doc 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.