Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Positivity

Description

Check that a datatype is strictly positive.

Synopsis

checkStrictlyPositive :: MutualId -> TCM () data OccursWhere = LeftOfArrow OccursWhere | DefArg QName Nat OccursWhere | VarArg OccursWhere | MetaArg OccursWhere | ConArgType QName OccursWhere | InClause Nat 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 class ComputeOccurrences a where occurrences :: [Maybe Item] -> a -> 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 :: MutualId -> TCM () Source

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

data OccursWhere Source

Description of an occurrence. Constructors LeftOfArrow OccursWhere DefArg QName Nat OccursWhere in the nth argument of a define constant 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 InClause Nat OccursWhere in the nth clause of a defined function InDefOf QName OccursWhere in the definition of a constant Here Unknown an unknown position (treated as negative)

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

data Item Source

Constructors AnArg Nat ADef QName

type Occurrences = Map Item [OccursWhere] Source

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

concatOccurs :: [Occurrences] -> Occurrences Source

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

here :: Item -> Occurrences Source

class ComputeOccurrences a where Source

Methods occurrences :: [Maybe Item] -> a -> Occurrences Source The first argument is the items corresponding to the free variables.

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 update telescope or permutation! This is used instead of special treatment of lambdas (which was unsound: issue 121)

data Node Source

Constructors DefNode QName ArgNode QName Nat

data Edge Source

Constructors Edge Occurrence OccursWhere

buildOccurrenceGraph :: Set QName -> TCM (Graph Node 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.

Produced by Haddock version 2.6.0