Module PeNatural

This module performs the partial evaluation of a given expression, based on the natural semantics defined in [NatSem] and improved by Peemöller and Skrlac [PS14].

To ensure termination, the partial evaluator performs at most one unfolding step, where an unfolding step is either

The replacement of a function call with the function's body (and an appropiate substitution for the function's variables)
The replacement of a bound variable by the value of the expression it is bound to. This is necessary to ensure termination for situations like in @let ones = 1 : ones in ones@ where unbound replacements would result in non-termination.

Author: Björn Peemöller

Version: December 2018

Summary of exported operations:

pevalExpr
                  ::  Options -> Prog -> Expr -> Expr

Partial evaluation.

Exported operations:

pevalExpr :: Options -> Prog -> Expr -> Expr

Partial evaluation. It is crucial that the free variables of the input expression directly correspond to the free variables of the output expression, as these may later be substituted by concrete arguments.

Example call:: (pevalExpr opts p e)

Parameters:

opts : Global parameters, used for en/disabling tracing.
p : Program
e : expression to be evaluated

Returns:: partially evaluated expression e'