Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
35 lines (25 sloc) 1.01 KB
module Printf
%default total
data Format = FInt Format
| FString Format
| FOther Char Format
| 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 End = String
formatString : String -> Format
formatString s = format ( unpack s )
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 ) ""