From 77890ba54934b3307f2548766996da605cb940b5 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Thu, 27 Feb 2025 00:47:28 -0500
Subject: [PATCH] Parse inline text

---
 SSG.ipkg                |   2 +
 src/SSG/Djot/Block.idr  |   1 +
 src/SSG/Djot/Inline.idr | 139 ++++++++++++++++++++++++++++++++++++++++
 todo.org                |   5 +-
 4 files changed, 145 insertions(+), 2 deletions(-)
 create mode 100644 src/SSG/Djot/Block.idr
 create mode 100644 src/SSG/Djot/Inline.idr

diff --git a/SSG.ipkg b/SSG.ipkg
index 3b2c315..f9dc0c4 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -26,6 +26,8 @@ modules = SSG.HTML
         , SSG.HTML.ElementTypes
         , SSG.Djot
         , SSG.Djot.Lines
+        , SSG.Djot.Block
+        , SSG.Djot.Inline
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr
new file mode 100644
index 0000000..5601433
--- /dev/null
+++ b/src/SSG/Djot/Block.idr
@@ -0,0 +1 @@
+module SSG.Djot.Block
diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr
new file mode 100644
index 0000000..ecc713d
--- /dev/null
+++ b/src/SSG/Djot/Inline.idr
@@ -0,0 +1,139 @@
+||| Djot inline formatting parser
+module SSG.Djot.Inline
+
+import Control.Eff
+import Data.List.Lazy
+import Data.Maybe
+import Data.String
+import Derive.Prelude
+import Derive.Pretty
+
+-- Just for iutils unit tests
+import System
+
+%language ElabReflection
+
+--******************************
+--*       Data Structures      *
+--******************************
+
+||| Types of inline styling
+public export
+data Inline : Type where
+  Text : (text : String) -> Inline
+
+%runElab derive "Inline" [Eq, Show, Pretty]
+
+--******************************
+--*      Parsing Utilities     *
+--******************************
+
+||| Type alias for inline parsing
+IParser : Type -> Type
+IParser t = Eff [State (List Char), Choose] t
+
+||| Get the next char, modifiying the state
+popChar : IParser Char
+popChar = do
+  x :: xs <- get
+    | [] => empty
+  put xs
+  pure x
+
+||| Get the next char, without modifying the state
+peekChar : IParser Char
+peekChar = do
+  x :: xs <- get
+    | [] => empty
+  pure x
+
+||| Attempt to parse something without propagating the failure
+try : IParser t -> IParser (Maybe t)
+try x = do
+  state <- get
+  x <- lift . runChoose {f = Maybe} $ x
+  case x of
+    Nothing => do
+      put state
+      pure Nothing
+    Just y => pure $ Just y
+
+||| Choose a parser
+oneOf : List (IParser t) -> IParser t
+oneOf [] = empty
+oneOf (x :: xs) = x `alt` oneOf xs
+
+||| Parse 0+ of something
+many : IParser t -> IParser (List t)
+many x = do
+  Just y <- try x
+    | _ => pure []
+  map (y ::) $ many x
+
+||| Run a parser
+runIParser : (str : String) -> IParser t -> Maybe t
+runIParser str x = 
+  fst . extract . runState (unpack str) . runChoose {f = Maybe} $ x
+
+--******************************
+--*           Syntax           *
+--******************************
+
+-- Forward declare so we can get mutually recursive
+||| Top level parser function for Inline Content
+pInline : IParser Inline
+
+||| Parse a character as plain text
+text : IParser Inline
+text = do
+  c <- popChar
+  pure $ Text (singleton c)
+
+-- Definition of pInline
+pInline = oneOf
+  [ text
+  ]
+
+--******************************
+--*       Post Processing      *
+--******************************
+
+||| Combine adjacent Text entries
+combineTexts : List Inline -> List Inline
+combineTexts (Text a :: (Text b :: xs)) =
+  combineTexts (Text (a ++ b) :: xs)
+combineTexts xs = xs
+
+||| Top level post processor
+postProcess : List Inline -> List Inline
+postProcess xs = combineTexts xs
+
+--******************************
+--* Top Level Parsing Function *
+--******************************
+
+||| Parse a string as inline content
+export
+inline : (input : String) -> List Inline
+inline input =
+  postProcess . fromMaybe [] . runIParser input $ many pInline
+
+--******************************
+--*         Unit Tests         *
+--******************************
+
+golden : (input : String) -> (reference : List Inline) -> IO Bool
+golden input reference = do
+  putStrLn "Input: \{show input}"
+  let opts = Opts 78
+  let ref_pretty = Doc.render opts $ pretty reference
+  putStrLn "Reference:\n\{unlines . map ("  " ++) . lines $ ref_pretty}"
+  let output = inline input
+  let out_pretty = Doc.render opts $ pretty output
+  putStrLn "Output:\n\{unlines . map ("  " ++) . lines $ out_pretty}"
+  pure $ reference == output
+
+-- @@test Just text parses as text
+testTextAsText : IO Bool
+testTextAsText =
+  golden "Hello World!" [Text "Hello World!"]
diff --git a/todo.org b/todo.org
index baee7e9..72f3155 100644
--- a/todo.org
+++ b/todo.org
@@ -9,7 +9,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se
 ** TODO Refine =location= in =ParserLocation=
 ** TODO Error messages
 ** TODO Combinators for predictive parsing
-* Djot [0/31]
+* Djot [1/33]
 :PROPERTIES:
 :COOKIE_DATA: recursive
 :END:
@@ -30,7 +30,8 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se
 **** TODO Block Attributes
 **** TODO Heading Links
 *** Inline
-**** TODO Ordinary Text
+**** DONE Ordinary Text
+**** TODO Escaped Text
 **** TODO Link
 **** TODO Image
 **** TODO Autolink