Check that a datatype is strictly positive.

- checkStrictlyPositive :: MutualId -> TCM ()
- data OccursWhere
- (>*<) :: OccursWhere -> OccursWhere -> OccursWhere
- data Item
- 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
- 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.

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) |

(>*<) :: OccursWhere -> OccursWhere -> OccursWhereSource

type Occurrences = Map Item [OccursWhere]Source

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

concatOccurs :: [Occurrences] -> OccurrencesSource

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

here :: Item -> OccurrencesSource

class ComputeOccurrences a whereSource

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

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

ComputeOccurrences Clause | |

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 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)

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.