Safe Haskell  None 

Language  Haskell98 
Check that a datatype is strictly positive.
 type Graph n e = Graph n n e
 checkStrictlyPositive :: MutualInfo > Set QName > TCM ()
 getDefArity :: Definition > TCM Int
 data OccursWhere
 data Where
 (>*<) :: 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
 getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] > a > TCM OccurrencesBuilder
 class ComputeOccurrences a where
 computeOccurrences :: QName > TCM Occurrences
 computeOccurrences' :: QName > TCM OccurrencesBuilder
 etaExpandClause :: Nat > Clause > Clause
 data Node
 data Edge = Edge !Occurrence OccursWhere
 buildOccurrenceGraph :: Set QName > TCM (Graph Node Edge)
 computeEdges :: Set QName > QName > OccurrencesBuilder > TCM [Edge Node 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 #
data OccursWhere Source #
Description of an occurrence.
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 builtin ∞ 
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 
InClause Nat  in the nth clause of a defined function 
Matched  matched against in a clause of a defined function 
InDefOf QName  in the definition of a constant 
(>*<) :: 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 #
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.
etaExpandClause :: Nat > Clause > Clause Source #
Eta expand a clause to have the given number of variables. Warning: doesn't put correct types in telescope! This is used instead of special treatment of lambdas (which was unsound: issue 121)
Edge labels for the positivity graph.
Eq Edge Source #  
Ord Edge Source #  
Show Edge Source #  
Arbitrary Edge Source #  
CoArbitrary Edge Source #  
StarSemiRing Edge Source #  As E.g. 
SemiRing Edge Source #  These operations form a semiring if we quotient by the relation
"the 
Null Edge Source #  
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 Node Edge] 
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:
,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.