Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Positivity

Description

Check that a datatype is strictly positive.

Synopsis

Documentation

type Graph n e = Graph 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.

data Item Source #

Constructors

AnArg Nat 
ADef QName 

Instances

Instances details
Pretty Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Item -> Doc Source #

prettyPrec :: Int -> Item -> Doc Source #

prettyList :: [Item] -> Doc Source #

HasRange Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range Source #

Show Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

showsPrec :: Int -> Item -> ShowS

show :: Item -> String

showList :: [Item] -> ShowS

Eq Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Item -> Item -> Bool

(/=) :: Item -> Item -> Bool

Ord Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Item -> Item -> Ordering

(<) :: Item -> Item -> Bool

(<=) :: Item -> Item -> Bool

(>) :: Item -> Item -> Bool

(>=) :: Item -> Item -> Bool

max :: Item -> Item -> Item

min :: Item -> Item -> Item

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.

Instances

Instances details
Monoid OccurrencesBuilder Source #

The monoid laws only hold up to flattening of Concat.

Instance details

Defined in Agda.TypeChecking.Positivity

Semigroup OccurrencesBuilder Source #

The semigroup laws only hold up to flattening of Concat.

Instance details

Defined in Agda.TypeChecking.Positivity

flatten :: OccurrencesBuilder -> Map Item Integer 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.

Instances

Instances details
(Semigroup a, Monoid a) => Monoid (OccM a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

mempty :: OccM a

mappend :: OccM a -> OccM a -> OccM a

mconcat :: [OccM a] -> OccM a

type OccM = Reader OccEnv Source #

Monad for computing occurrences.

getOccurrences Source #

Arguments

:: (Show a, PrettyTCM a, ComputeOccurrences a) 
=> [Maybe Item]

Extension of the OccEnv, usually a local variable context.

-> a 
-> TCM OccurrencesBuilder 

Running the monad

class ComputeOccurrences a where Source #

Minimal complete definition

Nothing

Methods

occurrences :: a -> OccM OccurrencesBuilder Source #

default occurrences :: forall (t :: Type -> Type) b. (Foldable t, ComputeOccurrences b, t b ~ a) => a -> OccM OccurrencesBuilder Source #

Instances

Instances details
ComputeOccurrences Clause Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Level Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Term Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Type Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences a => ComputeOccurrences [a] Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

computeOccurrences :: QName -> TCM (Map Item Integer) Source #

Computes the number of occurrences of different Items 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.

data Node Source #

Constructors

DefNode !QName 
ArgNode !QName !Nat 

Instances

Instances details
Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc Source #

prettyPrec :: Int -> Node -> Doc Source #

prettyList :: [Node] -> Doc Source #

PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Node -> m Doc Source #

Eq Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Node -> Node -> Bool

(/=) :: Node -> Node -> Bool

Ord Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Node -> Node -> Ordering

(<) :: Node -> Node -> Bool

(<=) :: Node -> Node -> Bool

(>) :: Node -> Node -> Bool

(>=) :: Node -> Node -> Bool

max :: Node -> Node -> Node

min :: Node -> Node -> Node

data Edge a Source #

Edge labels for the positivity graph.

Constructors

Edge !Occurrence a 

Instances

Instances details
Functor Edge Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

fmap :: (a -> b) -> Edge a -> Edge b

(<$) :: a -> Edge b -> Edge a #

PrettyTCMWithNode (Edge OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

SemiRing (Edge (Seq OccursWhere)) Source #

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

Instance details

Defined in Agda.TypeChecking.Positivity

Show a => Show (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

showsPrec :: Int -> Edge a -> ShowS

show :: Edge a -> String

showList :: [Edge a] -> ShowS

Eq a => Eq (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

(==) :: Edge a -> Edge a -> Bool

(/=) :: Edge a -> Edge a -> Bool

Ord a => Ord (Edge a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

compare :: Edge a -> Edge a -> Ordering

(<) :: Edge a -> Edge a -> Bool

(<=) :: Edge a -> Edge a -> Bool

(>) :: Edge a -> Edge a -> Bool

(>=) :: Edge a -> Edge a -> Bool

max :: Edge a -> Edge a -> Edge a

min :: Edge a -> Edge a -> Edge a

mergeEdges :: Edge a -> Edge a -> Edge a Source #

Merges two edges between the same source and target.

buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere)) 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 (Edge OccursWhere)] 

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:

Orphan instances

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source #