Safe Haskell	None
Language	Haskell2010

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 #
Methods minBound :: Occurrence # maxBound :: Occurrence #
Enum Occurrence Source #
Methods succ :: Occurrence -> Occurrence # pred :: Occurrence -> Occurrence # toEnum :: Int -> Occurrence # fromEnum :: Occurrence -> Int # enumFrom :: Occurrence -> [Occurrence] # enumFromThen :: Occurrence -> Occurrence -> [Occurrence] # enumFromTo :: Occurrence -> Occurrence -> [Occurrence] # enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence] #
Eq Occurrence Source #
Methods (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool #
Data Occurrence Source #
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 #
Methods compare :: Occurrence -> Occurrence -> Ordering # (<) :: Occurrence -> Occurrence -> Bool # (<=) :: Occurrence -> Occurrence -> Bool # (>) :: Occurrence -> Occurrence -> Bool # (>=) :: Occurrence -> Occurrence -> Bool # max :: Occurrence -> Occurrence -> Occurrence # min :: Occurrence -> Occurrence -> Occurrence #
Show Occurrence Source #
Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS #
NFData Occurrence Source #
Methods rnf :: Occurrence -> () #
Null Occurrence Source #
Methods empty :: Occurrence Source # null :: Occurrence -> Bool Source #
Pretty Occurrence Source #
Methods pretty :: Occurrence -> Doc Source # prettyPrec :: Int -> Occurrence -> Doc Source # prettyList :: [Occurrence] -> Doc Source #
StarSemiRing Occurrence Source #
Methods ostar :: Occurrence -> Occurrence Source #
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.
Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source #
KillRange Occurrence Source #
Methods killRange :: KillRangeT Occurrence Source #
PrettyTCM Occurrence Source #
Methods prettyTCM :: Occurrence -> TCM Doc Source #
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source #
Methods prettyTCM :: WithNode n Occurrence -> TCM Doc Source #

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 #
Methods (==) :: OccursWhere -> OccursWhere -> Bool # (/=) :: OccursWhere -> OccursWhere -> Bool #
Data OccursWhere Source #
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 #
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 #
Show OccursWhere Source #
Methods showsPrec :: Int -> OccursWhere -> ShowS # show :: OccursWhere -> String # showList :: [OccursWhere] -> ShowS #
Pretty OccursWhere Source #
Methods pretty :: OccursWhere -> Doc Source # prettyPrec :: Int -> OccursWhere -> Doc Source # prettyList :: [OccursWhere] -> Doc Source #

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 #
Methods (==) :: Where -> Where -> Bool # (/=) :: Where -> Where -> Bool #
Data Where Source #
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 #
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 #
Methods showsPrec :: Int -> Where -> ShowS # show :: Where -> String # showList :: [Where] -> ShowS #
Pretty Where Source #
Methods pretty :: Where -> Doc Source # prettyPrec :: Int -> Where -> Doc Source # prettyList :: [Where] -> Doc Source #

boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)] Source #

The map contains bindings of the form bound |-> es, 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 n e -> n -> n -> Occurrence -> Maybe e Source #

productOfEdgesInBoundedWalk occ g u v bound returns Just e 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 e is the product foldr1 otimes c for one such walk.

Preconditions: u and v must belong to g, and bound must belong to the domain of boundToEverySome.