Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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
HasRange Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range Source #

Pretty Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

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.

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

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
PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

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