Created
October 28, 2015 11:21
-
-
Save danielwaterworth/2a6e4cb6c267d8e79e92 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module main | |
data FormatString : List Char -> Type -> Type where | |
Empty : FormatString [] String | |
InsertNumber : FormatString s t -> FormatString ('%' :: 'd' :: s) (Int -> t) | |
InsertString : FormatString s t -> FormatString ('%' :: 's' :: s) (String -> t) | |
Other : (x /= '%' = True) -> FormatString s t -> FormatString (x :: s) t | |
printf' : List Char -> FormatString format ty -> ty | |
printf' s Empty = pack (reverse s) | |
printf' s (Other _ {x=c} next) = printf' (c :: s) next | |
printf' s (InsertNumber next) = (\x => printf' (reverse (unpack (show x)) ++ s) next) | |
printf' s (InsertString next) = (\x => printf' (reverse (unpack x) ++ s) next) | |
printf : (format : String) -> {auto ok : FormatString (unpack format) ty} -> ty | |
printf format {ok} = | |
printf' [] ok |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment