Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

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

KillRange Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCMWithNode Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

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

StarSemiRing Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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

Enum Occurrence Source # 
Instance details

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

Abstract [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Sized OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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

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

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

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

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