Agda.TypeChecking.Positivity

Check that a datatype is strictly positive.

Documentation

checkStrictlyPositive :: 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 -> TCMT IO Int

data OccursWhere

Description of an occurrence.

Constructors

LeftOfArrow OccursWhere

DefArg QName Nat OccursWhere

in the nth argument of a define constant

UnderInf OccursWhere

in the principal argument of built-in ∞

VarArg OccursWhere

as an argument to a bound variable

MetaArg OccursWhere

as an argument of a metavariable

ConArgType QName OccursWhere

in the type of a constructor

IndArgType QName OccursWhere

in a datatype index of a constructor

InClause Nat OccursWhere

in the nth clause of a defined function

Matched OccursWhere

matched against in a clause of a defined function

InDefOf QName OccursWhere

in the definition of a constant

Here

Unknown

an unknown position (treated as negative)

Instances

Eq OccursWhere

Show OccursWhere

PrettyTCM OccursWhere

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

data Item

Constructors

AnArg Nat

ADef QName

Instances

Eq Item

Ord Item

Show Item

type Occurrences = Map Item [OccursWhere]

(>+<) :: Occurrences -> Occurrences -> Occurrences

concatOccurs :: [Occurrences] -> Occurrences

occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences

here :: Item -> Occurrences

onlyVarsUpTo :: Nat -> Occurrences -> Occurrences

onlyVarsUpTo n occs discards occurrences of de Bruijn index >= n.

data OccEnv

Context for computing occurrences.

Constructors

OccEnv

Fields

vars :: [Maybe Item]

Items corresponding to the free variables.

inf :: Maybe QName

Name for ∞ builtin.

type OccM = Reader OccEnv

Monad for computing occurrences.

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

getOccurrences :: ComputeOccurrences a => [Maybe Item] -> a -> TCM Occurrences

Running the monad

class ComputeOccurrences a where

Methods

occurrences :: a -> OccM Occurrences

Instances

ComputeOccurrences Clause

ComputeOccurrences LevelAtom

ComputeOccurrences PlusLevel

ComputeOccurrences Level

ComputeOccurrences Type

ComputeOccurrences Term

ComputeOccurrences a => ComputeOccurrences [a]

ComputeOccurrences a => ComputeOccurrences (Tele a)

ComputeOccurrences a => ComputeOccurrences (Abs a)

ComputeOccurrences a => ComputeOccurrences (Elim' a)

ComputeOccurrences a => ComputeOccurrences (Dom a)

ComputeOccurrences a => ComputeOccurrences (Arg a)

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

computeOccurrences :: QName -> TCM Occurrences

Compute the occurrences in a given definition.

etaExpandClause :: Nat -> Clause -> Clause

Eta expand a clause to have the given number of variables. Warning: doesn't update telescope or permutation! 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

Ord Node

Show Node

PrettyTCM Node

data WithNode n a

Constructors

WithNode n a

Instances

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

PrettyTCM n => PrettyTCM (WithNode n Edge)

data Edge

Constructors

Edge Occurrence OccursWhere

Instances

Show Edge

SemiRing Edge

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

PrettyTCM n => PrettyTCM (WithNode n Edge)

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

computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)

Given an OccursWhere computes the target node and an Edge. The first argument is the set of names in the current mutual block.