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

Summary of exported operations:

litAsCons :: Literal -> (String,String)  Deterministic 
A literal l is represented as a constructor ("",l).

Exported datatypes:

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.

Constructors:

DType2

The DType instance of TermDomain for depth 2.

Constructors:

DType5

The DType instance of TermDomain for depth 5.

Constructors:

Exported operations:

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

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