Safe Haskell | None |
---|
Check that a datatype is strictly positive.
- checkStrictlyPositive :: Set QName -> TCM ()
- getDefArity :: Definition -> TCMT IO Int
- 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
- onlyVarsUpTo :: Nat -> Occurrences -> Occurrences
- data OccEnv = OccEnv {}
- type OccM = Reader OccEnv
- withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
- getOccurrences :: ComputeOccurrences a => [Maybe Item] -> a -> TCM Occurrences
- class ComputeOccurrences a where
- occurrences :: a -> OccM 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 :: Set QName -> TCM ()Source
Check that the datatypes in the mutual block containing the given declarations are strictly positive.
getDefArity :: Definition -> TCMT IO IntSource
data OccursWhere Source
Description of an occurrence.
LeftOfArrow OccursWhere | |
DefArg QName Nat OccursWhere | in the nth argument of a define constant |
UnderInf OccursWhere | in the principal argument of built-in ∞ |
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 |
IndArgType QName OccursWhere | in a datatype index of a constructor |
InClause Nat OccursWhere | in the nth clause of a defined function |
Matched OccursWhere | matched against in a 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
onlyVarsUpTo :: Nat -> Occurrences -> OccurrencesSource
onlyVarsUpTo n occs
discards occurrences of de Bruijn index >= n
.
Context for computing occurrences.
getOccurrences :: ComputeOccurrences a => [Maybe Item] -> a -> TCM OccurrencesSource
Running the monad
class ComputeOccurrences a whereSource
occurrences :: a -> OccM OccurrencesSource
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.