{- |
Module      : Parser.Rule
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 defines parsers for t'RuleApplication's and t'Reference's.
-}
module Parser.Rule where

import Control.Monad.Combinators.Expr (
  Operator (InfixL, Prefix),
  makeExprParser,
 )
import Fitch.Proof
import Parser.Util
import Text.Megaparsec (
  MonadParsec (eof, try),
  PosState (
    PosState,
    pstateInput,
    pstateLinePrefix,
    pstateOffset,
    pstateSourcePos,
    pstateTabWidth
  ),
  SourcePos (SourcePos, sourceColumn, sourceLine, sourceName),
  State (
    State,
    stateInput,
    stateOffset,
    stateParseErrors,
    statePosState
  ),
  defaultTabWidth,
  errorBundlePretty,
  mkPos,
  pos1,
  runParser',
  sepBy,
  (<?>),
 )
import Text.Megaparsec.Char (digitChar, letterChar, printChar, space1, string)
import Text.Megaparsec.Char.Lexer qualified as L

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

-- * Parsers

-- | Parses a positive integer as a line number.
pLine :: (Parser m) => m Int
pLine :: forall (m :: * -> *). Parser m => m Int
pLine = m Int -> m Int
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Int
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal m Int -> String -> m Int
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"line number"

{- | Parses a t'Reference': either a v'ProofReference' (a line range @m-n@)
or a v'LineReference' (a single line number @n@).
-}
pReference :: (Parser m) => m Reference
pReference :: forall (m :: * -> *). Parser m => m Reference
pReference = m Reference
proofReference m Reference -> m Reference -> m Reference
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Reference
lineReference
 where
  proofReference :: m Reference
proofReference =
    (Int -> Int -> Reference) -> m Int -> m Int -> m Reference
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Int -> Int -> Reference
ProofReference (m Int -> m Int
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (m Int -> m Int) -> m Int -> m Int
forall a b. (a -> b) -> a -> b
$ m Int
forall (m :: * -> *). Parser m => m Int
pLine m Int -> m Text -> m Int
forall a b. m a -> m b -> m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Text
forall (m :: * -> *). Parser m => m Text
minus) m Int
forall (m :: * -> *). Parser m => m Int
pLine
      m Reference -> String -> m Reference
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"line range"
  lineReference :: m Reference
lineReference = Int -> Reference
LineReference (Int -> Reference) -> m Int -> m Reference
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Int
forall (m :: * -> *). Parser m => m Int
pLine m Reference -> String -> m Reference
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"line number"

{- | Parses a t'RuleApplication': a rule name enclosed in parentheses,
followed by a comma-separated list of t'Reference's.
-}
pRule :: (Parser m) => m RuleApplication
pRule :: forall (m :: * -> *). Parser m => m RuleApplication
pRule =
  (Text -> [Reference] -> RuleApplication)
-> m Text -> m [Reference] -> m RuleApplication
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2
    Text -> [Reference] -> RuleApplication
RuleApplication
    (m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
parens (m Text -> m Text
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try m Text
forall (m :: * -> *). Parser m => m Text
pSymbolicName m Text -> m Text -> m Text
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> m Text
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
""))
    (m Reference -> m Reference
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Reference
forall (m :: * -> *). Parser m => m Reference
pReference m Reference -> m Text -> m [Reference]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` m Text
forall (m :: * -> *). Parser m => m Text
comma)

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

-- * Entry point

{- | Parses a t'RuleApplication' from a t'Text'.
Returns 'Left' with a human-readable error message on failure,
or 'Right' with the parsed t'RuleApplication' on success.
-}
parseRuleApplication ::
  -- | Line number, used to anchor error positions.
  Int ->
  -- | Input t'Text' to parse.
  Text ->
  Either Text RuleApplication
parseRuleApplication :: Int -> Text -> Either Text RuleApplication
parseRuleApplication Int
lineNo Text
input = case Parsec Void Text RuleApplication
-> State Text Void
-> (State Text Void,
    Either (ParseErrorBundle Text Void) RuleApplication)
forall e s a.
Parsec e s a
-> State s e -> (State s e, Either (ParseErrorBundle s e) a)
runParser' (Parsec Void Text RuleApplication
forall (m :: * -> *). Parser m => m RuleApplication
pRule Parsec Void Text RuleApplication
-> ParsecT Void Text Identity ()
-> Parsec Void Text RuleApplication
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) State Text Void
initialParserState of
  (State Text Void
_, Left ParseErrorBundle Text Void
e) -> Text -> Either Text RuleApplication
forall a b. a -> Either a b
Left (Text -> Either Text RuleApplication)
-> (String -> Text) -> String -> Either Text RuleApplication
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. ToText a => a -> Text
toText (String -> Either Text RuleApplication)
-> String -> Either Text RuleApplication
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle Text Void
e
  (State Text Void
_, Right RuleApplication
ra) -> RuleApplication -> Either Text RuleApplication
forall a b. b -> Either a b
Right RuleApplication
ra
 where
  initialParserState :: State Text Void
initialParserState =
    State
      { stateInput :: Text
stateInput = Text
input
      , stateOffset :: Int
stateOffset = Int
0
      , statePosState :: PosState Text
statePosState =
          PosState
            { pstateInput :: Text
pstateInput = Text
input
            , pstateOffset :: Int
pstateOffset = Int
0
            , pstateSourcePos :: SourcePos
pstateSourcePos =
                SourcePos{sourceName :: String
sourceName = String
"", sourceLine :: Pos
sourceLine = Int -> Pos
mkPos Int
lineNo, sourceColumn :: Pos
sourceColumn = Pos
pos1}
            , pstateTabWidth :: Pos
pstateTabWidth = Pos
defaultTabWidth
            , pstateLinePrefix :: String
pstateLinePrefix = String
""
            }
      , stateParseErrors :: [ParseError Text Void]
stateParseErrors = []
      }