@@ -26,17 +26,15 @@ import Control.Monad.State.Strict
2626import Data.Char
2727import qualified Data.HashSet as HS
2828import Data.List
29−import Data.List.NonEmpty (NonEmpty(..))
3029import qualified Data.List.NonEmpty as NonEmpty
3130import qualified Data.Map as M
3231import Data.Maybe
33−import qualified Data.Set as Set
3432import qualified Data.Text as T
33+import Data.Void (Void(..))
3534import System.FilePath
3635import qualified Text.Parser.Char
3736import qualified Text.Parser.Combinators
3837import qualified Text.Parser.Token as Tok
39−import Text.PrettyPrint.ANSI.Leijen ((<>), (<+>))
4038import qualified Text.PrettyPrint.ANSI.Leijen as PP
4139import Text.Megaparsec ((<?>))
4240import qualified Text.Megaparsec as P
@@ -46,46 +44,15 @@ import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
4644
4745-- | Idris parser with state used during parsing
4846type IdrisParser = StateT IState IdrisInnerParser
49−type IdrisInnerParser = P.Parsec () String
47+type IdrisInnerParser = P.Parsec Void String
5048type ParseState = P.State String
51−type ParseError = P.ParseError (P.Token String) ()
49+type ParseError = P.ParseError (P.Token String) Void
5250
5351parseErrorDoc :: ParseError -> PP.Doc
54−parseErrorDoc (P.TrivialError (pos :| _) un ex)
55− = ppLocation pos <> PP.text ": error:" <+> ppCommas (ppUnexpected un ++ ppExpected ex)
56− where
57− ppCommas :: [PP.Doc] -> PP.Doc
58− ppCommas = PP.sep . PP.punctuate (PP.char ',')
59−
60− ppUnexpected :: Maybe (P.ErrorItem (P.Token String)) -> [PP.Doc]
61− ppUnexpected Nothing = []
62− ppUnexpected (Just item) = [PP.text "unexpected" <+> ppCommas (ppItem item)]
63−
64− ppExpected :: Set.Set (P.ErrorItem (P.Token String)) -> [PP.Doc]
65− ppExpected items
66− | Set.null items = []
67− | otherwise = [PP.text "expected" <+> ppCommas (join . map ppItem . Set.toList $ items)]
68−
69− ppItem :: P.ErrorItem (P.Token String) -> [PP.Doc]
70− ppItem (P.Tokens ts) = (PP.char '"' <>) . (<> PP.char '"') . PP.char <$> NonEmpty.toList ts
71− ppItem (P.Label lbl) = [PP.text $ NonEmpty.toList lbl]
72− ppItem P.EndOfInput = [PP.text "end of input"]
73−parseErrorDoc (P.FancyError (pos :| _) errs) = PP.vcat $ (ppError pos <+>) . ppErrorFancy <$> Set.toList errs
74− where
75− ppErrorFancy :: P.ErrorFancy e -> PP.Doc
76− ppErrorFancy (P.ErrorFail msg) = PP.text msg
77− ppErrorFancy (P.ErrorIndentation ord ref act) = undefined -- Not using megaparsec's indentation yet
78− ppErrorFancy (P.ErrorCustom _) = undefined -- Not using custom errors yet
79−
80−ppLocation :: P.SourcePos -> PP.Doc
81−ppLocation (P.SourcePos name line col) =
82− PP.text name <> PP.char ':' <> PP.int (P.unPos line) <> PP.char ':' <> PP.int (P.unPos col)
83−
84−ppError :: P.SourcePos -> PP.Doc
85−ppError pos = ppLocation pos <> PP.char ':' <+> PP.text "error:"
52+parseErrorDoc = PP.string . P.parseErrorPretty
8653
8754-- | Generalized monadic parsing constraint type
88−type MonadicParsing m = (P.MonadParsec () String m, Tok.TokenParsing m)
55+type MonadicParsing m = (P.MonadParsec Void String m, Tok.TokenParsing m)
8956
9057someSpace' :: MonadicParsing m => m ()
9158someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()