Type-safe printf in Lean 4.

printf.lean

inductive Format : Type
| string : Format → Format
| int : Format → Format
| other : Char → Format → Format
| nil : Format
deriving Repr

open Format

def mkSignature (res : Type) : Format → Type
| string fmt => String → mkSignature res fmt
| int fmt => Int → mkSignature res fmt
| other _ fmt => mkSignature res fmt
| nil => res

def mkBody {res : Type} (f : String → res) : (fmt : Format) → mkSignature res fmt := loop ""
where
loop : String → (fmt : Format) → mkSignature res fmt
| s₁, string fmt => λ s₂ => loop (s₁ ++ s₂) fmt
| s, int fmt => λ n => loop (s ++ toString n) fmt
| s, other c fmt => loop (s.push c) fmt
| s, nil => f s

def format : List Char → Format
| '%' :: 's' :: cs => string (format cs)
| '%' :: 'd' :: cs => int (format cs)
| c :: cs => other c (format cs)
| [] => nil

def sprintf (s : String) := mkBody id (format s.toList)
def printf  (s : String) := mkBody IO.println (format s.toList)