Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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
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

Null Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty 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

Data Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Occurrence -> c Occurrence #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Occurrence #

toConstr :: Occurrence -> Constr #

dataTypeOf :: Occurrence -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Occurrence) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence) #

gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r #

gmapQ :: (forall d. Data d => d -> u) -> Occurrence -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Occurrence -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m 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

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

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

Methods

size :: OccursWhere -> Int Source #

Data OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OccursWhere #

toConstr :: OccursWhere -> Constr #

dataTypeOf :: OccursWhere -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OccursWhere) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OccursWhere) #

gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r #

gmapQ :: (forall d. Data d => d -> u) -> OccursWhere -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> OccursWhere -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere #

Generic OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep OccursWhere :: Type -> Type #

Show OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

NFData OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: OccursWhere -> () #

Eq OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Ord OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

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

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

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

Data Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Where -> c Where #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Where #

toConstr :: Where -> Constr #

dataTypeOf :: Where -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Where) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where) #

gmapT :: (forall b. Data b => b -> b) -> Where -> Where #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r #

gmapQ :: (forall d. Data d => d -> u) -> Where -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Where -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Where -> m Where #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where #

Generic Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep Where :: Type -> Type #

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 #

NFData Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

rnf :: Where -> () #

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

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.