(* Translated from Example 10 in Schuermann, Poswolsky, and Sarnat's 2004 technical report on the nabla-calculus. *) (* The current prototype does not allow distinguishing two sorts of atoms, so variable names and continuation names are mixed. *) type term = | Var of atom | Value of value | App of term * term | Callcc of < atom * inner term > | Throw of cont * term type value = | VLam of < atom * inner term > (* The current prototype does not have higher-order functions, so continuations are data structures. *) type cont = | CVar of atom | CApp1 of term * cont | CApp2 of value * cont (* Evaluation. *) fun ev accepts e, k where free(e) == empty and free(k) == empty produces v = case e of | Var (_) -> absurd | App (e1, e2) -> ev (e1, CApp1 (e2, k)) | Value (v) -> apply (k, v) | Callcc (kappa, e1) -> ev (csub (kappa, k, e1), k) | Throw (k, e1) -> ev (e1, k) end fun apply accepts k, v where free(v) == empty and free(k) == empty produces w = case v, k of | _, CVar (_) -> absurd | v1, CApp1 (e2, k) -> ev (e2, CApp2 (v1, k)) | v2, CApp2 (VLam (x, t1), k) -> ev (sub (x, v2, t1), k) end (* Substitution for variable names has to be hand-coded. *) fun sub accepts a, t, s produces u where free(u) <= free(t) U (free(s) \ free(a)) = case s of | Var (b) -> if a == b then Value (t) else Var (b) end | Value (v) -> Value (subv (a, t, v)) | App (u, v) -> App (sub (a, t, u), sub (a, t, v)) | Callcc (x, u) -> Callcc (x, sub (a, t, u)) | Throw (k, u) -> Throw (subk (a, t, k), sub (a, t, u)) end fun subv accepts a, v, w produces x where free(x) <= free(v) U (free(w) \ free(a)) = case w of | VLam (x, t) -> VLam (x, sub (a, v, t)) end fun subk accepts a, v, k produces k' where free(k') <= free(v) U (free(k) \ free(a)) = case k of | CVar (x) -> if a == x then fail (* TEMPORARY test will be avoided when multiple sorts are supported *) else CVar (x) end | CApp1 (t, k) -> CApp1 (sub (a, v, t), subk (a, v, k)) | CApp2 (w, k) -> CApp2 (subv (a, v, w), subk (a, v, k)) end (* Substitution for continuation names has to be hand-coded. *) fun csub accepts a, k, s produces u where free(u) <= free(k) U (free(s) \ free(a)) = case s of | Var (b) -> if a == b then fail (* TEMPORARY test will be avoided when multiple sorts are supported *) else Var (b) end | Value (v) -> Value (csubv (a, k, v)) | App (u, v) -> App (csub (a, k, u), csub (a, k, v)) | Callcc (x, t) -> Callcc (x, csub (a, k, t)) | Throw (j, t) -> Throw (csubk (a, k, j), csub (a, k, t)) end fun csubv accepts a, v, w produces x where free(x) <= free(v) U (free(w) \ free(a)) = case w of | VLam (x, t) -> VLam (x, csub (a, v, t)) end fun csubk accepts a, j, k produces k' where free(k') <= free(j) U (free(k) \ free(a)) = case k of | CVar (x) -> if x == a then j else k end | CApp1 (t, k) -> CApp1 (csub (a, j, t), csubk (a, j, k)) | CApp2 (w, k) -> CApp2 (csubv (a, j, w), csubk (a, j, k)) end