Safe Haskell | None |
---|---|
Language | Haskell2010 |
Check that a datatype is strictly positive.
Synopsis
- type Graph n e = Graph n e
- checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
- getDefArity :: Definition -> TCM Int
- (>*<) :: OccursWhere -> OccursWhere -> OccursWhere
- data Item
- type Occurrences = Map Item [OccursWhere]
- data OccurrencesBuilder
- data OccurrencesBuilder'
- emptyOB :: OccurrencesBuilder
- (>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
- preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
- data OccursWheres
- flatten :: OccurrencesBuilder -> Occurrences
- data OccEnv = OccEnv {}
- type OccM = Reader OccEnv
- withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
- withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
- getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder
- class ComputeOccurrences a where
- occurrences :: a -> OccM OccurrencesBuilder
- computeOccurrences :: QName -> TCM Occurrences
- computeOccurrences' :: QName -> TCM OccurrencesBuilder
- data Node
- data Edge = Edge !Occurrence OccursWhere
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
- computeEdges :: Set QName -> QName -> OccurrencesBuilder -> TCM [Edge Node Edge]
Documentation
checkStrictlyPositive :: MutualInfo -> Set QName -> TCM () Source #
Check that the datatypes in the mutual block containing the given declarations are strictly positive.
Also add information about positivity and recursivity of records to the signature.
getDefArity :: Definition -> TCM Int Source #
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere Source #
type Occurrences = Map Item [OccursWhere] Source #
data OccurrencesBuilder Source #
Used to build Occurrences
and occurrence graphs.
Concat [OccurrencesBuilder] | |
OccursAs Where OccurrencesBuilder | |
OccursHere Item | |
OnlyVarsUpTo Nat OccurrencesBuilder |
|
data OccurrencesBuilder' Source #
Used to build Occurrences
and occurrence graphs.
preprocess :: OccurrencesBuilder -> OccurrencesBuilder' Source #
Removes OnlyVarsUpTo
entries and adds OccursWhere
entries.
WARNING: There can be lots of sharing between the generated
OccursWhere
entries. Traversing all of these entries could be
expensive. (See computeEdges
for an example.)
data OccursWheres Source #
A type used locally in flatten
.
flatten :: OccurrencesBuilder -> Occurrences Source #
An interpreter for OccurrencesBuilder
.
WARNING: There can be lots of sharing between the generated
OccursWhere
entries. Traversing all of these entries could be
expensive. (See computeEdges
for an example.)
Context for computing occurrences.
getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder Source #
Running the monad
class ComputeOccurrences a where Source #
occurrences :: a -> OccM OccurrencesBuilder Source #
Instances
computeOccurrences :: QName -> TCM Occurrences Source #
Computes the occurrences in the given definition.
WARNING: There can be lots of sharing between the OccursWhere
entries. Traversing all of these entries could be expensive. (See
computeEdges
for an example.)
computeOccurrences' :: QName -> TCM OccurrencesBuilder Source #
Computes the occurrences in the given definition.
Edge labels for the positivity graph.
Instances
Eq Edge Source # | |
Ord Edge Source # | |
Show Edge Source # | |
Null Edge Source # | |
StarSemiRing Edge Source # | As E.g. |
SemiRing Edge Source # | These operations form a semiring if we quotient by the relation
"the |
PrettyTCM n => PrettyTCM (WithNode n Edge) Source # | |
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge) Source #
WARNING: There can be lots of sharing between the OccursWhere
entries in the edges. Traversing all of these entries could be
expensive. (See computeEdges
for an example.)
:: Set QName | The names in the current mutual block. |
-> QName | The current name. |
-> OccurrencesBuilder | |
-> TCM [Edge Node Edge] |
Computes all non-ozero
occurrence graph edges represented by
the given OccurrencesBuilder
.
WARNING: There can be lots of sharing between the OccursWhere
entries in the edges. Traversing all of these entries could be
expensive. For instance, for the function F
in
benchmarkmiscSlowOccurrences.agda
a large number of edges from
the argument X
to the function F
are computed. These edges have
polarity StrictPos
, JustNeg
or JustPos
, and contain the
following OccursWhere
elements:
,Known
(fromList
[InDefOf
F,InClause
0])
,Known
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
])
,Known
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
,LeftOfArrow
])
,Known
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
,LeftOfArrow
,LeftOfArrow
])- and so on.