Glue.icl

module Glue

import StdEnv

:: Name :== String

:: Term
  = Loc Name
  | Top Name
  | App Term Term
  | Let Name Term Term
  | Lam Name Term

:: Spine
  = SNil
  | SApp Spine Value

:: Value
  = VLam Name (Value -> Value)
  | VLoc Name Spine
  | VTop Name Spine Value

:: TopEnv :== [(Name, Value)]
:: LocalEnv :== [(Name, Value)]

lookup :: k [(k, v)] -> v | == k
lookup i [(k, v) : xs]
  | k == i = v
  | otherwise = lookup i xs

eval :: TopEnv LocalEnv Term -> Value
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 \u -> eval top [(x, u) : loc] t

vapp :: Value Value -> Value
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)

contains :: k [(k, v)] -> Bool | == k
contains _ [] = False
contains i [(k, _) : xs]
  | k == i = True
  | otherwise = contains i xs

fresh :: LocalEnv Name -> Name
fresh env x
  | contains x env = fresh env (x +++ "'")
  | otherwise = x

:: UnfoldTop :== Bool

quoteSp :: LocalEnv UnfoldTop Term Spine -> Term
quoteSp loc unf h SNil = h
quoteSp loc unf h (SApp sp u) = App (quoteSp loc unf h sp) (quote loc unf u)

quote :: LocalEnv UnfoldTop Value -> Term
quote loc unf (VLoc x sp) = quoteSp loc unf (Loc x) sp
quote loc unf (VLam x t)
  # n = fresh loc x
  # v = VLoc n SNil
  = Lam n (quote [(x, v) : loc] unf (t v))
quote loc unf (VTop x sp t)
  | unf = quote loc unf t
  | otherwise = quoteSp loc unf (Top x) sp

evalTop :: [(Name, Term)] Term -> Value
evalTop top t = eval topvals [] t
  where topvals = foldl (\top (x, t) -> [(x, eval top [] t) : top]) [] top

nfTop :: UnfoldTop [(Name, Term)] Term -> Term
nfTop unf top t = quote [] unf (evalTop top t)


($) infixr 0
($) f x = f x

($$) infixl 8
($$) a b = App a b

top :: [(Name, Term)]
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")
  ]

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

Start = nfTop True top tm