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 # | |

Arbitrary Occurrence Source # | |

CoArbitrary Occurrence Source # | |

NFData Occurrence Source # | |

StarSemiRing Occurrence Source # | |

SemiRing Occurrence Source # |
It forms a commutative semiring where For |

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`

e`c`

(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) `<=`

bound`e`

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`

.