test.idr

module Main

data Token : Type where
  C : String -> Token
  I : Token
  S : Token
infixr 9 :>

instance Show Token where
  show t = case t of
    C c => "C " ++ show c
    I => "I"
    S => "S"

parse : String -> List Token
parse = inner "" . unpack
  where
    inner : String -> List Char -> List Token
    inner acc s = case s of
      ('%' :: 's' :: rest) => C acc :: S :: inner "" rest
      ('%' :: 'i' :: rest) => C acc :: I :: inner "" rest
      (a :: r) => inner (acc ++ singleton a) r
      [] => case acc of
        "" => []
        _ => [C acc]

printfTypeH : List Token -> Type
printfTypeH format = case format of
  (C _ :: rest) => printfTypeH rest
  (I :: rest) => Int -> printfTypeH rest
  (S :: rest) => String -> printfTypeH rest
  Nil => String

printfType : String -> Type
printfType = printfTypeH . parse

printfH : (format : List Token) -> printfTypeH format
printfH = inner []
  where
    inner : List String -> (format : List Token)
      -> printfTypeH format
    inner acc format = case format of
      Nil => concat $ reverse acc
      (C c :: rest) => inner (c :: acc) rest
      (I :: rest) => (\ i => inner (show i :: acc) rest)
      (S :: rest) => (\ s => inner (s :: acc) rest)

printf : (format : String) -> printfType format
printf format = printfH (parse format)

main : IO ()
main = do
  putStrLn $ printf "foo"
  putStrLn $ printf "n: %i" 42
  putStrLn $ printf "n: %i, msg: %s" 42 "foo"