Add Utility file

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

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

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
+

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

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