Smallstep 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!

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 l = []  	// assign-rhs-frame

K = F*

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

Reductions on expressions:

-(n1,n2)-> p    (if p = n1-n2) 

if %true then e1 else e2 -> e1

if %false then e1 else e2 -> e2

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

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

Reductions on configurations:

       l -> r
--------------------      Ordinary reductions lift to configurations
<K[l],s> -> <K[r],s>

Store operations:

<K[loc(n)],s> -> <K[v],s>  where v = s(n)

<K[(proc(x)e v)], s> -> <K[e[loc(n)/x]], s[v/n]>  where n not in dom(s).

<K[let x=v in e], s> -> <K[e[loc(n)/x]], s[v/n]>  where n not in dom(s).

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