Institute of Computer Science
Faculty of Engineering, Christian-Albrechts-University of Kiel
| Computer-Aided Program
Development Institute of Computer Science Faculty of Engineering, Christian-Albrechts-University of Kiel |
|
| RAP Examples - A Small Compiler |
{***********************************************************************}
{* ABSTRACT SYNTAX SOURCE LANGUAGE *}
{***********************************************************************}
type EXPRESSION
basedon ID, NAT
sort Expr, Op
cons ad, su, mu : Op,
nexpr : (Nat)Expr,
iexpr : (Id)Expr,
comp : (Expr,Op,Expr)Expr
endoftype
complete EXPRESSION
display EXPRESSION nexpr = "_",
iexpr = "_",
comp = "(_ _ _)",
ad = "+",
su = "-",
mu = "*"
{***********************************************************************}
{* ENVIRONMENT *}
{***********************************************************************}
type ENVIRONMENT
basedon ID, NAT, BOOL
sort Env
cons init : Env,
update : (Env,Id,Nat)Env
func sel : (Env,Id)Nat,
isdef : (Env,Id)Bool
axioms all (i,j : Id, e : Env, n : Nat)
equal_Id(i,j) = false => sel(update(e,i,n),j) -> sel(e,j),
sel(update(e,i,n),i) -> n,
isdef(init,i) -> false,
equal_Id(i,j) = false => isdef(update(e,i,n),j) -> isdef(e,j),
isdef(update(e,i,n),i) -> true
endoftype
complete ENVIRONMENT except sel
noetherian ENVIRONMENT
{***********************************************************************}
{* SEMANTICS SOURCE LANGUAGE *}
{***********************************************************************}
type SSEMANTICS
basedon ID, NAT, EXPRESSION, ENVIRONMENT
func ssem : (Env,Expr)Nat
axioms all (e : Env, l, r : Expr, i : Id, n : Nat)
ssem(e,nexpr(n)) -> n,
ssem(e,iexpr(i)) -> sel(e,i)
ssem(e,comp(l,ad,r)) -> add(ssem(e,l),ssem(e,r)),
ssem(e,comp(l,su,r)) -> sub(ssem(e,l),ssem(e,r)),
ssem(e,comp(l,mu,r)) -> mult(ssem(e,l),ssem(e,r))
endoftype
complete SSEMANTICS
noetherian SSEMANTICS
{***********************************************************************}
{* SEMANTICS OF A SAMPLE EXPRESSION *}
{***********************************************************************}
task SSEM
basedon ID, NAT, EXPRESSION, ENVIRONMENT, SSEMANTICS
unknown env : Env, source_expr : Expr, value : Nat
goals env = update(update(init,'x,3),'y,5),
source_expr = comp(comp(nexpr(3), mu, iexpr('x)),
ad,
comp(nexpr(6), mu, iexpr('y))),
value = ssem(env, source_expr)
endoftask
{***********************************************************************}
{* ABSTRACT SYNTAX TARGET LANGUAGE *}
{***********************************************************************}
type SEQUINSTRUCTION
basedon ID, NAT, BOOL
sort Instr, SequInstr
cons ADD, SUB, MUL : Instr,
NST : (Nat)Instr,
IST : (Id)Instr,
emptysequ : SequInstr,
prefix : (Instr,SequInstr)SequInstr
func first : (SequInstr)Instr,
rest : (SequInstr)SequInstr,
isemptysequ : (SequInstr)Bool,
postfix : (SequInstr,Instr)SequInstr,
conc : (SequInstr,SequInstr)SequInstr
axioms all (s, t : SequInstr, i, j : Instr)
first(prefix(i,s)) -> i,
rest(prefix(i,s)) -> s,
isemptysequ(emptysequ) -> true,
isemptysequ(prefix(i,s)) -> false,
conc(emptysequ,t) -> t,
conc(prefix(i,s),t) -> prefix(i,conc(s,t)),
postfix(s,i) -> conc(s,prefix(i,emptysequ))
endoftype
complete SEQUINSTRUCTION except first, rest
noetherian SEQUINSTRUCTION
display SEQUINSTRUCTION NST = "NST _ ",
IST = "IST _",
ADD = "ADD ",
SUB = "SUB ",
MUL = "MUL ",
prefix = "_ &\_",
postfix = "_ &\_",
conc = "_ &\_",
emptysequ = "<>",
isemptysequ = "_=<>"
{***********************************************************************}
{* SEMANTICS TARGET LANGUAGE *}
{***********************************************************************}
type NATSTACK
basedon NAT, BOOL
sort Stack
cons emptystack : Stack,
append : (Nat,Stack)Stack
func top : (Stack)Nat,
pop : (Stack)Stack,
isemptystack : (Stack)Bool
axioms all (s : Stack, n : Nat)
top(append(n,s)) -> n,
pop(append(n,s)) -> s,
isemptystack(emptystack) -> true,
isemptystack(append(n,s)) -> false
endoftype
complete NATSTACK except top, pop
noetherian NATSTACK
display NATSTACK emptystack = "<>",
isemptystack = "_=<>"
type TSEMANTICS
basedon ID, NAT, ENVIRONMENT, SEQUINSTRUCTION, NATSTACK
func tsem : (Env,SequInstr)Nat,
ts : (Env,SequInstr,Stack)Stack
axioms all (e : Env, s : SequInstr, k : Stack, i : Id, n : Nat)
tsem(e,s) -> top(ts(e,s,emptystack))
ts(e,prefix(NST(n),s),k)
-> ts(e,s,append(n,k)),
ts(e,prefix(IST(i),s),k)
-> ts(e,s,append(sel(e,i),k)),
ts(e,prefix(ADD,s),k)
-> ts(e,s,append(add(top(pop(k)),top(k)),pop(pop(k)))),
ts(e,prefix(SUB,s),k)
-> ts(e,s,append(sub(top(pop(k)),top(k)),pop(pop(k)))),
ts(e,prefix(MUL,s),k)
-> ts(e,s,append(mult(top(pop(k)),top(k)),pop(pop(k)))),
ts(e,emptysequ,k)
-> k
endoftype
complete TSEMANTICS
noetherian TSEMANTICS
{***********************************************************************}
{* SEMANTICS OF A SAMPLE SEQUENCE *}
{***********************************************************************}
task TSEM
basedon ID, NAT, ENVIRONMENT, SSEMANTICS, SEQUINSTRUCTION, TSEMANTICS
unknown env : Env, program : SequInstr, result : Nat
goals env = update(update(init,'x,3),'y,5),
program = prefix(NST(3),
prefix(IST('x),
prefix(MUL,
prefix(NST(4),
prefix(ADD, emptysequ))))),
result = tsem(env, program)
endoftask
{***********************************************************************}
{* COMPARISON OF SOURCE SEMANTICS AND TARGET SEMANTICS *}
{***********************************************************************}
task STSEM
basedon ID, NAT, EXPRESSION, ENVIRONMENT, SSEMANTICS,
SEQUINSTRUCTION, TSEMANTICS
unknown env : Env, source_expr : Expr, target_program : SequInstr,
value, result : Nat
goals env = update(update(init,'x,3),'y,5),
source_expr = comp(comp(nexpr(3), mu, iexpr('x)),
ad,
comp(nexpr(6), mu, iexpr('y))),
target_program = prefix(NST(3),
prefix(IST('x),
prefix(MUL,
prefix(NST(6),
prefix(IST('y),
prefix(MUL,
prefix(ADD, emptysequ))))))),
value = ssem(env, source_expr),
result = tsem(env, target_program)
endoftask
{***********************************************************************}
{* CODE GENERATION *}
{***********************************************************************}
type COMPILER
basedon ID, NAT, EXPRESSION, SEQUINSTRUCTION
func compile : (Expr)SequInstr
axioms all (l, r : Expr, i : Id, n : Nat)
compile(nexpr(n)) -> postfix(emptysequ,NST(n)),
compile(iexpr(i)) -> postfix(emptysequ,IST(i)),
compile(comp(l,ad,r)) -> postfix(conc(compile(l),compile(r)),ADD),
compile(comp(l,su,r)) -> postfix(conc(compile(l),compile(r)),SUB),
compile(comp(l,mu,r)) -> postfix(conc(compile(l),compile(r)),MUL)
endoftype
complete COMPILER
noetherian COMPILER
{***********************************************************************}
{* EXAMPLE OF COMPILATION *}
{***********************************************************************}
task COMP
basedon ID, NAT, EXPRESSION, SEQUINSTRUCTION, COMPILER
unknown source_expr : Expr, target_program : SequInstr
goals source_expr = comp(nexpr(9),su,comp(nexpr(2),ad,nexpr(3))),
target_program = compile(source_expr)
endoftask
{***********************************************************************}
{* PARTIAL EVALUATION *}
{***********************************************************************}
type PARTEVAL
basedon ID, NAT, SEQUINSTRUCTION
func pev : (SequInstr)SequInstr,
pv : (SequInstr,SequInstr)SequInstr,
rev : (SequInstr)SequInstr
axioms all (l, s : SequInstr, x : Instr, i : Id, m, n, p : Nat)
pev(s) -> rev(pv(emptysequ,s)),
rev(emptysequ) -> emptysequ,
rev(prefix(x,s)) -> postfix(rev(s),x)
pv(l,emptysequ) -> l,
pv(l,prefix(NST(n),emptysequ)) -> prefix(NST(n),l),
pv(l,prefix(IST(i),s)) -> pv(prefix(IST(i),l),s),
pv(l,prefix(ADD,s)) -> pv(prefix(ADD,l),s),
pv(l,prefix(SUB,s)) -> pv(prefix(SUB,l),s),
pv(l,prefix(MUL,s)) -> pv(prefix(MUL,l),s),
pv(l,prefix(NST(m),prefix(NST(n),emptysequ)))
-> prefix(NST(n),prefix(NST(m),l)),
pv(l,prefix(NST(m),prefix(IST(i),s)))
-> pv(prefix(NST(m),l),prefix(IST(i),s)),
pv(l,prefix(NST(m),prefix(ADD,s)))
-> pv(prefix(NST(m),l),prefix(ADD,s)),
pv(l,prefix(NST(m),prefix(SUB,s)))
-> pv(prefix(NST(m),l),prefix(SUB,s)),
pv(l,prefix(NST(m),prefix(MUL,s)))
-> pv(prefix(NST(m),l),prefix(MUL,s)),
pv(l,prefix(NST(m),prefix(NST(n),prefix(NST(p),s))))
-> pv(prefix(NST(m),l),prefix(NST(n),prefix(NST(p),s))),
pv(l,prefix(NST(m),prefix(NST(n),prefix(IST(i),s))))
-> pv(prefix(NST(m),l),prefix(NST(n),prefix(IST(i),s))),
pv(emptysequ,prefix(NST(m),prefix(NST(n),prefix(ADD,s))))
-> pv(emptysequ,prefix(NST(add(m,n)),s)),
pv(emptysequ,prefix(NST(m),prefix(NST(n),prefix(SUB,s))))
-> pv(emptysequ,prefix(NST(sub(m,n)),s)),
pv(emptysequ,prefix(NST(m),prefix(NST(n),prefix(MUL,s))))
-> pv(emptysequ,prefix(NST(mult(m,n)),s)),
pv(prefix(x,l),prefix(NST(m),prefix(NST(n),prefix(ADD,s))))
-> pv(l,prefix(x,prefix(NST(add(m,n)),s))),
pv(prefix(x,l),prefix(NST(m),prefix(NST(n),prefix(SUB,s))))
-> pv(l,prefix(x,prefix(NST(sub(m,n)),s))),
pv(prefix(x,l),prefix(NST(m),prefix(NST(n),prefix(MUL,s))))
-> pv(l,prefix(x,prefix(NST(mult(m,n)),s)))
endoftype
complete PARTEVAL
noetherian PARTEVAL
{***********************************************************************}
{* SAMPLE TASKS FOR COMPILATION AND DECOMPILATION *}
{***********************************************************************}
task COMP_PE
basedon ID, NAT, EXPRESSION, SEQUINSTRUCTION, COMPILER, PARTEVAL
unknown source_expr : Expr, target_program, part_eval_prog : SequInstr
goals source_expr = comp(comp(iexpr('y),
mu,
comp(nexpr(9),
su,
comp(nexpr(2),ad,nexpr(3)))),
ad,
comp(nexpr(1),
ad,
comp(nexpr(2),
mu,
comp(nexpr(3),su,nexpr(1))))),
target_program = compile(source_expr),
part_eval_prog = pev(target_program)
endoftask
task DECOMP
basedon COMPILER, EXPRESSION, SEQUINSTRUCTION, ID, NAT
unknown source_expr : Expr, target_program : SequInstr
goals target_program = prefix(NST( 3),
prefix(IST('x),
prefix(MUL,
prefix(NST( 4),
prefix(ADD, emptysequ))))),
compile(source_expr) = target_program
endoftask
task DECOMPOPT
basedon COMPILER, PARTEVAL, EXPRESSION, SEQUINSTRUCTION, ID, NAT
unknown source_expr : Expr, target_program : SequInstr
goals target_program = prefix(NST(3), emptysequ),
pev(compile(source_expr)) = target_program
endoftask
task DEOPT
basedon PARTEVAL, SEQUINSTRUCTION, NAT
unknown source_sequ, part_eval_sequ : SequInstr
goals part_eval_sequ = prefix(NST(3), emptysequ),
pev(source_sequ) = part_eval_sequ
endoftask