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
 data Item
 type Occurrences = Map Item [OccursWhere]
 data OccurrencesBuilder
 data OccurrencesBuilder'
 preprocess :: OccurrencesBuilder > OccurrencesBuilder'
 flatten :: OccurrencesBuilder > Map Item Integer
 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 (Map Item Integer)
 computeOccurrences' :: QName > TCM OccurrencesBuilder
 data Node
 data Edge a = Edge !Occurrence a
 mergeEdges :: Edge a > Edge a > Edge a
 buildOccurrenceGraph :: Set QName > TCM (Graph Node (Edge OccursWhere))
 computeEdges :: Set QName > QName > OccurrencesBuilder > TCM [Edge Node (Edge OccursWhere)]
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 #
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 

Instances
Semigroup OccurrencesBuilder Source #  The semigroup laws only hold up to flattening of 
Defined in Agda.TypeChecking.Positivity (<>) :: OccurrencesBuilder > OccurrencesBuilder > OccurrencesBuilder # sconcat :: NonEmpty OccurrencesBuilder > OccurrencesBuilder # stimes :: Integral b => b > OccurrencesBuilder > OccurrencesBuilder #  
Monoid OccurrencesBuilder Source #  The monoid laws only hold up to flattening of 
Defined in Agda.TypeChecking.Positivity 
data OccurrencesBuilder' Source #
Used to build Occurrences
and occurrence graphs.
preprocess :: OccurrencesBuilder > OccurrencesBuilder' Source #
Removes OnlyVarsUpTo
entries.
flatten :: OccurrencesBuilder > Map Item Integer 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.
:: (Show a, PrettyTCM a, ComputeOccurrences a)  
=> [Maybe Item]  Extension of the 
> a  
> TCM OccurrencesBuilder 
Running the monad
class ComputeOccurrences a where Source #
Nothing
occurrences :: a > OccM OccurrencesBuilder Source #
occurrences :: (Foldable t, ComputeOccurrences b, t b ~ a) => a > OccM OccurrencesBuilder Source #
Instances
computeOccurrences :: QName > TCM (Map Item Integer) Source #
Computes the number of occurrences of different Item
s 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.
Edge !Occurrence a 
Instances
Functor Edge Source #  
Eq a => Eq (Edge a) Source #  
Ord a => Ord (Edge a) Source #  
Show a => Show (Edge a) 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 #  
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source #  
Defined in Agda.TypeChecking.Positivity prettyTCM :: MonadPretty m => WithNode n (Edge OccursWhere) > m Doc Source # 
mergeEdges :: Edge a > Edge a > Edge a Source #
Merges two edges between the same source and target.
buildOccurrenceGraph :: Set QName > TCM (Graph Node (Edge OccursWhere)) 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 OccursWhere)] 
Computes all nonozero
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:
,OccursWhere
_empty
(fromList
[InDefOf
F,InClause
0])
,OccursWhere
_empty
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
])
,OccursWhere
_empty
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
,LeftOfArrow
])
,OccursWhere
_empty
(fromList
[InDefOf
F,InClause
0,LeftOfArrow
,LeftOfArrow
,LeftOfArrow
]) and so on.
Orphan instances
PrettyTCM (Seq OccursWhere) Source #  
prettyTCM :: MonadPretty m => Seq OccursWhere > m Doc Source # 