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

Jump to...

- Off-line partial evaluator...
- Benchamark list

Example: fliptree

[ Original program ]  [ Annotated program ]  [ Specialized program ] [ Runtimes ]

Original program

This example is based too on Wadler's deforestation, main t, (function to be specialized) is a composition of functions that generate an intermediate structure, and after this is flipped .

 
import Benchmark(runBenchmark)

data Nat = Z | S Nat
data TreeN = Leaf Nat | Tree Nat TreeN TreeN

main t =  (fliptree  (gentree (S (S (S (S (S (S (S (S (S  t)))))))))))

gentree Z    = Leaf Z
gentree (S n)= Tree (S n) (gentree n) (gentree n)

fliptree (Leaf a) = Leaf a
fliptree (Tree (S n) l r) = Tree n (fliptree r) (fliptree l)

GEN x = x

bench = runBenchmark 10 (\_ -> print (x =:= main (n2s 5)  ))
        where x free

n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z    =  0
s2n (S n)= (s2n n) +1   
       
        

The program is going to be specialized for trees of depth 9 (expressed in Peano natural numbers).

Annotated program [ go top ]

The right-hand sides of the program become linear, thanks to the marks GEN.

 
import Benchmark(runBenchmark)


data Nat = Z | S Nat
data TreeN = Leaf Nat | Tree Nat TreeN TreeN

main t =  (fliptree  (gentree (S (S (S (S (S (S (S (S (S  t)))))))))))


gentree Z    = Leaf Z
gentree (S n)= Tree (S n) (gentree (GEN n)) (gentree (GEN n))

fliptree (Leaf a) = Leaf a
fliptree (Tree (S n) l r) = Tree n (fliptree r) (fliptree l)


GEN x = x

bench = runBenchmark 10 (\_ -> print (x =:= main (n2s 5)  ))
        where x free

n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z    =  0
s2n (S n)= (s2n n) +1   
          
        

Specialized program [ go top ]

In order to specialize, in PACKS environment, first load OffPeval, then run mix "examples/fliptree", and finally load and show the partially evaluated program.

 
prelude> :l fliptree_pe
Compiled Curry program 'fliptree_pe.pl' is up-to-date.

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

-- Program file: fliptree_pe
module fliptree(Nat(Z,S),TreeN(Leaf,Tree),gentree,fliptree,GEN,bench,n2s,s2n,main,fliptree_pe1) where

import Benchmark

data Nat = Z | S Nat
data TreeN = Leaf Nat | Tree Nat TreeN TreeN

gentree :: Nat -> TreeN
gentree eval flex
gentree Z = Leaf Z
gentree (S v1) = Tree (S v1) (gentree (GEN v1)) (gentree (GEN v1))

fliptree :: TreeN -> TreeN
fliptree eval flex
fliptree (Leaf v1) = Leaf v1
fliptree (Tree (S v5) v3 v4) = Tree v5 (fliptree v4) (fliptree v3)

GEN :: a -> a
GEN v0 = v0

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

n2s :: Int -> Nat
n2s v0 = 
   if v0 == 0
   then Z
   else S (n2s (v0 - 1))

s2n :: Nat -> Int
s2n eval flex
s2n Z = 0
s2n (S v1) = (s2n v1) + 1

fliptree_lambda0_0 :: TreeN -> Int -> IO ()
fliptree_lambda0_0 v0 v1 = print (v0 =:= (main (n2s 5)))

main :: b -> a
main v0 = Tree (S (S (S (S (S (S (S (S v0)))))))) (fliptree_pe1 (S (S (S (S (S (S (S (S v0))))))))) 
               (fliptree_pe1 (S (S (S (S (S (S (S (S v0)))))))))

fliptree_pe1 :: b -> a
fliptree_pe1 eval flex
fliptree_pe1 Z = Leaf Z
fliptree_pe1 (S v702) = Tree v702 (fliptree_pe1 v702) (fliptree_pe1 v702)

-- end of module fliptree_pe

Deforestation has been performed, now fliptree_pe1 is not more a composition (w.r.t. the source fliptree), it has changed by a recursive function that builds one Tree, which is already output of the program.

Runtimes [ go top ]

[ go to top ]