Off-line narrowing-driven partial evaluator for inductively sequential programs

Jump to...

- main page...
 off-line partial evaluator...
- Benchmarks

The partial evaluator

This is a purely declarative partial evaluator for inductively sequential programs expressed as typical (first-order) Haskell or Curry programs. It has been implemented in Curry by J. Guadalupe Ramos, Josep Silva, and Germán Vidal.

In contrast to previous narrowing-driven partial evaluators, here we follow the offline approach for ensuring termination. In this way, the system scales up better to more realistic problems (like interpreter specialization). A detailed description of new scheme can be found in [RSV05].

The sources of the partial evaluator, together with some selected benchmarks, can be found here. Once you download this file, you can uncompress it with:

  tar xfv offPeval.tar

The main module is OffPeval.curry. It implements the specialization phase of the offline narrowing-driven partial evaluator, first constructing a generalizing needed narrowing (GNN) tree from the program to be specialized, and then extracting and adequating the new program. It calls the following modules:

In order to use the partial evaluator, first you need to install the PAKCS environment for Curry. Then, start PAKCS and load in the file OffPeval.curry as follows:

[user@host]$ pakcs
  ______      __       _    _    ______   _______
 |  __  |    /  \     | |  / /  |  ____| |  _____|   Portland Aachen Kiel
 | |  | |   / /\ \    | |_/ /   | |      | |_____    Curry System
 | |__| |  / /__\ \   |  _  |   | |      |_____  |
 |  ____| / ______ \  | | \ \   | |____   _____| |   Version 1.6.0
 |_|     /_/      \_\ |_|  \_\  |______| |_______|   March 2004

Curry2Prolog Compiler Environment (Version of 02/03/04)
(RWTH Aachen, CAU Kiel, Portland State University)

prelude> :l OffPeval
...
{compiled /home/user/OffPeval/OffPeval.pl in module user, 4820 msec 1836284 bytes}
OffPeval>

Now, you have available the command mix. It takes an annotated program with possible occurrences of the special function for annotations: GEN, and computes a partial evaluation of this program w.r.t. the first function call in it.

There are several intermediate steps that can be shown only if the user is interested in:

• the GNN tree constructed
• the GNN tree including memoized expressions
• the set of resultants
• the computed renaming
• the renamed resultants
• the program obtained after post-unfolding simplification

For instance, a typical session is as follows:

OffPeval> mix "examples/power"
Offline Narrowing-Driven Partial Evaluator
(Version 0.1 of July 2005)
(Technical University of Valencia)

power.curry: compilation completed.
File 'examples/power.fcy' is up-to-date.

Main call: (main v0 v1)

Writing original program into "examples/power_pe.fcy"...
       

Now, in order to see the specialized program, first load the specialized program and then you should use :show utility, which presents a flat curry program in curry style code, thus.

prelude> :l power_pe

power_pe(module: power)> :show
No source program file available, generating source from FlatCurry...

-- Program file: power_pe
module power(Nat(Z,S),pow,mult,sum,GEN,bench,main,pow_pe1,mult_pe2,sum_pe3) where

import Benchmark

data Nat = Z | S Nat

pow :: Nat -> Nat -> Nat
pow eval flex
pow v0 Z = S Z
pow v0 (S v2) = mult v0 (GEN (pow v0 v2))

mult :: Nat -> Nat -> Nat
mult eval flex
mult Z v1 = Z
mult (S v2) v1 = sum v1 (GEN (mult v2 v1))

sum :: Nat -> Nat -> Nat
sum eval flex
sum Z v1 = v1
sum (S v2) v1 = S (sum v2 v1)

GEN :: a -> a
GEN v0 = v0

bench :: IO ()
bench = Benchmark.runBenchmark 10 (power_lambda0_0 v0) where v0 free

power_lambda0_0 :: Nat -> Int -> IO ()
power_lambda0_0 v0 v1 =
    print (v0 =:= (main (S (S (S (S Z)))) (S (S (S (S (S (S (S (S Z))))))))))

main :: c -> b -> a
main v0 v1 = pow_pe1 v0 v1

pow_pe1 :: c -> b -> a
pow_pe1 eval flex
pow_pe1 v0 Z = S Z
pow_pe1 v0 (S v204) = mult_pe2 v0 (pow_pe1 v0 v204)

mult_pe2 :: c -> b -> a
mult_pe2 eval flex
mult_pe2 Z v208 = Z
mult_pe2 (S v304) v208 = sum_pe3 v208 (mult_pe2 v304 v208)

sum_pe3 :: c -> b -> a
sum_pe3 eval flex
sum_pe3 Z v309 = v309
sum_pe3 (S v404) v309 = S (sum_pe3 v404 v309)

-- end of module power_pe
        

Benchmarks

Follow the links for a detailed description of the partial evaluation process for several selected benchmarks.

go to top...