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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

- type PragmaPolarities = List1 (Ranged Occurrence)
- data Occurrence
  - = Mixed
  - | JustNeg
  - | JustPos
  - | StrictPos
  - | GuardPos
  - | Unused
- data OccursWhere = OccursWhere Range (Seq Where) (Seq Where)
- data Where
  - = LeftOfArrow
  - | DefArg QName Nat
  - | UnderInf
  - | VarArg Occurrence Nat
  - | MetaArg
  - | ConArgType QName
  - | IndArgType QName
  - | ConEndpoint 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
- modalPolarityToOccurrence :: ModalPolarity -> Occurrence

# Documentation

type PragmaPolarities = List1 (Ranged Occurrence) Source #

List of polarities stemming from POLARITY pragma.

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

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 #
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 Word32 Source # icod_ :: Occurrence -> S Word32 Source # value :: Word32 -> R Occurrence Source #
Null Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence Source # null :: Occurrence -> Bool 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 #
NFData Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: Occurrence -> () Source #
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 #

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

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 #
Null OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: OccursWhere Source # null :: OccursWhere -> Bool Source #
Sized OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods size :: OccursWhere -> Int Source # natSize :: OccursWhere -> Peano Source #
NFData OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: OccursWhere -> () Source #
Generic OccursWhere Source # |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep OccursWhere |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: OccursWhere -> Rep OccursWhere x Source #

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

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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Occurrence Nat | as an argument to a bound variable. The polarity, if given, is the polarity of the argument the occurence is in
MetaArg | as an argument of a metavariable
ConArgType QName | in the type of a constructor
IndArgType QName | in a datatype index of a constructor
ConEndpoint QName | in an endpoint of a higher 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 #
NFData Where Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: Where -> () Source #
Generic Where Source # |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Associated Types

type Rep Where |

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Occurrence) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: (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 "ConEndpoint" '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))))))

Methods

from :: Where -> Rep Where x Source #

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

Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Occurrence) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)) :+: (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 "ConEndpoint" '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`.

modalPolarityToOccurrence :: ModalPolarity -> Occurrence Source #