Safe Haskell | None |
---|---|
Language | Haskell98 |
Check that a datatype is strictly positive.
- checkStrictlyPositive :: Set QName -> TCM ()
- getDefArity :: Definition -> TCM 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 WithNode n a = WithNode n a
- 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.
Also add information about positivity and recursivity of records to the signature.
getDefArity :: Definition -> TCM Int Source
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 -> OccursWhere Source
type Occurrences = Map Item [OccursWhere] Source
(>+<) :: Occurrences -> Occurrences -> Occurrences Source
concatOccurs :: [Occurrences] -> Occurrences Source
occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences Source
here :: Item -> Occurrences Source
onlyVarsUpTo :: Nat -> Occurrences -> Occurrences Source
onlyVarsUpTo n occs
discards occurrences of de Bruijn index >= n
.
Context for computing occurrences.
getOccurrences :: ComputeOccurrences a => [Maybe Item] -> a -> TCM Occurrences Source
Running the monad
class ComputeOccurrences a where Source
occurrences :: a -> OccM Occurrences Source
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)
Pairing something with a node (for printing only).
WithNode n a |
Edge labels for the positivity graph.
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.