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 #

checkStrictlyPositive :: MutualInfo -> Set QName -> TCM () #

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 #

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

data Item #

Constructors

AnArg Nat
ADef QName

Instances

Eq Item #
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Item -> Item -> Bool # (/=) :: Item -> Item -> Bool #
Ord Item #
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 #
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Item -> ShowS # show :: Item -> String # showList :: [Item] -> ShowS #
HasRange Item #
Instance details Defined in Agda.TypeChecking.Positivity Methods getRange :: Item -> Range #

type Occurrences = Map Item [OccursWhere] #

data OccurrencesBuilder #

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

Used to build Occurrences and occurrence graphs.

Constructors

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

emptyOB :: OccurrencesBuilder #

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

preprocess :: OccurrencesBuilder -> OccurrencesBuilder' #

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 #

A type used locally in flatten.

Constructors

OccursWheres :++ OccursWheres
Occurs OccursWhere

flatten :: OccurrencesBuilder -> Occurrences #

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 #

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 #

Monad for computing occurrences.

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 #

Running the monad

class ComputeOccurrences a where #

Minimal complete definition

occurrences

Methods

occurrences :: a -> OccM OccurrencesBuilder #

Instances

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

computeOccurrences :: QName -> TCM Occurrences #

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 #

Computes the occurrences in the given definition.

data Node #

Constructors

DefNode !QName
ArgNode !QName !Nat

Instances

Eq Node #
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Node -> Node -> Bool # (/=) :: Node -> Node -> Bool #
Ord Node #
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 #
Instance details Defined in Agda.TypeChecking.Positivity Methods pretty :: Node -> Doc # prettyPrec :: Int -> Node -> Doc # prettyList :: [Node] -> Doc #
PrettyTCM Node #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: Node -> TCM Doc #

data Edge #

Edge labels for the positivity graph.

Constructors

Edge !Occurrence OccursWhere

Instances

Eq Edge #
Instance details Defined in Agda.TypeChecking.Positivity Methods (==) :: Edge -> Edge -> Bool # (/=) :: Edge -> Edge -> Bool #
Ord Edge #
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 #
Instance details Defined in Agda.TypeChecking.Positivity Methods showsPrec :: Int -> Edge -> ShowS # show :: Edge -> String # showList :: [Edge] -> ShowS #
Null Edge #
Instance details Defined in Agda.TypeChecking.Positivity Methods empty :: Edge # null :: Edge -> Bool #
StarSemiRing Edge #	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 #
SemiRing Edge #	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 # oone :: Edge # oplus :: Edge -> Edge -> Edge # otimes :: Edge -> Edge -> Edge #
PrettyTCM n => PrettyTCM (WithNode n Edge) #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: WithNode n Edge -> TCM Doc #

buildOccurrenceGraph :: Set QName -> TCM (Graph Node Edge) #

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 #

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 #
Instance details Methods size :: OccursWhere -> Int #
PrettyTCM OccursWhere #
Instance details Methods prettyTCM :: OccursWhere -> TCM Doc #