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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Positivity

Contents

- Orphan instances

Description

Check that a datatype is strictly positive.

Synopsis

- type Graph n e = Graph n e
- checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
- getDefArity :: Definition -> TCM Int
- data Item
  - = AnArg Nat
  - | ADef QName
- type Occurrences = Map Item [OccursWhere]
- data OccurrencesBuilder
  - = Concat [OccurrencesBuilder]
  - | OccursAs Where OccurrencesBuilder
  - | OccursHere Item
  - | OnlyVarsUpTo Nat OccurrencesBuilder
- data OccurrencesBuilder'
  - = Concat' [OccurrencesBuilder']
  - | OccursAs' Where OccurrencesBuilder'
  - | OccursHere' Item
- preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
- flatten :: OccurrencesBuilder -> Map Item Integer
- data OccEnv = OccEnv {
  - vars :: [Maybe Item]
  - inf :: Maybe QName
  }
- type OccM = Reader OccEnv
- withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
- withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
- getOccurrences :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder
- class ComputeOccurrences a where
  - occurrences :: a -> OccM OccurrencesBuilder
- computeOccurrences :: QName -> TCM (Map Item Integer)
- computeOccurrences' :: QName -> TCM OccurrencesBuilder
- data Node
  - = DefNode !QName
  - | ArgNode !QName !Nat
- data Edge a = Edge !Occurrence a
- mergeEdges :: Edge a -> Edge a -> Edge a
- buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
- computeEdges :: Set QName -> QName -> OccurrencesBuilder -> TCM [Edge Node (Edge OccursWhere)]

# 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.

getDefArity :: Definition -> TCM Int Source #

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 Methods pretty :: Item -> Doc Source # prettyPrec :: Int -> Item -> Doc Source # prettyList :: [Item] -> Doc Source #
Show Item Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Item -> ShowS Source # show :: Item -> String Source # showList :: [Item] -> ShowS Source #
Eq Item Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Item -> Item -> Bool Source # (/=) :: Item -> Item -> Bool Source #
Ord Item Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods compare :: Item -> Item -> Ordering Source # (<) :: Item -> Item -> Bool Source # (<=) :: Item -> Item -> Bool Source # (>) :: Item -> Item -> Bool Source # (>=) :: Item -> Item -> Bool Source # max :: Item -> Item -> Item Source # min :: Item -> Item -> Item Source #

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`.

#### Instances

Instances details

Monoid OccurrencesBuilder Source # | The monoid laws only hold up to flattening of `Concat`.
Instance details Defined in Agda.TypeChecking.Positivity Methods mempty :: OccurrencesBuilder Source # mappend :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder Source # mconcat :: [OccurrencesBuilder] -> OccurrencesBuilder Source #
Semigroup OccurrencesBuilder Source # | The semigroup laws only hold up to flattening of `Concat`.
Instance details Defined in Agda.TypeChecking.Positivity Methods (<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder Source # sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder Source # stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder Source #

data OccurrencesBuilder' Source #

Used to build `Occurrences` and occurrence graphs.

Constructors

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

preprocess :: OccurrencesBuilder -> OccurrencesBuilder' Source #

Removes `OnlyVarsUpTo` entries.

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 Source # mappend :: OccM a -> OccM a -> OccM a Source # mconcat :: [OccM a] -> OccM a Source #

type OccM = Reader OccEnv Source #

Monad for computing occurrences.

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

withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a Source #

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 :: (Foldable t, ComputeOccurrences b, t b ~ a) => a -> OccM OccurrencesBuilder Source #

#### Instances

Instances details

ComputeOccurrences Clause Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Clause -> OccM OccurrencesBuilder Source #
ComputeOccurrences Level Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
ComputeOccurrences PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
ComputeOccurrences Type Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Arg a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Maybe a -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences [a] Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: [a] -> OccM OccurrencesBuilder Source #
(ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: (a, b) -> OccM OccurrencesBuilder Source #

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

Computes the number of occurrences of different `Item`s 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 Methods pretty :: Node -> Doc Source # prettyPrec :: Int -> Node -> Doc Source # prettyList :: [Node] -> Doc Source #
Eq Node Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Node -> Node -> Bool Source # (/=) :: Node -> Node -> Bool Source #
Ord Node Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods compare :: Node -> Node -> Ordering Source # (<) :: Node -> Node -> Bool Source # (<=) :: Node -> Node -> Bool Source # (>) :: Node -> Node -> Bool Source # (>=) :: Node -> Node -> Bool Source # max :: Node -> Node -> Node Source # min :: Node -> Node -> Node Source #

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 Source # (<$) :: a -> Edge b -> Edge a Source #
PrettyTCMWithNode (Edge OccursWhere) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #
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 Methods ozero :: Edge (Seq OccursWhere) Source # oone :: Edge (Seq OccursWhere) Source # oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source # otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source #
Show a => Show (Edge a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Edge a -> ShowS Source # show :: Edge a -> String Source # showList :: [Edge a] -> ShowS Source #
Eq a => Eq (Edge a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Edge a -> Edge a -> Bool Source # (/=) :: Edge a -> Edge a -> Bool Source #
Ord a => Ord (Edge a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods compare :: Edge a -> Edge a -> Ordering Source # (<) :: Edge a -> Edge a -> Bool Source # (<=) :: Edge a -> Edge a -> Bool Source # (>) :: Edge a -> Edge a -> Bool Source # (>=) :: Edge a -> Edge a -> Bool Source # max :: Edge a -> Edge a -> Edge a Source # min :: Edge a -> Edge a -> Edge a Source #

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:

- ``OccursWhere` _ `empty` (`fromList` [`InDefOf` F, `InClause` 0])`,
- ``OccursWhere` _ `empty` (`fromList` [`InDefOf` F, `InClause` 0, `LeftOfArrow`])`,
- ``OccursWhere` _ `empty` (`fromList` [`InDefOf` F, `InClause` 0, `LeftOfArrow`, `LeftOfArrow`])`,
- ``OccursWhere` _ `empty` (`fromList` [`InDefOf` F, `InClause` 0, `LeftOfArrow`, `LeftOfArrow`, `LeftOfArrow`])`,
- and so on.

# Orphan instances

PrettyTCM (Seq OccursWhere) Source # |
Instance details Methods prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source #