Safe Haskell | None |
---|---|
Language | Haskell98 |
Occurrences.
- data Occurrence
- boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
- productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e
- tests :: IO Bool
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
.
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 |
Bounded Occurrence Source | |
Enum Occurrence Source | |
Eq Occurrence Source | |
Ord Occurrence Source | |
Show Occurrence Source | |
NFData Occurrence Source | |
StarSemiRing Occurrence Source | |
SemiRing Occurrence Source |
It forms a commutative semiring where For |
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
productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e Source
productOfEdgesInBoundedWalk occ g u v bound
returns
iff there is a walk Just
ec
(a list of edges) in g
, from u
to v
,
for which the product
.
In this case the returned value foldr1
otimes
(map
occ c) <=
bounde
is the product
for one such walk.foldr1
otimes
c
Preconditions: u
and v
must belong to g
, and bound
must
belong to the domain of boundToEverySome
.