[an error occurred while processing this directive]
{***********************************************************************} {* 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[an error occurred while processing this directive] 31-Jul-2012, 14:17:23 CEST