{- |
Module      : Parser.Util
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (ghc-wasm-meta)

This module provides shared utility parsers
used across all other @Parser.*@ modules.
-}
module Parser.Util where

import Control.Monad.Combinators.Expr
import Data.Char (isLetter, isLowerCase, isUpperCase)
import Data.Text qualified as T
import Text.Megaparsec (
  MonadParsec (hidden, takeWhile1P, takeWhileP),
  between,
  match,
  (<?>),
 )
import Text.Megaparsec.Char (space1)
import Text.Megaparsec.Char.Lexer qualified as L

------------------------------------------------------------------------------------------

-- * Types

{- | Constraint alias for a Megaparsec parser over a t'Text' stream with no custom
error type.
-}
type Parser = MonadParsec Void Text

------------------------------------------------------------------------------------------

-- * Lexer

-- | Space consumer that only skips whitespace
sc :: (MonadParsec Void Text m) => m ()
sc :: forall (m :: * -> *). MonadParsec Void Text m => m ()
sc =
  m () -> m () -> m () -> m ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space
    m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1 -- discard spaces
    m ()
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty -- no line comments
    m ()
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty -- no block comments

-- | Wraps a parser so that it consumes trailing whitespace via 'sc'.
lexeme :: (Parser m) => m a -> m a
lexeme :: forall (m :: * -> *) a. Parser m => m a -> m a
lexeme = m () -> m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m () -> m a -> m a
L.lexeme m ()
forall (m :: * -> *). MonadParsec Void Text m => m ()
sc

-- | Parses the exact given t'Text' token and consumes any trailing whitespace.
symbol :: (Parser m) => Text -> m Text
symbol :: forall (m :: * -> *). Parser m => Text -> m Text
symbol = m () -> Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> Tokens s -> m (Tokens s)
L.symbol m ()
forall (m :: * -> *). MonadParsec Void Text m => m ()
sc

-- | Runs a t'Parser' via 'match' but strips whitespace from the resulting 'Text'.
matchNoSpaces :: (Parser m) => m a -> m (Text, a)
matchNoSpaces :: forall (m :: * -> *) a. Parser m => m a -> m (Text, a)
matchNoSpaces m a
p = (Text -> Text) -> (Text, a) -> (Text, a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Text -> Text
T.strip ((Text, a) -> (Text, a)) -> m (Text, a) -> m (Text, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (Tokens Text, a)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> m (Tokens s, a)
match m a
p

------------------------------------------------------------------------------------------

-- * Name parsers

{- | Parses a name that starts with one or more uppercase letters,
followed by zero or more letters.
Used for predicate symbols.
-}
pUpperName :: (Parser m) => m Text
pUpperName :: forall (m :: * -> *). Parser m => m Text
pUpperName =
  do
    start <- Maybe String -> (Token Text -> Bool) -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhile1P (String -> Maybe String
forall a. a -> Maybe a
Just String
"uppercase") Char -> Bool
Token Text -> Bool
isUpperCase
    end <- takeWhileP (Just "letter") isLetter
    pure (start <> end)

{- | Parses a name that starts with one or more lowercase letters,
followed by zero or more letters.
Used for function symbols and variables.
-}
pLowerName :: (Parser m) => m Text
pLowerName :: forall (m :: * -> *). Parser m => m Text
pLowerName =
  do
    start <- Maybe String -> (Token Text -> Bool) -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhile1P (String -> Maybe String
forall a. a -> Maybe a
Just String
"lowercase") Char -> Bool
Token Text -> Bool
isLowerCase
    end <- takeWhileP (Just "letter") isLetter
    pure (start <> end)

{- | Parses a symbolic name, i.e. any non-empty sequence of characters
that are neither @(@ nor @)@.
Used for parsing rule applications.
-}
pSymbolicName :: (Parser m) => m Text
pSymbolicName :: forall (m :: * -> *). Parser m => m Text
pSymbolicName =
  Maybe String -> (Token Text -> Bool) -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhile1P (String -> Maybe String
forall a. a -> Maybe a
Just String
"symbolic letter") (Char -> String -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` (String
"()" :: String))
    m Text -> String -> m Text
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"name"

{- | Parses arbitrary characters, excluding the control characters
@\\28@, @\\29@, @\\30@, and @\\31@ that are used as separators in
t'Parser.IncompleteProof'.
-}
pText :: (Parser m) => m Text
pText :: forall (m :: * -> *). Parser m => m Text
pText = Maybe String -> (Token Text -> Bool) -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP (String -> Maybe String
forall a. a -> Maybe a
Just String
"text") (Char -> String -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`notElem` (String
"\28\29\30\31" :: String)) m Text -> String -> m Text
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"text"

------------------------------------------------------------------------------------------

-- * Symbol parsers

-- | Parses a comma @,@.
comma :: (Parser m) => m Text
comma :: forall (m :: * -> *). Parser m => m Text
comma = Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
","

-- | Parses a minus sign @-@.
minus :: (Parser m) => m Text
minus :: forall (m :: * -> *). Parser m => m Text
minus = Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"-"

-- | Wraps a parser between @(@ and @)@.
parens :: (Parser m) => m a -> m a
parens :: forall (m :: * -> *) a. Parser m => m a -> m a
parens = m Text -> m Text -> m a -> m a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"(") (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
")")

-- | Wraps a parser between @[@ and @]@.
brackets :: (Parser m) => m a -> m a
brackets :: forall (m :: * -> *) a. Parser m => m a -> m a
brackets = m Text -> m Text -> m a -> m a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"[") (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"]")

------------------------------------------------------------------------------------------

-- * Operator combinators

-- | Creates a left-associative infix operator for use with 'makeExprParser'.
binary :: (Parser m) => Text -> (a -> a -> a) -> Operator m a
binary :: forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a -> a) -> Operator m a
binary Text
name a -> a -> a
f = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (a -> a -> a
f (a -> a -> a) -> m Text -> m (a -> a -> a)
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ m Text -> m Text
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
hidden (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
name))

{- | Creates a prefix operator for use with 'makeExprParser'.
Defined specifically so that multiple prefix symbols can get parsed without parentheses.
-}
prefix :: (Parser m) => Text -> (a -> a) -> Operator m a
prefix :: forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a) -> Operator m a
prefix Text
name a -> a
f = m (a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (m (a -> a) -> Operator m a) -> m (a -> a) -> Operator m a
forall a b. (a -> b) -> a -> b
$ ((a -> a) -> (a -> a) -> a -> a) -> (a -> a) -> [a -> a] -> a -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) a -> a
forall a. a -> a
id ([a -> a] -> a -> a) -> m [a -> a] -> m (a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a -> a) -> m [a -> a]
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (a -> a
f (a -> a) -> m Text -> m (a -> a)
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ m Text -> m Text
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
hidden (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
name))