| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Positivity
Contents
Description
Check that a datatype is strictly positive.
- type Graph n e = Graph n n e
- checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
- getDefArity :: Definition -> TCM Int
- data OccursWhere
- data Where
- (>*<) :: OccursWhere -> OccursWhere -> OccursWhere
- data Item
- type Occurrences = Map Item [OccursWhere]
- data OccurrencesBuilder
- data OccurrencesBuilder'
- emptyOB :: OccurrencesBuilder
- (>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
- preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
- data OccursWheres
- flatten :: OccurrencesBuilder -> 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 OccurrencesBuilder
- class ComputeOccurrences a where
- computeOccurrences :: QName -> TCM Occurrences
- computeOccurrences' :: QName -> TCM OccurrencesBuilder
- etaExpandClause :: Nat -> Clause -> Clause
- data Node
- data Edge = Edge !Occurrence OccursWhere
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
- computeEdges :: Set QName -> QName -> OccurrencesBuilder -> TCM [Edge Node Node Edge]
Documentation
checkStrictlyPositive :: MutualInfo -> 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.
One part of the description of an occurrence.
Constructors
| LeftOfArrow | |
| DefArg QName Nat | in the nth argument of a define constant |
| UnderInf | in the principal argument of built-in ∞ |
| VarArg | as an argument to a bound variable |
| MetaArg | as an argument of a metavariable |
| ConArgType QName | in the type of a constructor |
| IndArgType QName | in a datatype index of a constructor |
| InClause Nat | in the nth clause of a defined function |
| Matched | matched against in a clause of a defined function |
| InDefOf QName | in the definition of a constant |
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere Source #
type Occurrences = Map Item [OccursWhere] Source #
data OccurrencesBuilder Source #
Used to build Occurrences and occurrence graphs.
Constructors
| Concat [OccurrencesBuilder] | |
| OccursAs Where OccurrencesBuilder | |
| OccursHere Item | |
| OnlyVarsUpTo Nat OccurrencesBuilder |
|
data OccurrencesBuilder' Source #
Used to build Occurrences and occurrence graphs.
preprocess :: OccurrencesBuilder -> OccurrencesBuilder' Source #
Removes OnlyVarsUpTo entries and adds OccursWhere entries.
WARNING: There can be lots of sharing between the generated
OccursWhere entries. Traversing all of these entries could be
expensive. (See computeEdges for an example.)
data OccursWheres Source #
A type used locally in flatten.
Constructors
| OccursWheres :++ OccursWheres | |
| Occurs OccursWhere |
flatten :: OccurrencesBuilder -> Occurrences Source #
An interpreter for OccurrencesBuilder.
WARNING: There can be lots of sharing between the generated
OccursWhere entries. Traversing all of these entries could be
expensive. (See computeEdges for an example.)
Context for computing occurrences.
getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder Source #
Running the monad
class ComputeOccurrences a where Source #
Minimal complete definition
Methods
occurrences :: a -> OccM OccurrencesBuilder Source #
Instances
computeOccurrences :: QName -> TCM Occurrences Source #
Computes the occurrences in the given definition.
WARNING: There can be lots of sharing between the OccursWhere
entries. Traversing all of these entries could be expensive. (See
computeEdges for an example.)
computeOccurrences' :: QName -> TCM OccurrencesBuilder Source #
Computes the occurrences in the 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.
Constructors
| Edge !Occurrence OccursWhere |
Instances
| Eq Edge Source # | |
| Ord Edge Source # | |
| Show Edge Source # | |
| Arbitrary Edge Source # | |
| CoArbitrary Edge Source # | |
| StarSemiRing Edge Source # | As E.g. |
| SemiRing Edge Source # | These operations form a semiring if we quotient by the relation
"the |
| Null Edge Source # | |
| PrettyTCM n => PrettyTCM (WithNode n Edge) Source # | |
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge) Source #
WARNING: There can be lots of sharing between the OccursWhere
entries in the edges. Traversing all of these entries could be
expensive. (See computeEdges for an example.)
Arguments
| :: Set QName | The names in the current mutual block. |
| -> QName | The current name. |
| -> OccurrencesBuilder | |
| -> TCM [Edge Node Node Edge] |
Computes all non-ozero occurrence graph edges represented by
the given OccurrencesBuilder.
WARNING: There can be lots of sharing between the OccursWhere
entries in the edges. Traversing all of these entries could be
expensive. For instance, for the function F in
benchmarkmiscSlowOccurrences.agda a large number of edges from
the argument X to the function F are computed. These edges have
polarity StrictPos, JustNeg or JustPos, and contain the
following OccursWhere elements:
Known(fromList[InDefOfF,InClause0])Known(fromList[InDefOfF,InClause0,LeftOfArrow])Known(fromList[InDefOfF,InClause0,LeftOfArrow,LeftOfArrow])Known(fromList[InDefOfF,InClause0,LeftOfArrow,LeftOfArrow,LeftOfArrow])- and so on.