printf with totality problem

Printf.idr

module Main

%default total

data Format = End
            | FInt Nat Format
            | FStr Nat Format
            | FChar Char Format

data Digit : Char -> Type where
  Zero  : Digit '0'
  One   : Digit '1'
  Two   : Digit '2'
  Three : Digit '3'
  Four  : Digit '4'
  Five  : Digit '5'
  Six   : Digit '6'
  Seven : Digit '7'
  Eight : Digit '8'
  Nine  : Digit '9'

getDigit : (c:Char) -> Maybe (Digit c)
getDigit '0' = Just Zero
getDigit '1' = Just One
getDigit '2' = Just Two
getDigit '3' = Just Three
getDigit '4' = Just Four
getDigit '5' = Just Five
getDigit '6' = Just Six
getDigit '7' = Just Seven
getDigit '8' = Just Eight
getDigit '9' = Just Nine
getDigit _   = Nothing

data Digits : List Char -> Type where
  None : Digits []
  Some : Digit c -> Digits cs -> Digits (cs ++ [c])

digits2nat : Digits cs -> Nat
digits2nat None                = Z
digits2nat (Some {c} {cs} _ _) = fromInteger $ cast $ pack (c :: cs)

data FormatDirective : List Char -> Type where
  FD_Chars : (cs : List Char) -> FormatDirective cs
  FD_Int   : Digits ds -> (cs : List Char) -> FormatDirective (ds ++ 'd' :: cs)
  FD_Str   : Digits ds -> (cs : List Char) -> FormatDirective (ds ++ 's' :: cs)

parseFD : (xs : List Char) -> FormatDirective xs
parseFD cs = go None cs
  where
    go : Digits ds -> (cs : List Char) -> FormatDirective (ds ++ cs)
    go None []  = FD_Chars ([] ++ [])
    go (Some {c} {cs} _ _) []  = FD_Chars ((cs ++ [c]) ++ [])
    go ds' ('d' :: xs) = FD_Int ds' xs
    go ds' ('s' :: xs) = FD_Str ds' xs
    go ds' (x :: xs) with (getDigit x)
      -- I use 'believe_me' here to 'show' that ds ++ x :: xs = ds ++ [x] ++ xs
      go ds' (x :: xs) | Just d   = believe_me $ go (Some d ds') xs
      go (Some {c} {cs} _ _) (x :: xs) | Nothing  = FD_Chars ((cs ++ [c]) ++ x :: xs)
      go None (x :: xs) | Nothing  = FD_Chars ([] ++ x :: xs)

fmtStr2Fmt : List Char -> Format
fmtStr2Fmt []                                                = End
fmtStr2Fmt ('%' :: cs)                   with (parseFD cs)
  fmtStr2Fmt ('%' :: cs)                 | (FD_Chars cs)     = FChar '%' (fmtStr2Fmt cs)
  fmtStr2Fmt ('%' :: (ds ++ 'd' :: cs')) | (FD_Int ds' cs')  = FInt (digits2nat ds') (fmtStr2Fmt cs')
  fmtStr2Fmt ('%' :: (ds ++ 's' :: cs')) | (FD_Str ds' cs')  = FStr (digits2nat ds') (fmtStr2Fmt cs')
fmtStr2Fmt (c :: cs)                                         = FChar c (fmtStr2Fmt cs)

PrintfType : Format -> Type
PrintfType End            = String
PrintfType (FInt _ rest)  = Int -> PrintfType rest
PrintfType (FStr _ rest) = String -> PrintfType rest
PrintfType (FChar c rest) = PrintfType rest

printf : (fmt: String) -> PrintfType (fmtStr2Fmt $ unpack fmt)
printf fmt = printFormat (fmtStr2Fmt $ unpack fmt) where
 printFormat : (fmt: Format) -> PrintfType fmt
 printFormat fmt = rec fmt "" where
   rec : (f: Format) -> String -> PrintfType f
   rec End acc            = acc
   rec (FInt _ rest) acc  = \i: Int => rec rest (acc ++ (show i))
   rec (FStr _ rest) acc    = \s: String => rec rest (acc ++ s)
   rec (FChar c rest) acc = rec rest (acc ++ (strCons c ""))

test : String
test = printf "The %s is %d" -- "answer" 42

main : IO ()
main = putStrLn test

idiris Printf.idr reports

Type checking ./Printf.idr
Printf.idr:63:1:Main.fmtStr2Fmt is possibly not total due to: {Main.fmtStr2Fmt41}