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
(>*<) :: OccursWhere -> OccursWhere -> OccursWhere
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 OccursWhere
emptyOB :: OccurrencesBuilder
(>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
data OccursWheres
- = OccursWheres :++ OccursWheres
- | Occurs OccursWhere
flatten :: OccurrencesBuilder -> Occurrences
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
computeOccurrences :: QName -> TCM Occurrences
computeOccurrences' :: QName -> TCM OccurrencesBuilder
data Node
- = DefNode !QName
- | ArgNode !QName !Nat
data Edge = Edge !Occurrence OccursWhere
buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge)
computeEdges :: Set QName -> QName -> OccurrencesBuilder -> TCM [Edge Node Edge]

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 #

(>*<) :: OccursWhere -> OccursWhere -> OccursWhere Source #

data Item Source #

Constructors

AnArg Nat
ADef QName

Instances

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

data OccurrencesBuilder' Source #

Used to build Occurrences and occurrence graphs.

Constructors

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

emptyOB :: OccurrencesBuilder Source #

(>+<) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder Source #

preprocess :: OccurrencesBuilder -> OccurrencesBuilder' Source #

Removes OnlyVarsUpTo entries and adds OccursWhere entries.

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

A type used locally in flatten.

Constructors

OccursWheres :++ OccursWheres
Occurs OccursWhere

flatten :: OccurrencesBuilder -> Occurrences 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.

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 :: (Show a, PrettyTCM a, ComputeOccurrences a) => [Maybe Item] -> a -> TCM OccurrencesBuilder Source #

Running the monad

class ComputeOccurrences a where Source #

Minimal complete definition

occurrences

Methods

occurrences :: a -> OccM OccurrencesBuilder Source #

Instances

ComputeOccurrences Clause Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Clause -> OccM OccurrencesBuilder Source #
ComputeOccurrences LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: LevelAtom -> 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 (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom 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 (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 (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' 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 Occurrences Source #

Computes the occurrences 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

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 :: Node -> TCM Doc Source #

data Edge Source #

Edge labels for the positivity graph.

Constructors

Edge !Occurrence OccursWhere

Instances

Eq Edge Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Edge -> Edge -> Bool # (/=) :: Edge -> Edge -> Bool #
Ord Edge Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods compare :: Edge -> Edge -> Ordering # (<) :: Edge -> Edge -> Bool # (<=) :: Edge -> Edge -> Bool # (>) :: Edge -> Edge -> Bool # (>=) :: Edge -> Edge -> Bool # max :: Edge -> Edge -> Edge # min :: Edge -> Edge -> Edge #
Show Edge Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Edge -> ShowS # show :: Edge -> String # showList :: [Edge] -> ShowS #
Null Edge Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods empty :: Edge Source # null :: Edge -> Bool Source #
StarSemiRing Edge Source #	As `OccursWhere` does not have an `oplus` we cannot do something meaningful for the `OccursWhere` here. E.g. `ostar (Edge JustNeg w) = Edge Mixed (w oplus (w >*< w))` would probably more sense, if we could do it.
Instance details Defined in Agda.TypeChecking.Positivity Methods ostar :: Edge -> Edge Source #
SemiRing Edge 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 Source # oone :: Edge Source # oplus :: Edge -> Edge -> Edge Source # otimes :: Edge -> Edge -> Edge Source #
PrettyTCM n => PrettyTCM (WithNode n Edge) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: WithNode n Edge -> TCM Doc Source #

buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge) 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]

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:

Known (fromList [InDefOf F, InClause 0]),
Known (fromList [InDefOf F, InClause 0, LeftOfArrow]),
Known (fromList [InDefOf F, InClause 0, LeftOfArrow, LeftOfArrow]),
Known (fromList [InDefOf F, InClause 0, LeftOfArrow, LeftOfArrow, LeftOfArrow]),
and so on.

Orphan instances

Sized OccursWhere Source #
Instance details Methods size :: OccursWhere -> Int Source #
PrettyTCM OccursWhere Source #
Instance details Methods prettyTCM :: OccursWhere -> TCM Doc Source #