towards a working example

Printf.idr

module Printf

import Lightyear.Char
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%access public export
%default total

orElse : a -> Maybe a -> a
orElse a Nothing  = a
orElse a (Just b) = b

option : a -> Parser a -> Parser a
option def parser = (orElse def) <$> (opt parser)

data FormatSpec = FSInt Nat
                | FSString
                | FSLit String

Show FormatSpec where
     show (FSInt n) = "%" ++ (show n) ++ "d"
     show FSString  = "%s"
     show (FSLit s) = s

pFSInt : Parser FormatSpec
pFSInt = (FSInt . cast) <$> (option 0 integer <* char 'd')

pFSString : Parser FormatSpec
pFSString = (const FSString) <$> char 's'

pFSLitSpecial : Parser FormatSpec
pFSLitSpecial = (FSLit . singleton) <$> anyChar

pFSSpecial : Parser FormatSpec
pFSSpecial = pFSInt <|> pFSString <|> pFSLitSpecial

pFSTerm : Parser FormatSpec
pFSTerm = char '%' *!> pFSSpecial

pFSLitOther : Parser FormatSpec
pFSLitOther = (FSLit . pack) <$> some (noneOf "%")

pFormatSpec : Parser (List FormatSpec)
pFormatSpec = many $ pFSTerm <|> pFSLitOther

-- Formatting AST.
data Format
  = FInt Nat Format
  | FString Format
  | FOther String Format
  | FEnd

Show Format where
     show (FInt n f) = "%" ++ (show n) ++ "d" ++ show f
     show (FString f) = "%s" ++ (show f)
     show (FOther s f) = s ++ show f
     show FEnd = "$"

formatFromSpec : List FormatSpec -> Format
formatFromSpec []                = FEnd
formatFromSpec (FSInt n   :: fs) = FInt n     (formatFromSpec fs)
formatFromSpec (FSString  :: fs) = FString    (formatFromSpec fs)
formatFromSpec (FSLit str :: fs) = FOther str (formatFromSpec fs)

parseFormat : Parser Format
parseFormat = assert_total $ do
  fs <- pFormatSpec
  pure $ formatFromSpec fs

-- Parse the format string (list of characters) into an AST.
-- Example: "%d,%s"  →   (FInt (FOther ',' (FString FEnd)))
format : String -> Format
format s = case (assert_total (parse parseFormat s)) of
           Right f => f
           Left e  => FEnd

-- Convert a format AST into a type.
-- Example: FInt (FOther ',' (FString FEnd))   →   Int -> String -> String
interpFormat' : Format -> Type
interpFormat' (FInt _ f)   = Int -> interpFormat' f
interpFormat' (FString f)  = String -> interpFormat' f
interpFormat' (FOther _ f) = interpFormat' f
interpFormat' FEnd         = String

interpFormat : Format -> Type
interpFormat f = assert_total (interpFormat' f)

repeat : Char -> Nat -> String
repeat c Z     = ""
repeat c (S k) = singleton c ++ repeat c k

padLeft : Char -> Nat -> String -> String
padLeft c k s = repeat c (minus k (length s)) ++ s

pad : Nat -> Int -> String
pad n i = padLeft '0' n (show i)

-- Dependently-typed part: turn a formatting AST into a well-typed
-- function accepting n arguments.
-- Example:
--      toFunction (FInt (FString FEnd))
--    →
--      \a i s => a ++ (show i) ++ s
toFunction : (fmt : Format) -> String -> interpFormat fmt
toFunction (FInt n f) a   = \i => toFunction f $ a ++ pad n i
toFunction (FString f) a  = \s => toFunction f $ a ++ s
toFunction (FOther s f) a = toFunction f $ a ++ s
toFunction FEnd a         = a

-- Dependently-typed part: turn a formatting string into a well-typed
-- function accepting n arguments.
-- Example: printf "%d%s" → \i s => (show i) ++ s
printf : (s : String) -> interpFormat (format s)
printf s = toFunction (format s) ""


p : String
p = printf "%3d%s" 3 "toto"