Safe Haskell | None |
---|---|
Language | Haskell98 |
Check that a datatype is strictly positive.
- type Graph n e = Graph n n e
- 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 :: (Show a, PrettyTCM a, 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.
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) |
Eq OccursWhere Source | |
Ord OccursWhere Source | |
Show OccursWhere Source | |
CoArbitrary OccursWhere Source | |
Arbitrary OccursWhere Source | |
PrettyTCM OccursWhere Source |
(>*<) :: 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 :: (Show a, PrettyTCM a, 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 put correct types in telescope! This is used instead of special treatment of lambdas (which was unsound: issue 121)
Edge labels for the positivity graph.
Eq Edge Source | |
Ord Edge Source | |
Show Edge Source | |
StarSemiRing Edge Source | As E.g. |
SemiRing Edge Source | These operations form a semiring if we quotient by the relation
"the |
CoArbitrary Edge Source | |
Arbitrary Edge Source | |
Null Edge Source | |
PrettyTCM n => PrettyTCM (WithNode n 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.