Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Check that a datatype is strictly positive.



type Graph n e = Graph n n e Source

checkStrictlyPositive :: Set QName -> TCM () Source

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.

data OccursWhere Source

Description of an occurrence.


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


an unknown position (treated as negative)

data Item Source


AnArg Nat 
ADef QName 

onlyVarsUpTo :: Nat -> Occurrences -> Occurrences Source

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

data OccEnv Source

Context for computing occurrences.




vars :: [Maybe Item]

Items corresponding to the free variables.

inf :: Maybe QName

Name for ∞ builtin.

type OccM = Reader OccEnv Source

Monad for computing occurrences.

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

Running the monad

computeOccurrences :: QName -> TCM Occurrences Source

Compute the occurrences in a given definition.

etaExpandClause :: Nat -> Clause -> Clause Source

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 Edge Source

Edge labels for the positivity graph.


Eq Edge Source 
Ord Edge Source 
Show Edge Source 
StarSemiRing Edge Source

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.

SemiRing Edge Source

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

CoArbitrary Edge Source 
Arbitrary Edge Source 
Null Edge Source 
PrettyTCM n => PrettyTCM (WithNode n Edge) Source 

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

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

Generators and tests