Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Positivity

Contents

Description

Check that a datatype is strictly positive.

Synopsis

Documentation

type Graph n e = Graph n n e Source

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

getDefArity :: Definition -> TCM Int Source

data OccursWhere Source

Description of an occurrence.

Constructors

Unknown

an unknown position (treated as negative)

Known (Seq Where)

The elements of the sequence, from left to right, explain how to get to the occurrence.

Instances

data Where Source

One part of the description of an occurrence.

Constructors

LeftOfArrow 
DefArg QName Nat

in the nth argument of a define constant

UnderInf

in the principal argument of built-in ∞

VarArg

as an argument to a bound variable

MetaArg

as an argument of a metavariable

ConArgType QName

in the type of a constructor

IndArgType QName

in a datatype index of a constructor

InClause Nat

in the nth clause of a defined function

Matched

matched against in a clause of a defined function

InDefOf QName

in the definition of a constant

Instances

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

data Item Source

Constructors

AnArg Nat 
ADef QName 

Instances

type Occurrences = Map Item [OccursWhere] Source

data OccurrencesBuilder Source

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

Used to build Occurrences and occurrence graphs.

Constructors

Concat' [OccurrencesBuilder'] 
OccursAs' Where OccurrencesBuilder' 
OccursHere' Item OccursWhere 

emptyOB :: OccurrencesBuilder Source

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

preprocess :: OccurrencesBuilder -> OccurrencesBuilder' Source

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 Source

A type used locally in flatten.

Constructors

OccursWheres :++ OccursWheres 
Occurs OccursWhere 

flatten :: OccurrencesBuilder -> Occurrences Source

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 Source

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 Source

Monad for computing occurrences.

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

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

Running the monad

class ComputeOccurrences a where Source

Methods

occurrences :: a -> OccM OccurrencesBuilder Source

Instances

computeOccurrences :: QName -> TCM Occurrences Source

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 Source

Computes the occurrences in the 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 Node Source

Constructors

DefNode !QName 
ArgNode !QName !Nat 

Instances

data Edge Source

Edge labels for the positivity graph.

Constructors

Edge !Occurrence OccursWhere 

Instances

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 

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

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 Source

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:

Generators and tests