From 25920def747869d050ec0384e0ec4cb0799c53fa Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 9 Feb 2025 07:52:44 -0500 Subject: [PATCH 1/7] tweak alert styles a bit --- resources/admonitions.css | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/resources/admonitions.css b/resources/admonitions.css index 801cf4d..eed2bb5 100644 --- a/resources/admonitions.css +++ b/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 */ From 5ad9ff656f95d610b2abee01dc1272023cecdfc0 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 9 Feb 2025 07:57:22 -0500 Subject: [PATCH 2/7] Add blog entry to about page --- projects/Markdown/About.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/projects/Markdown/About.md b/projects/Markdown/About.md index 0ac75d5..1b76ca4 100644 --- a/projects/Markdown/About.md +++ b/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/) From 972b73f665c50f201db383a748f6b13b6608fe22 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 9 Feb 2025 17:10:46 -0500 Subject: [PATCH 3/7] Link styling tweaks --- lib/Render/Head.rakumod | 1 - lib/Render/Util.rakumod | 3 +- .../Idris/src/LessMacrosMoreTypes/Printf.md | 38 ++++++++++++++----- 3 files changed, 31 insertions(+), 11 deletions(-) diff --git a/lib/Render/Head.rakumod b/lib/Render/Head.rakumod index c93c3ff..22fa4ee 100644 --- a/lib/Render/Head.rakumod +++ b/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; ] } diff --git a/lib/Render/Util.rakumod b/lib/Render/Util.rakumod index 79ece58..0d7adcb 100644 --- a/lib/Render/Util.rakumod +++ b/lib/Render/Util.rakumod @@ -10,7 +10,8 @@ sub show-html($html) is export { # Work around HTML::Functional automatically putting newlines between tags $out ~~ s:g/'' \v+ ''/<\/i>/; $out ~~ s:g/\v+ ''/<\/a>/; - $out ~~ s:g/',' \v+ ' [!NOTE] > As this is a literate Idris document, and we haven't defined our `printf` @@ -33,13 +34,32 @@ 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 + example_usage = printf "%s %d %2d" "hello" 1 2 ``` - - ## 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) -> 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 +``` + ## Calculating a Type From a Format String ## printf + +## Working with run-time format strings From 448908c18eb095a4aae4aee57037f0a4569fc7cd Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 9 Feb 2025 18:09:06 -0500 Subject: [PATCH 4/7] post now command --- blog | 15 +++++++++++++++ lib/DB/Post.rakumod | 1 + lib/Render/Util.rakumod | 1 - resources/code.css | 1 + 4 files changed, 17 insertions(+), 1 deletion(-) diff --git a/blog b/blog index 6784af9..5051bef 100755 --- a/blog +++ b/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", diff --git a/lib/DB/Post.rakumod b/lib/DB/Post.rakumod index c1e98c7..d231956 100644 --- a/lib/DB/Post.rakumod +++ b/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), diff --git a/lib/Render/Util.rakumod b/lib/Render/Util.rakumod index 0d7adcb..d2b2d77 100644 --- a/lib/Render/Util.rakumod +++ b/lib/Render/Util.rakumod @@ -11,7 +11,6 @@ sub show-html($html) is export { $out ~~ s:g/'' \v+ ''/<\/i>/; $out ~~ s:g/\v+ ''/<\/a>/; $out ~~ s:g/\s+ ',' \s+ ' code { padding: 0 0.25rem; + border-radius: 0.25rem; } /* Styling for fenced code blocks */ From e4e0349a32206333cf2cd7fab970dc0d6be232ef Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 9 Feb 2025 22:27:17 -0500 Subject: [PATCH 5/7] Unit test styling --- lib/Render/Util.rakumod | 2 ++ resources/code.css | 26 ++++++++++++++++++++++++++ resources/colors.css | 10 ++++++++++ 3 files changed, 38 insertions(+) diff --git a/lib/Render/Util.rakumod b/lib/Render/Util.rakumod index d2b2d77..475a79a 100644 --- a/lib/Render/Util.rakumod +++ b/lib/Render/Util.rakumod @@ -11,6 +11,8 @@ sub show-html($html) is export { $out ~~ s:g/'' \v+ ''/<\/i>/; $out ~~ s:g/\v+ ''/<\/a>/; $out ~~ s:g/\s+ ',' \s+ '' \s* '
  '/
<\/i>Unit Test<\/span>
/;
    $out
 }
 
diff --git a/resources/code.css b/resources/code.css
index f633095..a3e1758 100644
--- a/resources/code.css
+++ b/resources/code.css
@@ -19,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;
 }
diff --git a/resources/colors.css b/resources/colors.css
index 42db252..5c9ec9c 100644
--- a/resources/colors.css
+++ b/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 {

From cc9b482431d80188c5fdf06ec4f43966bd590abc Mon Sep 17 00:00:00 2001
From: Nathan McCarty 
Date: Sun, 9 Feb 2025 23:16:20 -0500
Subject: [PATCH 6/7] GFM Alert tweaks

---
 resources/admonitions.css | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/resources/admonitions.css b/resources/admonitions.css
index eed2bb5..0c57da9 100644
--- a/resources/admonitions.css
+++ b/resources/admonitions.css
@@ -65,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);
 }

From f887be396badcb17ae210144ac25cd3d0dbc017b Mon Sep 17 00:00:00 2001
From: Nathan McCarty 
Date: Mon, 10 Feb 2025 09:37:42 -0500
Subject: [PATCH 7/7] Writing checkpoint

---
 .../Idris/src/LessMacrosMoreTypes/Printf.md   | 182 +++++++++++++++++-
 1 file changed, 176 insertions(+), 6 deletions(-)

diff --git a/projects/Idris/src/LessMacrosMoreTypes/Printf.md b/projects/Idris/src/LessMacrosMoreTypes/Printf.md
index 96da238..4e05b99 100644
--- a/projects/Idris/src/LessMacrosMoreTypes/Printf.md
+++ b/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
@@ -33,10 +34,19 @@ equivalent:
 
 ```idris
 failing
-  example_usage : String
-  example_usage = printf "%s %d %2d" "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
@@ -47,9 +57,9 @@ be supporting, as well as a constructor to hold literal components.
 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
+  ||| A slot that should be filled  in with a number, padded to a certian number
   ||| of digits
-  PaddedNumber : (digits : Nat) -> Format
+  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
@@ -58,8 +68,168 @@ data Format : Type where
   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
 
-## Working with run-time format strings
+### 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
+
+ 
+