Module Abstract

This module performs the abstraction of expressions. Depending on the criteria used for abstractions, this module comes to a decision if parts of the given expressions should be further evaluated. This part is crucial to ensure termination of the whole process.

Note: In contrast to the original work we do not remove expressions from the set during abstraction because we want to avoid both re-evaluation of expressions or the loss of the more specific results.

Author: Elvira Albert, German Vidal, Michael Hanus, Björn Peemöller

Version: December 2018

Summary of exported operations:

abstract
                  ::  Options -> Prog -> [Expr] -> [Expr] -> [Expr]

Abstraction operator.

Exported operations:

abstract :: Options -> Prog -> [Expr] -> [Expr] -> [Expr]

Abstraction operator.

Example call:: (abstract otps p q es)

Parameters:

otps : Options passed to partiall evaluator.
p : program.
q : already abstracted expressions.
es : new expressions to be abstracted.