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")))
Hey @larsrh, thanks for linking to this gist.
Hi @quephird, that's an interesting one. I'm by no means an experienced Idris user but maybe we can tackle this problem together. Let's see if we can rewrite
toFormat
to make it total. To do this we will employ views.Views—just like pattern matching—allow us to destructure data. Using pattern matching we can destructure values by applying their constructors.
Views on the other hand allow us to destructure data in a more arbitrary way.
Here,
snocList
is a covering function of theSnocList
view. It gives us another perspective for looking at lists; namely, from the other end.Let's define a recursive view over a list of characters. There are three cases:
We need to supplement our view with a covering function. It will take a
List Char
as an argument and return aFormatString
for the given list.First two cases cover strings with zero or one character. They cannot contain any formatting patterns. Then we address a number of cases for fixed-width formatting patterns. It's kind of repetitive; I'm wondering if it could be simplified. The last two cases are triggered when we run into a formatting pattern or a literal.
Here we keep taking elements from
rest
and appending them toprefix
until we hit an'f'
. Everything up to and including'f'
becomes our formatting pattern. Then we continue parsing the rest withformatString
. I hope it's a satisfactory approximation of yoursearchNumericSpecs
.We need to rewrite some types in order to satisfy the type checker.
appendAssociative
allows us to prove that the following equality holds.Patterns such as
"%03f"
are covered. Now we need to parse literals for as long as we don't hit a'%'
.If you take a close look you'll notice that the structure of
formatStringFormatHelper
andformatStringLitHelper
is very similar. Keep appending characters toprefix
until you see a'%'
. Then fall back toformatString
.Three functions above are mutually recursive. Because of that they have to be defined in a single
mutual
block.The resulting covering function is total and we can use it in
toFormat
.Our input string is either empty or consists of two parts: a literal or a formating string, postfixed with the rest. Let's finish the definition.
In the last case—when none of the constant formatting patterns match—I'm attempting to parse it as a floating point pattern. If it doesn't work I give up and return a literal, just as your code does.
The resulting function is total.
As a closing note, I can't recommend enough the TDD with Idris book. Chapter 10 discusses views in depth.
I hope this helps! As I wrote above, I'm new to all of this and I welcome all feedback and improvement ideas.