Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Positivity
Description
Check that a datatype is strictly positive.
Synopsis
checkStrictlyPositive :: MutualId -> TCM ()
data OccursWhere
= LeftOfArrow OccursWhere
| DefArg QName Nat OccursWhere
| VarArg OccursWhere
| MetaArg OccursWhere
| ConArgType QName OccursWhere
| InClause Nat OccursWhere
| InDefOf QName OccursWhere
| Here
| Unknown
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere
data Item
= AnArg Nat
| ADef QName
type Occurrences = Map Item [OccursWhere]
(>+<) :: Occurrences -> Occurrences -> Occurrences
concatOccurs :: [Occurrences] -> Occurrences
occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences
here :: Item -> Occurrences
class ComputeOccurrences a where
occurrences :: [Maybe Item] -> a -> Occurrences
computeOccurrences :: QName -> TCM Occurrences
etaExpandClause :: Nat -> Clause -> Clause
data Node
= DefNode QName
| ArgNode QName Nat
data Edge = Edge Occurrence OccursWhere
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)
Documentation
checkStrictlyPositive :: MutualId -> TCM ()Source
Check that the datatypes in the given mutual block are strictly positive.
data OccursWhere Source
Description of an occurrence.
Constructors
LeftOfArrow OccursWhere
DefArg QName Nat OccursWherein the nth argument of a define constant
VarArg OccursWhereas an argument to a bound variable
MetaArg OccursWhereas an argument of a metavariable
ConArgType QName OccursWherein the type of a constructor
InClause Nat OccursWherein the nth clause of a defined function
InDefOf QName OccursWherein the definition of a constant
Here
Unknownan unknown position (treated as negative)
show/hide Instances
(>*<) :: OccursWhere -> OccursWhere -> OccursWhereSource
data Item Source
Constructors
AnArg Nat
ADef QName
show/hide Instances
type Occurrences = Map Item [OccursWhere]Source
(>+<) :: Occurrences -> Occurrences -> OccurrencesSource
concatOccurs :: [Occurrences] -> OccurrencesSource
occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> OccurrencesSource
here :: Item -> OccurrencesSource
class ComputeOccurrences a whereSource
Methods
occurrences :: [Maybe Item] -> a -> OccurrencesSource
The first argument is the items corresponding to the free variables.
show/hide Instances
computeOccurrences :: QName -> TCM OccurrencesSource
Compute the occurrences in a given definition.
etaExpandClause :: Nat -> Clause -> ClauseSource
Eta expand a clause to have the given number of variables. Warning: doesn't update telescope or permutation! This is used instead of special treatment of lambdas (which was unsound: issue 121)
data Node Source
Constructors
DefNode QName
ArgNode QName Nat
show/hide Instances
data Edge Source
Constructors
Edge Occurrence OccursWhere
show/hide Instances
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)Source
computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)Source
Given an OccursWhere computes the target node and an Edge. The first argument is the set of names in the current mutual block.
Produced by Haddock version 2.4.2