Agda.TypeChecking.Positivity.Occurrence

Occurrences.

Documentation

data Occurrence

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

Bounded Occurrence

Methods

minBound :: Occurrence

maxBound :: Occurrence

Enum Occurrence

Methods

succ :: Occurrence -> Occurrence

pred :: Occurrence -> Occurrence

toEnum :: Int -> Occurrence

fromEnum :: Occurrence -> Int

enumFrom :: Occurrence -> [Occurrence]

enumFromThen :: Occurrence -> Occurrence -> [Occurrence]

enumFromTo :: Occurrence -> Occurrence -> [Occurrence]

enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]

Eq Occurrence

Methods

(==) :: Occurrence -> Occurrence -> Bool

(/=) :: Occurrence -> Occurrence -> Bool

Ord Occurrence

Methods

compare :: Occurrence -> Occurrence -> Ordering

(<) :: Occurrence -> Occurrence -> Bool

(<=) :: Occurrence -> Occurrence -> Bool

(>) :: Occurrence -> Occurrence -> Bool

(>=) :: Occurrence -> Occurrence -> Bool

max :: Occurrence -> Occurrence -> Occurrence

min :: Occurrence -> Occurrence -> Occurrence

Show Occurrence

Methods

showsPrec :: Int -> Occurrence -> ShowS

show :: Occurrence -> String

showList :: [Occurrence] -> ShowS

NFData Occurrence

Methods

rnf :: Occurrence -> ()

StarSemiRing Occurrence

Methods

ostar :: Occurrence -> Occurrence

SemiRing Occurrence

Occurrence is a complete lattice with least element Mixed and greatest element Unused.

It forms a commutative semiring where oplus is meet (glb) and otimes is composition. Both operations are idempotent.

For oplus, Unused is neutral (zero) and Mixed is dominant. For otimes, StrictPos is neutral (one) and Unused is dominant.

Methods

ozero :: Occurrence

oone :: Occurrence

oplus :: Occurrence -> Occurrence -> Occurrence

otimes :: Occurrence -> Occurrence -> Occurrence

Null Occurrence

Methods

empty :: Occurrence

null :: Occurrence -> Bool

KillRange Occurrence

Methods

killRange :: KillRangeT Occurrence

PrettyTCM Occurrence

Methods

prettyTCM :: Occurrence -> TCM Doc

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Methods

prettyTCM :: WithNode n Occurrence -> TCM Doc

data OccursWhere

Description of an occurrence.

Constructors

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

Eq OccursWhere

Methods

(==) :: OccursWhere -> OccursWhere -> Bool

(/=) :: OccursWhere -> OccursWhere -> Bool

Ord OccursWhere

Methods

compare :: OccursWhere -> OccursWhere -> Ordering

(<) :: OccursWhere -> OccursWhere -> Bool

(<=) :: OccursWhere -> OccursWhere -> Bool

(>) :: OccursWhere -> OccursWhere -> Bool

(>=) :: OccursWhere -> OccursWhere -> Bool

max :: OccursWhere -> OccursWhere -> OccursWhere

min :: OccursWhere -> OccursWhere -> OccursWhere

Show OccursWhere

Methods

showsPrec :: Int -> OccursWhere -> ShowS

show :: OccursWhere -> String

showList :: [OccursWhere] -> ShowS

data Where

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

InDefOf QName

in the definition of a constant

Instances

Eq Where

Methods

(==) :: Where -> Where -> Bool

(/=) :: Where -> Where -> Bool

Ord Where

Methods

compare :: Where -> Where -> Ordering

(<) :: Where -> Where -> Bool

(<=) :: Where -> Where -> Bool

(>) :: Where -> Where -> Bool

(>=) :: Where -> Where -> Bool

max :: Where -> Where -> Where

min :: Where -> Where -> Where

Show Where

Methods

showsPrec :: Int -> Where -> ShowS

show :: Where -> String

showList :: [Where] -> ShowS

boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]

The map contains bindings of the form bound |-> es, satisfying the following property: for every non-empty list w, foldr1 otimes w <= bound iff or [ all every w && any some w | (every, some) <- ess ].

productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n n e -> n -> n -> Occurrence -> Maybe e

productOfEdgesInBoundedWalk occ g u v bound returns Just e 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) <= bound. In this case the returned value e is the product foldr1 otimes c for one such walk.

Preconditions: u and v must belong to g, and bound must belong to the domain of boundToEverySome.