Safe Haskell | None |
---|---|
Language | Haskell2010 |
Occurrences.
Synopsis
- 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
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
.
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.
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 pretty :: OccursWhere -> Doc Source # prettyPrec :: Int -> OccursWhere -> Doc Source # prettyList :: [OccursWhere] -> Doc Source # | |||||
Sized OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence size :: OccursWhere -> Int Source # natSize :: OccursWhere -> Peano Source # | |||||
NFData OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence rnf :: OccursWhere -> () | |||||
Generic OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence
from :: OccursWhere -> Rep OccursWhere x to :: Rep OccursWhere x -> OccursWhere | |||||
Show OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence showsPrec :: Int -> OccursWhere -> ShowS show :: OccursWhere -> String showList :: [OccursWhere] -> ShowS | |||||
Eq OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence (==) :: OccursWhere -> OccursWhere -> Bool (/=) :: OccursWhere -> OccursWhere -> Bool | |||||
Ord OccursWhere Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence 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 prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source # | |||||
PrettyTCMWithNode (Edge OccursWhere) Source # | |||||
Defined in Agda.TypeChecking.Positivity 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 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.6.20240714-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))))) |
One part of the description of an occurrence.
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 |
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 # | |||||
NFData Where Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence | |||||
Generic Where Source # | |||||
Defined in Agda.TypeChecking.Positivity.Occurrence
| |||||
Show Where Source # | |||||
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.6.20240714-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 "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
,
iff
foldr1
otimes
w <=
bound
.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
. 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
.