Improving offline narrowing-driven partial evaluation using size-change graphs

Jump to...

- schg page

Example: pascal's function

[ Original program ]  [ Annotated program ]

Original program

This is the classical function: Pascal,  which computes a coeficient of a polynomial.

 
         
data Nat = Z | S Nat

pascal  row col = cond col row

cond Z      _     = (S Z)
cond (S c) (S r)  = 
  ite  (eq c r)   (S Z)   (sum (pascal  r c)  (pascal  r (S c)))

ite True   x  _ = x
ite False  _  y = y

eq Z        Z   = True
eq Z     (S _ ) = False
eq (S _)    Z   = False
eq (S x) (S y)  = eq x y

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

        

Annotated program [ go top ]

In this example all annotations are introduced to ensure the right linearity property.

 
module pascalS where

data Nat
     = Z
     | S Nat

GEN :: a -> a
GEN x
     | success
     = x

pascal :: Nat -> Nat -> Nat
pascal row col = cond col row

cond :: Nat -> Nat -> Nat
cond Z _ = S Z
cond (S c) (S r) = ite (eq c r) (S Z) (sum (pascal (GEN r) (GEN c)) (pascal (GEN r) (S (GEN c))))

ite :: Bool -> a -> a -> a
ite True x _ = x
ite False _ y = y

eq :: Nat -> Nat -> Bool
eq Z Z = True
eq Z (S _) = False
eq (S _) Z = False
eq (S x) (S y) = eq x y

sum :: Nat -> Nat -> Nat
sum Z y = y
sum (S x) y = S (sum x y)    

[ go top ]