Agda.TypeChecking.Positivity

Check that a datatype is strictly positive.

Documentation

type Graph n e = Graph n 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

(>*<) :: OccursWhere -> OccursWhere -> OccursWhere

data Item

Constructors

AnArg Nat

ADef QName

Instances

Eq Item

Methods

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

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

Ord Item

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

Show Item

Methods

showsPrec :: Int -> Item -> ShowS

show :: Item -> String

showList :: [Item] -> ShowS

HasRange Item

Methods

getRange :: Item -> Range

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.

data OccurrencesBuilder'

Used to build Occurrences and occurrence graphs.

Constructors

Concat' [OccurrencesBuilder']

OccursAs' Where OccurrencesBuilder'

OccursHere' Item OccursWhere

emptyOB :: OccurrencesBuilder

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

preprocess :: OccurrencesBuilder -> OccurrencesBuilder'

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

A type used locally in flatten.

Constructors

OccursWheres :++ OccursWheres

Occurs OccursWhere

flatten :: OccurrencesBuilder -> Occurrences

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.

type OccM = Reader OccEnv

Monad for computing occurrences.

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

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

getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder

Running the monad

class ComputeOccurrences a where

Minimal complete definition

occurrences

Methods

occurrences :: a -> OccM OccurrencesBuilder

Instances

ComputeOccurrences Clause

Methods

occurrences :: Clause -> OccM OccurrencesBuilder

ComputeOccurrences LevelAtom

Methods

occurrences :: LevelAtom -> OccM OccurrencesBuilder

ComputeOccurrences PlusLevel

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

ComputeOccurrences Level

Methods

occurrences :: Level -> OccM OccurrencesBuilder

ComputeOccurrences Type

Methods

occurrences :: Type -> OccM OccurrencesBuilder

ComputeOccurrences Term

Methods

occurrences :: Term -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences [a]

Methods

occurrences :: [a] -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Maybe a)

Methods

occurrences :: Maybe a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Dom a)

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Arg a)

Methods

occurrences :: Arg a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Tele a)

Methods

occurrences :: Tele a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Abs a)

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder

ComputeOccurrences a => ComputeOccurrences (Elim' a)

Methods

occurrences :: Elim' a -> OccM OccurrencesBuilder

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

Methods

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

computeOccurrences :: QName -> TCM Occurrences

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

Computes the occurrences in the given definition.

etaExpandClause :: Nat -> Clause -> Clause

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)

data Node

Constructors

DefNode !QName

ArgNode !QName !Nat

Instances

Eq Node

Methods

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

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

Ord Node

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

Show Node

Methods

showsPrec :: Int -> Node -> ShowS

show :: Node -> String

showList :: [Node] -> ShowS

PrettyTCM Node

Methods

prettyTCM :: Node -> TCM Doc

data Edge

Edge labels for the positivity graph.

Constructors

Edge !Occurrence OccursWhere

Instances

Eq Edge

Methods

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

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

Ord Edge

Methods

compare :: Edge -> Edge -> Ordering

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

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

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

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

max :: Edge -> Edge -> Edge

min :: Edge -> Edge -> Edge

Show Edge

Methods

showsPrec :: Int -> Edge -> ShowS

show :: Edge -> String

showList :: [Edge] -> ShowS

StarSemiRing Edge

As OccursWhere does not have an oplus we cannot do something meaningful for the OccursWhere here.

E.g. ostar (Edge JustNeg w) = Edge Mixed (w oplus (w >*< w)) would probably more sense, if we could do it.

Methods

ostar :: Edge -> Edge

SemiRing Edge

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

Methods

ozero :: Edge

oone :: Edge

oplus :: Edge -> Edge -> Edge

otimes :: Edge -> Edge -> Edge

Null Edge

Methods

empty :: Edge

null :: Edge -> Bool

PrettyTCM n => PrettyTCM (WithNode n Edge)

Methods

prettyTCM :: WithNode n Edge -> TCM Doc

buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)

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 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 [InDefOf F, InClause 0]),
• Known (fromList [InDefOf F, InClause 0, LeftOfArrow]),
• Known (fromList [InDefOf F, InClause 0, LeftOfArrow, LeftOfArrow]),
• Known (fromList [InDefOf F, InClause 0, LeftOfArrow, LeftOfArrow, LeftOfArrow]),
• and so on.

Orphan instances

Sized OccursWhere

Methods

size :: Integral n => OccursWhere -> n

PrettyTCM OccursWhere

Methods

prettyTCM :: OccursWhere -> TCM Doc