Safe Haskell | None |
---|---|
Language | Haskell2010 |
Occurrences.
- data Occurrence
- data OccursWhere
- data Where
- boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
- productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e
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 # | |
Data Occurrence Source # | |
Ord Occurrence Source # | |
Show Occurrence Source # | |
NFData Occurrence Source # | |
Null Occurrence Source # | |
Pretty Occurrence Source # | |
StarSemiRing Occurrence Source # | |
SemiRing Occurrence Source # |
It forms a commutative semiring where For |
KillRange Occurrence Source # | |
PrettyTCM Occurrence Source # | |
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # | |
data OccursWhere Source #
Description of an occurrence.
One part of the description of an occurrence.
LeftOfArrow | |
DefArg QName Nat | in the nth argument of a define constant |
UnderInf | in the principal argument of built-in ∞ |
VarArg | as an argument to a bound variable |
MetaArg | as an argument of a metavariable |
ConArgType QName | in the type of a constructor |
IndArgType QName | in a datatype index of a constructor |
InClause Nat | in the nth clause of a defined function |
Matched | matched against in a clause of a defined function |
InDefOf QName | in the definition of a constant |
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
.