Introduce better logging.

Led to immediate bug fixes for Pi types.

1 files changed, 17 insertions, 33 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index c9705fb..f9daa62 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -2,6 +2,7 @@ module Obs.Parser
 
 import Data.String
 
+import Obs.Logging
 import Obs.Sort
 import Obs.Syntax
 
@@ -13,12 +14,6 @@ import Text.Parser
 
 %default total
 
-Error : Type -> Type -> Type
-Error tok = Either (List1 (ParsingError tok))
-
-report : List1 (ParsingError tok) -> Error tok a
-report = Left
-
 data ObsTokenKind
   = OTNewline
   | OTIgnore
@@ -230,35 +225,24 @@ postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of
   (OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks
   _ => if ignored tok then postprocess tail else tok :: postprocess tail
 
+castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
+castErr (Right x) = pure x
+castErr (Left errs) = do
+  for_ {b = ()} errs
+    (\(Error msg bounds) =>
+      error $
+      maybe
+        (irrelevantBounds $ msg)
+        (\bounds => MkBounded msg False bounds) $
+      bounds)
+  abort
+
 partial
 export
-parse : String -> Error ObsToken (List Definition)
+parse : String -> Logging ann (List Definition)
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
-    | (_, l, c, rem) => report (Error "failed to lex input" (Just $ MkBounds { startLine = l, startCol = c, endLine = l, endCol = c }) ::: [])
-  (defs, []) <- parse file $ postprocess toks
-    | (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: [])
-  pure defs
-
-printErr : ParsingError tok -> IO ()
-printErr (Error str Nothing)  = putStrLn "error: \{str}"
-printErr (Error str (Just b)) = putStrLn
-  "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
-
-reportErrs : List (ParsingError tok) -> IO a
-reportErrs []          = exitFailure
-reportErrs (e :: errs) = do
-  () <- printErr e
-  reportErrs errs
-
-partial
-export
-parseFile : (fname : String) -> IO (List Definition)
-parseFile fname = do
-  Right str <- readFile fname
-    | Left err => do
-      () <- putStrLn "error: \{show err}"
-      exitFailure
-  let Right defs = parse str
-    | Left err => reportErrs (forget err)
+    | (_, l, c, rem) => inScope "lex" $ fatal "failed to lex input"
+  (defs, []) <- inScope "parse" $ castErr $ parse file $ postprocess toks
+    | (_, (t :: _)) => inScope "parse" $ fatal "unparsed tokens"
   pure defs