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

Jump to...

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

Example: power

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

Original program

This is the classical example for partial evaluation, here we specialize it by means of our offline narrowing-driven partial evaluator.

pow makes power of x to n, where n is known.

 
import Benchmark (runBenchmark)

data Nat = Z | S Nat

main x  = pow x (S(S(S(S(S(S(S(S Z))))))))

pow x Z     = S Z
pow x (S n) = mult x (pow x n)

mult Z     n  = Z
mult (S v) n  = sum n (mult v n)

sum Z     n = n
sum (S v) n = S (sum v n)

--for annotations
GEN x = x

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

s2n Z = 0
s2n (S n) = 1 + (s2n n )

       

The program will be specialized w.r.t. main x, i.e., pow x 8 (as Peano natural numbers).

Annotated program [ go top ]

At the program we annotate the nested function calls.

 
import Benchmark (runBenchmark)

data Nat = Z | S Nat

main x  = pow x (S(S(S(S(S(S(S(S Z))))))))

pow x Z     = S Z
pow x (S n) = mult x (GEN (pow x n))

mult Z     n  = Z
mult (S v) n  = sum n (GEN (mult v n))

sum Z     n = n
sum (S v) n = S (sum v n)

--for annotations
GEN x = x

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

s2n Z = 0
s2n (S n) = 1 + (s2n n )

         
        

Specialized program [ go top ]

Once in PAKCS environment, we load the power program, and the specialized version can be shown .

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

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,s2n,main,mult_pe1,sum_pe2,pow_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

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

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

main :: b -> a
main v0 = mult_pe1 v0 (pow_pe3 v0)

mult_pe1 :: c -> b -> a
mult_pe1 eval flex
mult_pe1 Z v4 = Z
mult_pe1 (S v304) v4 = sum_pe2 v4 (mult_pe1 v304 v4)

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

pow_pe3 :: b -> a
pow_pe3 v0 = mult_pe1 v0 (mult_pe1 v0 (mult_pe1 v0 (mult_pe1 v0 (mult_pe1 v0 
                   (mult_pe1 v0 (mult_pe1 v0 (S Z)))))))


-- end of module power_pe

We look at results that pow function is completely unfolded.

Runtimes [ go top ]

[ go to top ]