From 2033a48c3e079372d2ce73d04da87f86c812dc28 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 19 Feb 2025 11:22:25 -0500
Subject: [PATCH] Add Utility file

---
 SSG.ipkg                    |   1 +
 src/SSG/Parser/Core.idr     |   5 ++
 src/SSG/Parser/Markdown.idr |   9 ++++
 src/SSG/Parser/Util.idr     | 101 ++++++++++++++++++++++++++++++++++++
 todo.org                    |   1 +
 5 files changed, 117 insertions(+)
 create mode 100644 src/SSG/Parser/Util.idr

diff --git a/SSG.ipkg b/SSG.ipkg
index dadbfdb..5775c67 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -19,6 +19,7 @@ depends = structures
 
 -- modules to install
 modules = SSG.Parser.Core
+        , SSG.Parser.Util
         , SSG.Parser.Markdown
         , SSG.HTML
         , SSG.HTML.ElementTypes
diff --git a/src/SSG/Parser/Core.idr b/src/SSG/Parser/Core.idr
index 17c7725..ab8cc92 100644
--- a/src/SSG/Parser/Core.idr
+++ b/src/SSG/Parser/Core.idr
@@ -106,6 +106,11 @@ export
 skipChars : Has Parser fs => (predicate : Char -> Bool) -> Eff fs ()
 skipChars predicate = send $ SkipChars predicate
 
+||| Detect EoF
+export
+parseEoF : Has Parser fs => Eff fs Bool
+parseEoF = send ParseEoF
+
 --------------------
 -- Effect handler --
 --------------------
diff --git a/src/SSG/Parser/Markdown.idr b/src/SSG/Parser/Markdown.idr
index e760e1b..4f4ade3 100644
--- a/src/SSG/Parser/Markdown.idr
+++ b/src/SSG/Parser/Markdown.idr
@@ -1 +1,10 @@
 module SSG.Parser.Markdown
+
+import SSG.Parser.Core
+import SSG.Parser.Util
+
+import Data.List1
+import Data.Vect
+import Data.Nat
+import Control.Eff
+
diff --git a/src/SSG/Parser/Util.idr b/src/SSG/Parser/Util.idr
new file mode 100644
index 0000000..22aeeeb
--- /dev/null
+++ b/src/SSG/Parser/Util.idr
@@ -0,0 +1,101 @@
+module SSG.Parser.Util
+
+import SSG.Parser.Core
+
+import Data.List1
+import Data.Vect
+import Control.Eff
+
+||| Type alias for parsing errors
+public export
+ParseError : Type
+ParseError = String
+
+||| Type alias for a parser equipped with exception handling
+public export
+PS : Type -> Type
+PS a = Eff [Parser, Except ParseError] a
+
+||| Attempt to run a fallible parser, backtracking on failure
+export
+try : (f : PS a) -> (err : ParseError -> PS a) -> PS a
+try f err = do
+  state <- save
+  result <- lift . runExcept $ f
+  case result of
+    Left e => do
+      load state
+      err e
+    Right result => pure result
+
+||| Variant of `try` that wraps the result in a `Maybe`
+export
+tryMaybe : (f : PS a) -> PS (Maybe a)
+tryMaybe f = try (map Just f) (\_ => pure Nothing)
+
+||| Variant of `try` that wraps the result in an `Either`
+export
+tryEither : (f : PS a) -> PS (Either ParseError a)
+tryEither f = try (map Right f) (\e => pure $ Left e)
+
+||| Attempt to parse each of a list of parsers, returning the first that
+||| succeeds
+export
+oneOfE : (err : ParseError) -> List (PS a) -> PS a
+oneOfE err [] = throw err
+oneOfE err (x :: xs) = do
+  res <- tryMaybe x
+  case res of
+    Nothing => oneOfE err xs
+    Just y => pure y
+
+||| Attempt to parse 0+ of a thing
+export
+many : (f : PS a) -> PS (List a)
+many f = do
+  Just next <- tryMaybe f
+    | _ => pure []
+  map (next ::) (many f)
+
+||| Attempt to parse at least one of a thing, giving the supplied error on
+||| failure
+export
+atLeastOne : (err : ParseError) -> (f : PS a) -> PS (List1 a)
+atLeastOne err f = do
+  Just head <- tryMaybe f
+    | _ => throw err
+  tail <- many f
+  pure $ head ::: tail
+
+||| Attempt to parse one of a list of strings
+export
+theseStrings : List String -> PS String
+theseStrings strs = theseStrings' strs
+  where
+    theseStrings' : List String -> PS String
+    theseStrings' [] = throw "Expected one of \{show strs}"
+    theseStrings' (x :: xs) = do
+      res <- parseExact x
+      case res of
+        Got y => pure y
+        _ => theseStrings' xs
+
+||| Attempt to parse one of a list of chars
+export
+theseChars : List Char -> PS Char
+theseChars cs = do
+  Just [next] <- peek 1
+    | _ => throw "Unexpected EoF"
+  if any (== next) cs
+    then pure next
+    else throw "Expected one of \{show cs}, got \{show next}"
+
+||| Attempt to parse any char not in the list
+export
+notTheseChars : List Char -> PS Char
+notTheseChars cs = do
+  Just [next] <- peek 1
+    | _ => throw "Unexpected EoF"
+  if any (== next) cs
+    then throw "Expected not one of \{show cs}, got \{show next}"
+    else pure next
diff --git a/todo.org b/todo.org
index a8cb81f..1a2d61b 100644
--- a/todo.org
+++ b/todo.org
@@ -6,3 +6,4 @@ Probably want to refine the attribute and value strings, and be smarter about ho
 Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense
 * Parser Core
 ** TODO Refine =location= in =ParserLocation=
+** TODO Error messages