-- Author: Mukesh Tiwari
-- https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr


import Data.String

%default total


data Format = FInt Nat Format
            | FString Format
            | FOther Char Format
            | FEnd


charToNat : Char -> Nat
charToNat '0' = 0
charToNat '1' = 1
charToNat '2' = 2
charToNat '3' = 3
charToNat '4' = 4
charToNat '5' = 5
charToNat '6' = 6
charToNat '7' = 7
charToNat '8' = 8
charToNat '9' = 9
charToNat _ = 0


toNat' : List Char -> Nat -> Nat -> Nat
toNat' (c :: cs) dnum acc = toNat' cs (dnum * 10) (acc + dnum * (charToNat c))
toNat' [] dnum acc = acc

toNat : String -> Nat
toNat str = toNat' (unpack (reverse str)) 1 0

joinToString' : List Char -> String -> String
joinToString' (c :: cs) acc = joinToString' cs (acc ++ show c)
joinToString' [] acc = acc

joinToString : List Char -> String
joinToString cs = joinToString' cs ""


generateZeros' : Nat -> String -> String
generateZeros' (S n) acc = "0" ++ (generateZeros' n acc)
generateZeros' Z acc = acc

generateZeros : Nat -> String
generateZeros n = generateZeros' n ""

getNumber : List Char -> String -> ((List Char), Nat)
getNumber (c :: cs) acc = if (isDigit c) then (getNumber cs (acc ++ show c)) else (cs, Main.toNat acc)

format : List Char -> Format
format ('%' :: 'd' :: cs ) = FInt 0 ( format cs )
format ('%' :: 's' :: cs ) = FString ( format cs )
-- format ('%' :: '0' :: nums) =
--     let tmp = getNumber nums "" in
--     let cs = fst tmp in
--     let count = snd tmp in
--         FInt count (format cs)
format ('%' :: '0' :: '0' :: 'd' :: cs) = FInt 0 (format cs)
format ('%' :: '0' :: '1' :: 'd' :: cs) = FInt 1 (format cs)
format ('%' :: '0' :: '2' :: 'd' :: cs) = FInt 2 (format cs)
format ('%' :: '0' :: '3' :: 'd' :: cs) = FInt 3 (format cs)
format ('%' :: '0' :: '4' :: 'd' :: cs) = FInt 4 (format cs)
format ('%' :: '0' :: '5' :: 'd' :: cs) = FInt 5 (format cs)
format ('%' :: '0' :: '6' :: 'd' :: cs) = FInt 6 (format cs)
format ('%' :: '0' :: '7' :: 'd' :: cs) = FInt 7 (format cs)
format ('%' :: '0' :: '8' :: 'd' :: cs) = FInt 8 (format cs)
format ('%' :: '0' :: '9' :: 'd' :: cs) = FInt 9 (format cs)


format ( c :: cs )         = FOther c ( format cs )
format []                  = FEnd

interpFormat : Format -> Type
interpFormat ( FInt _ f )     = Int -> interpFormat f
interpFormat ( FString f )  = String -> interpFormat f
interpFormat ( FOther _ f ) = interpFormat f
interpFormat FEnd           = String


formatString : String -> Format
formatString s = format ( unpack s )

toFunction : ( fmt : Format ) -> String -> interpFormat fmt
toFunction ( FInt count format ) acc = \i => toFunction format (acc ++ (generateZeros count) ++ show i)
toFunction ( FString f ) a  = \s => toFunction f ( a ++ s )
toFunction ( FOther c f ) a = toFunction f ( a ++ singleton c )
toFunction FEnd a           = a


sprintf : ( s : String ) -> interpFormat ( formatString s )
sprintf s = toFunction ( formatString s ) ""

main : IO ()
main = putStrLn (sprintf "String parameter: %s, integer parameter: %05d" "alpha" (10+23))