| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 OccursWhere | in the nth argument of a define constant
VarArg OccursWhere | as an argument to a bound variable
MetaArg OccursWhere | as an argument of a metavariable
ConArgType QName OccursWhere | in the type of a constructor
InClause Nat OccursWhere | in the nth clause of a defined function
InDefOf QName OccursWhere | in the definition of a constant
Here |
Unknown | an unknown position (treated as negative)

Instances

Eq OccursWhere
Show OccursWhere
PrettyTCM OccursWhere

(>*<) :: OccursWhere -> OccursWhere -> OccursWhere | Source

data Item | Source

Constructors

AnArg Nat |
ADef QName |

Instances

Eq Item
Ord Item
Show Item

type Occurrences = Map Item [OccursWhere] | Source

(>+<) :: Occurrences -> Occurrences -> Occurrences | Source

concatOccurs :: [Occurrences] -> Occurrences | Source

occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences | Source

here :: Item -> Occurrences | Source

class ComputeOccurrences a where | Source

Methods

occurrences :: [Maybe Item] -> a -> Occurrences | Source

The first argument is the items corresponding to the free variables.

Instances

ComputeOccurrences Clause
ComputeOccurrences Telescope
ComputeOccurrences Type
ComputeOccurrences Term
ComputeOccurrences a => ComputeOccurrences ([] a)
ComputeOccurrences a => ComputeOccurrences (Arg a)
ComputeOccurrences a => ComputeOccurrences (Abs a)
(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences ((,) a b)

computeOccurrences :: QName -> TCM Occurrences | Source

Compute the occurrences in a given definition.

etaExpandClause :: Nat -> Clause -> Clause | Source

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 |

Instances

Eq Node
Ord Node
Show Node
PrettyTCM Node

data Edge | Source

Constructors

Edge Occurrence OccursWhere |

Instances

Show Edge
SemiRing Edge

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