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

Pretty Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc

prettyPrec :: Int -> Occurrence -> Doc

prettyList :: [Occurrence] -> Doc

KillRange Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

killRange :: KillRangeT Occurrence

PrettyTCM Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCMWithNode Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj Occurrence

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Occurrence -> S Int32

icod_ :: Occurrence -> S Int32

value :: Int32 -> R Occurrence

Null Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

empty :: Occurrence

null :: Occurrence -> Bool

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

StarSemiRing Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ostar :: Occurrence -> Occurrence

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]

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 -> ()

Eq Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

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

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]

data OccursWhere

Description of an occurrence.

Constructors

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

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.Occurrence

Methods

size :: OccursWhere -> Int

natSize :: OccursWhere -> Peano

Generic OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "OccursWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)))))

Methods

from :: OccursWhere -> Rep OccursWhere x

to :: Rep OccursWhere x -> OccursWhere

Show OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> OccursWhere -> ShowS

show :: OccursWhere -> String

showList :: [OccursWhere] -> ShowS

NFData OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: OccursWhere -> ()

Eq OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

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

PrettyTCM (Seq OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc

PrettyTCMWithNode (Edge OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

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

SemiRing (Edge (Seq OccursWhere))

These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

Defined in Agda.TypeChecking.Positivity

Methods

ozero :: Edge (Seq OccursWhere)

oone :: Edge (Seq OccursWhere)

oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)

otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)

type Rep OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.4.3-inplace" 'False) (C1 ('MetaCons "OccursWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)))))

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

ConEndpoint QName

in an endpoint of a higher 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

Pretty Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc

prettyPrec :: Int -> Where -> Doc

prettyList :: [Where] -> Doc

Generic Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep Where

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "LeftOfArrow" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DefArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: C1 ('MetaCons "UnderInf" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "VarArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MetaArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "IndArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "ConEndpoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))) :+: (C1 ('MetaCons "Matched" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InDefOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))

Methods

from :: Where -> Rep Where x

to :: Rep Where x -> Where

Show Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Where -> ShowS

show :: Where -> String

showList :: [Where] -> ShowS

NFData Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: Where -> ()

Eq Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

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

type Rep Where

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.4.3-inplace" 'False) (((C1 ('MetaCons "LeftOfArrow" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DefArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: C1 ('MetaCons "UnderInf" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "VarArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MetaArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "IndArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "ConEndpoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))) :+: (C1 ('MetaCons "Matched" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InDefOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))

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.