Agda.TypeChecking.Positivity

Check that a datatype is strictly positive.

Documentation

type Graph n e = Graph n e

checkStrictlyPositive :: 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.

getDefArity :: Definition -> TCM Int

data Item

Constructors

AnArg Nat

ADef QName

Instances

HasRange Item

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range

Pretty Item

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Item -> Doc

prettyPrec :: Int -> Item -> Doc

prettyList :: [Item] -> Doc

Show Item

Defined in Agda.TypeChecking.Positivity

Methods

showsPrec :: Int -> Item -> ShowS

show :: Item -> String

showList :: [Item] -> ShowS

Eq Item

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Item -> Item -> Bool

(/=) :: Item -> Item -> Bool

Ord Item

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Item -> Item -> Ordering

(<) :: Item -> Item -> Bool

(<=) :: Item -> Item -> Bool

(>) :: Item -> Item -> Bool

(>=) :: Item -> Item -> Bool

max :: Item -> Item -> Item

min :: Item -> Item -> Item

type Occurrences = Map Item [OccursWhere]

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

Instances

Monoid OccurrencesBuilder

The monoid laws only hold up to flattening of Concat.

Defined in Agda.TypeChecking.Positivity

Methods

mempty :: OccurrencesBuilder

mappend :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder

mconcat :: [OccurrencesBuilder] -> OccurrencesBuilder

Semigroup OccurrencesBuilder

The semigroup laws only hold up to flattening of Concat.

Defined in Agda.TypeChecking.Positivity

Methods

(<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder

sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder

stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder

data OccurrencesBuilder'

Used to build Occurrences and occurrence graphs.

Constructors

Concat' [OccurrencesBuilder']

OccursAs' Where OccurrencesBuilder'

OccursHere' Item

preprocess :: OccurrencesBuilder -> OccurrencesBuilder'

Removes OnlyVarsUpTo entries.

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

data OccEnv

Context for computing occurrences.

Constructors

OccEnv

Fields

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

Instances

(Semigroup a, Monoid a) => Monoid (OccM a)

Defined in Agda.TypeChecking.Positivity

Methods

mempty :: OccM a

mappend :: OccM a -> OccM a -> OccM a

mconcat :: [OccM a] -> OccM a

type OccM = Reader OccEnv

Monad for computing occurrences.

withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a

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

getOccurrences

Arguments

:: (Show a, PrettyTCM a, ComputeOccurrences a)

=> [Maybe Item]

Extension of the OccEnv, usually a local variable context.

-> a

-> TCM OccurrencesBuilder

Running the monad

class ComputeOccurrences a where

Minimal complete definition

Nothing

Methods

occurrences :: a -> OccM OccurrencesBuilder

default occurrences :: (Foldable t, ComputeOccurrences b, t b ~ a) => a -> OccM OccurrencesBuilder

Instances

ComputeOccurrences Clause

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Clause -> OccM OccurrencesBuilder

ComputeOccurrences Level

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Level -> OccM OccurrencesBuilder

ComputeOccurrences PlusLevel

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

ComputeOccurrences Term

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Term -> OccM OccurrencesBuilder

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Arg a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Arg a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Abs a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Dom a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Tele a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Tele a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Elim' a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Elim' a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Maybe a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Maybe a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences [a]

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: [a] -> OccM OccurrencesBuilder

(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: (a, b) -> OccM OccurrencesBuilder

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

computeOccurrences' :: QName -> TCM OccurrencesBuilder

Computes the occurrences in the given definition.

data Node

Constructors

DefNode !QName

ArgNode !QName !Nat

Instances

PrettyTCM Node

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Node -> m Doc

Pretty Node

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc

prettyPrec :: Int -> Node -> Doc

prettyList :: [Node] -> Doc

Eq Node

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Node -> Node -> Bool

(/=) :: Node -> Node -> Bool

Ord Node

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Node -> Node -> Ordering

(<) :: Node -> Node -> Bool

(<=) :: Node -> Node -> Bool

(>) :: Node -> Node -> Bool

(>=) :: Node -> Node -> Bool

max :: Node -> Node -> Node

min :: Node -> Node -> Node

data Edge a

Edge labels for the positivity graph.

Constructors

Edge !Occurrence a

Instances

Functor Edge

Defined in Agda.TypeChecking.Positivity

Methods

fmap :: (a -> b) -> Edge a -> Edge b

(<$) :: a -> Edge b -> Edge a

PrettyTCMWithNode (Edge OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc

SemiRing (Edge (Seq OccursWhere))

These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

Defined in Agda.TypeChecking.Positivity

Methods

ozero :: Edge (Seq OccursWhere)

oone :: Edge (Seq OccursWhere)

oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)

otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)

Show a => Show (Edge a)

Defined in Agda.TypeChecking.Positivity

Methods

showsPrec :: Int -> Edge a -> ShowS

show :: Edge a -> String

showList :: [Edge a] -> ShowS

Eq a => Eq (Edge a)

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Edge a -> Edge a -> Bool

(/=) :: Edge a -> Edge a -> Bool

Ord a => Ord (Edge a)

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Edge a -> Edge a -> Ordering

(<) :: Edge a -> Edge a -> Bool

(<=) :: Edge a -> Edge a -> Bool

(>) :: Edge a -> Edge a -> Bool

(>=) :: Edge a -> Edge a -> Bool

max :: Edge a -> Edge a -> Edge a

min :: Edge a -> Edge a -> Edge a

mergeEdges :: Edge a -> Edge a -> Edge a

Merges two edges between the same source and target.

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

computeEdges

Arguments

:: 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

PrettyTCM (Seq OccursWhere)

Methods

prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc