type expr = Var of int
          | Fun of (int * expr)
          | App of (expr * expr)
          | Update of (int * expr)
          | Cl of (int * expr * env)
and env = (int * int) list
and mem = (int * expr) list

exception LookupFailed

let rec lookup m x = match m with
	[] -> raise LookupFailed
	| (y, v)::m2 -> if (x = y) then v else lookup m2 x

let lookup_mem = lookup
let lookup_addr = lookup

let rec lookup_env n m x = match n with
	[] -> Var x
	| (y, a)::n2 -> if (x = y) then (lookup_mem m a) else lookup_env n2 m x

let init_addr = ref 0

let new_address () =
	let a = !init_addr in
		init_addr := a + 1; a

let rec eval (n : env) (m : mem) e = match e with
(*
	Note: => used in place of \Downarrow

	a = lookup_env(n, x)  v = lookup_mem(m, a)
	------------------------------------------
	(n, m, x) => (m, v)
*)
	Var x -> (m, (lookup_env n m x))
(*
	------------------------------------
	(n, m, ,\ x . e) => (m, Cl(x, e, n))
*)
	| Fun (x, e) -> (m, Cl (x, e, n))
(*
	(n, m, e1) => (m', Cl(x, e, n'))  (n, m', e2) => (m'', v)  (n'', m'', e) => (m''', v')
	--------------------------------------------------------------------------------------
	(n, m, e1 e2) => (m''', v')

	where n'' = (x, v)::n'
*)
	| App (e1, e2) ->
		let (m1, v1) = eval n m e1 in
		let (m2, v2) = eval n m1 e2 in
			(match v1 with
			Cl (x, e, n1) ->
				let a = new_address () in
				let n2 = (x, a)::n1 in
				let m3 = (a, v2)::m2 in
					eval n2 m3 e
			| _ -> (m2, App (v1, v2)))
(*
	(n, m, e) => (m', v)  a = lookup(n, x)
	--------------------------------------
	(n, m, x := e) => ((a, v)::m', v)
*)
	| Update (x, e) ->
		let (m2, v) = eval n m e
		and a = lookup_addr n x
		in
			((a, v)::m2, v)
	| e -> (m, e)