Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Positivity.Warnings

Synopsis

Documentation

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

Methods

pretty :: OccursWhere -> Doc Source #

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

prettyList :: [OccursWhere] -> Doc Source #

Null OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Methods

empty :: OccursWhere Source #

null :: OccursWhere -> Bool Source #

NFData OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Methods

rnf :: OccursWhere -> () #

Eq OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Methods

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

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

Ord OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

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 #

Generic OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Associated Types

type Rep OccursWhere 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Warnings" "Agda-2.9.0-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.Warnings

Methods

showsPrec :: Int -> OccursWhere -> ShowS #

show :: OccursWhere -> String #

showList :: [OccursWhere] -> ShowS #

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

type Rep OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Warnings" "Agda-2.9.0-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 Occurrence Nat

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

InIndex

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

Methods

pretty :: Where -> Doc Source #

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

prettyList :: [Where] -> Doc Source #

NFData Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Methods

rnf :: Where -> () #

Eq Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Methods

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

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

Ord Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

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 #

Generic Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

Associated Types

type Rep Where 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Warnings" "Agda-2.9.0-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) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Occurrence) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: (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 "InIndex" '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.Warnings

Methods

showsPrec :: Int -> Where -> ShowS #

show :: Where -> String #

showList :: [Where] -> ShowS #

type Rep Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Warnings

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Warnings" "Agda-2.9.0-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) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Occurrence) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: (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 "InIndex" '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.

There is a property for this function in Internal.Utils.Graph.AdjacencyMap.Unidirectional.