data Format = Number Format
| Str Format
| Ch Format
| Float Format
| Lit String Format
| End
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Ch fmt) = (char : Char) -> PrintfType fmt
PrintfType (Float fmt) = (float : Double) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Ch fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Float fmt) acc = \f => printfFmt fmt (acc ++ show f)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Ch (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Float (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
Lit lit chars' => Lit (strCons c lit) chars'
fmt => Lit (strCons c "") fmt
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""
λΠ> :t printf "%c %f %d %s"
printf "%c %f %d %s" : Char -> Double -> Int -> String -> String
λΠ> printf "%c %f %d %s" 'A' 1.234 1 "LOR"
"'A' 1.234 1 LOR" : String
λΠ> printf "%c %f %d %s" 'A' 1.234 1.0 "LOR"
builtin:Type mismatch between
Double (Type of 1.0)
and
Int (Expected type)
Еще есть ЯП общего назначения, которые так могут (ну кроме лиспов с макрами, где и то если типы параметров printf известны в compile-time), при этом разработчику не нужно патчить компилятор на каждый чих?
