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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

minBound :: Occurrence

maxBound :: Occurrence

Enum Occurrence

Defined in Agda.TypeChecking.Positivity.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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Data Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Occurrence -> c Occurrence

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Occurrence

toConstr :: Occurrence -> Constr

dataTypeOf :: Occurrence -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Occurrence)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)

gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r

gmapQ :: (forall d. Data d => d -> u) -> Occurrence -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Occurrence -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence

Ord Occurrence

Defined in Agda.TypeChecking.Positivity.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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Occurrence -> ShowS

show :: Occurrence -> String

showList :: [Occurrence] -> ShowS

NFData Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: Occurrence -> ()

Null Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

empty :: Occurrence

null :: Occurrence -> Bool

Pretty Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc

prettyPrec :: Int -> Occurrence -> Doc

prettyList :: [Occurrence] -> Doc

StarSemiRing Occurrence

Defined in Agda.TypeChecking.Positivity.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.

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ozero :: Occurrence

oone :: Occurrence

oplus :: Occurrence -> Occurrence -> Occurrence

otimes :: Occurrence -> Occurrence -> Occurrence

KillRange Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

killRange :: KillRangeT Occurrence

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

PrettyTCM Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Occurrence -> TCM Doc

Abstract [Occurrence]

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> [Occurrence] -> [Occurrence]

Apply [Occurrence]

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [Occurrence] -> Args -> [Occurrence]

applyE :: [Occurrence] -> Elims -> [Occurrence]

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Data OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OccursWhere

toConstr :: OccursWhere -> Constr

dataTypeOf :: OccursWhere -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OccursWhere)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OccursWhere)

gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r

gmapQ :: (forall d. Data d => d -> u) -> OccursWhere -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OccursWhere -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere

Ord OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> OccursWhere -> ShowS

show :: OccursWhere -> String

showList :: [OccursWhere] -> ShowS

Pretty OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursWhere -> Doc

prettyPrec :: Int -> OccursWhere -> Doc

prettyList :: [OccursWhere] -> Doc

Sized OccursWhere

Defined in Agda.TypeChecking.Positivity

Methods

size :: OccursWhere -> Int

PrettyTCM OccursWhere

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: OccursWhere -> TCM Doc

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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Data Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

toConstr :: Where -> Constr

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

Defined in Agda.TypeChecking.Positivity.Occurrence

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

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Where -> ShowS

show :: Where -> String

showList :: [Where] -> ShowS

Pretty Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc

prettyPrec :: Int -> Where -> Doc

prettyList :: [Where] -> Doc

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

The map contains bindings of the form bound |-> ess, 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 e -> n -> n -> Occurrence -> Maybe e

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) <= bound. In this case the returned value is Just (foldr1 otimes c) for one such walk c.

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