Lines effect

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

src/SSG/Djot.idr

@@ -1 +1 @@
-module Djot
+module SSG.Djot

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'

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"
   ]

test/djot-to-html/001-hello-world/Main.idr

@@ -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

test/djot-to-html/001-hello-world/expected

@@ -1,6 +0,0 @@
-<!DOCTYPE HTML>
-<html lang=en>
-  <body>
-    <p>Hello World!</p>
-  </body>
-</html>

test/djot-to-html/001-hello-world/test.dj

@@ -1 +0,0 @@
-Hello World!

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)
+      ]
+  ]

test/hedgehog/001-lines/expected

@@ -0,0 +1,3 @@
+━━━ Lines effect ━━━
+  ✓ Lines effect equivalent to lines passed 1000 tests.
+  ✓ 1 succeeded.

test/hedgehog/001-lines/pack.toml

@@ -0,0 +1,5 @@
+[custom.all.SSG]
+type = "local"
+path = "../../.."
+ipkg = "SSG.ipkg"
+test = "test/test.ipkg"

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/

test/hedgehog/001-lines/test.ipkg

@@ -1,6 +1,8 @@
 package a-test
 
 depends = SSG
+        , hedgehog
+        , eff
 
 main = Main
 

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