[WIP] Improve parse error (#20)

leanprover · Oct 9, 2024 · cf77ce5 · cf77ce5
1 parent 038c38c
commit cf77ce5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/SHerLOC/Parsing/Operations.lean b/SHerLOC/Parsing/Operations.lean
@@ -160,15 +160,15 @@ def parseOpCode : PState OpCode := do
   if let some op := opCode then
     parseItem "\""
     return op
-  else throw <| (← error "op code")
+  else throw (← errorSimple (String.join ["Unknown op code: '", opCodeString, "'"]))
 
 mutual
 
   partial def parseInputFunc : PState InputFunc := do
     parseItem "{"
     let mut funcInputs : List FuncInput := []
     if ← is "^" then
-      discard <| parseUnusedId
+      discard parseUnusedId
       funcInputs ← parseInputFuncInputs
       parseItem ":"
     let body ← parseInputFuncBody

diff --git a/SHerLOC/Parsing/Parser.lean b/SHerLOC/Parsing/Parser.lean
@@ -46,7 +46,7 @@ structure ParsingState where
 
 abbrev PState (T : Type) := StateT ParsingState (Except (String × List Trace × List Derivation)) T
 
-def error (msg : String) : PState (String × (List Trace) × (List Derivation) ):= do
+def error (msg : String) : PState (String × (List Trace) × (List Derivation)) := do
   let st ← get
   let mut token := ""
   let mut started := false
@@ -62,6 +62,11 @@ def error (msg : String) : PState (String × (List Trace) × (List Derivation) )
   let errorMsg := s!"Parsing error line {st.lineNumber}, column {st.columnNumber} : expected {msg} but found {token}"
   return (errorMsg, st.trace, st.derivations)
 
+def errorSimple (msg : String) : PState (String × (List Trace) × (List Derivation)) := do
+  let st ← get
+  let errorMsg := s!"Parsing error line {st.lineNumber}, column {st.columnNumber} : {msg}"
+  return (errorMsg, st.trace, st.derivations)
+
 def report (msg : String) : PState Unit := do
   let st ← get
   let msg := s!"line {st.lineNumber}, column {st.columnNumber}: {msg}\n"