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 2023
litAsCons
:: Literal -> (String,String)
A literal l
is represented as a constructor ("",l) .
|
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:
The DType
instance of TermDomain
for depth 2.
Constructors:
The DType
instance of TermDomain
for depth 5.
Constructors: