Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

Documentation

type PragmaPolarities = List1 (Ranged Occurrence) Source #

List of polarities stemming from POLARITY pragma.

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

No occurrence.

Instances

Instances details
Pretty Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc Source #

prettyPrec :: Int -> Occurrence -> Doc Source #

prettyList :: [Occurrence] -> Doc Source #

KillRange Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

killRange :: KillRangeT Occurrence Source #

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Occurrence -> m Doc Source #

PrettyTCMWithNode Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc Source #

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Word32 Source #

icod_ :: Occurrence -> S Word32 Source #

value :: Word32 -> R Occurrence Source #

Null Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

empty :: Occurrence Source #

null :: Occurrence -> Bool Source #

SemiRing Occurrence Source #

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.

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ozero :: Occurrence Source #

oone :: Occurrence Source #

oplus :: Occurrence -> Occurrence -> Occurrence Source #

otimes :: Occurrence -> Occurrence -> Occurrence Source #

StarSemiRing Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ostar :: Occurrence -> Occurrence Source #

NFData Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: Occurrence -> () #

Eq Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Ord Occurrence Source # 
Instance details

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 #

Bounded Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

minBound :: Occurrence #

maxBound :: Occurrence #

Enum Occurrence Source # 
Instance details

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] #

Exception Occurrence Source #

Exception for short-circuiting when finding a Mixed path from source to target.

Instance details

Defined in Agda.TypeChecking.Positivity.OccurrenceAnalysis

Methods

toException :: Occurrence -> SomeException #

fromException :: SomeException -> Maybe Occurrence #

displayException :: Occurrence -> String #

backtraceDesired :: Occurrence -> Bool #

Show Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Occurrence -> ShowS #

show :: Occurrence -> String #

showList :: [Occurrence] -> ShowS #

Abstract [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

Apply [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

modalPolarityToOccurrence :: ModalPolarity -> Occurrence Source #

data OccursPath Source #

Constructors

Root 
LeftOfArrow !OccursPath 
DefArg !OccursPath !QName !Nat

in the nth argument of a defined constant

MutDefArg !OccursPath !QName !Nat

in the nth argument of a def in the current mutual block. (def given by Int index in the block)

UnderInf !OccursPath

in the principal argument of built-in ∞

VarArg !OccursPath !Nat !Occurrence

as an argument to a bound variable with given polarity. The polarity is only used for warning printing.

MetaArg !OccursPath

as an argument of a metavariable

ConArgType !OccursPath !QName

in the type of a constructor

IndArgType !OccursPath !QName

in a datatype index of a constructor

ConEndpoint !OccursPath !QName

in an endpoint of a higher constructor

InClause !OccursPath !Nat

in the nth clause of a defined function

Matched !OccursPath

matched against in a clause of a defined function

InIndex !OccursPath

is an index of an inductive family

InDefOf !OccursPath !QName

in the definition of a constant

Instances

Instances details
Pretty OccursPath Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursPath -> Doc Source #

prettyPrec :: Int -> OccursPath -> Doc Source #

prettyList :: [OccursPath] -> Doc Source #

NFData OccursPath Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: OccursPath -> () #

Eq OccursPath Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

(==) :: OccursPath -> OccursPath -> Bool #

(/=) :: OccursPath -> OccursPath -> Bool #

Show OccursPath Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> OccursPath -> ShowS #

show :: OccursPath -> String #

showList :: [OccursPath] -> ShowS #

data OccursWhere Source #

Constructors

OccursWhere !Range !OccursPath 

Instances

Instances details
Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursWhere -> Doc Source #

prettyPrec :: Int -> OccursWhere -> Doc Source #

prettyList :: [OccursWhere] -> Doc Source #

Eq OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Show OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> OccursWhere -> ShowS #

show :: OccursWhere -> String #

showList :: [OccursWhere] -> ShowS #

PrettyTCMWithNode (Edge OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.OccurrenceAnalysis

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #

data Node Source #

Constructors

DefNode QName

Definition site of a mutual definition

ArgNode QName Int

Occurrence of the nth definition argument inside the definition.

Instances

Instances details
Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Node -> Doc Source #

prettyPrec :: Int -> Node -> Doc Source #

prettyList :: [Node] -> Doc Source #

PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Node -> m Doc Source #

Eq Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

(==) :: Node -> Node -> Bool #

(/=) :: Node -> Node -> Bool #

Ord Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

compare :: Node -> Node -> Ordering #

(<) :: Node -> Node -> Bool #

(<=) :: Node -> Node -> Bool #

(>) :: Node -> Node -> Bool #

(>=) :: Node -> Node -> Bool #

max :: Node -> Node -> Node #

min :: Node -> Node -> Node #

Show Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Node -> ShowS #

show :: Node -> String #

showList :: [Node] -> ShowS #

Hashable Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

hashWithSalt :: Int -> Node -> Int #

hash :: Node -> Int #

data Edge a Source #

Constructors

Edge !Occurrence !a 

Instances

Instances details
Functor Edge Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

fmap :: (a -> b) -> Edge a -> Edge b #

(<$) :: a -> Edge b -> Edge a #

PrettyTCMWithNode (Edge OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.OccurrenceAnalysis

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #

Pretty a => PrettyTCMWithNode (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge a) -> m Doc Source #

Monoid a => SemiRing (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ozero :: Edge a Source #

oone :: Edge a Source #

oplus :: Edge a -> Edge a -> Edge a Source #

otimes :: Edge a -> Edge a -> Edge a Source #

Eq a => Eq (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

(==) :: Edge a -> Edge a -> Bool #

(/=) :: Edge a -> Edge a -> Bool #

Ord a => Ord (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

compare :: Edge a -> Edge a -> Ordering #

(<) :: Edge a -> Edge a -> Bool #

(<=) :: Edge a -> Edge a -> Bool #

(>) :: Edge a -> Edge a -> Bool #

(>=) :: Edge a -> Edge a -> Bool #

max :: Edge a -> Edge a -> Edge a #

min :: Edge a -> Edge a -> Edge a #

Show a => Show (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Edge a -> ShowS #

show :: Edge a -> String #

showList :: [Edge a] -> ShowS #

mergeEdges :: Edge a -> Edge a -> Edge a Source #