From d1e1dd5f59844b66b45ad7d7d1faad588ef7bad5 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 21 Feb 2025 05:40:02 -0500
Subject: [PATCH] Post process inline parsing

---
 src/SSG/Djot/Inline.idr | 82 ++++++++++++++++++++++++++++++-----------
 src/SSG/Djot/Render.idr | 19 +---------
 2 files changed, 62 insertions(+), 39 deletions(-)

diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr
index eed029d..19b07ed 100644
--- a/src/SSG/Djot/Inline.idr
+++ b/src/SSG/Djot/Inline.idr
@@ -6,6 +6,7 @@ import SSG.Parser.Util
 import SSG.Djot.Common
 
 import Control.Eff
+import Control.Monad.Eval
 import Derive.Prelude
 
 -- For iutils unit tests
@@ -13,9 +14,9 @@ import System
 
 %language ElabReflection
 
---**************
---* Data Types *
---**************
+--******************
+--*   Data Types   *
+--******************
 
 public export
 data Inline : Type where
@@ -26,9 +27,51 @@ data Inline : Type where
 
 %runElab derive "Inline" [Show, Eq]
 
---**************
---*   Syntax   *
---**************
+--******************
+--* PostProcessing *
+--******************
+
+-- Combine adjacent `Text`s in the parsed output
+combineTexts : List1 Inline -> Eval (List1 Inline)
+combineTexts xs@(Text c ::: []) = pure xs
+combineTexts (Text c ::: (Text d :: xs)) =
+  combineTexts (Text (c ++ d) ::: xs)
+combineTexts (x ::: tail) = do
+  rest <- combineTexts' tail
+  pure $ x ::: rest
+  where
+    combineTexts' : List Inline -> Eval (List Inline)
+    combineTexts' [] = pure []
+    combineTexts' (y :: []) = pure [y]
+    combineTexts' (Text c :: (Text d :: xs)) =
+      combineTexts' (Text (c ++ d) :: xs)
+    combineTexts' (y :: ys) = do
+      rest <- combineTexts' ys
+      pure $ y :: rest
+
+-- Remove a trailing soft line break from a list of inlines
+removeTrailingSoftBreak : List1 Inline -> Eval (List1 Inline)
+removeTrailingSoftBreak (head ::: tail) = do
+  tail <- inner tail
+  pure $ head ::: tail
+  where
+    inner : List Inline -> Eval (List Inline)
+    inner [] = pure []
+    inner (SoftLineBreak :: []) = pure []
+    inner (x :: xs) = do
+      xs <- inner xs
+      pure $ x :: xs
+
+-- Combine all post processing steps
+postProcess : List1 Inline -> List1 Inline
+postProcess xs = eval $ do
+  xs <- combineTexts xs
+  xs <- removeTrailingSoftBreak xs
+  pure xs
+
+--******************
+--*     Syntax     *
+--******************
 
 ------------------------
 -- Escaped Whitespace --
@@ -98,30 +141,25 @@ inlineElement = oneOfE "" [
 
 export
 inline : PS (List1 Inline)
-inline = atLeastOne "Expected Inline Content" inlineElement
+inline = map postProcess $
+  atLeastOne "Expected Inline Content" inlineElement
 
---**************
---* Unit Tests *
---**************
+--******************
+--*   Unit Tests   *
+--******************
 
 -------------------------------
 -- Testing Utility Functions --
 -------------------------------
 
-export
-inlineFromString : String -> List (Inline)
-inlineFromString str with (asList str)
-  inlineFromString "" | [] = []
-  inlineFromString (strCons c str) | (c :: x) =
-    Text (singleton c) :: inlineFromString str | x
 
 export
 inlineFromString' : String -> List1 (Inline)
-inlineFromString' str =
-  case inlineFromString str of
-    [] => assert_total $ idris_crash "Bad unit test fromString"
-    (x :: xs) => x ::: xs
+inlineFromString' str = Text str ::: []
 
+export
+inlineFromString : String -> List (Inline)
+inlineFromString = forget . inlineFromString'
 -----------
 -- Tests --
 -----------
@@ -130,13 +168,13 @@ inlineFromString' str =
 inlineTextSmoke : IO Bool
 inlineTextSmoke =
   let input = "Hello World!" in
-  golden input (map (Text . singleton) . unpack $ input) (map forget inline)
+  golden input (inlineFromString input) (map forget inline)
 
 -- @@test Escaped Text
 inlineEscapedSmoke : IO Bool
 inlineEscapedSmoke =
   let input = "Hello\\n\\*World"
-      ref = inlineFromString "Hello" ++ [Text "\n", Text "*"] ++ inlineFromString "World"
+      ref = inlineFromString "Hello\n*World"
   in golden input ref (map forget inline)
 
 -- @@test Hard Line Break
diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr
index 7bc1b06..4daf1ce 100644
--- a/src/SSG/Djot/Render.idr
+++ b/src/SSG/Djot/Render.idr
@@ -21,25 +21,10 @@ renderInline NonBreakingSpace =
 renderInline (Text c) =
   (_ ** Text c)
 
--- BUG: Coverage checker bug here?
-partial
-combineTexts : (types : List String ** DList _ Html types)
-  -> (types' : List String ** DList _ Html types')
-combineTexts (_ ** []) = (_ ** [])
-combineTexts xs@(_ ** (elem :: [])) = xs
-combineTexts (_ ** Text content :: (Text str :: rest)) =
-  combineTexts (_ ** Text (content ++ str) :: rest)
-combineTexts (_ ** Text content :: (next :: rest)) =
-  let (_ ** rest) = combineTexts (_ ** (next :: rest))
-  in (_ ** Text content :: rest)
-combineTexts (_ ** (x :: (next :: rest))) =
-  let (_ ** rest) = combineTexts (_ ** (next :: rest))
-  in (_ ** x :: rest)
-
 export
 renderInlines : List Inline -> (types : List String ** DList _ Html types)
-renderInlines xs = assert_total $
-  combineTexts . fromList . map renderInline $ xs
+renderInlines xs =
+  fromList . map renderInline $ xs
 
 headingLevel : HeaderLevel -> (h : String ** IsNormal h)
 headingLevel H1 = ("h1" ** IsH1)