glue.sml

(* based on https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784 *)

type name = string

datatype term
  = Loc of name
  | Top of name
  | App of term * term
  | Let of name * term * term
  | Lam of name * term

and spine
  = SNil
  | SApp of spine * value

and value
  = VLam of name * (value -> value)
  | VLoc of name * spine
  | VTop of name * spine * value

type top_env = (name * value) list
type local_env = (name * value) list

fun lookup s ((k, v) :: xs) =
  if k = s
  then v
  else lookup s xs

fun eval top loc (Loc x) = lookup x loc
  | eval top loc (Top x) = VTop (x, SNil, lookup x top)
  | eval top loc (App (t, u)) = vapp (eval top loc t) (eval top loc u)
  | eval top loc (Let (x, t, u)) = eval top ((x, eval top loc t) :: loc) u
  | eval top loc (Lam (x, t)) = VLam (x, fn u => eval top ((x, u) :: loc) t)
and vapp (VLam (_, t)) u = t u
  | vapp (VLoc (x, sp)) u = VLoc (x, SApp (sp, u))
  | vapp (VTop (x, sp, t)) u = VTop (x, SApp (sp, u), vapp t u)

fun contains s ((k, _) :: xs) = if s = k then true else contains s xs
  | contains _ [] = false

fun fresh env x =
  if contains x env
  then fresh env (x ^ "'")
  else x

fun quote_sp loc unf h SNil = h
  | quote_sp loc unf h (SApp (sp, u)) = App (quote_sp loc unf h sp, quote loc unf u)
and quote loc unf (VLoc (x, sp)) = quote_sp loc unf (Loc x) sp
  | quote loc unf (VLam (x, t)) =
    let val n = fresh loc x
        val v = VLoc (n, SNil)
    in Lam (n, quote ((x, v) :: loc) unf (t v))
    end
  | quote loc unf (VTop (x, sp, t)) =
    if unf
    then quote loc unf t
    else quote_sp loc unf (Top x) sp

fun eval_top top t =
  let val topvals = foldl (fn ((x, t), top) => (x, eval top [] t) :: top) [] top
  in eval topvals [] t
  end

fun nf_top unf top t = quote [] unf (eval_top top t)

val $$ = App

infix 8 $$

val top =
  [ ("zero", Lam ("s", Lam ("z", Loc "z")))
  , ("suc", Lam ("n", Lam ("s", Lam ("z",
      Loc "s" $$ (Loc "n" $$ (Loc "s" $$ Loc "z"))))))
  , ("add", Lam ("a", Lam ("b", Lam ("s", Lam ("z",
      Loc "a" $$ Loc "s" $$ (Loc "b" $$ Loc "s" $$ Loc "z"))))))
  , ("mul", Lam ("a", Lam ("b", Lam ("s", Lam ("z",
      Loc "a" $$ (Loc "b" $$ Loc "s") $$ Loc "s" $$ Loc "z")))))
  , ("5", Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "zero"))))))
  , ("10", Top "add" $$ Top "5" $$ Top "5")
  , ("100", Top "mul" $$ Top "10" $$ Top "10")
  ]

val tm = Let ("five", Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ Top "zero")))),
           Top "mul" $$ Loc "five" $$ Top "5")