datatype lamexp with (sb, nat) =
    {n:nat | n > 0} One(0,n)
  | {n:nat} Int(0,n) of int
  | {b1:sb,b2:sb,b3:sb,n:nat}
    Ifz(0,n) of lamexp(b1,n) * lamexp(b2,n) * lamexp(b3,n)
  | {b1:sb,b2:sb,n:nat} Add(0,n) of lamexp(b1,n) * lamexp(b2,n)
  | {b1:sb,b2:sb,n:nat} Sub(0,n) of lamexp(b1,n) * lamexp(b2,n)
  | {b1:sb,b2:sb,n:nat} Mul(0,n) of lamexp(b1,n) * lamexp(b2,n)
  | {b1:sb,b2:sb,n:nat} Div(0,n) of lamexp(b1,n) * lamexp(b2,n)
  | {b:sb,n:nat} Shift(0,n+1) of lamexp(b,n)
  | {b:sb,n:nat | n >= 1} Lam(1,n-1) of lamexp(b,n)
  | {b1:sb,b2:sb,n:nat} App(0,n) of lamexp(b1,n) * lamexp(b2,n)
  | {b:sb,n:nat | n >= 2} Fix(1,n-2) of lamexp(b,n)

datatype closure =
    Cint of int
  | {n:nat} Cfun of lamexp(1,n) * closure list(n)

fun evaluate (e) =
    let
        fun eval (One, c :: _) = c
	  | eval (e as Int n, _) = Cint n
	  | eval (Ifz (e0, e1, e2), env) =
	    let
		val Cint n = eval (e0, env)
	    in
		if n = 0 then eval (e1, env) else eval (e2, env)
	    end
	  | eval (Add (e1, e2), env) =
	    let
		val Cint n1 = eval (e1, env)
		val Cint n2 = eval (e2, env)
	    in
		Cint (n1 + n2)
	    end
	  | eval (Sub (e1, e2), env) =
	    let
		val Cint n1 = eval (e1, env)
		val Cint n2 = eval (e2, env)
	    in
		Cint (n1 - n2)
	    end
	  | eval (Mul (e1, e2), env) =
	    let
		val Cint n1 = eval (e1, env)
		val Cint n2 = eval (e2, env)
	    in
		Cint (n1 * n2)
	    end
	  | eval (Div (e1, e2), env) =
	    let
		val Cint n1 = eval (e1, env)
		val Cint n2 = eval (e2, env)
	    in
		Cint (n1 / n2)
	    end
          | eval (Shift e, _ :: env) = eval (e, env)
          | eval (e as Lam _, env) = Cfun (e, env)
          | eval (App (e1, e2), env) =
            let
                val clo1 = eval (e1, env)
                val clo2 = eval (e2, env)
            in
		case clo1 of
		    Cfun(Lam body, env') => eval (body, clo2 :: env')
		  | Cfun(Fix body, env') => eval (body, clo2 :: clo1 :: env')
            end
	  | eval (e as Fix _, env) = Cfun (e, env)
        withtype {b:sb,n:nat} lamexp(b,n) * closure list(n) -> closure
    in
        eval (e, [])
    end
withtype {b:sb} lamexp(b,0) -> closure

val two = Shift (One: lamexp (0,1))

val fact =
    Fix (Ifz ((One:lamexp(0,2)),
	      Int 1, Mul (App (two, Sub (One, Int 1)), One)))

val ans = evaluate (App (fact, Int 10))