Writing checkpoint

blog

@@ -284,6 +284,21 @@ multi MAIN(
     $db.write: $db-dir;
 }
 
+#| Update the posted-at time on a post to the current time
+multi MAIN(
+   "post",
+   "now",
+    #| The id of the post to update the posted-at time
+    Int $id,
+    #| The path of the database directory
+    IO::Path(Str) :$db-dir = $default-db-dir,
+){
+    my $db = read-db $db-dir;
+    my $post = $db.posts{$id.Int};
+    $post.posted-at = DateTime.now;
+    $db.write: $db-dir;
+}
+
 #| Create a new series
 multi MAIN(
     "series",

lib/DB/Post.rakumod

@@ -16,6 +16,7 @@ IO::Path:D $.source
 #| The time to display for the creation of the post
 has
 DateTime:D $.posted-at
+           is rw
            is required
            is json(
     :to-json(*.Str),

lib/Render/Head.rakumod

@@ -47,7 +47,6 @@ sub site-header(BlogMeta:D $meta) is export {
     sub header-link($name, $path, $icon) {
         a :href("$path"), [
             icon $icon;
-            ' ';
             span $name;
         ]
     }

lib/Render/Util.rakumod

@@ -10,7 +10,9 @@ sub show-html($html) is export {
    # Work around HTML::Functional automatically putting newlines between tags
    $out ~~ s:g/'</i>' \v+ '<span>'/<\/i><span>/;
    $out ~~ s:g/\v+ '</a>'/<\/a>/;
-   $out ~~ s:g/',' \v+ '<span'/,<span/;
+   $out ~~ s:g/\s+ ',' \s+ '<span'/, <span/;
+   # Fixup unit test divs
+   $out ~~ s:g/'<div class="unit-test">' \s* '<pre><code class="idris-code">&nbsp;&nbsp;'/<div class="unit-test"><span><i class='bx bx-check-circle'><\/i>Unit Test<\/span><pre><code class="idris-code">/;
    $out
 }
 

projects/Idris/src/LessMacrosMoreTypes/Printf.md

@@ -3,7 +3,8 @@
 ```idris hide
 module LessMacrosMoreTypes.Printf
 
-%default total
+import Data.List
+import System
 ```
 
 While C can provide convenient string formatting by having hideously memory
@@ -11,18 +12,19 @@ unsafe variadics, and dynamic languages, like python, can do the same while
 being memory safe by not being type safe, many type safe languages, such as
 Rust, are forced to provide such functionality through the use of a macro.
 Dependently typed languages, like Idris, can provide a printf like formatting
-interface, while maintaining both memory and type saftey, without the need for
+interface, while maintaining both memory and type safety, without the need for
 the macro. We will explore this by implementing a simplified version of `printf`
 in Idris from scratch.
 
-This article is inspired by an exercise from chapter 6 of [Type Driven
-Development with
-Idris](https://www.manning.com/books/type-driven-development-with-idris), and is
-written as a literate Idris file.
+This article is inspired by an exercise from chapter 6 of
+[Type Driven Development with Idris](https://www.manning.com/books/type-driven-development-with-idris),
+and is written as a literate Idris file, with the source available
+[here](https://git.stranger.systems/thatonelutenist/website/src/branch/trunk/projects/Idris/src/LessMacrosMoreTypes/Printf.md).
 
 ## Gameplan
 
-Our goal is to provide a printf function that can be called, much like it's C equivlant, like so:
+Our goal is to provide a printf function that can be called, much like it's C
+equivalent:
 
 > [!NOTE]
 > As this is a literate Idris document, and we haven't defined our `printf`
@@ -32,14 +34,202 @@ Our goal is to provide a printf function that can be called, much like it's C eq
 
 ```idris
 failing
-  example_usage : String
-  example_usage = printf "%s %d %02d" "hello" 1 2
+  printf "%s %d %2d" "hello" 1 2
 ```
 
+Idris lacks a dedicated facility for variadics, but we can call functions in
+type signatures, Idris allows us to manipulate types as first class values, and
+we can use the runtime values of previous arguments to the function we are
+defining as arguments to our type-level function.
 
+To get our variadic `printf` function, we can parse our format string into a
+data structure, then pass that data structure into a type-level function that
+calculates the rest of the type signature of our `printf` function based on its
+contents.
 
 ## Parsing a Format String
 
+First, we need a data structure to describe our format string. We define the
+`Format` data type, with constructors for each of the format specifiers we will
+be supporting, as well as a constructor to hold literal components.
+
+```idris
+data Format : Type where
+  ||| A slot that should be filled in with a number
+  Number : (next : Format) -> Format
+  ||| A slot that should be filled  in with a number, padded to a certian number
+  ||| of digits
+  PaddedNumber : (digits : Nat) -> (next : Format) -> Format
+  ||| A slot that should be filled in with a string
+  Str : (next : Format) -> Format
+  ||| A literal component of the format string that should not be interpolated
+  Literal : (literal : String) -> (next : Format) -> Format
+  ||| The end of the format string
+  End : Format
+```
+
+We'll need to be able to parse numbers for our `PaddedNumber` constructor, so
+we'll write a little helper function to handle that component of the parsing.
+Simply keep pulling off characters, converting them to integers by shifting
+their ordinal values.
+
+> [!WARNING]
+> On Idris 2's chez scheme backend, these are unicode ordinals, where the digit
+> characters are in numerical order, but the values are backend dependent and
+> this code is not guaranteed to work properly on other backends.
+
+```idris
+parseNumber : (xs : List Char) -> (acc : Nat) -> (Nat, List Char)
+parseNumber [] acc = (acc, [])
+parseNumber (x :: xs) acc = 
+  if isDigit x
+    then let value = cast $ (ord x) - (ord '0')
+    in parseNumber xs (acc * 10 + value)
+    else (acc, x :: xs)
+```
+
+We'll also want another one to scoop up a literal into a `List Char`, continuing
+until we hit the end of the string or the next `%`. This is optional, we could
+have each literal consist of an individual char, but we will go ahead and group
+them together.
+
+```idris
+parseLiteral : (xs : List Char) -> (List Char, List Char)
+parseLiteral [] = ([], [])
+parseLiteral ('%' :: xs) = ([], '%' :: xs)
+parseLiteral (x :: xs) = 
+  let (literal, rest) = parseLiteral xs
+  in (x :: literal, rest)
+```
+
+Parse our format string into our `Format` data structure. The specifics of the
+parsing here aren't really material to the main point of this article, but we
+use a basic pattern matching approach, calling into our helper functions as
+appropriate. 
+
+```idris
+parseFormat : (xs : List Char) -> Maybe Format
+parseFormat [] = Just End
+-- A `%` has to come before a specifier
+parseFormat ('%' :: []) = Nothing
+parseFormat ('%' :: (x :: xs)) = 
+  if isDigit x
+    -- Invoke parseNumber to get our padding specifier
+    then let (digits, rest) = parseNumber (x :: xs) 0
+    in case rest of
+      -- A padding specifier has to come before something
+      [] => Nothing
+      ('d' :: ys) => do
+        rest <- parseFormat ys
+        Just $ PaddedNumber digits rest
+      -- A padding specifier is only valid before a number specifier
+      (y :: ys) => Nothing
+    -- Parse as an unpadded specifier
+    else case x of
+      'd' => do
+        rest <- parseFormat xs
+        Just $ Number rest
+      's' => do
+        rest <- parseFormat xs
+        Just $ Str rest
+      -- Any other character here is an invalid specifier
+      _ => Nothing
+parseFormat (x :: xs) = 
+  let (literal, rest) = parseLiteral (x :: xs)
+  in do
+    rest <- parseFormat rest
+    Just $ Literal (pack literal) rest
+```
+
 ## Calculating a Type From a Format String
 
+```idris 
+PrintfType' : Format -> Type
+PrintfType' (Number next) =
+  (num : Nat) -> PrintfType' next
+PrintfType' (PaddedNumber digits next) =
+  (num : Nat) -> PrintfType' next
+PrintfType' (Str next) = 
+  (str : String) -> PrintfType' next
+PrintfType' (Literal literal next) = 
+  PrintfType' next
+PrintfType' End = String
+
+PrintfType : Maybe Format -> Type
+PrintfType Nothing = Void -> String
+PrintfType (Just x) = PrintfType' x
+```
+
 ## printf
+
+### With the Format Structure
+
+```idris hide
+left_pad : (len : Nat) -> (pad : Char) -> (str : String) -> String
+left_pad len pad str = 
+  let cs = unpack str
+  in if length cs < len
+    then pack $ replicate (len `minus` length cs) pad ++ cs
+    else str
+```
+
+```idris
+printfFmt : (fmt : Maybe Format) -> (acc : String) -> PrintfType fmt
+printfFmt Nothing acc = 
+  \void => absurd void
+printfFmt (Just x) acc = printfFmt' x acc
+  where 
+    printfFmt' : (fmt : Format) -> (acc : String) -> PrintfType' fmt
+    printfFmt' (Number next) acc = 
+      \i => printfFmt' next (acc ++ show i)
+    printfFmt' (PaddedNumber digits next) acc = 
+      \i => printfFmt' next (acc ++ left_pad digits '0' (show i))
+    printfFmt' (Str next) acc =
+      \str => printfFmt' next (acc ++ str)
+    printfFmt' (Literal literal next) acc = 
+      printfFmt' next (acc ++ literal)
+    printfFmt' End acc = acc
+```
+
+### With a Format String
+
+```idris
+printf : (fmt : String) -> PrintfType (parseFormat (unpack fmt))
+printf fmt = printfFmt _ ""
+```
+
+We can call `printf` as expected, with the number of and types of the arguments
+being determined by the provided format string:
+
+```idris hide
+-- @@test printf hello world
+helloWorld : IO Bool
+helloWorld = do
+  pure $
+```
+
+```idris
+  printf "%s %s%s %3d %d" "Hello" "world" "!" 1 23 == "Hello world! 001 23"
+```
+
+It will even fail to compile if you attempt to provide arguments to an invalid
+format string, which we can demonstrate by trying to apply a padding modifier to
+a string specifier:
+
+> [!NOTE]
+> `failing` blocks have an additional feature, they will trigger a compiler
+> error if their contents _do_ compile successfully.
+
+```idris
+failing
+  printf "Hello %s %3s" "world" "!"
+```
+
+## Working With Run-Time Format Strings
+
+## Conclusions
+
+### Why this API isn't really a great idea
+
+<!-- Doesn't fail to compile if you don't pass any arguments --> 
+

projects/Markdown/About.md

@@ -55,6 +55,16 @@ I've written a few libraries and utilities for Idris 2 already:
   provides comment-based unit testing capability. Currently written in Raku, I
   hope to eventually rewrite this in idris.
 
+### Raku
+
+- [blog](https://git.stranger.systems/thatonelutenist/website)
+
+  The static site generator powering this blog. This is a horribly cursed tangle
+  of ill-thought-through raku code that is not meant to be reused. Feel free to
+  take a look and maybe take inspiration from it, or at the very least feel
+  better about your own just-get-it-done code, but don't let me catch you
+  forking it.
+
 ### Books
 
 - [Idris by Highly Contrived Example](https://static.stranger.systems/idris-by-contrived-example/)

resources/admonitions.css

@@ -12,7 +12,7 @@
     color: var(--fg-1);
     padding: 0.5rem;
     border-radius: 1rem;
-    border: solid 0.5rem;
+    border: solid 0.35rem;
     margin-top: var(--box-margin-vert);
     margin-bottom: var(--box-margin-vert);
 }
@@ -29,8 +29,6 @@
 .warning .title p,
 .caution .title p {
     font-size: 0;
-    display: inline-block;
-    position: relative;
 }
 .note .title p::before,
 .tip .title p::before,
@@ -38,8 +36,7 @@
 .warning .title p::before,
 .caution .title p::before {
     font-family: 'boxicons' !important;
-    font-size: 3rem;
-    display: inline-block;
+    font-size: 4rem;
 }
 
 /* Notes */
@@ -68,17 +65,17 @@
 }
 /* Warnings */
 .warning {
-    border-color: var(--orange);
+    border-color: var(--yellow);
 }
 .warning .title p::before {
-    content: "\e9a3";
-    color: var(--orange);
+    content: "\eac5";
+    color: var(--yellow);
 }
 /* Cautions */
 .caution {
     border-color: var(--red);
 }
 .caution .title p::before {
-    content: "\ee87";
+    content: "\eac6";
     color: var(--red);
 }

resources/code.css

@@ -6,6 +6,7 @@ code {
 /* Styling for inline code blocks */
 :not(pre) > code {
     padding: 0 0.25rem;
+    border-radius: 0.25rem;
 }
 
 /* Styling for fenced code blocks */
@@ -18,4 +19,30 @@ pre > code {
 }
 pre {
     width: 90%;
+    box-sizing: border-box;
+}
+
+/* Styling for unit tests */
+.unit-test {
+    width: 90%;
+    display: flex;
+    flex-direction: column;
+    align-items: center;
+    padding: 1rem;
+    border-radius: 0.55rem / 0.5rem;
+    box-sizing: border-box;
+}
+.unit-test > span {
+    display: flex;
+    flex-direction: row;
+    align-items: center;
+    padding: 0.5rem;
+    border-radius: 0.55rem / 0.5rem;
+}
+.unit-test > pre {
+    width: auto;
+}
+.unit-test i {
+    font-size: 1.5rem;
+    margin-right: 0.5rem;
 }

resources/colors.css

@@ -78,6 +78,16 @@ a:visited {
 blockquote {
   background-color: var(--bg-1);
 }
+.unit-test {
+  background-color: var(--bg-1);
+}
+.unit-test > span {
+  background-color: var(--bg-2);
+  color: var(--fg-1);
+}
+.unit-test i {
+  color: var(--green);
+}
 
 /* Colorization for idris code blocks */
 code {