Type safe printf

Changes

1 changed files (+26/-0)

• Printf.lean (new)
  • @@ -0,0 +1,26 @@
    + -- https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity.html + + inductive Fmt where + | FArg : Fmt → Fmt + | FChar : Char → Fmt → Fmt + | FEnd + + def toFmt : List Char → Fmt + | '*' :: xs => .FArg <| toFmt xs + | x :: xs => .FChar x <| toFmt xs + | [] => .FEnd + + def PrintfType : Fmt → Type 1 + | .FArg fmt => {α : Type} → [ToString α] → α → PrintfType fmt + | .FChar _ fmt => PrintfType fmt + | .FEnd => PLift String + + def printf (fmt : String) : PrintfType <| toFmt <| fmt.toList := + let rec printfAux (fmt : Fmt) (acc : List Char) : PrintfType fmt := + match fmt with + | .FArg fmt => fun x => printfAux fmt <| acc ++ (toString x).toList + | .FChar c fmt => printfAux fmt <| acc ++ [c] + | .FEnd => .up acc.asString + printfAux (toFmt <| fmt.toList) [] + + #eval printf "Hello * *" 42 "Meow" |>.down