Skip to content

Instantly share code, notes, and snippets.

@yuga

yuga/printf.idr

Created May 17, 2014
Embed
What would you like to do?
skills matterにVideoがあがっていたIdrisで書く型安全なprintf; youtube => http://youtu.be/fVBck2Zngjo
module Printf
%default total
data Format = FInt Format -- %d
| FString Format -- %s
| FOther Char Format -- [a-zA-Z0-9]
| FEnd --
format : List Char -> Format
format ('%'::'d'::cs) = FInt (format cs)
format ('%'::'s'::cs) = FString (format cs)
format (c::cs) = FOther c (format cs)
format [] = FEnd
interpFormat : Format -> Type
interpFormat (FInt f) = Int -> interpFormat f
interpFormat (FString f) = String -> interpFormat f
interpFormat (FOther _ f) = interpFormat f
interpFormat FEnd = String
formatString : String -> Format
formatString s = format (unpack s) -- string is not a list unlike haskell.
toFunction : (fmt : 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 FEnd a = a
printf : (s : String) -> interpFormat (formatString s)
printf s = toFunction (formatString s) ""
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment