Appendix for Final
------------------

----------------------------------------------------------------------
Fig 3.7: abstract syntax of Fun
----------------------------------------------------------------------

   v ::= x, y, z, ...    (alphanumeric variables)
   n ::= 0, 1, 2, ...    (natural numbers)
   b ::= true, false     (boolean values)

   prim ::= Plus, Times, Minus, ...  (primitive arithmetic operators)
            Eq, LT, GT, ...          (primitive relational operators)
   
   e ::=  Num(n) | Bool(b) | Var(v)
       |  Bapp(prim, e, e)
       |  If(e, e, e)
       |  Let(v, e, e)
       |  Fun(v, e)
       |  App(e, e)


------------------------------------------------------------ 
Fun[CEKv]
------------------------------------------------------------ 
Values: 

    v ::=  NUM(n)
        |  BOOL(b)
        |  FUN(x, e, E)   -- function closure

Frames: 

    f ::=  Bapp(prim, [], e2, E) | Bapp*(prim, n, [])
        |  Let(v, [], e2, E)
        |  If([], e1, e2, E)
        |  App([], e2, E)
        |  App*(v1, [])

Stack/Context:

    k = nil | f :: k

Environments: E ∈ env = (variable * value) list
    emptyEnv : env = []
    look : variable * env -> Nat
       look (v, []) = undef
       look (v, ((v',n):env)) = if v=v' then n else look(v, env)
    bind : variable * Nat * env -> env
       bind (v, n, env) = (v,n)::env

States: the state set consists of two components:

   (e, E, k)   - states where we are beginning to evaluate expr e
   (v, k)      - where we are returning value v as an intermediate result

We can distinguish these two forms by calling the first "expression
states", abbreviated as "e-states",and the second form "value states"
or "v-states".

Transition Rules:

(1)  (Bapp(bop,e1,e2), E, k)             =>  (e1, E, Bapp(bop,[],e2,E)::k)

(2)  (NUM(n), Bapp(prim,[],e2,E')::k)    =>  (e2, E', Bapp*(prim,n,[])::k)

(3)  (NUM(n), Bapp*(prim,NUM(m),[])::k)  =>  (NUM(p), k)
      where p = prim(prim,m,n)

(4)  (Let(x,e1,e2), E, k)                =>  (e1, E, Let(x,[],e2,E)::k)

(5)  (v, Let(x,[],e2,E')::k)             =>  (e2, bind(x,v,E'), k)

(6)  (If(e1,e2,e3), E, k)                =>  (e1, E, If([],e2,e3,E)::k)

(7)  (BOOL(true), If([],e2,e3,E')::k)    =>  (e2, E', k)

(8)  (BOOL(false), If([],e2,e3,E')::k)   =>  (e3, E', k)

(9)  (App(e1,e2), E, k)                  =>  (e1, E, App([],e2,E)::k)

(10) (v, App([],e2,E')::k)               =>  (e2, E', App*(v,[])::k)

(11) (v, App*(FUN(x,e,E),[])::k)         =>  (e, bind(x,v,E), k)

(12) (Var(x), E, k)                      =>  (look(x,E), k)

(13) (Num n, E, k)                       =>  (NUM n, k)

(14) (Bool b, E, k)                      =>  (BOOL b, k)

(15) (Fun(x,e), E, k)                    =>  (FUN(x,e,E), k)


Here we find that the transitions can be characterized as follows:

  e-state => e-state:  (1), (4), (7), (9)

    the analysis transitions

  e-state => v-state:  (12), (13), (14), (15)
    
    evaluating variables and "value expressions"

  v-state => v-state:  (3)                    

    reducing Bapp redexes

  v-state => e-state:  (2), (5), (7), (8), (10), (11)

    shift transitions ((2), (10)) and reductions ((5), (7), (8), (11))