From bd94410c019a6c46a70e4e47023d43ea61b5b6c8 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sun, 23 Feb 2025 21:34:10 -0500
Subject: [PATCH] Lines effect

---
 SSG.ipkg                                      |   2 +-
 src/SSG/Djot.idr                              |   2 +-
 src/SSG/Djot/Lines.idr                        | 102 ++++++++++++++++++
 test/Main.idr                                 |   2 +-
 test/djot-to-html/001-hello-world/Main.idr    |  16 ---
 test/djot-to-html/001-hello-world/expected    |   6 --
 test/djot-to-html/001-hello-world/test.dj     |   1 -
 test/hedgehog/001-lines/Main.idr              |  28 +++++
 test/hedgehog/001-lines/expected              |   3 +
 test/hedgehog/001-lines/pack.toml             |   5 +
 .../001-lines}/run                            |   2 +-
 .../001-lines}/test.ipkg                      |   2 +
 todo.org                                      |   2 +
 13 files changed, 146 insertions(+), 27 deletions(-)
 create mode 100644 src/SSG/Djot/Lines.idr
 delete mode 100644 test/djot-to-html/001-hello-world/Main.idr
 delete mode 100644 test/djot-to-html/001-hello-world/expected
 delete mode 100644 test/djot-to-html/001-hello-world/test.dj
 create mode 100644 test/hedgehog/001-lines/Main.idr
 create mode 100644 test/hedgehog/001-lines/expected
 create mode 100644 test/hedgehog/001-lines/pack.toml
 rename test/{djot-to-html/001-hello-world => hedgehog/001-lines}/run (60%)
 rename test/{djot-to-html/001-hello-world => hedgehog/001-lines}/test.ipkg (65%)

diff --git a/SSG.ipkg b/SSG.ipkg
index d156215..3b2c315 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -17,7 +17,6 @@ depends = contrib
         , structures
         , tailrec
         , eff
-        , refined
         , elab-util
         , elab-pretty
         , prettier
@@ -26,6 +25,7 @@ depends = contrib
 modules = SSG.HTML
         , SSG.HTML.ElementTypes
         , SSG.Djot
+        , SSG.Djot.Lines
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr
index 2f11ffc..584fa6a 100644
--- a/src/SSG/Djot.idr
+++ b/src/SSG/Djot.idr
@@ -1 +1 @@
-module Djot
+module SSG.Djot
diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr
new file mode 100644
index 0000000..f8fa26d
--- /dev/null
+++ b/src/SSG/Djot/Lines.idr
@@ -0,0 +1,102 @@
+||| An effect for reading an input as a list of lines
+module SSG.Djot.Lines
+
+import Data.String
+
+import Control.Eff
+
+-- Only for iutils unit tests
+import System
+
+--*********************
+--* Effect Definition *
+--*********************
+
+export
+data Lines : Type -> Type where
+  ||| Peek the next line
+  Peek : Lines (Maybe String)
+  ||| Take the next line
+  Take : Lines (Maybe String)
+
+--*********************
+--*  Effect Actions   *
+--*********************
+
+export
+peek : Has Lines fs => Eff fs (Maybe String)
+peek = send Peek
+
+export
+take : Has Lines fs => Eff fs (Maybe String)
+take = send Take
+
+--*********************
+--*  Effect Handlers  *
+--*********************
+
+||| Split the next line from a string
+nextLine : String -> Maybe (String, String)
+nextLine str =
+  if null str
+    then Nothing
+    else
+      let 
+        (before, after) = break (\c => any (== c) ['\r', '\n']) str
+      in Just (before, removeNewline after)
+  where
+    -- If `after` is empty, we have hit the end of the string, and there is no newline
+    -- character to remove. If it has contents, then we need to remove the newline
+    removeNewline : String -> String
+    removeNewline str with (strM str)
+      removeNewline "" | StrNil = ""
+      removeNewline (strCons '\n' xs) | (StrCons '\n' xs) = xs
+      -- Handle either a \r or a \r\n
+      removeNewline (strCons '\r' xs) | (StrCons '\r' xs) with (strM xs)
+        removeNewline (strCons '\r' "") | (StrCons '\r' "") | StrNil = ""
+        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons '\n' xs1) = xs1
+        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons x xs1) = strCons x xs1
+      -- We shouldn't ever hit this case, as we would have to have contents after the
+      -- break, but no newline character, but we fill it in for the sake of totality
+      removeNewline (strCons x xs) | (StrCons x xs) = str
+
+unLines : String -> Lines s -> (s, String)
+unLines str Peek =
+  case nextLine str of
+    Nothing => (Nothing, str)
+    Just (before, after) => (Just before, str)
+unLines str Take =
+  case nextLine str of
+    Nothing => (Nothing, str)
+    Just (before, after) => (Just before, after)
+
+||| Feed a `Lines` from a provided input string
+export
+runLines : Has Lines fs =>
+  (input : String) -> Eff fs t -> Eff (fs - Lines) (t, String)
+runLines input =
+  handleRelayS input (\x, y => pure (y, x)) $ \input2, lns, f =>
+    let (vv, input3) = unLines input2 lns
+    in f input3 vv
+
+--*********************
+--*    Unit Tests     *
+--*********************
+
+-- @@test runLines Smoke Test
+runLinesSmoke : IO Bool
+runLinesSmoke = do
+  let input = "Hello\nWorld\n\n"
+  putStrLn "Input: \{show input}"
+  let reference = lines input
+  putStrLn "Reference: \{show reference}"
+  let (output, rest) = extract $ runLines input lines'
+  putStrLn "Output: \{show output}"
+  putStrLn "Rest: \{show rest}"
+  pure $ output == reference && null rest
+  where
+    lines' : Eff [Lines] (List String)
+    lines' = do
+      Just next <- take
+        | _ => pure []
+      map (next ::) lines'
diff --git a/test/Main.idr b/test/Main.idr
index 0437780..b8ffd00 100644
--- a/test/Main.idr
+++ b/test/Main.idr
@@ -4,5 +4,5 @@ import Test.Golden.RunnerHelper
 
 main : IO ()
 main = goldenRunner
-  [ "Djot -> HTML Golden Values" `atDir` "djot-to-html"
+  [ "Hedgehog Tests" `atDir` "hedgehog"
   ]
diff --git a/test/djot-to-html/001-hello-world/Main.idr b/test/djot-to-html/001-hello-world/Main.idr
deleted file mode 100644
index 97d8771..0000000
--- a/test/djot-to-html/001-hello-world/Main.idr
+++ /dev/null
@@ -1,16 +0,0 @@
-module Main
-
-import SSG.Djot
-import SSG.HTML
-
-import System
-import System.File
-
-main : IO ()
-main = do
-  Right contents <- readFile "test.dj"
-    | Left err => do
-      printLn err
-      exitFailure
-  let parsed = djot contents
-  putStr . render . renderHtml $ parsed
diff --git a/test/djot-to-html/001-hello-world/expected b/test/djot-to-html/001-hello-world/expected
deleted file mode 100644
index 130955a..0000000
--- a/test/djot-to-html/001-hello-world/expected
+++ /dev/null
@@ -1,6 +0,0 @@
-<!DOCTYPE HTML>
-<html lang=en>
-  <body>
-    <p>Hello World!</p>
-  </body>
-</html>
\ No newline at end of file
diff --git a/test/djot-to-html/001-hello-world/test.dj b/test/djot-to-html/001-hello-world/test.dj
deleted file mode 100644
index 980a0d5..0000000
--- a/test/djot-to-html/001-hello-world/test.dj
+++ /dev/null
@@ -1 +0,0 @@
-Hello World!
diff --git a/test/hedgehog/001-lines/Main.idr b/test/hedgehog/001-lines/Main.idr
new file mode 100644
index 0000000..4d35aff
--- /dev/null
+++ b/test/hedgehog/001-lines/Main.idr
@@ -0,0 +1,28 @@
+module Main
+
+import SSG.Djot.Lines
+
+import Control.Eff
+import Data.String
+import Hedgehog
+
+lines' : Eff [Lines] (List String)
+lines' = do
+  Just next <- take
+    | _ => pure []
+  map (next ::) lines'
+
+propLinesEquiv : Property
+propLinesEquiv = property $ do
+  str <- forAll $ string (linear 0 256) ascii
+  let std_lines = lines str
+  let (our_lines, rest) = extract $ runLines str lines'
+  our_lines === std_lines
+
+main : IO ()
+main = test $
+  [ MkGroup
+      "Lines effect"
+      [ ("Lines effect equivalent to lines", propLinesEquiv)
+      ]
+  ]
diff --git a/test/hedgehog/001-lines/expected b/test/hedgehog/001-lines/expected
new file mode 100644
index 0000000..9050bda
--- /dev/null
+++ b/test/hedgehog/001-lines/expected
@@ -0,0 +1,3 @@
+━━━ Lines effect ━━━
+  ✓ Lines effect equivalent to lines passed 1000 tests.
+  ✓ 1 succeeded.
diff --git a/test/hedgehog/001-lines/pack.toml b/test/hedgehog/001-lines/pack.toml
new file mode 100644
index 0000000..d2e5465
--- /dev/null
+++ b/test/hedgehog/001-lines/pack.toml
@@ -0,0 +1,5 @@
+[custom.all.SSG]
+type = "local"
+path = "../../.."
+ipkg = "SSG.ipkg"
+test = "test/test.ipkg"
diff --git a/test/djot-to-html/001-hello-world/run b/test/hedgehog/001-lines/run
similarity index 60%
rename from test/djot-to-html/001-hello-world/run
rename to test/hedgehog/001-lines/run
index 6b5ab53..4d6fd1b 100644
--- a/test/djot-to-html/001-hello-world/run
+++ b/test/hedgehog/001-lines/run
@@ -1,6 +1,6 @@
 rm -rf build/
 
 flock "$1" pack -q install-deps test.ipkg
-pack -q run test.ipkg
+HEDGEHOG_COLOR=0 pack -q run test.ipkg -n 1000
 
 rm -rf build/
diff --git a/test/djot-to-html/001-hello-world/test.ipkg b/test/hedgehog/001-lines/test.ipkg
similarity index 65%
rename from test/djot-to-html/001-hello-world/test.ipkg
rename to test/hedgehog/001-lines/test.ipkg
index 0efef9e..e727cbf 100644
--- a/test/djot-to-html/001-hello-world/test.ipkg
+++ b/test/hedgehog/001-lines/test.ipkg
@@ -1,6 +1,8 @@
 package a-test
 
 depends = SSG
+        , hedgehog
+        , eff
 
 main = Main
 
diff --git a/todo.org b/todo.org
index 330438e..baee7e9 100644
--- a/todo.org
+++ b/todo.org
@@ -47,3 +47,5 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se
 **** TODO Symbols
 **** TODO Raw Inline
 **** TODO Inline Attributes
+*** Lines effect
+**** TODO =IO= Backed implementation