| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Positivity.Occurrence
Description
Occurrences.
Synopsis
- data Occurrence
- data OccursWhere = OccursWhere Range (Seq Where) (Seq Where)
- data Where
- boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
- productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph 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.
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
data OccursWhere Source #
Description of an occurrence.
Constructors
| OccursWhere Range (Seq Where) (Seq Where) | The elements of the sequences, read from left to right, explain how to get to the occurrence. The second sequence includes the main information, and if the first sequence is non-empty, then it includes information about the context of the second sequence. |
Instances
One part of the description of an occurrence.
Constructors
| 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 |
| IsIndex | is an index of an inductive family |
| InDefOf QName | in the definition of a constant |
Instances
boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)] Source #
productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e Source #
productOfEdgesInBoundedWalk occ g u v bound returns a value
distinct from Nothing 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) <= boundJust (foldr1 otimes c)c.
Preconditions: u and v must belong to g, and bound must
belong to the domain of boundToEverySome.