ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Positivity

Check that a datatype is strictly positive.

9 types
1 class
12 values

PackageAgda-2.7.0.1
Exports22
LanguageHaskell2010
LicenceMIT
SourcePositivity.hs

typetype Graph n e = Graph n e

valuecheckStrictlyPositive :: MutualInfo -> Set QName -> TCM ()

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.

valuegetDefArity :: Definition -> TCM Int

datadata Item

Constructors

AnArg Nat
ADef QName

Instances5Eq, Ord, Show, Pretty, HasRange

Eq ItemDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Ord ItemDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Show ItemDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Pretty ItemDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
HasRange ItemDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity

typetype Occurrences = Map Item [OccursWhere]

datadata OccurrencesBuilder

Used to build Occurrences and occurrence graphs.

Constructors

Concat [OccurrencesBuilder]
OccursAs Where OccurrencesBuilder
OccursHere Item
OnlyVarsUpTo Nat OccurrencesBuilder
OnlyVarsUpTo n occs discards occurrences of de Bruijn index >= n.

Instances2Semigroup, Monoid

Semigroup OccurrencesBuilderDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
The semigroup laws only hold up to flattening of Concat.
Monoid OccurrencesBuilderDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
The monoid laws only hold up to flattening of Concat.

datadata OccurrencesBuilder'

Used to build Occurrences and occurrence graphs.

valuepreprocess :: OccurrencesBuilder -> OccurrencesBuilder'

Removes OnlyVarsUpTo entries.

valueflatten :: OccurrencesBuilder -> Map Item Integer

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.)

datadata OccEnv

Context for computing occurrences.

Constructors

OccEnv
- vars :: [Maybe Item]
  Items corresponding to the free variables.
  Potential invariant: It seems as if the list has the form genericReplicate n Nothing ++ map (Just . AnArg) is, for some n and is, where is is decreasing (non-strictly).
- inf :: Maybe QName
  Name for ∞ builtin.

Instances1Monoid

(Semigroup a, Monoid a) => Monoid (OccM a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity

typetype OccM = Reader OccEnv

Monad for computing occurrences.

valuewithExtendedOccEnv :: Maybe Item -> OccM a -> OccM a

valuewithExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a

valuegetOccurrences

:: (Show a, PrettyTCM a, ComputeOccurrences a)
=> [Maybe Item]
Extension of the OccEnv, usually a local variable context.
-> a
-> TCM OccurrencesBuilder

Running the monad

classclass ComputeOccurrences a where

Methods

occurrences :: a -> OccM OccurrencesBuilder

Instances13ComputeOccurrences, …

ComputeOccurrences ClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Tele a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
ComputeOccurrences a => ComputeOccurrences [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity

valuecomputeOccurrences :: QName -> TCM (Map Item Integer)

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.)

valuecomputeOccurrences' :: QName -> TCM OccurrencesBuilder

Computes the occurrences in the given definition.

datadata Node

Constructors

DefNode !QName
ArgNode !QName !Nat

Instances4Eq, Ord, Pretty, PrettyTCM

Eq NodeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Ord NodeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Pretty NodeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
PrettyTCM NodeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity

datadata Edge a

Edge labels for the positivity graph.

Constructors

Edge !Occurrence a

Instances6Functor, Eq, Ord, Show, PrettyTCMWithNode, SemiRing

Functor EdgeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Eq a => Eq (Edge a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Ord a => Ord (Edge a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
Show a => Show (Edge a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
PrettyTCMWithNode (Edge OccursWhere)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
SemiRing (Edge (Seq OccursWhere))Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

valuemergeEdges :: Edge a -> Edge a -> Edge a

Merges two edges between the same source and target.

valuebuildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))

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.)

valuecomputeEdges

:: Set QName
The names in the current mutual block.
-> QName
The 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.

Orphan instances

1 instance

PrettyTCM (Seq OccursWhere)