{- |
Module: Agda.Unused.Parse

Parsers for roots.
-}
module Agda.Unused.Parse
  ( parseConfig
  ) where

import Agda.Unused.Types.Name
  (Name(..), NamePart(..), QName(..))
import Agda.Unused.Types.Root
  (Root(..), Roots, fromList)
import Agda.Unused.Utils
  (mapLeft)

import Control.Monad
  (void)
import Data.Char
  (isSpace)
import Data.Text
  (Text)
import qualified Data.Text
  as T
import Data.Void
  (Void)
import Text.Megaparsec
  (Parsec, (<|>), between, many, parse, satisfy, some, try)
import Text.Megaparsec.Char
  (char, space1)
import qualified Text.Megaparsec.Char.Lexer
  as L
import Text.Megaparsec.Error
  (errorBundlePretty)

-- ## Utilities

isNameChar
  :: Char
  -> Bool
isNameChar :: Char -> Bool
isNameChar '.'
  = Bool
False
isNameChar '('
  = Bool
False
isNameChar ')'
  = Bool
False
isNameChar c :: Char
c | Char -> Bool
isSpace Char
c
  = Bool
False
isNameChar _
  = Bool
True

listMaybe
  :: [a]
  -> Maybe [a]
listMaybe :: [a] -> Maybe [a]
listMaybe []
  = Maybe [a]
forall a. Maybe a
Nothing
listMaybe xs :: [a]
xs@(_ : _)
  = [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
xs

-- ## Parsers

type Parser
  = Parsec Void Text

parseSpace
  :: Parser ()
parseSpace :: Parser ()
parseSpace
  = Parser () -> Parser () -> Parser () -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1
    (Tokens Text -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment "--")
    (Tokens Text -> Tokens Text -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> Tokens s -> m ()
L.skipBlockComment "{-" "-}")

parseDot
  :: Parser ()
parseDot :: Parser ()
parseDot
  = ParsecT Void Text Identity Char -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Token Text
'.')

parseHyphen
  :: Parser ()
parseHyphen :: Parser ()
parseHyphen
  = ParsecT Void Text Identity Char -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Token Text
'-')

parseParens
  :: Parser a
  -> Parser a
parseParens :: Parser a -> Parser a
parseParens
  = ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Token Text
'(') (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Token Text
')')

parseNamePart
  :: Parser NamePart
parseNamePart :: Parser NamePart
parseNamePart
  = RawName -> NamePart
Id (RawName -> NamePart)
-> ParsecT Void Text Identity RawName -> Parser NamePart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity RawName
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ((Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
Token Text -> Bool
isNameChar)

parseName
  :: Parser Name
parseName :: Parser Name
parseName
  = [NamePart] -> Name
Name ([NamePart] -> Name)
-> ParsecT Void Text Identity [NamePart] -> Parser Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser NamePart -> ParsecT Void Text Identity [NamePart]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser NamePart
parseNamePart

parseQName
  :: Parser QName
parseQName :: Parser QName
parseQName
  = Parser QName -> Parser QName
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Name -> QName -> QName
Qual (Name -> QName -> QName)
-> Parser Name -> ParsecT Void Text Identity (QName -> QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Name
parseName ParsecT Void Text Identity (QName -> QName)
-> Parser () -> ParsecT Void Text Identity (QName -> QName)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
parseDot ParsecT Void Text Identity (QName -> QName)
-> Parser QName -> Parser QName
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser QName
parseQName)
  Parser QName -> Parser QName -> Parser QName
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> QName
QName (Name -> QName) -> Parser Name -> Parser QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Name
parseName

parseIgnore
  :: Parser QName
parseIgnore :: Parser QName
parseIgnore
  = Parser QName -> Parser QName
forall a. Parser a -> Parser a
parseParens (Parser () -> Parser () -> Parser QName -> Parser QName
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between Parser ()
parseSpace Parser ()
parseSpace Parser QName
parseQName)
  Parser QName -> Parser () -> Parser QName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
parseSpace

parseRootName
  :: Parser QName
parseRootName :: Parser QName
parseRootName
  = Parser ()
parseHyphen
  Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
parseSpace
  Parser () -> Parser QName -> Parser QName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser QName
parseQName
  Parser QName -> Parser () -> Parser QName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
parseSpace

parseRootNames
  :: Parser (Maybe [QName])
parseRootNames :: Parser (Maybe [QName])
parseRootNames
  = [QName] -> Maybe [QName]
forall a. [a] -> Maybe [a]
listMaybe ([QName] -> Maybe [QName])
-> ParsecT Void Text Identity [QName] -> Parser (Maybe [QName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser QName -> ParsecT Void Text Identity [QName]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser QName
parseRootName

parseRoot
  :: Parser Root
parseRoot :: Parser Root
parseRoot
  = QName -> Maybe [QName] -> Root
Root
  (QName -> Maybe [QName] -> Root)
-> Parser QName
-> ParsecT Void Text Identity (Maybe [QName] -> Root)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser QName
parseQName
  ParsecT Void Text Identity (Maybe [QName] -> Root)
-> Parser () -> ParsecT Void Text Identity (Maybe [QName] -> Root)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
parseSpace
  ParsecT Void Text Identity (Maybe [QName] -> Root)
-> Parser (Maybe [QName]) -> Parser Root
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe [QName])
parseRootNames

parseRootEither
  :: Parser (Either QName Root)
parseRootEither :: Parser (Either QName Root)
parseRootEither
  = QName -> Either QName Root
forall a b. a -> Either a b
Left (QName -> Either QName Root)
-> Parser QName -> Parser (Either QName Root)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser QName
parseIgnore
  Parser (Either QName Root)
-> Parser (Either QName Root) -> Parser (Either QName Root)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Root -> Either QName Root
forall a b. b -> Either a b
Right (Root -> Either QName Root)
-> Parser Root -> Parser (Either QName Root)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Root
parseRoot

parseRoots
  :: Parser Roots
parseRoots :: Parser Roots
parseRoots
  = [Either QName Root] -> Roots
fromList ([Either QName Root] -> Roots)
-> ParsecT Void Text Identity [Either QName Root] -> Parser Roots
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Either QName Root)
-> ParsecT Void Text Identity [Either QName Root]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser (Either QName Root)
parseRootEither

-- | Parse configuration, producing either an error or a collection of roots.
parseConfig
  :: Text
  -> Either Text Roots
parseConfig :: Text -> Either Text Roots
parseConfig
  = (RawName -> Text) -> Either RawName Roots -> Either Text Roots
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft RawName -> Text
T.pack
  (Either RawName Roots -> Either Text Roots)
-> (Text -> Either RawName Roots) -> Text -> Either Text Roots
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ParseErrorBundle Text Void -> RawName)
-> Either (ParseErrorBundle Text Void) Roots
-> Either RawName Roots
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft ParseErrorBundle Text Void -> RawName
forall s e.
(Stream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> RawName
errorBundlePretty
  (Either (ParseErrorBundle Text Void) Roots -> Either RawName Roots)
-> (Text -> Either (ParseErrorBundle Text Void) Roots)
-> Text
-> Either RawName Roots
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Roots
-> RawName -> Text -> Either (ParseErrorBundle Text Void) Roots
forall e s a.
Parsec e s a -> RawName -> s -> Either (ParseErrorBundle s e) a
parse (Parser ()
parseSpace Parser () -> Parser Roots -> Parser Roots
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Roots
parseRoots) ".agda-roots"