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

Jump to...

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

Example:  function gauss

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

Original program

This is the classical Gauss' function, which computes a serie of sums for n (i.e., 1 + 2 +,..,+(n-1) + n), here expressed in Peano natural numbers.

 
         
import Benchmark(runBenchmark)

data Nat = Z | S Nat

main x = gauss (S(S(S(S(S x)))))

gauss    Z  = Z
gauss (S n) = sum (S n)  (gauss n) 

sum Z     y = y
sum (S x) y = S (sum x y)


GEN x = x

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

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

        

Annotated program [ go top ]

The gauss function presents the second rule with a nested function call, which is marked with GEN.

 
import Benchmark(runBenchmark)

data Nat = Z | S Nat

main x = gauss (S(S(S(S(S x)))))

gauss    Z  = Z
gauss (S n) = sum (S n)  (GEN (gauss n)) 

sum Z     y = y
sum (S x) y = S (sum x y)


GEN x = x

bench = runBenchmark 10 (\_ -> print (x =:= main (n2s 500)  ))
        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 load OffPeval in PAKCS, we do "mix examples/gauss" an then we load and show the specialized fuction, thus.

 
         
prelude> :l gauss_pe
Compiled Curry program 'gauss_pe.pl' is up-to-date.
 
gauss_pe(module: gauss)> :show
No source program file available, generating source from FlatCurry...

-- Program file: gauss_pe
module gauss(Nat(Z,S),gauss,sum,GEN,bench,n2s,s2n,main,sum_pe1,sum_pe2,sum_pe3,sum_pe4,
           sum_pe5,sum_pe6,gauss_pe7,gauss_pe11) where

import Benchmark

data Nat = Z | S Nat

gauss :: Nat -> Nat
gauss eval flex
gauss Z = Z
gauss (S v1) = sum (S v1) (GEN (gauss 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 (gauss_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

gauss_lambda0_0 :: Nat -> Int -> IO ()
gauss_lambda0_0 v0 v1 = print (v0 =:= (main (n2s 500)))

main :: b -> a
main v0 = sum_pe1 v0 (gauss_pe7 v0)

sum_pe1 :: c -> b -> a
sum_pe1 v0 v4 = S (sum_pe2 v0 v4)

sum_pe2 :: c -> b -> a
sum_pe2 v0 v4 = S (sum_pe3 v0 v4)

sum_pe3 :: c -> b -> a
sum_pe3 v0 v4 = S (sum_pe4 v0 v4)

sum_pe4 :: c -> b -> a
sum_pe4 v0 v4 = S (sum_pe5 v0 v4)

sum_pe5 :: c -> b -> a
sum_pe5 v0 v4 = S (sum_pe6 v0 v4)

sum_pe6 :: c -> b -> a
sum_pe6 eval flex
sum_pe6 Z v4 = v4
sum_pe6 (S v1304) v4 = S (sum_pe6 v1304 v4)

gauss_pe7 :: b -> a
gauss_pe7 v0 = sum_pe2 v0 (sum_pe3 v0 (sum_pe4 v0 (sum_pe5 v0 (gauss_pe11 v0))))

gauss_pe11 :: b -> a
gauss_pe11 eval flex
gauss_pe11 Z = Z
gauss_pe11 (S v1102) = sum_pe5 v1102 (gauss_pe11 v1102)


-- end of module gauss_pe
       
          
        

Runtimes [ go top ]

[ go to top ]