(* In this version, the environment contains computations, as opposed to values. This delays the normalisation of arguments of applications until they are actually used, but can cause them to be normalised several times, as far as I can see. It does not change the end result. *) type lam = | Var of atom | Lam of < atom * inner lam > | App of lam * lam type semantic_value = | L of < env * atom * inner lam > | N of neutral type neutral = | V of atom | A of neutral * semantic_value type env binds = | ENil | ECons of env * atom * outer delayed_semantic_value type delayed_semantic_value = | DImmediate of semantic_value | DEvals of < env * inner lam > fun reify accepts s produces t = case s of | L (env, x, t) -> (*latex \label{line:L1} *) fresh y in (*latex \label{line:fresh} *) Lam (y, reify (evals (ECons (env, x, DImmediate (N (V (y)))), t))) | 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 s where free(s) <= outer(env) U (free(t) \ bound(env)) = case t of | Var (x) -> case env of | ENil -> N (V (x)) (*latex \label{line:post1} *) | ECons (tail, y, dv) -> if x == y then force (dv) (*latex \label{line:post2} *) else evals (tail, t) end (*latex \label{line:post3} *) end | Lam (x, body) -> (*latex \label{line:Lam} *) L (env, x, body) (*latex \label{line:post4} *) | App (t1, t2) -> case evals (env, t1) of | L (cenv, x, body) -> (*latex \label{line:L2} *) evals (ECons (cenv, x, DEvals (env, t2)), body) (*latex \label{line:post5} *) | N (n) -> N (A (n, evals (env, t2))) (*latex \label{line:post6} *) end end fun force accepts dv produces v = case dv of | DImmediate (v) -> v | DEvals (env, t) -> evals (env, t) end fun eval accepts t produces s = evals (ENil, t) fun normalize accepts t produces u = reify (eval (t))