Skip to content

Instantly share code, notes, and snippets.

@puffnfresh puffnfresh/Main.idr
Created Oct 14, 2016

Embed
What would you like to do?
Type-safe printf, using runtime provided strings. An extension on https://gist.github.com/puffnfresh/11202637
module Main
%default total
data Format
= FInt -- %d
| FString -- %s
| FOther Char -- [a-zA-Z0-9]
format : List Char -> List Format
format ('%'::'d'::cs) = FInt :: format cs
format ('%'::'s'::cs) = FString :: format cs
format (c::cs) = FOther c :: format cs
format [] = []
interpFormat : List Format -> Type
interpFormat (FInt :: f) = Int -> interpFormat f
interpFormat (FString :: f) = String -> interpFormat f
interpFormat (FOther _ :: f) = interpFormat f
interpFormat [] = String
formatString : String -> List Format
formatString s = format (unpack s)
toFunction : (fmt : List Format) -> String -> interpFormat fmt
toFunction (FInt :: f) a = \i => toFunction f (a ++ show i)
toFunction (FString :: f) a = \s => toFunction f (a ++ s)
toFunction (FOther c :: f) a = toFunction f (a ++ singleton c)
toFunction [] a = a
printf : (s : String) -> interpFormat (formatString s)
printf s = toFunction (formatString s) ""
runFormat : (fmt : List Format) -> interpFormat fmt -> IO ()
runFormat [] f =
putStrLn f
runFormat (FInt :: xs) f = do
putStr "Enter an integer: "
s <- getLine
runFormat xs (f (cast s))
runFormat (FString :: xs) f = do
putStr "Enter a string: "
s <- getLine
runFormat xs (f s)
runFormat (FOther _ :: xs) f =
runFormat xs f
main : IO ()
main = do
putStr "Your printf string: "
s <- getLine
runFormat (formatString s) (printf s)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.