From b1a4e1a941b648ceadcc7560767646ddc2c3b15f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sun, 26 Jan 2025 20:51:00 -0500
Subject: [PATCH] core: Remove type argument from ParseCharResult

---
 src/Parser/Interface.md   |  6 +++---
 src/Parser/ParserState.md | 42 +++++++++++++--------------------------
 2 files changed, 17 insertions(+), 31 deletions(-)

diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md
index 18df77a..ddf26c5 100644
--- a/src/Parser/Interface.md
+++ b/src/Parser/Interface.md
@@ -236,7 +236,7 @@ export
 parseExactChar : Char -> Parser Char
 parseExactChar c = do
   pnote "Parsing exact char: \{show c}"
-  result <- parseChar (== c) id
+  result <- parseChar (== c)
   case result of
     GotChar char => pure char
     GotError err => throwParseError "Got \{show err} Expected \{show c}"
@@ -250,7 +250,7 @@ export
 parseTheseChars : List Char -> Parser Char
 parseTheseChars cs = do
   pnote "Parsing one of: \{show cs}"
-  result <- parseChar (\x => any (== x) cs) id
+  result <- parseChar (\x => any (== x) cs)
   case result of
     GotChar char => pure char
     GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
@@ -268,7 +268,7 @@ exactString str with (asList str)
     pure ""
   exactString input@(strCons c str) | (c :: x) = do
     pnote "Parsing exact string \{show input}"
-    GotChar next <- parseChar (== c) id
+    GotChar next <- parseChar (== c)
       | GotError err => throwParseError "Got \{show err} expected \{show c}"
       | EndOfInput => throwParseError "End of input"
     rest <- exactString str | x
diff --git a/src/Parser/ParserState.md b/src/Parser/ParserState.md
index fb7c481..703e5a7 100644
--- a/src/Parser/ParserState.md
+++ b/src/Parser/ParserState.md
@@ -195,10 +195,10 @@ btraverse fun (MkInternal input length line_starts position end_of_input) =
 ```idris
 ||| Three way result returned from attempting to parse a single char
 public export
-data ParseCharResult : Type -> Type where
-  GotChar : (char : Char) -> ParseCharResult e
-  GotError : (err : e) -> ParseCharResult e
-  EndOfInput : ParseCharResult e
+data ParseCharResult : Type where
+  GotChar : (char : Char) -> ParseCharResult
+  GotError : (err : Char) -> ParseCharResult
+  EndOfInput : ParseCharResult
 ```
 
 ## The Effect Type
@@ -210,8 +210,7 @@ data ParserState : Type -> Type where
   Load : (ParserInternal Id) -> ParserState ()
   -- TODO: Maybe add a ParseString that parses a string of characters as a 
   -- string using efficent slicing?
-  ParseChar : (predicate : Char -> Bool) -> (err : Char -> e) 
-    -> ParserState (ParseCharResult e)
+  ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult
   ParseEoF : ParserState Bool
   Note : Lazy String -> ParserState ()
 ```
@@ -220,7 +219,7 @@ data ParserState : Type -> Type where
 Show (ParserState t) where
   show Save = "Saving state"
   show (Load pi) = "Loading state \{show pi}"
-  show (ParseChar predicate err) = "Parsing char"
+  show (ParseChar predicate) = "Parsing char"
   show ParseEoF = "Parsing EoF"
   show (Note _) = "Note"
 -->
@@ -242,22 +241,9 @@ load pi = send $ Load pi
 ||| predicate, updates the state if parsing succeeds, does not alter it in an 
 ||| error condition.
 export 
-parseChar : Has ParserState fs => (predicate : Char -> Bool) -> (err : Char -> e) 
-  -> Eff fs (ParseCharResult e)
-parseChar predicate err = send $ ParseChar predicate err
-
-||| Wrapper for parseChar that folds the error message into effect stack with the
-||| provided callback
-export
-parseCharE : Has ParserState fs => Has (Except e) fs => 
-  (predicate : Char -> Bool) -> (err : Char -> e) -> (eof : Lazy e)
-  -> Eff fs Char
-parseCharE predicate err eof = do
-  result <- parseChar predicate id
-  case result of 
-    GotChar char => pure char
-    GotError x => throw $ err x
-    EndOfInput => throw eof
+parseChar : Has ParserState fs => (predicate : Char -> Bool)
+  -> Eff fs ParseCharResult
+parseChar predicate = send $ ParseChar predicate 
 
 ||| "Parse" the end of input, returning `True` if the parser state is currently
 ||| at the end of the input
@@ -285,14 +271,14 @@ handleParserStateIO pi Save = do
 handleParserStateIO pi (Load pj) = do
   pj <- btraverse newIORef pj
   writeIORef pi pj
-handleParserStateIO pi (ParseChar predicate err) = do
+handleParserStateIO pi (ParseChar predicate) = do
   pi <- readIORef pi
   False <- readIORef pi.end_of_input
-    | _ => pure $ EndOfInput
+    | _ => pure EndOfInput
   position <- readIORef pi.position
   let char = assert_total $ strIndex pi.input (cast position.index)
   True <- pure $ predicate char
-    | _ => pure . GotError $ err char
+    | _ => pure $ GotError char
   -- Our refinement type on the position forces us to check that the length is
   -- in bounds after incrementing it, if its out of bounds, set the end_of_input
   -- flag
@@ -342,7 +328,7 @@ handleParserStateIODebug x y = do
 unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id)
 unPS pi Save = (pi, pi)
 unPS pi (Load pj) = ((), pi)
-unPS pi (ParseChar predicate err) = 
+unPS pi (ParseChar predicate) = 
   if pi.end_of_input
     then (EndOfInput, pi)
     else let
@@ -353,7 +339,7 @@ unPS pi (ParseChar predicate err) =
           (GotChar char, {end_of_input := True} pi)
         Just (Element next _) => 
           (GotChar char, {position := MkIndex next} pi)
-      else (GotError $ err char, pi)
+      else (GotError char, pi)
 unPS pi ParseEoF = (pi.end_of_input, pi)
 unPS pi (Note _) = ((), pi)