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

Safe Haskell | None

Agda.TypeChecking.Positivity

Description

Check that a datatype is strictly positive.

Synopsis

- checkStrictlyPositive :: Set QName -> TCM ()
- getDefArity :: Definition -> TCMT IO Int
- data OccursWhere
  - = LeftOfArrow OccursWhere
  - | DefArg QName Nat OccursWhere
  - | UnderInf OccursWhere
  - | VarArg OccursWhere
  - | MetaArg OccursWhere
  - | ConArgType QName OccursWhere
  - | IndArgType QName OccursWhere
  - | InClause Nat OccursWhere
  - | Matched OccursWhere
  - | InDefOf QName OccursWhere
  - | Here
  - | Unknown
- (>*<) :: OccursWhere -> OccursWhere -> OccursWhere
- data Item
  - = AnArg Nat
  - | ADef QName
- type Occurrences = Map Item [OccursWhere]
- (>+<) :: Occurrences -> Occurrences -> Occurrences
- concatOccurs :: [Occurrences] -> Occurrences
- occursAs :: (OccursWhere -> OccursWhere) -> Occurrences -> Occurrences
- here :: Item -> Occurrences
- onlyVarsUpTo :: Nat -> Occurrences -> Occurrences
- data OccEnv = OccEnv {
  - vars :: [Maybe Item]
  - inf :: Maybe QName
  }
- type OccM = Reader OccEnv
- withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
- getOccurrences :: ComputeOccurrences a => [Maybe Item] -> a -> TCM Occurrences
- class ComputeOccurrences a where
  - occurrences :: a -> OccM Occurrences
- computeOccurrences :: QName -> TCM Occurrences
- etaExpandClause :: Nat -> Clause -> Clause
- data Node
  - = DefNode QName
  - | ArgNode QName Nat
- data Edge = Edge Occurrence OccursWhere
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
- computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)

# Documentation

checkStrictlyPositive :: Set QName -> TCM ()

Check that the datatypes in the mutual block containing the given declarations are strictly positive.

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 (Arg a) |
ComputeOccurrences a => ComputeOccurrences (Dom a) |
ComputeOccurrences a => ComputeOccurrences (Tele a) |
ComputeOccurrences a => ComputeOccurrences (Abs 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 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 (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.