Module Analysis.TermDomain

This module defines a class TermDomain which collects operations on an abstract domain approximating sets of data terms to be used in program analyses. Furthermore, it defines instances for a domain of top-level constructors and domains of depth-bounded constructor terms.

Author
Michael Hanus
Version
November 2024
Exported Datatypes:
ATypeDType2DType5
Exported Functions:
litAsCons
Exported Classes:
TermDomain

Exported Datatypes

data AType

An abstract term domain where terms are abstracted into their top-level constructors. AAny represents any expression, and ACons cs a value rooted by some of the constructor cs.

An invariant (ensured by the interface operations): the constructors in the ACons argument are always ordered.

Known instances:

data DType2

The DType instance of TermDomain for depth 2.

Known instances:

data DType5

The DType instance of TermDomain for depth 5.

Known instances:

Exported Functions

litAsCons :: Literal -> (String, String)  Deterministic 

A literal l is represented as a constructor ("",l).

Exported Classes

class (Read a, Show a, Eq a, ReadWrite a) => TermDomain a

The class TermDomain contains operations necessary to implement program analyses related to abstract domains approximating sets of data terms. The additional class contexts are required since abstract domains have to be stored, read and compared for equality in fixpoint operations.

Methods:

emptyType :: a  

Abstract representation of no possible value.

isEmptyType :: a -> Bool  

Does an abstract type represent no value?

anyType :: a  

Abstract representation of the type of all values.

isAnyType :: a -> Bool  

Does an abstract type represent any value?

aCons :: QName -> [a] -> a  

The representation of a constructor application to a list of abstract argument types.

aLit :: Literal -> a  

consOfType :: a -> [QName]  

argTypesOfCons :: QName -> Int -> a -> [a]  

lubType :: a -> a -> a  

joinType :: a -> a -> a  

showType :: a -> String