Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

data Occurrence
- = Mixed
- | JustNeg
- | JustPos
- | StrictPos
- | GuardPos
- | Unused
data OccursWhere = OccursWhere Range (Seq Where) (Seq Where)
data Where
- = LeftOfArrow
- | DefArg QName Nat
- | UnderInf
- | VarArg
- | MetaArg
- | ConArgType QName
- | IndArgType QName
- | InClause Nat
- | Matched
- | IsIndex
- | 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 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 Methods killRange :: KillRangeT Occurrence Source #
PrettyTCM Occurrence Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Occurrence -> m Doc Source #
PrettyTCMWithNode Occurrence Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc Source #
EmbPrj Occurrence Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Occurrence -> S Int32 Source # icod_ :: Occurrence -> S Int32 Source # value :: Int32 -> R Occurrence Source #
Null Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence Source # null :: Occurrence -> Bool Source #
Pretty Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: Occurrence -> Doc Source # prettyPrec :: Int -> Occurrence -> Doc Source # prettyList :: [Occurrence] -> Doc 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.
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source #
StarSemiRing Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence Source #
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 Methods minBound :: Occurrence # maxBound :: Occurrence #
Enum Occurrence Source #
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] #
Show Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS #
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 Methods (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool #
Ord Occurrence Source #
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 #
Abstract [Occurrence] Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Apply [Occurrence] Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #

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 Methods pretty :: OccursWhere -> Doc Source # prettyPrec :: Int -> OccursWhere -> Doc Source # prettyList :: [OccursWhere] -> Doc Source #
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 # Methods from :: OccursWhere -> Rep OccursWhere x # to :: Rep OccursWhere x -> OccursWhere #
Show OccursWhere Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> OccursWhere -> ShowS # show :: OccursWhere -> String # showList :: [OccursWhere] -> ShowS #
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 Methods (==) :: OccursWhere -> OccursWhere -> Bool # (/=) :: OccursWhere -> OccursWhere -> Bool #
Ord OccursWhere Source #
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 #
PrettyTCM (Seq OccursWhere) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source #
PrettyTCMWithNode (Edge OccursWhere) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #
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 Methods ozero :: Edge (Seq OccursWhere) Source # oone :: Edge (Seq OccursWhere) Source # oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source # otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source #
type Rep OccursWhere Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "OccursWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq Where)))))

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 Methods pretty :: Where -> Doc Source # prettyPrec :: Int -> Where -> Doc Source # prettyList :: [Where] -> Doc Source #
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 type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.6.2.1.20220327-inplace" 'False) (((C1 ('MetaCons "LeftOfArrow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DefArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat))) :+: (C1 ('MetaCons "UnderInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "VarArg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MetaArg" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "ConArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "IndArgType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))) :+: (C1 ('MetaCons "Matched" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InDefOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))

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.