de Bruijn index の評価器

unlambda から brainfuck への変換器を作ろうしていましたが、なぜか de Bruijn index のラムダ式の評価器を Haskell で作った時点で飽きました。そんな残骸ですが、メモ代わりに公開します。de Bruijn index でも代入の定義はやっぱり複雑なんですね。
de Bruijn index はラムダ式の記法の一種です。普通のラムダ式と違うのは、変数を文字列ではなく数字で表現するところです。その数字のある位置から左方向にλを数えていって、その数字番目のλで束縛された変数を指示します。例えば λx.x は λ 1 になり、λx.λy.x は λ λ 2 に、λf.λg.λx.f x (g x) は λ λ λ 3 1 (2 1) になります。詳しくは wikipedia:de Bruijn index を参照してください。

-- ラムダ式 (出力機能付き)
data Expr = A Expr Expr   -- Application
          | O String Expr -- Output
          | L Expr        -- Lambda Abstraction
          | V Int         -- Variable

-- 簡約
step :: Expr -> Maybe (String, Expr)
step (A   (L m) n@(L _)) = Just ("", subst m n)
step (A m@(L _) n      ) = step n >>= \(c, n) -> return (c, A m n)
step (A m       n      ) = step m >>= \(c, m) -> return (c, A m n)
step (O s m)             = Just (s, m)
step _                   = Nothing

-- 代入
subst :: Expr -> Expr -> Expr
subst m n = trav aux1 m
 where aux1 d x | x >  d = V (x - 1)
                | x == d = trav aux2 n
                | x <  d = V x
        where aux2 d' x | x >= d' = V (x + d)
                        | x <  d' = V x
trav f e = aux 0 e
 where aux d (A m n) = A (aux d m) (aux d n)
       aux d (O s m) = O s (aux d m)
       aux d (L m)   = L (aux (d + 1) m)
       aux d (V x)   = f d x

-- 評価
eval :: Expr -> String
eval e = aux (step e)
 where aux (Just (s, e)) = s ++ eval e
       aux Nothing = ""

-- unlambda から de Bruijn 記法への変換
trans :: String -> (Expr, String)
trans ('`':s) = (A m n, s'')
 where (m, s')  = trans s
       (n, s'') = trans s'
trans ('s':s) = (L (L (L (A (A (V 2) (V 0)) (A (V 1) (V 0))))), s)
trans ('k':s) = (L (L (V 1)), s)
trans ('i':s) = (L (V 0), s)
trans ('r':s) = (L (O "\n" (V 0)), s)
trans ('.':c:s) = (L (O [c] (V 0)), s)
trans (_:s) = trans s

-- テスト
main :: IO ()
main = putStrLn $ eval $ fst $ trans test
test = "```s``s``sii`ki" ++
       "  `k.*``s``s`ks" ++
       " ``s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk" ++
       "  `k``s`ksk"