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

Safe Haskell | None
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 [Occurrence]
  - | 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 = ReaderT OccEnv ReduceM
- 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.

Find polarity of datatypes parameters and indices.

Also add information about positivity and recursivity of records to the signature.

getDefArity :: Definition -> TCM Int Source #

data Item Source #

Constructors

AnArg Nat [Occurrence] |
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 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 = ReaderT OccEnv ReduceM 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 :: 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 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 Int Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Int -> 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 x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Boundary' x 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

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