Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

data Occurrence
- = Mixed
- | JustNeg
- | JustPos
- | StrictPos
- | GuardPos
- | Unused
data OccursWhere
- = Unknown
- | Known Range (Seq Where)
data Where
- = LeftOfArrow
- | DefArg QName Nat
- | UnderInf
- | VarArg
- | MetaArg
- | ConArgType QName
- | IndArgType QName
- | InClause Nat
- | Matched
- | InDefOf QName
boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
productOfEdgesInBoundedWalk :: (SemiRing e, Ord n) => (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e

Documentation

data Occurrence #

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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods minBound :: Occurrence # maxBound :: Occurrence #
Enum Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence 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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool #
Data Occurrence #
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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence 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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS #
NFData Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: Occurrence -> () #
Null Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence # null :: Occurrence -> Bool #
Pretty Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: Occurrence -> Doc # prettyPrec :: Int -> Occurrence -> Doc # prettyList :: [Occurrence] -> Doc #
StarSemiRing Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence #
SemiRing Occurrence #	`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 Methods ozero :: Occurrence # oone :: Occurrence # oplus :: Occurrence -> Occurrence -> Occurrence # otimes :: Occurrence -> Occurrence -> Occurrence #
KillRange Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods killRange :: KillRangeT Occurrence #
EmbPrj Occurrence #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Int32 # icod_ :: Occurrence -> S Int32 # value :: Int32 -> R Occurrence #
PrettyTCM Occurrence #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Occurrence -> TCM Doc #
Abstract [Occurrence] #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] #
Apply [Occurrence] #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Occurrence] -> Args -> [Occurrence] # applyE :: [Occurrence] -> Elims -> [Occurrence] #
PrettyTCM n => PrettyTCM (WithNode n Occurrence) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithNode n Occurrence -> TCM Doc #

data OccursWhere #

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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: OccursWhere -> OccursWhere -> Bool # (/=) :: OccursWhere -> OccursWhere -> Bool #
Data OccursWhere #
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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence 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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> OccursWhere -> ShowS # show :: OccursWhere -> String # showList :: [OccursWhere] -> ShowS #
Pretty OccursWhere #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: OccursWhere -> Doc # prettyPrec :: Int -> OccursWhere -> Doc # prettyList :: [OccursWhere] -> Doc #
Sized OccursWhere #
Instance details Defined in Agda.TypeChecking.Positivity Methods size :: OccursWhere -> Int #
PrettyTCM OccursWhere #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: OccursWhere -> TCM Doc #

data Where #

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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: Where -> Where -> Bool # (/=) :: Where -> Where -> Bool #
Data Where #
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 #
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 #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Where -> ShowS # show :: Where -> String # showList :: [Where] -> ShowS #
Pretty Where #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: Where -> Doc # prettyPrec :: Int -> Where -> Doc # prettyList :: [Where] -> Doc #

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

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 #

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.