Jump to...
-
Off-line partial evaluator...
- Benchamark list
Example : a simple interpreter with a library
[ Original program ] [ Annotated program ] [ Specialized program ] [ Runtimes ]
This is another version of the simple interpreter program, this has a little difference, here our interpreter support function calls to a function set in a library, a typical use of the interpreter is:int program [variables] [values] [name_of_functions] [functions]
where functions parameter contains the body of each function, which its corresponding name is in name_of_functions, thus, at program, our library has a first function that calculates the square of an argument and other that computes the cube. The only allowed argument in library functions is represented by VarL . A call to a library function is done as follows:
(Call f a)
f represents the function name expressed as Peano natural numbers, a is the expression to be passed as argument, which should be a valid token, e.g. (Cst Z), (Plus (Cst (S Z)) (Var Z)), and so on. When a function is called its argument is computed in a new variable at variables list, the value computed is added to values. The local variable VarL is expanded to the new variable already created. Now the function body can be performed, and the rest of program processed.
In this example our main interest is specialize an interpreter w.r.t. a library, as it could be made with domain specific embedded languages.
import Benchmark (runBenchmark)
data Nat = Z | S Nat | E
data Token = Cst Nat | Var Nat | Plus Token Token | Minus Token Token | VarL Nat
| Mult Token Token | Call Nat Token
main x y z = int x y z [Z,(S Z)] [ (Mult (VarL Z) (VarL Z)),
(Mult (VarL Z) (Mult (VarL Z) (VarL Z))) ]
int :: Token -> [Nat] -> [Nat] -> [Nat]->[Token] -> Nat
int (Cst x ) _ _ _ _ = x
int (Var x ) vars vals _ _ = lookup x vars vals
int (Plus x y) vars vals fs lib = add (int x vars vals fs lib) (int y vars vals fs lib)
int (Minus x y) vars vals fs lib = minus (int x vars vals fs lib) (int y vars vals fs lib)
int (Mult x y) vars vals fs lib = mult (int x vars vals fs lib) (int y vars vals fs lib)
int (Call f a) vars vals fs lib =
int (expand (S(lengthP vars)) (lookupF f fs lib)) --change VarL for a new var
((S(lengthP vals)) : vars )
((int a vars vals fs lib): vals )
fs lib
lookup _ [] _ = E
lookup _ ( _:_) [] = E
lookup x (nv:nvs) (v:vs ) = ifte (eq x nv) v (lookup x nvs vs)
lookupF _ _ [] = Cst E
lookupF _ [] ( _:_) = Cst E
lookupF f (fn:fns) (b:bs) = ifte (eq f fn) b (lookupF f fns bs)
expand :: Nat-> Token -> Token
expand a (VarL _ ) = Var a
expand _ (Cst x ) = Cst x
expand a (Plus x y) = Plus (expand a x) (expand a y)
expand a (Minus x y) = Minus (expand a x) (expand a y)
expand a (Mult x y) = Mult (expand a x) (expand a y)
lengthP [] = Z
lengthP (_:xs) = S (lengthP xs)
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)
---------- tools ------------------
GEN x = x
bench = runBenchmark 10 (\_ -> print (x =:=
main (Mult (genPlus (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
(Call Z (Cst (S (S Z))))) [] [] ))
where x free
genMult (S Z) = (Cst (S(S Z)))
genMult (S (S n))= (Mult (genMult (S n)) (genMult (S n)))
genPlus (S Z) = (Cst (S Z))
genPlus (S (S n))= (Plus (genPlus (S n)) (genPlus (S n)) )
n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z =0
s2n (S n)= 1+ s2n n
The annotated program considering aspects of linearity and nested function calls is as follows:
import Benchmark (runBenchmark)
data Nat = Z | S Nat | E
data Token = Cst Nat | Var Nat | Plus Token Token | Minus Token Token
| VarL Nat | Mult Token Token | Call Nat Token
main x y z = int x y z [Z,(S Z)] [ (Mult (VarL Z) (VarL Z)),
(Mult (VarL Z) (Mult (VarL Z) (VarL Z))) ]
int :: Token -> [Nat] -> [Nat] -> [Nat]->[Token] -> Nat
int (Cst x ) _ _ _ _ = x
int (Var x ) vars vals _ _ = lookup x vars vals
int (Plus x y) vars vals fs lib = add (GEN (int x vars vals fs lib)) (GEN (int y vars vals fs lib))
int (Minus x y) vars vals fs lib = minus (GEN (int x vars vals fs lib)) (GEN (int y vars vals fs lib))
int (Mult x y) vars vals fs lib = mult (GEN (int x vars vals fs lib)) (GEN (int y vars vals fs lib))
int (Call f a) vars vals fs lib =
int
(GEN( expand (GEN (S(lengthP vars)) ) (GEN (lookupF f fs lib)) )) --change VarL to newVar
(GEN( (S (lengthP vals)) : vars ))
(GEN( (int a vars vals fs lib): vals ))
fs lib
lookup _ [] _ = E
lookup _ ( _:_) [] = E
lookup x (nv:nvs) (v:vs ) = ifte (GEN (eq x nv)) v (GEN (lookup x nvs vs ))
lookupF _ _ [] = Cst E
lookupF _ [] ( _:_) = Cst E
lookupF f (fn:fns) (b:bs) = ifte (GEN (eq f fn)) b (GEN (lookupF f fns bs))
expand :: Nat-> Token -> Token
expand a (VarL _ ) = Var a
expand _ (Cst x ) = Cst x
expand a (Plus x y) = Plus (expand a x) (expand (GEN a) y)
expand a (Minus x y) = Minus (expand a x) (expand (GEN a) y)
expand a (Mult x y) = Mult (expand a x) (expand (GEN a) y)
lengthP [] = Z
lengthP (_:xs) = S (lengthP xs)
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 (GEN (mult x y))
---------- tools ------------------
GEN x = x
bench = runBenchmark 10 (\_ -> print (x =:=
main (Mult (genPlus (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
(Call Z (Cst (S (S Z))))) [] [] ))
where x free
genMult (S Z) = (Cst (S(S Z)))
genMult (S (S n))= (Mult (genMult (S n)) (genMult (S n)))
genPlus (S Z) = (Cst (S Z))
genPlus (S (S n))= (Plus (genPlus (S n)) (genPlus (S n)) )
n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z =0
s2n (S n)= 1+ s2n n
Specialized program
[ go top ]
In PAKCS, loading OffPEval, and after of specialize with mix "examples/intWithLib", we bring the partially evaluated program thus:
prelude> :l intWithLib_pe
Compiled Curry program 'intWithLib_pe.pl' is up-to-date.
intWithLib_pe(module: intWithLib)> :show
No source program file available, generating source from FlatCurry...
-- Program file: intWithLib_pe
module intWithLib(Nat(Z,S,E),Token(Cst,Var,Plus,Minus,VarL,Mult,Call),int,lookup,lookupF,expand,
lengthP,eq,ifte,add,minus,mult,GEN,bench,genMult,genPlus,n2s,s2n,main,int_pe1,lookup_pe2,eq_pe4,
add_pe5,minus_pe6,mult_pe7,expand_pe8,lengthP_pe9) where
import Benchmark
data Nat = Z | S Nat | E
data Token = Cst Nat | Var Nat | Plus Token Token | Minus Token Token | VarL Nat
| Mult Token Token | Call Nat Token
int :: Token -> [Nat] -> [Nat] -> [Nat] -> [Token] -> Nat
int eval flex
int (Cst v5) v1 v2 v3 v4 = v5
int (Var v6) v1 v2 v3 v4 = lookup v6 v1 v2
int (Plus v7 v8) v1 v2 v3 v4 = add (GEN (int v7 v1 v2 v3 v4)) (GEN (int v8 v1 v2 v3 v4))
int (Minus v9 v10) v1 v2 v3 v4 = minus (GEN (int v9 v1 v2 v3 v4)) (GEN (int v10 v1 v2 v3 v4))
int (Mult v11 v12) v1 v2 v3 v4 = mult (GEN (int v11 v1 v2 v3 v4)) (GEN (int v12 v1 v2 v3 v4))
int (Call v13 v14) v1 v2 v3 v4 = int (GEN (expand (GEN (S (lengthP v1))) (GEN (lookupF v13 v3 v4))))
(GEN ((S (lengthP v2)) : v1)) (GEN ((int v14 v1 v2 v3 v4) : v2)) v3 v4
lookup :: Nat -> [Nat] -> [Nat] -> Nat
lookup eval flex
lookup v0 [] v2 = E
lookup v0 (v3 : v4) [] = E
lookup v0 (v3 : v4) (v5 : v6) = ifte (GEN (eq v0 v3)) v5 (GEN (lookup v0 v4 v6))
lookupF :: Nat -> [Nat] -> [Token] -> Token
lookupF eval flex
lookupF v0 v1 [] = Cst E
lookupF v0 [] (v3 : v4) = Cst E
lookupF v0 (v5 : v6) (v3 : v4) = ifte (GEN (eq v0 v5)) v3 (GEN (lookupF v0 v6 v4))
expand :: Nat -> Token -> Token
expand eval flex
expand v0 (VarL v2) = Var v0
expand v0 (Cst v3) = Cst v3
expand v0 (Plus v4 v5) = Plus (expand v0 v4) (expand (GEN v0) v5)
expand v0 (Minus v6 v7) = Minus (expand v0 v6) (expand (GEN v0) v7)
expand v0 (Mult v8 v9) = Mult (expand v0 v8) (expand (GEN v0) v9)
lengthP :: [a] -> Nat
lengthP eval flex
lengthP [] = Z
lengthP (v1 : v2) = S (lengthP v2)
eq :: Nat -> Nat -> Bool
eq eval flex
eq Z Z = True
eq Z (S v2) = False
eq (S v3) Z = False
eq (S v3) (S v4) = eq v3 v4
ifte :: Bool -> a -> a -> a
ifte eval flex
ifte True v1 v2 = v1
ifte False v1 v2 = v2
add :: Nat -> Nat -> Nat
add eval flex
add Z v1 = v1
add (S v2) v1 = S (add v2 v1)
minus :: Nat -> Nat -> Nat
minus eval flex
minus v0 Z = v0
minus (S v3) (S v2) = minus v3 v2
mult :: Nat -> Nat -> Nat
mult eval flex
mult Z v1 = Z
mult (S v2) v1 = add v1 (GEN (mult v2 v1))
GEN :: a -> a
GEN v0 = v0
bench :: IO ()
bench = Benchmark.runBenchmark 10 (intWithLib_lambda0_0 v0) where v0 free
genMult :: Nat -> Token
genMult eval flex
genMult (S Z) = Cst (S (S Z))
genMult (S (S v2)) = Mult (genMult (S v2)) (genMult (S v2))
genPlus :: Nat -> Token
genPlus eval flex
genPlus (S Z) = Cst (S Z)
genPlus (S (S v2)) = Plus (genPlus (S v2)) (genPlus (S v2))
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) = 1 + (s2n v1)
intWithLib_lambda0_0 :: Nat -> Int -> IO ()
intWithLib_lambda0_0 v0 v1 = print (v0 =:=
(main (Mult (genPlus (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
(Call Z (Cst (S (S Z)))))
[] [] ))
main :: d -> c -> b -> a
main v0 v1 v2 = int_pe1 v0 v1 v2
int_pe1 :: d -> c -> b -> a
int_pe1 eval flex
int_pe1 (Cst v319) v1 v2 = v319
int_pe1 (Var v320) v1 v2 = lookup_pe2 v320 v1 v2
int_pe1 (Plus v321 v322) v1 v2 = add_pe5 (int_pe1 v321 v1 v2) (int_pe1 v322 v1 v2)
int_pe1 (Minus v323 v324) v1 v2 = minus_pe6 (int_pe1 v323 v1 v2) (int_pe1 v324 v1 v2)
int_pe1 (Mult v325 v326) v1 v2 = mult_pe7 (int_pe1 v325 v1 v2) (int_pe1 v326 v1 v2)
int_pe1 (Call v327 v328) v1 v2 = int_pe1 (expand_pe8
(S (lengthP_pe9 ((S (lengthP_pe9 ((int_pe1 v328 v1 v2) : v2))) : v1)))
(fcase (eq_pe4 v327 Z) of
True -> Mult (VarL Z) (VarL Z)
False -> fcase (eq_pe4 v327 (S Z)) of
True -> Mult (VarL Z) (Mult (VarL Z) (VarL Z))
False -> Cst E
)) ((S (lengthP_pe9 ((int_pe1 v328 v1 v2) : v2))) : v1) ((int_pe1 v328 v1 v2) : v2)
lookup_pe2 :: d -> c -> b -> a
lookup_pe2 eval flex
lookup_pe2 v320 [] v2 = E
lookup_pe2 v320 (v409 : v410) [] = E
lookup_pe2 v320 (v409 : v410) (v411 : v412) = fcase (eq_pe4 v320 v409) of
True -> v411
False -> lookup_pe2 v320 v410 v412
eq_pe4 :: c -> b -> a
eq_pe4 eval flex
eq_pe4 Z Z = True
eq_pe4 Z (S v506) = False
eq_pe4 (S v507) Z = False
eq_pe4 (S v507) (S v508) = eq_pe4 v507 v508
add_pe5 :: c -> b -> a
add_pe5 eval flex
add_pe5 Z v328 = v328
add_pe5 (S v404) v328 = S (add_pe5 v404 v328)
minus_pe6 :: c -> b -> a
minus_pe6 eval flex
minus_pe6 v329 Z = v329
minus_pe6 (S v406) (S v405) = minus_pe6 v406 v405
mult_pe7 :: c -> b -> a
mult_pe7 eval flex
mult_pe7 Z v332 = Z
mult_pe7 (S v404) v332 = add_pe5 v332 (mult_pe7 v404 v332)
expand_pe8 :: c -> b -> a
expand_pe8 eval flex
expand_pe8 v334 (VarL v411) = Var v334
expand_pe8 v334 (Cst v412) = Cst v412
expand_pe8 v334 (Plus v413 v414) = Plus (expand_pe8 v334 v413) (expand_pe8 v334 v414)
expand_pe8 v334 (Minus v415 v416) = Minus (expand_pe8 v334 v415) (expand_pe8 v334 v416)
expand_pe8 v334 (Mult v417 v418) = Mult (expand_pe8 v334 v417) (expand_pe8 v334 v418)
lengthP_pe9 :: b -> a
lengthP_pe9 eval flex
lengthP_pe9 [] = Z
lengthP_pe9 (v403 : v404) = S (lengthP_pe9 v404)
-- end of module intWithLib_pe
We can observe the propagation of library functions in the interpreter rules. The benchmark proof is made applying a great program to the new specialized library_interpreter (int_pe1) .
| program | original runtime average | specialized runtime average | speed up |
|
intWithLib |
[ go to top ]