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

Jump to...

- schg page

Example: a simple functional interpreter

[ Original program ]  [ Annotated program ]

Original program

Here we present a simple functional interpreter which computes arithmetic programs. The instructions of such programs are expressions  that contain natural numbers (as constants) or  variables (where their values are natural numbers too).

 
         
data Nat    =  Z | S Nat | E
data Token  =  Cst Nat   | Var Nat  |  Plus Token Token  |  Minus Token Token
                                                         |  Mult  Token Token
 
 

int :: Token -> [Nat] -> [Nat]    -> Nat
int (Cst   x  ) _    _      =  x
int (Var   x  ) vars vals   =  lookup  x  vars  vals
int (Plus  x y) vars vals   =  add     (int x vars vals ) (int y vars vals )
int (Minus x y) vars vals   =  minus   (int x vars vals ) (int y vars vals )
int (Mult  x y) vars vals   =  mult    (int x vars vals ) (int y vars vals )

lookup   _    []    ( _:_)  = E   
lookup   _ ( _:_ )    []    = E 
lookup   x (nv:nvs) (v:vs)  = ifte (eq x nv)  v  (lookup  x nvs vs )


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

ifte True  x  _ = x
ifte False _  y = y

add Z      y = y
add (S x)  y = S(add x y)

minus     x    Z  =  x 
minus  (S x) (S y)= minus x y

mult  Z    _ = Z
mult (S x) y = add y (mult x y)
        

Annotated program [ go top ]

Below, the annotated program. All annotations are introduced due to right linearity violations.

 
module interMineS where

data Nat
     = Z
     | S Nat
     | E

data Token
     = Cst Nat
     | Var Nat
     | Plus Token Token
     | Minus Token Token
     | Mult Token Token

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

int :: Token -> [Nat] -> [Nat] -> Nat
int (Cst x) _ _ = x
int (Var x) vars vals = lookup x vars vals
int (Plus  x y) vars vals = add   (int x vars vals) (int y (GEN vars) (GEN vals))
int (Minus x y) vars vals = minus (int x vars vals) (int y (GEN vars) (GEN vals))
int (Mult  x y) vars vals = mult  (int x vars vals) (int y (GEN vars) (GEN vals))

lookup :: Nat -> [Nat] -> [Nat] -> Nat
lookup _ [] (_:_) = E
lookup _ (_:_) [] = E
lookup x (nv:nvs) (v:vs) = ifte (eq x nv) v (lookup (GEN x) nvs vs)

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

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

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

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

mult :: Nat -> Nat -> Nat
mult  Z    _ = Z
mult (S x) y = add y (mult x (GEN y))

[ go top ]