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

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 #
Show Item Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Item -> ShowS # show :: Item -> String # showList :: [Item] -> ShowS #
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 #

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

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

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

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 PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
ComputeOccurrences Level Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
ComputeOccurrences Type Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
ComputeOccurrences a => ComputeOccurrences [a] Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: [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 (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Arg 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 (Tele a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele 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 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 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

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

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 #
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 #
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 #
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 #
PrettyTCMWithNode (Edge OccursWhere) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc 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 #