ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Positivity
Check that a datatype is strictly positive.
- 9 types
- 1 class
- 12 values
- PackageAgda-2.8.0.2
- Exports22
- LanguageHaskell2010
- LicenceMIT
- SourcePositivity.hs
Check that the datatypes in the mutual block containing the given declarations are strictly positive.
Find polarity of datatypes parameters and indices.
Also add information about positivity and recursivity of records to the signature.
Constructors
Instances5Eq, Ord, Show, Pretty, HasRange
Eq ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityOrd ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityShow ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityPretty ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityHasRange ItemDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
Used to build Occurrences and occurrence graphs.
Constructors
Concat [OccurrencesBuilder]OccursAs Where OccurrencesBuilderOccursHere ItemOnlyVarsUpTo Nat OccurrencesBuilderOnlyVarsUpTo n occsdiscards occurrences of de Bruijn index>= n.
Instances2Semigroup, Monoid
Semigroup OccurrencesBuilderDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityThe semigroup laws only hold up to flattening of Concat.
Monoid OccurrencesBuilderDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityThe monoid laws only hold up to flattening of Concat.
Used to build Occurrences and occurrence graphs.
Removes OnlyVarsUpTo entries.
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.
Monad for computing occurrences.
getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a)=> [Maybe Item]Extension of the OccEnv, usually a local variable context.
-> a-> TCM OccurrencesBuilder
Running the monad
Methods
occurrences :: a -> OccM OccurrencesBuilder
Instances15ComputeOccurrences, …
ComputeOccurrences ClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences LevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences PlusLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences TypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences IntDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Abs a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Dom a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Tele a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences (Maybe a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityComputeOccurrences a => ComputeOccurrences [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity(ComputeOccurrences x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
Computes the number of occurrences of different Items 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.)
Computes the occurrences in the given definition.
Edge labels for the positivity graph.
Constructors
Edge !Occurrence a
Instances6Functor, Eq, Ord, Show, SemiRing, PrettyTCMWithNode
Functor EdgeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityEq a => Eq (Edge a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityOrd a => Ord (Edge a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityShow a => Show (Edge a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivitySemiRing (Edge (Seq OccursWhere))Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityThese operations form a semiring if we quotient by the relation "the Occurrence components are equal".
PrettyTCMWithNode (Edge OccursWhere)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
Merges two edges between the same source and target.
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.)
computeEdges :: Set QNameThe names in the current mutual block.
-> QNameThe current name.
-> OccurrencesBuilder-> TCM [Edge Node (Edge OccursWhere)]
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:
OccursWhere _ empty (fromList [InDefOf,F, InClause 0])OccursWhere _ empty (fromList [InDefOf,F, InClause 0, LeftOfArrow])OccursWhere _ empty (fromList [InDefOf,F, InClause 0, LeftOfArrow, LeftOfArrow])OccursWhere _ empty (fromList [InDefOf,F, InClause 0, LeftOfArrow, LeftOfArrow, LeftOfArrow])and so on.