Safe Haskell | None |
---|---|
Language | Haskell2010 |
Occurrences.
Synopsis
- data Occurrence
- data OccursWhere
- 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.
Unknown | an unknown position (treated as negative) |
Known Range (Seq Where) | The elements of the sequence, from left to right, explain how to get to the occurrence. |
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 |
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
.