OK... this has very weak support for the %f
format specification, but it works:
module IO.Printf
toOctal : Int -> String
toOctal n = let (q, r) = (div n 8, mod n 8) in
case q == 0 of
True => show r
False => toOctal q ++ show r
data Caps = Up | Down
toHex' : Int -> Int -> String
toHex' offset n = let (q, r) = (div n 16, mod n 16) in
case q == 0 of
True => show' r
False => toHex' offset q ++ show' r
where
show' : Int -> String
show' r = case r < 10 of
True => show r
False => singleton $ chr (r + offset)
toHex : Caps -> Int -> String
toHex Up n = toHex' 55 n
toHex Down n = toHex' 87 n
-- This is a recursive type for describing a format specifier
-- For example, "%s is %d%" would be expressed as
-- Str (Lit " is " (Number (Lit "%" End)))
data Format = Number Format
| Oct Format
| Hex Caps Format
| Str Format
| Chr Format
| Dbl Format
| Lit String Format
| End
-- This function takes a format specifier in the form of a string
-- and recursively builds and returns a Format type
total
toFormat : (string : List Char) -> Format
toFormat string = case string of
[] => End
('%' :: 'd' :: chars) => Number $ toFormat chars
('%' :: 'o' :: chars) => Oct $ toFormat chars
('%' :: '#' :: 'o' :: chars) => Lit "0" $ Oct $ toFormat chars
('%' :: 'x' :: chars) => Hex Down $ toFormat chars
('%' :: '#' :: 'x' :: chars) => Lit "0x" $ Hex Down $ toFormat chars
('%' :: 'X' :: chars) => Hex Up (toFormat chars)
('%' :: '#' :: 'X' :: chars) => Lit "0X" $ Hex Up $ toFormat chars
('%' :: 's' :: chars) => Str $ toFormat chars
('%' :: 'c' :: chars) => Chr $ toFormat chars
('%' :: 'f' :: chars) => Dbl $ toFormat chars
(c :: chars) => case toFormat chars of
Lit lit chars' => Lit (strCons c lit) chars'
fmt => Lit (strCons c "") fmt
-- This is also a recursive type that describes
-- the return type of the printf function
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Oct fmt) = (i : Int) -> PrintfType fmt
PrintfType (Hex caps fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Chr fmt) = (char : Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (dbl : Double) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String
-- This function is a helper for the printf function
-- and is actually the one that does all the work by
-- accumulating the output string
printfHelper : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfHelper (Number fmt) acc = \i => printfHelper fmt $ acc ++ show i
printfHelper (Oct fmt) acc = \i => printfHelper fmt $ acc ++ toOctal i
printfHelper (Hex caps fmt) acc = \i => printfHelper fmt $ acc ++ toHex caps i
printfHelper (Str fmt) acc = \s => printfHelper fmt $ acc ++ s
printfHelper (Chr fmt) acc = \c => printfHelper fmt $ pack $ unpack acc ++ [c]
printfHelper (Dbl fmt) acc = \d => printfHelper fmt $ acc ++ show d
printfHelper (Lit str fmt) acc = printfHelper fmt $ acc ++ str
printfHelper End acc = acc
-- The actual interface and point of entry, it passes an empty
-- accumulator to the helper above
printf : (fmt : String) -> PrintfType $ toFormat $ unpack fmt
printf fmt = printfHelper _ ""
And when I test that implementation it works:
danielle@danielles-MacBook-Pro-2 ~/p/i/src> idris
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :module IO.Printf
*IO/Printf> printf "%f is an approximation to %s" 3.14 "pi"
"3.14 is an approximation to pi" : String
But when I try to start moving in a direction to support width and precision specifiers I run into trouble:
data SearchResults = NoSpec
| FSpec Nat Nat (List Char)
total
searchNumericSpecs : List Char -> SearchResults
searchNumericSpecs chars = case span (/= 'f') chars of
(_, []) => NoSpec
([], 'f' :: chars') => FSpec 0 6 chars'
(spec, 'f' :: chars') => FSpec 0 6 chars'
(_, _) => NoSpec
total
toFormat : (string : List Char) -> Format
toFormat string = case string of
[] => End
('%' :: 'd' :: chars) => Number $ toFormat chars
('%' :: 'o' :: chars) => Oct $ toFormat chars
('%' :: '#' :: 'o' :: chars) => Lit "0" $ Oct $ toFormat chars
('%' :: 'x' :: chars) => Hex Down $ toFormat chars
('%' :: '#' :: 'x' :: chars) => Lit "0x" $ Hex Down $ toFormat chars
('%' :: 'X' :: chars) => Hex Up (toFormat chars)
('%' :: '#' :: 'X' :: chars) => Lit "0X" $ Hex Up $ toFormat chars
('%' :: 's' :: chars) => Str $ toFormat chars
('%' :: 'c' :: chars) => Chr $ toFormat chars
('%' :: chars) => case searchNumericSpecs chars of
NoSpec => Lit "%" $ toFormat chars
FSpec width prec chars' => Dbl $ toFormat chars'
(c :: chars) => case toFormat chars of
Lit lit chars' => Lit (strCons c lit) chars'
fmt => Lit (strCons c "") fmt
That compiles and satisfies the type checker, but everything is broken now:
danielle@danielles-MacBook-Pro-2 ~/p/i/src> idris
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :module IO.Printf
*IO/Printf> printf "%f is an approximation to %s" 3.14 "pi"
(input):1:1-47:printf "%f is an approximation to %s" does not have a function type (PrintfType (toFormat (unpack "%f is an approximation to %s")))
*IO/Printf> printf "%s" "WAT?"
(input):1:1-18:printf "%s" does not have a function type (PrintfType (toFormat (unpack "%s")))
Cause
When you compile your updated Idris file, you should see a warning like this:
(Line number might be different on your end.)
The reason is this line:
You're performing a recursive call to
toFormat
withchars'
which you obtained fromsearchNumericSpecs
. Unfortunately, Idris' termination checker won't be able to figure out thatchars'
is in fact shorter thanchars
, which would be needed for termination.The reason why you're seeing the strange output in the REPL is as follows: To figure out how many arguments
printf
takes, the Idris compiler has to evaluate thetoFormat
function at compile-time. It will refuse to do so if it believes the function is not total (that which the warning message indicated).Quick fix
There's a "quick fix", namely just to assert totality/termination:
This will make your examples go through:
Proper fix
Prove termination of this function properly, without
assert_total
. I'm afraid my Idris knowledge is not advanced enough for this. It would probably require returning a dependent pair fromsearchNumericSpecs
that proved that the resulting list is strictly shorter than the input list.