tapl7.hs

import Data.Functor.Identity
import Control.Monad.State
import Data.List
import System.Random

type Info = String

data Term = Var Info Int Int
          | Abs Info String Term
          | App Info Term Term

data Binding = NameBind

data Context = Context { randgen :: StdGen
                       , names   :: [(String, Binding)]
                       }

printtm :: Term -> IO ()
printtm term = do
    seed <- randomIO :: IO Int
    let context = Context {randgen = mkStdGen seed, names = []}
    putStrLn $ evalState (printtm' term) context

printtm' :: Term -> State Context String
printtm' (Abs fi x t1)  = do
    x'  <- pickfreshname x
    out <- printtm' t1
    return $ "(λ " ++ x' ++ ". " ++ out ++ ")"
printtm' (App fi t1 t2) = do
    out1 <- printtm' t1
    out2 <- printtm' t2
    return $ "(" ++ out1 ++ " " ++ out2 ++ ")"
printtm' (Var fi x n) = do
    ctx <- gets names
    if length ctx == n
        then index2name fi x
        else error "bad index"

pickfreshname :: String -> State Context String
pickfreshname x = do
    ctx  <- gets names
    let candidates = ['a'..'z'] ++ ['A'..'Z']
    name <- ($ (head x)) . fix $ \loop name -> do
            case lookup x ctx of
                Nothing -> return [name]
                Just _  -> do
                    g       <- gets randgen
                    let (i, g') = randomR (0, length candidates - 1) g
                    put $ Context g' ctx
                    loop (candidates !! i)
    g <- gets randgen
    put $ Context g $ (name, NameBind) : ctx
    return name

index2name :: String -> Int -> State Context String
index2name fi x = do
    ctx <- gets names
    return . fst $ ctx !! x

main :: IO ()
main = printtm $ App "" (Abs "" "x" (Var "" 0 1)) (Abs "" "x" (Var "" 0 2))