Skip to content

Instantly share code, notes, and snippets.

@paulkoerbitz
Created April 25, 2014 08:09
Show Gist options
  • Save paulkoerbitz/11281614 to your computer and use it in GitHub Desktop.
Save paulkoerbitz/11281614 to your computer and use it in GitHub Desktop.
printf with totality problem
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
@paulkoerbitz
Copy link
Author

idiris Printf.idr reports

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment