summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Parser/Monad.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Parser/Monad.hs')
-rw-r--r--src/full/Agda/Syntax/Parser/Monad.hs85
1 files changed, 40 insertions, 45 deletions
diff --git a/src/full/Agda/Syntax/Parser/Monad.hs b/src/full/Agda/Syntax/Parser/Monad.hs
index c5cb2d6..3b1015e 100644
--- a/src/full/Agda/Syntax/Parser/Monad.hs
+++ b/src/full/Agda/Syntax/Parser/Monad.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Agda.Syntax.Parser.Monad
@@ -32,7 +32,7 @@ module Agda.Syntax.Parser.Monad
import Control.Exception
import Data.Int
-import Data.Typeable
+import Data.Typeable ( Typeable )
import Control.Monad.State
import Control.Applicative
@@ -44,6 +44,8 @@ import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import qualified Agda.Utils.IO.UTF8 as UTF8
+import Agda.Utils.Pretty
+
{--------------------------------------------------------------------------
The parse monad
--------------------------------------------------------------------------}
@@ -90,12 +92,11 @@ data ParseFlags = ParseFlags
-- | What you get if parsing fails.
data ParseError = ParseError
- { errPos :: Position -- ^ where the error occured
- , errInput :: String -- ^ the remaining input
- , errPrevToken :: String -- ^ the previous token
- , errMsg :: String -- ^ hopefully an explanation
- -- of what happened
- }
+ { errPos :: Position -- ^ where the error occured
+ , errInput :: String -- ^ the remaining input
+ , errPrevToken :: String -- ^ the previous token
+ , errMsg :: String -- ^ hopefully an explanation of what happened
+ }
deriving (Typeable)
instance Exception ParseError
@@ -109,55 +110,49 @@ data ParseResult a = ParseOk ParseState a
--------------------------------------------------------------------------}
instance Monad Parser where
- return x = P $ \s -> ParseOk s x
- P m >>= f = P $ \s -> case m s of
- ParseFailed e -> ParseFailed e
- ParseOk s' x -> unP (f x) s'
- fail msg = P $ \s -> ParseFailed $
- ParseError { errPos = parseLastPos s
- , errInput = parseInp s
- , errPrevToken = parsePrevToken s
- , errMsg = msg
- }
+ return x = P $ \s -> ParseOk s x
+
+ P m >>= f = P $ \s -> case m s of
+ ParseFailed e -> ParseFailed e
+ ParseOk s' x -> unP (f x) s'
+
+ fail msg = P $ \s -> ParseFailed $
+ ParseError { errPos = parseLastPos s
+ , errInput = parseInp s
+ , errPrevToken = parsePrevToken s
+ , errMsg = msg
+ }
instance Functor Parser where
- fmap = liftM
+ fmap = liftM
instance Applicative Parser where
- pure = return
- (<*>) = ap
+ pure = return
+ (<*>) = ap
instance MonadError ParseError Parser where
- throwError e = P $ \_ -> ParseFailed e
- P m `catchError` h = P $ \s -> case m s of
- ParseFailed err -> unP (h err) s
- m' -> m'
+ throwError e = P $ \_ -> ParseFailed e
+
+ P m `catchError` h = P $ \s -> case m s of
+ ParseFailed err -> unP (h err) s
+ m' -> m'
instance MonadState ParseState Parser where
- get = P $ \s -> ParseOk s s
- put s = P $ \_ -> ParseOk s ()
+ get = P $ \s -> ParseOk s s
+ put s = P $ \_ -> ParseOk s ()
instance Show ParseError where
- show err =
- unlines
- [ pos ++ ": " ++ errMsg err
- --, replicate (length pos + 2) ' ' ++ "on '" ++ errPrevToken err ++ "'"
- , errPrevToken err ++ "<ERROR>\n" ++ take 30 (errInput err) ++ "..."
- ]
- where
- pos = show (errPos err)
-
--- showInp "" = "at end of file"
--- showInp t = "on input " ++ elide 5 t
---
--- elide 3 s
--- | length (take 4 s) < 4 = s
--- | otherwise = "..."
--- elide n (c:s) = c : elide (n - 1) s
--- elide _ "" = ""
+ show = prettyShow
+
+instance Pretty ParseError where
+ pretty err = vcat
+ [ pretty (errPos err) <> colon <+> text (errMsg err)
+ , text $ errPrevToken err ++ "<ERROR>"
+ , text $ take 30 (errInput err) ++ "..."
+ ]
instance HasRange ParseError where
- getRange err = posToRange (errPos err) (errPos err)
+ getRange err = posToRange (errPos err) (errPos err)
{--------------------------------------------------------------------------
Running the parser