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

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

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

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 #