Fmt.idr

-- Based off https://www.youtube.com/watch?v=fVBck2Zngjo

module Fmt

%default total

data FPart
  = FShow        -- "{}"  (Show a => a)
  | FInt         -- "{i}" (Int)
  | FString      -- "{s}" (String)
  | FOther Char  -- Any other character

Format : Type
Format = List FPart

parseFormat : String -> Format
parseFormat = fromChars . unpack
  where
    fromChars : List Char -> Format
    fromChars ('{' :: '}'        :: cs) = FShow :: fromChars cs
    fromChars ('{' :: 'i' :: '}' :: cs) = FInt :: fromChars cs
    fromChars ('{' :: 's' :: '}' :: cs) = FString :: fromChars cs
    fromChars (c                 :: cs) = FOther c :: fromChars cs
    fromChars []                        = []

||| Create the type of a string formatter based on the given `Format`.
|||
||| # Examples:
|||
||| ```
||| format (parseFormat "hello {}!") : {a : Type} -> Show a => a -> String
||| format (parseFormat "{i}{s}") : Int -> String -> String
||| ```
interpret : Format -> Type
interpret (FShow    :: fs) = {a : Type} -> Show a => a -> interpret fs
interpret (FInt     :: fs) = Int -> interpret fs
interpret (FString  :: fs) = String -> interpret fs
interpret (FOther _ :: fs) = interpret fs
interpret []               = String


||| Create a string formatting function based off the format string `s`.
|||
||| # Examples:
|||
||| ```
||| format "hello {}!" "world"
||| format "{i} bottles of beer" 3
||| ```
format : (s : String) -> interpret (parseFormat s)
format s = toFunction (parseFormat s) ""
  where
    toFunction : (fmt : Format) -> String -> interpret fmt
    toFunction (FShow    :: fs) acc = \x => toFunction fs (acc ++ show x)
    toFunction (FInt     :: fs) acc = \x => toFunction fs (acc ++ show x)
    toFunction (FString  :: fs) acc = \x => toFunction fs (acc ++ x)
    toFunction (FOther c :: fs) acc = toFunction fs (acc ++ singleton c)
    toFunction []               acc = acc