Agda-2.5.4: 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
Bounded Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Enum Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Eq 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 :: (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 #

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

Null Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

StarSemiRing 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

KillRange Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

EmbPrj Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Abstract [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data OccursWhere Source #

Description of an occurrence.

Constructors

Unknown

an unknown position (treated as negative)

Known Range (Seq Where)

The elements of the sequence, from left to right, explain how to get to the occurrence.

Instances
Eq OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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 :: (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 #

Ord OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Show OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Sized OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

size :: OccursWhere -> Int Source #

PrettyTCM OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

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

InDefOf QName

in the definition of a constant

Instances
Eq Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

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

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

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 :: (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 #

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 #

Show Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

showsPrec :: Int -> Where -> ShowS #

show :: Where -> String #

showList :: [Where] -> ShowS #

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