type lam = | Var of atom | Lam of < atom * inner lam > (*latex \label{line:def:Lam} *) | App of lam * lam type sem = | L of < env * atom * inner lam > (*latex \label{line:def:L} *) | N of neu type neu = | V of atom | A of neu * sem type env binds = (*latex \label{line:env} *) | ENil | ECons of env * atom * outer sem (*latex \label{line:def:ECons} *) fun reify accepts s produces t = case s of | L (env, y, t) -> (*latex \label{line:L1} *) fresh x in (*latex \label{line:fresh} *) Lam (x, reify (evals (ECons (env, y, N (V (x))), t)))(*latex \label{line:app1} *) | N (n) -> reifyn (n) end fun reifyn accepts n produces t = case n of | V (x) -> Var (x) | A (n, d) -> App (reifyn (n), reify (d)) end fun evals accepts env, t produces v where free(v) <= outer(env) U (free(t) \ bound(env)) = (*latex \label{line:postcond} *) case t of | Var (x) -> case env of | ENil -> N (V (x)) (*latex \label{line:post1} *) | ECons (tail, y, v) -> if x == y then v (*latex \label{line:post2} *) else evals (tail, t) end (*latex \label{line:post3} *) end | Lam (x, t) -> (*latex \label{line:Lam} *) L (env, x, t) (*latex \label{line:post4} *) | App (t1, t2) -> case evals (env, t1) of | L (cenv, x, t) -> (*latex \label{line:L2} *) evals (ECons (cenv, x, evals (env, t2)), t) (*latex \label{line:post5} *) (*latex \label{line:app2} *) | N (n) -> N (A (n, evals (env, t2))) (*latex \label{line:post6} *) end end fun eval accepts t produces s = evals (ENil, t) fun normalize accepts t produces u = reify (eval (t))