Add Nat case for printf

Changes

1 changed files (+19/-16)

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