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

Jump to...

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

Example: sumprod, sum and product of a list  

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

Original program

This is another example what could be transformed by tupling, here a data structure (a list of natural numbers) is explored twice, first to obtain the sum of its elements, and second to get the product of them.

 

import Benchmark(runBenchmark)

data Nat = Z | S Nat

main l =  sum (sumL ((S Z):(S(S Z)):S(S(S Z)):l))  (prodL  ((S Z):(S(S Z)):S(S(S Z)):l))

sumL []     = Z
sumL (x:xs) = sum x  (sumL xs)

prodL []     =(S Z)
prodL (x:xs) = mult x  (prodL xs)

sum Z     n = n
sum (S m) n = S(sum m n)

mult Z     _ = Z
mult (S m) n = sum n (mult m n)


-------------
GEN x = x

bench  = runBenchmark 10 (\_ -> print (x =:= ( main (map n2s [4..8] ) )  ) ) 
               where x free

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

In the example we provide a partially known list.

Annotated program [ go top ]

In order to get a finite partial evaluation process we mark with GEN those arguments or fuction calls that, either break the right-hand side linearity or they are nested function.

 
import Benchmark(runBenchmark)


data Nat = Z | S Nat

main l =  sum ( sumL ((S Z): (S(S Z)):S(S(S Z)):(GEN l))  ) 
              ( prodL  ((S Z):(S(S Z)):S(S(S Z)):l)  )

sumL []     = Z
sumL (x:xs) = sum x  (GEN (sumL xs))

prodL []     =(S Z)
prodL (x:xs) = mult x  (GEN (prodL xs))

sum Z     n = n
sum (S m) n = S(sum m n)

mult Z     _ = Z
mult (S m) n = sum n (GEN (mult m n))


-------------
GEN x = x

bench  = runBenchmark 10 (\_ -> print (x =:= ( main (map n2s [4..8] ) )  ) ) 
               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 ]

After of load OffPeval and mix the program with: mix "examples/sumprod", we can get de specialized version, as follows:

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

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

-- Program file: sumprod_pe
module sumprod(Nat(Z,S),sumL,prodL,sum,mult,GEN,bench,n2s,s2n,main,sum_pe1,prodL_pe3,
        mult_pe4,sum_pe5,mult_pe8,prodL_pe11,mult_pe12,sum_pe13,sumL_pe18) where

import Benchmark

data Nat = Z | S Nat

sumL :: [Nat] -> Nat
sumL eval flex
sumL [] = Z
sumL (v1 : v2) = sum v1 (GEN (sumL v2))

prodL :: [Nat] -> Nat
prodL eval flex
prodL [] = S Z
prodL (v1 : v2) = mult v1 (GEN (prodL v2))

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

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

GEN :: a -> a
GEN v0 = v0

bench :: IO ()
bench = Benchmark.runBenchmark 10 (sumprod_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

sumprod_lambda0_0 :: Nat -> Int -> IO ()
sumprod_lambda0_0 v0 v1 = print (v0 =:= (main (map n2s (enumFromTo 4 8))))

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

sum_pe1 :: c -> b -> a
sum_pe1 eval flex
sum_pe1 v2 v0 = S (fcase (sum_pe5 (S (S Z)) (sum_pe5 (S (S (S Z))) (sumL_pe18 v2))) of
     Z -> prodL_pe3 v0
     S v704 -> S (sum_pe13 v704 v0)
  )

prodL_pe3 :: b -> a
prodL_pe3 v0 = mult_pe4 (mult_pe8 (sum_pe5 (prodL_pe11 v0) (mult_pe8 (prodL_pe11 v0))))

mult_pe4 :: b -> a
mult_pe4 v13 = sum_pe5 v13 Z

sum_pe5 :: c -> b -> a
sum_pe5 eval flex
sum_pe5 Z v28 = v28
sum_pe5 (S v1404) v28 = S (sum_pe5 v1404 v28)

mult_pe8 :: b -> a
mult_pe8 v15 = sum_pe5 v15 (mult_pe4 v15)

prodL_pe11 :: b -> a
prodL_pe11 eval flex
prodL_pe11 [] = S Z
prodL_pe11 (v1603 : v1604) = mult_pe12 v1603 (prodL_pe11 v1604)

mult_pe12 :: c -> b -> a
mult_pe12 eval flex
mult_pe12 Z v1622 = Z
mult_pe12 (S v1704) v1622 = sum_pe5 v1622 (mult_pe12 v1704 v1622)

sum_pe13 :: c -> b -> a
sum_pe13 eval flex
sum_pe13 Z v0 = prodL_pe3 v0
sum_pe13 (S v1004) v0 = S (sum_pe13 v1004 v0)

sumL_pe18 :: b -> a
sumL_pe18 eval flex
sumL_pe18 [] = Z
sumL_pe18 (v1103 : v1104) = sum_pe5 v1103 (sumL_pe18 v1104)

-- end of module sumprod_pe

Nevertheless that our transformation does not perform tupling, a significative optimization w.r.t. source program is gained.

Runtimes [ go top ]

[ go to top ]