Dependently typed printf

Printf.lean

inductive Format :=
  | Int (rest: Format) -- %d
  | String (rest: Format) -- %s
  | Other (char: Char) (rest: Format) -- %c
  | End


def format : List Char -> Format
  | ('%' :: 'd' :: cs) => .Int (format cs)
  | ('%' :: 's' :: cs) => .String (format cs)
  | (c :: cs) => .Other c (format cs)
  | [] => .End

def formatString : String -> Format := (·.toList |> format)

def interpFormat : Format -> Type
  | (.Int f) => Int -> interpFormat f
  | (.String f) => String -> interpFormat f
  | (.Other _ f) => interpFormat f
  | .End => String

def toFunction (fmt : Format) : String -> interpFormat fmt :=
  match fmt with
  | .Int f => fun a i => toFunction f (a ++ i.repr)
  | .String f => fun a s => toFunction f (a ++ s)
  | .Other c f => fun a => toFunction f (a ++ c.toString)
  | .End => id

def printf (s : String) : interpFormat (formatString s) := toFunction (formatString s) ""

#eval printf "hello %d world %s" 2 "foo"
-- #eval printf "hello %s world %s" 2 "foo" will fail since 2 is not a string