gistfile1.idr

module Main

data FormatTy = FormatInt FormatTy
              | FormatChar Char FormatTy
              | FormatEnd

total
interpTy : FormatTy -> Type
interpTy (FormatInt ty)    = Int -> interpTy ty
interpTy (FormatChar x ty) = interpTy ty
interpTy FormatEnd         = String

total
PrintFormat : List Char -> FormatTy
PrintFormat ('%' :: 'd' :: rest) = FormatInt (PrintFormat rest)
PrintFormat (x :: rest)          = FormatChar x (PrintFormat rest)
PrintFormat []                   = FormatEnd

total
printf : (fmt : String) -> interpTy (PrintFormat (unpack fmt))
printf fmt = printf' "" (unpack fmt)
  where
    total
    printf' : (acc : String) -> (fmt : List Char) -> interpTy (PrintFormat fmt)
    printf' acc ('%' :: 'd' :: rest) = \x => printf' (acc ++ show x) rest
    printf' acc (x :: rest)          = printf' (acc ++ singleton x) rest
    printf' acc []                   = acc

{-

When elaborating right hand side of Main.printf, printf':
Can't unify
        interpTy (PrintFormat rest)
with
        interpTy (PrintFormat (x :: rest))

Specifically:
        Can't unify
                interpTy (PrintFormat rest)
        with
                interpTy (PrintFormat (x :: rest))
idris: bind: resource busy (Address already in use)
Metavariables: Main.printf

-}