Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

Agda.TypeChecking.Positivity

Description

Check that a datatype is strictly positive.

Synopsis

- checkStrictlyPositive :: MutualId -> TCM ()
- getDefArity :: Definition -> TCMT IO Nat
- 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
- prettyGraph :: PrettyTCM a => Graph a Edge -> TCM Doc
- data Edge = Edge Occurrence OccursWhere
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
- computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)

# Documentation

checkStrictlyPositive :: MutualId -> TCM ()

Check that the datatypes in the given mutual block are strictly positive.

getDefArity :: Definition -> TCMT IO Nat

data OccursWhere

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

data Item

Constructors

AnArg Nat |
ADef QName |

Instances

Eq Item |
Ord Item |
Show Item |

type Occurrences = Map Item [OccursWhere]

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

concatOccurs :: [Occurrences] -> Occurrences

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

here :: Item -> Occurrences

class ComputeOccurrences a where

Methods

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

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

Instances

ComputeOccurrences Clause |
ComputeOccurrences LevelAtom |
ComputeOccurrences PlusLevel |
ComputeOccurrences Level |
ComputeOccurrences Type |
ComputeOccurrences Term |
ComputeOccurrences a => ComputeOccurrences [a] |
ComputeOccurrences a => ComputeOccurrences (Arg a) |
ComputeOccurrences a => ComputeOccurrences (Abs a) |
ComputeOccurrences a => ComputeOccurrences (Tele a) |
(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) |

computeOccurrences :: QName -> TCM Occurrences

Compute the occurrences in a given definition.

etaExpandClause :: Nat -> Clause -> Clause

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

Constructors

DefNode QName |
ArgNode QName Nat |

Instances

Eq Node |
Ord Node |
Show Node |
PrettyTCM Node |

prettyGraph :: PrettyTCM a => Graph a Edge -> TCM Doc

data Edge

Constructors

Edge Occurrence OccursWhere |

Instances

Show Edge |
SemiRing Edge |

buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)

computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)

Given an `OccursWhere` computes the target node and an `Edge`. The first argument is the set of names in the current mutual block.