summaryrefslogtreecommitdiff
path: root/src/Obs/Parser.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Parser.idr')
-rw-r--r--src/Obs/Parser.idr50
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