Safe Haskell | None |
---|---|

Language | Haskell2010 |

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`

.

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.

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.

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

Eq Where Source # | |

Data Where Source # | |

Defined in Agda.TypeChecking.Positivity.Occurrence gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Where -> c Where # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Where # dataTypeOf :: Where -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Where) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where) # gmapT :: (forall b. Data b => b -> b) -> Where -> Where # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r # gmapQ :: (forall d. Data d => d -> u) -> Where -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Where -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Where -> m Where # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where # | |

Ord Where Source # | |

Show Where Source # | |

Pretty Where Source # | |

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

. In this case the returned value is
`foldr1`

`otimes`

(`map`

occ c) `<=`

bound

for one such walk `Just`

(`foldr1`

`otimes`

c)`c`

.

Preconditions: `u`

and `v`

must belong to `g`

, and `bound`

must
belong to the domain of `boundToEverySome`

.