Agda-2.6.1.3: 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
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 :: 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 #

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

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

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

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

Ord OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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

Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM n => PrettyTCM (WithNode n (Edge 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

IsIndex

is an index of an inductive family

InDefOf QName

in the definition of a constant

Instances

Instances details
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 :: 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 #

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.