To specialize the monadic interpreter to a given program we add two levels of staging annotations. The result of the first stage is the intermediate code, that if executed returns the value of the program. The use of the bracket annotation enables us to describe precisely the code that must be generated to run in the next stage. Escape annotations allow us to escape the recursive calls of the interpreter that are made when compiling a while-program.
(* eval2: Exp -> index -> <int M> *)
fun eval2 exp index =
case exp of
Constant n => <Return mswo ~(lift n)>
| Variable x =>
let val loc = position x index
in <read ~(lift loc)> end
| Minus(x,y) =>
<Do mswo { a <- ~(eval2 x index) ;
b <- ~(eval2 y index);
Return mswo (a - b) }>
| Greater(x,y) =>
<Do mswo { a <- ~(eval2 x index) ;
b <- ~(eval2 y index);
Return mswo (if a '>' b
then 1
else 0) }>
| Times(x,y) =>
<Do mswo { a <- ~(eval2 x index) ;
b <- ~(eval2 y index);
Return mswo (a * b) }>;
The lift operator inserts the value of loc as the argument to the read action. The value of loc is known in the first-stage (compile-time), so it is transformed into a constant in the second-stage (run-time) by lift.
To understand why the escape operators are necessary, let us consider a simple example: eval2 (Minus(Constant 3,Constant 1)) []. We will unfold this example by hand below:
eval2 (Minus(Constant 3,Constant 1)) [] =
< Do mswo
{ a <- ~(eval2 (Constant 3) []);
b <- ~(eval2 (Constant 1) []);
Return mswo (a-b)} > =
< Do mswo
{ a <- ~<Return mswo 3>;
b <- ~<Return mswo 1>;
Return mswo (a - b)} > =
< Do mswo
{ a <- Return mswo 3;
b <- Return mswo 1;
Return mswo (a - b)} > =
< Do %mswo
{ a <- Return %mswo 3;
b <- Return %mswo 1;
Return %mswo (a %- b)} >
Each recursive call produces a bracketed piece of code which is spliced into the larger piece being constructed. Recall that escapes may only appear at level-1 and higher. Splicing is axiomatized by the reduction rule: <x> x, which applies only at level-1. The final step, where mswo and - become %mswo and %-, occurs because both are free variables and are lexically captured.