
The "imperative-solve.power" Benchmark

   Part of the DPPD Library.
   
  General Description
  
   The program to be specialised is a solver for a small imperative
   language which uses environments to store values for variables. The
   program contains built-ins and negations. The task is to specialise a
   sub-program calculating the power (X^Y) for a known power and base but
   an unknown environment.
   
  The benchmark program
  
store([],Key,Value,[Key/Value]).
store([Key/Value2|T],Key,Value,[Key/Value|T]).
store([Key2/Value2|T],Key,Value,[Key2/Value2|BT]) :-
   Key \== Key2,
   store(T,Key,Value,BT).

lookup(Key,[Key/Value|T],Value).
lookup(Key,[Key2/Value2|T],Value) :-
   Key \== Key2,
   lookup(Key,T,Value).

power(Base,Power,E1,EOut) :-
        execute_statement(let(base,Base),E1,E2),
        execute_statement(let(power,Power),E2,E3),
        execute_statement(seq(seq(let(x,1),let(result,var(base))),
                           while_do('<'(var(x),var(power)),
                              seq(let(x,'+'(var(x),1)),
                                  let(result,'*'(var(result),var(base)))))),
                                           E3,EOut).

execute_statement(null,Env,Env).
execute_statement(let(V,Expr),Env,NEnv) :-
        eval_expression(Expr,Env,Val),
        store(Env,V,Val,NEnv).
execute_statement(if(Tst,Thn,Els),Env,NEnv) :-
        eval_test(Tst,Env,Bool),
        execute_cond_continuation(Bool,Thn,Els,Env,NEnv).
execute_statement(repeat_until(Loop,Tst),Env,NEnv) :-
        execute_statement(Loop,Env,IntEnv),
        eval_test(Tst,IntEnv,Bool),
        execute_cond_continuation(Bool,null,repeat_until(Loop,Tst),IntEnv,NEnv)
.
execute_statement(while_do(Tst,Loop),Env,NEnv) :-
        eval_test(Tst,Env,Bool),
        execute_cond_continuation(Bool,seq(Loop,while_do(Tst,Loop)),
                                        null,Env,NEnv).
execute_statement(seq(St1,St2),Env,NEnv) :-
        execute_statement(St1,Env,IntEnv),
        execute_statement(St2,IntEnv,NEnv).

execute_cond_continuation(true,Thn,Els,Env,NEnv) :-
        execute_statement(Thn,Env,NEnv).
execute_cond_continuation(false,Thn,Els,Env,NEnv) :-
        execute_statement(Els,Env,NEnv).
        
eval_test('<'(X,Y),Env,Bool) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        get_bool(VX < VY,Bool).
eval_test('=<'(X,Y),Env,Bool) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        get_bool(VX =< VY,Bool).
eval_test('>'(X,Y),Env,Bool) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        get_bool(VX > VY,Bool).
eval_test('>='(X,Y),Env,Bool) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        get_bool(VX >= VY,Bool).

get_bool(Tst,true) :- call(Tst).
get_bool(Tst,false) :- not(call(Tst)).

eval_expression(X,Env,X) :-
        integer(X).
eval_expression(var(V),Env,Val) :-
        lookup(V,Env,Val).
eval_expression('+'(X,Y),Env,Val) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        Val is VX + VY.
eval_expression('-'(X,Y),Env,Val) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        Val is VX - VY.
eval_expression('*'(X,Y),Env,Val) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        Val is VX * VY.
eval_expression('/'(X,Y),Env,Val) :-
        eval_expression(X,Env,VX),
        eval_expression(Y,Env,VY),
        Val is VX / VY.

  The partial deduction query
  
 :- power(2,5,Ein,Eout).

  The run-time queries
  
 :- power(2,5,[],Eout).
 :- power(2,5,[z/1,y/3],Eout).

  Example solution
  
to be inserted
     _________________________________________________________________
   
   
    Michael Leuschel / K.U. Leuven / michael@cs.kuleuven.ac.be
