Offline Narrowing-Driven Specialization in Practice

In this work we present two annotation procedures, an hybrid specializer and a purely offline specializer. Both annotators use the same monovariant  BTA similar to this, and the Size-change graphs principle  to guarantee termination. However they annotate in a different way. The hybrid specializer uses the function identity GEN as annotation to ensure termination according to the annotation approach explained in the paper Improving Offline Narrowing-Driven Partial Evaluation using Size-Change Graphs. The purely offline specializer uses additionally the function GEN; the identity functions UNF and MEM. In general terms: a function is annotated with UNF when this function can be safely unfolded and with MEM otherwise. As the first procedure the function GEN is used to generalize terms as well as to linerize expressions.

Regarding the specialization in the pure offline approach we have eliminated the modulo variable renaming test from the local control. This way we have integrated in this application both specialization modules:

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

  tar xvfz Offnpeip.tgz

In order to use the application modules, first you need to install the PAKCS (version 1.7.3) environment for Curry. Then, start PAKCS and load  the file Offpeval.curry as follows:

 

[gustavo@cmm2 prueba]$ cd Offnpeip/
[gustavo@cmm2 Offnpeip]$ pakcs
% restoring /usr/local/pakcs/curry2prolog/c2p.state...
  ______      __       _    _    ______   _______    
 |  __  |    /  \     | |  / /  |  ____| |  _____|   Portland Aachen Kiel
 | |  | |   / /\ \    | |_/ /   | |      | |_____    Curry System
 | |__| |  / /__\ \   |  _  |   | |      |_____  |  
 |  ____| / ______ \  | | \ \   | |____   _____| |   Version 1.7.3 (10)
 |_|     /_/      \_\ |_|  \_\  |______| |_______|   September 2006

Curry2Prolog(sicstus) Compiler Environment (Version of 15/09/06)
(RWTH Aachen, CAU Kiel, Portland State University)

Bug reports: mh@informatik.uni-kiel.de

Type ":h" for help

Prelude> :l OffPeval
...
OffPeval>

Now, you have available four commands:

For instance, a typical session is as follows:

OffPeval> fullannotate "examples/applastwb"
--------------------------------------------------
      Full Annotator using size-change graphs    
--------------------------------------------------
Loading AbstractCurry program
generating examples/applastwb.acy ...
Computing size-change graphs
Computing binding-time division
[("main",1,[D]),("applast",2,[S,D]),("app",2,[S,D]),("last",1,[D]),("last'",2,[D,D]),

("UNF",1,[S]),("MEM",1,[S]),("GEN",1,[S])]
Program loaded
Annotating program & linearizing...
Program succesfully annotated
Transforming annotated program to Curry...
Annotated program stored in <<examples/applastwb_ann.curry>>
OffPeval> mixpo "examples/applastwb_ann"
Offline Narrowing-Driven Partial Evaluator
(Version 0.1 of April 2007)
(Technical University of Valencia)

generating examples/applastwb_ann.fcy ...

Main call: (main v0)


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

We get,  the following programs (for program applastwb.curry from the ../examples):

before annotate

after annotate

data Nat = Z | S Nat

main xs = applast [1,2,3,4,5] xs

applast xs x = last (app xs [x])

app [] y = y
app (x:xs) y = x : app xs y

--last [x] = x
last (y:ys) = last' ys y

last' [] y = y
last' (w:ws) _  = last (w:ws)

--for annotations:
UNF x = x
MEM x = x
GEN x = x
 

module applastwb_ann where
import System

data Nat   = Z  | S Nat

main :: Int -> Int
main xs = applast [1,2,3,4,5] xs

applast :: [a] -> a -> a
applast xs x = last (app xs [x])

app :: [a] -> [a] -> [a]
app [] y = y
app (x:xs) y = (x:(app xs y))

last :: [a] -> a
last (y:ys) = last' ys (GEN y)

last' :: [a] -> a -> a
last' [] y = y
last' (w:ws) _ = last (w:ws)

UNF :: a -> a
UNF x = x

MEM :: a -> a
MEM x = x

GEN :: a -> a
GEN x = x

 
 

after fullannotate

after mixpo

module applastwb_ann where
import System

data Nat   = Z  | S Nat

main :: Int -> Int
main xs = UNF (applast [1,2,3,4,5] xs)

applast :: [a] -> a -> a
applast xs x = MEM (last (UNF (app xs [x])))

app :: [a] -> [a] -> [a]
app [] y = y
app (x:xs) y = (x:(UNF (app xs y)))

last :: [a] -> a
last (y:ys) = MEM (last' ys y)

last' :: [a] -> a -> a
last' [] y = y
last' (w:ws) _ = MEM (last (w:ws))

UNF :: a -> a
UNF x = x

MEM :: a -> a
MEM x = x

GEN :: a -> a
GEN x = x
 

-- Program file: examples/applastwb_ann_pe
module applastwb_ann(Nat(Z,S),applast,app,last,last',

UNF,MEM,GEN,main,last_pe1) where

import System

data Nat = Z | S Nat

applast :: [a] -> a -> a
applast v1 v2 = MEM (last (UNF (app v1 [v2])))

app :: [a] -> [a] -> [a]
app [] v2 = v2
app (v3 : v4) v2 = v3 : (UNF (app v4 v2))

last :: [a] -> a
last (v2 : v3) = MEM (last' v3 v2)

last' :: [a] -> a -> a
last' [] v2 = v2
last' (v3 : v4) v2 = MEM (last (v3 : v4))

UNF :: a -> a
UNF v1 = v1

MEM :: a -> a
MEM v1 = v1

GEN :: a -> a
GEN v1 = v1

main :: b -> a
main v0 = last_pe1 v0

last_pe1 :: b -> a
last_pe1 v0 = v0

-- end of module examples/applastwb_ann_pe

If you want to see the result of the specialization (mixpo), you can load in the residual program examples/applastwb_ann_pe and use the show utility as we show below:

OffPeval> :l examples/applastwb_ann_pe
Compiling 'examples/applastwb_ann_pe.fcy' into 'examples/applastwb_ann_pe.pl'...done
examples/applastwb_ann_pe(module: applastwb_ann)> :show
No source program file available, generating source from FlatCurry...

% restoring /usr/local/pakcs/tools/genint.state...
 

Please report any bug or comment to garroyo (at) dsic.upv.es.

MiST ELP GPLIS DSIC UPV

Last update / Gustavo Arroyo