Changes
2 changed files (+29/-29)
-
Format.lean (new)
-
@@ -0,0 +1,29 @@-- https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity.html inductive Fmt where | Arg : Fmt → Fmt | Nat : Fmt → Fmt | Char : Char → Fmt → Fmt | End def toFmt : List Char → Fmt | '*' :: xs => .Arg <| toFmt xs | '#' :: xs => .Nat <| toFmt xs | x :: xs => .Char x <| toFmt xs | [] => .End def FormatType : Fmt → Type 1 | .Arg fmt => {α : Type} → [ToString α] → α → FormatType fmt | .Nat fmt => Nat → FormatType fmt | .Char _ fmt => FormatType fmt | .End => PLift String def format (fmt : String) : FormatType <| toFmt fmt.toList := let rec formatAux (acc : String) : (fmt : Fmt) → FormatType fmt | .Arg fmt => fun x ↦ formatAux (acc ++ toString x) fmt | .Nat fmt => fun x ↦ formatAux (acc ++ "#" ++ toString x) fmt | .Char c fmt => formatAux (acc.push c) fmt | .End => .up acc formatAux "" <| toFmt fmt.toList #eval format "Hello * # * *" (-1) 1 [42, 69] "Meow" |>.down
-
-
Printf.lean (deleted)
-
@@ -1,29 +0,0 @@-- https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity.html inductive Fmt where | Arg : Fmt → Fmt | Nat : Fmt → Fmt | Char : Char → Fmt → Fmt | End def toFmt : List Char → Fmt | '*' :: xs => .Arg <| toFmt xs | '#' :: xs => .Nat <| toFmt xs | x :: xs => .Char x <| toFmt xs | [] => .End def PrintfType : Fmt → Type 1 | .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 (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 <| .ofList acc.toList printfAux #[] <| toFmt fmt.toList #eval printf "Hello * # * *" (-1) 1 [42, 69] "Meow" |>.down
-