Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

data Occurrence
- = Mixed
- | JustNeg
- | JustPos
- | StrictPos
- | GuardPos
- | Unused
data OccursWhere = OccursWhere Range (Seq Where) (Seq Where)
data Where
- = LeftOfArrow
- | DefArg QName Nat
- | UnderInf
- | VarArg
- | MetaArg
- | ConArgType QName
- | IndArgType QName
- | ConEndpoint QName
- | InClause Nat
- | Matched
- | IsIndex
- | InDefOf QName
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.

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

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 Int32 Source # icod_ :: Occurrence -> S Int32 Source # value :: Int32 -> 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 -> ()
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]
Show Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Occurrence -> ShowS show :: Occurrence -> String showList :: [Occurrence] -> ShowS
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
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 #

data OccursWhere Source #

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

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 #

Sized OccursWhere Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

size :: OccursWhere -> Int Source #

natSize :: OccursWhere -> Peano Source #

NFData OccursWhere Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: OccursWhere -> ()

Generic OccursWhere Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep OccursWhere

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.20240731-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 Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> OccursWhere -> ShowS

show :: OccursWhere -> String

showList :: [OccursWhere] -> ShowS

Eq OccursWhere Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Ord OccursWhere Source #

Instance details

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) Source #

Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

PrettyTCMWithNode (Edge OccursWhere) Source #

Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

SemiRing (Edge (Seq OccursWhere)) Source #

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

Instance details

Defined in Agda.TypeChecking.Positivity

Methods

ozero :: Edge (Seq OccursWhere) Source #

oone :: Edge (Seq OccursWhere) Source #

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

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

type Rep OccursWhere Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.20240731-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 Source #

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

Instances details

Pretty Where Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc Source #

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

prettyList :: [Where] -> Doc Source #

NFData Where Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: Where -> ()

Generic Where Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep Where

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.20240731-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 Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Where -> ShowS

show :: Where -> String

showList :: [Where] -> ShowS

Eq Where Source #

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

Ord Where Source #

Instance details

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

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.20240731-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)] Source #

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