Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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

Bounded Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods minBound :: Occurrence Source # maxBound :: Occurrence Source #
Enum Occurrence Source # |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

succ :: Occurrence -> Occurrence Source #

pred :: Occurrence -> Occurrence Source #

toEnum :: Int -> Occurrence Source #

fromEnum :: Occurrence -> Int Source #

enumFrom :: Occurrence -> [Occurrence] Source #

enumFromThen :: Occurrence -> Occurrence -> [Occurrence] Source #

enumFromTo :: Occurrence -> Occurrence -> [Occurrence] Source #

enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence] Source #

Eq Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: Occurrence -> Occurrence -> Bool Source # (/=) :: Occurrence -> Occurrence -> Bool 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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Occurrence Source #

toConstr :: Occurrence -> Constr Source #

dataTypeOf :: Occurrence -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Occurrence) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence) Source #

gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Occurrence -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Occurrence -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Occurrence -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence Source #

Ord Occurrence Source # |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

compare :: Occurrence -> Occurrence -> Ordering Source #

(<) :: Occurrence -> Occurrence -> Bool Source #

(<=) :: Occurrence -> Occurrence -> Bool Source #

(>) :: Occurrence -> Occurrence -> Bool Source #

(>=) :: Occurrence -> Occurrence -> Bool Source #

max :: Occurrence -> Occurrence -> Occurrence Source #

min :: Occurrence -> Occurrence -> Occurrence Source #

Show Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Occurrence -> ShowS Source # show :: Occurrence -> String Source # showList :: [Occurrence] -> ShowS Source #
NFData Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: 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 #
StarSemiRing Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence 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.
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 #
KillRange Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods killRange :: KillRangeT Occurrence 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 #
PrettyTCM Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Occurrence -> TCM Doc Source #
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 #
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithNode n Occurrence -> TCM Doc 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

Eq OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: OccursWhere -> OccursWhere -> Bool Source # (/=) :: OccursWhere -> OccursWhere -> Bool 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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OccursWhere Source #

toConstr :: OccursWhere -> Constr Source #

dataTypeOf :: OccursWhere -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OccursWhere) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OccursWhere) Source #

gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> OccursWhere -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> OccursWhere -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere Source #

Ord OccursWhere Source # |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

compare :: OccursWhere -> OccursWhere -> Ordering Source #

(<) :: OccursWhere -> OccursWhere -> Bool Source #

(<=) :: OccursWhere -> OccursWhere -> Bool Source #

(>) :: OccursWhere -> OccursWhere -> Bool Source #

(>=) :: OccursWhere -> OccursWhere -> Bool Source #

max :: OccursWhere -> OccursWhere -> OccursWhere Source #

min :: OccursWhere -> OccursWhere -> OccursWhere Source #

Show OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> OccursWhere -> ShowS Source # show :: OccursWhere -> String Source # showList :: [OccursWhere] -> ShowS Source #
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 #
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 #
PrettyTCM (Seq OccursWhere) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: Seq OccursWhere -> TCM Doc Source #
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: WithNode n (Edge OccursWhere) -> TCM 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
IsIndex | is an index of an inductive family
InDefOf QName | in the definition of a constant

Instances

Eq Where Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods (==) :: Where -> Where -> Bool Source # (/=) :: Where -> Where -> Bool 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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Where Source #

toConstr :: Where -> Constr Source #

dataTypeOf :: Where -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Where) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where) Source #

gmapT :: (forall b. Data b => b -> b) -> Where -> Where Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Where -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Where -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Where -> m Where Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Where -> m Where Source #

Ord Where Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods compare :: Where -> Where -> Ordering Source # (<) :: Where -> Where -> Bool Source # (<=) :: Where -> Where -> Bool Source # (>) :: Where -> Where -> Bool Source # (>=) :: Where -> Where -> Bool Source # max :: Where -> Where -> Where Source # min :: Where -> Where -> Where Source #
Show Where Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> Where -> ShowS Source # show :: Where -> String Source # showList :: [Where] -> ShowS Source #
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 #

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