Continuation rules for the implicit-refs machine

================================================================

Expressions:

e ::= n | -(e1,e2)
      zero?(e1) | if e1 then e2 else e3
      x | let x = e1 in e2 | proc(x)e | (e1 e2)
      letrec {f(x)=e}* in e
      begin e; e* end
      set x = e
      //---additional expression forms introduced by substitution---//
      %location(n)       // location values  {loc ranges over
      			       expressions of this form}
      %true              // boolean values
      %false             // 
      %set1(e1,e2)       // substituted a %loc(n) for a variable in a
                         // set!

Special cases:

(set x = e)[v/x] = %set1(v, e[v/x])
letrec D in e -> e[f_i |-> proc (x_i) letrec D in e_i]_i
  where D = (f_i x_i e_i)_i

Configurations:

C ::= <e, s>   where e is an expression and s is a store

================================================================

Values:

v ::= n 
      proc(x)e           // must be closed
      %true, %false
      %location(n)

================================================================

Frames and Reduction Contexts:

F ::= -([],e)		// diff1-frame
      -(v,[])		// diff2-frame
      zero?([])		// zero?-frame
      if [] then e1 else e2   // if-test-frame
      let id=[] in e2  	// let-rhs-frame
      ([] e2) 	   	// app-rator-frame
      (v [])		// app-rand-frame
      begin [] e* end	// begin-frame
      set loc = []  	// assign-rhs-frame

K = F*


================================================================

Machine transition rules (in the alternate grouping)

focus-down <K, n, s>              -> focus-up <K, n, s>
focus-down <K, proc(x)e, s>       -> focus-up <K, proc(x)e, s>
focus-down <K, %true, s> 	  -> focus-up <K, %true, s>
focus-down <K, %false, s>	  -> focus-up <K, %false, s>
focus-down <K, loc(n), s>         -> focus-up <K, s(n), s>

focus-down <K, letrec D in e, s>  -> focus-down <K, reduce-letrec(e,D), s> (see defn above)

focus-up <[], v, s>               -> v

focus-down <K, -(e1,e2),s>        -> focus-down <K o -([],e2), e1, s>
focus-up   <K o -([],e2), v1, s>  -> focus-down <K o -(v1,[]), e2, s>
focus-up   <K o -(v1,[]), v2, s>  -> focus-up   <K, p, s>  where p = v1-v2

focus-down <K, zero?(e1), s>      -> focus-down <K o zero?([]), e1, s>
focus-up   <K o zero?([]), v1, s> -> focus-up   <K, %true, s>   {or <K, %false, s>}

focus-down <K, if(e1,e2,e3), s>      -> focus-down <K o if([],e2,e3), e1, s>
focus-up   <K o if([],e2,e3), v1, s> -> focus-down <K, e2, s>   {or <K, e3, s>}

focus-down <K, let x=e1 in e2, s>      -> focus-down <K o let x=[] in e2, e1, s>
focus-up   <K o let x=[] in e2, v1, s> -> focus-down <K, e2[n/x], s[v1/n]>  where n is new in s.

focus-down <K, (e1 e2), s>             -> focus-down <K o ([] e2), e1, s>
focus-up   <K o ([] e2), v1, s>        -> focus-down <K o (v1 []), e2, s>
focus-up   <K o (proc(x)e []), v2, s>  -> focus-down <K, e2[n/x], s[v2/n]>  where n is new in s.

focus-down <K, begin e1 e* end, s>         -> focus-down <K o begin [] e*, e1, s>
focus-up   <K o begin [] empty, v1, s>     -> focus-up <K, v1, s>
focus-up   <K o begin [] (e2 . e*), v1, s> -> focus-down <K o begin [] e*, e2, s>

focus-down <K, set loc=e1, s>              -> focus-down <K o set loc=[], e1, s>
focus-up   <K o set loc=[], %loc(n), s>    -> focus-up <K, 27, s[v/n]>

================================================================