Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Positivity.Occurrence
Description
Occurrences.
Synopsis
- type PragmaPolarities = List1 (Ranged Occurrence)
- data Occurrence
- data OccursWhere = OccursWhere Range (Seq Where) (Seq Where)
- data Where
- 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
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
Pretty OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: OccursWhere -> Doc Source # prettyPrec :: Int -> OccursWhere -> Doc Source # prettyList :: [OccursWhere] -> Doc Source # | |||||
Null OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence | |||||
Sized OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence | |||||
Generic OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence Associated Types
| |||||
Show OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence Methods showsPrec :: Int -> OccursWhere -> ShowS # show :: OccursWhere -> String # showList :: [OccursWhere] -> ShowS # | |||||
NFData OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence Methods rnf :: OccursWhere -> () | |||||
Eq OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence | |||||
Ord OccursWhere Source # | |||||
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 # | |||||
Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source # | |||||
PrettyTCMWithNode (Edge OccursWhere) Source # | |||||
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 | ||||
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 # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence type Rep OccursWhere = D1 ('MetaData "OccursWhere" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" '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))))) |
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
Pretty Where Source # | |||||
Generic Where Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence Associated Types
| |||||
Show Where Source # | |||||
NFData Where Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence | |||||
Eq Where Source # | |||||
Ord Where Source # | |||||
type Rep Where Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence type Rep Where = D1 ('MetaData "Where" "Agda.TypeChecking.Positivity.Occurrence" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" '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 #
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
. In this case the returned value is
foldr1
otimes
(map
occ c) <=
bound
for one such walk Just
(foldr1
otimes
c)c
.
Preconditions: u
and v
must belong to g
, and bound
must
belong to the domain of boundToEverySome
.