Computer-Aided Program Development
Institute of Computer Science
Faculty of Engineering, Christian-Albrechts-University of Kiel
Logo of the Working Group
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


 
Rudolf Berghammer - rub@informatik.uni-kiel.de
Last modified: 31-Jul-2012, 14:17:23 CEST