{- |
Module      : Parser.Proof
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'Derivation's and full t'Proof's.
-}
module Parser.Proof where

import Data.List.NonEmpty (some1)
import Data.Text qualified as T
import Fitch.Proof
import Parser.Formula
import Parser.Rule
import Parser.Util
import Text.Megaparsec (
  ErrorItem (..),
  PosState (..),
  SourcePos (..),
  defaultTabWidth,
  eitherP,
  eof,
  errorBundlePretty,
  manyTill,
  match,
  pos1,
  runParserT',
  try,
  unexpected,
  (<?>),
 )
import Text.Megaparsec qualified as Parsec

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

-- * Line parsers

{- | Parses a t'Formula', capturing the source text and wrapping the result in
'ParsedValid'.
-}
pFormula :: (FormulaParser m) => m Formula
pFormula :: forall (m :: * -> *). FormulaParser m => m Formula
pFormula = m RawFormula -> m (Text, RawFormula)
forall (m :: * -> *) a. Parser m => m a -> m (Text, a)
matchNoSpaces (m RawFormula -> m RawFormula
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula) m (Text, RawFormula)
-> ((Text, RawFormula) -> Formula) -> m Formula
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Text -> RawFormula -> Formula) -> (Text, RawFormula) -> Formula
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid

{- | Parses an t'Assumption', capturing the source text and wrapping the result in
'ParsedValid'.
-}
pAssumption :: (FormulaParser m) => m Assumption
pAssumption :: forall (m :: * -> *). FormulaParser m => m Assumption
pAssumption =
  Wrapper RawAssumption -> Assumption
mkAssumption
    (Wrapper RawAssumption -> Assumption)
-> m (Wrapper RawAssumption) -> m Assumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m RawAssumption -> m (Text, RawAssumption)
forall (m :: * -> *) a. Parser m => m a -> m (Text, a)
matchNoSpaces (m RawAssumption -> m RawAssumption
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m RawAssumption
forall (m :: * -> *). FormulaParser m => m RawAssumption
pRawAssumption) m (Text, RawAssumption)
-> ((Text, RawAssumption) -> Wrapper RawAssumption)
-> m (Wrapper RawAssumption)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Text -> RawAssumption -> Wrapper RawAssumption)
-> (Text, RawAssumption) -> Wrapper RawAssumption
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> a -> Wrapper a
ParsedValid)

-- | Parses a t'Derivation': a t'Formula' followed by a t'RuleApplication'.
pDerivation :: (FormulaParser m) => m Derivation
pDerivation :: forall (m :: * -> *). FormulaParser m => m Derivation
pDerivation =
  (Formula -> Wrapper RuleApplication -> Derivation)
-> m Formula -> m (Wrapper RuleApplication) -> m Derivation
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
    Formula -> Wrapper RuleApplication -> Derivation
Derivation
    m Formula
forall (m :: * -> *). FormulaParser m => m Formula
pFormula
    (m RuleApplication -> m (Text, RuleApplication)
forall (m :: * -> *) a. Parser m => m a -> m (Text, a)
matchNoSpaces (m RuleApplication -> m RuleApplication
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m RuleApplication
forall (m :: * -> *). Parser m => m RuleApplication
pRule) m (Text, RuleApplication)
-> ((Text, RuleApplication) -> Wrapper RuleApplication)
-> m (Wrapper RuleApplication)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Text -> RuleApplication -> Wrapper RuleApplication)
-> (Text, RuleApplication) -> Wrapper RuleApplication
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid)

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

-- * Proof structure parsers

-- | Combinator that gates a parser behind @n@ leading @|@ symbols.
withIndent :: (Parser m) => Int -> m a -> m a
withIndent :: forall (m :: * -> *) a. Parser m => Int -> m a -> m a
withIndent Int
0 m a
p = m a
p
withIndent Int
n m a
p = Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"|" m Text -> m a -> m a
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> m a -> m a
forall (m :: * -> *) a. Parser m => Int -> m a -> m a
withIndent (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) m a
p

{- | Parses the @---@ separator that divides t'Assumption's from t'Derivation's
in a t'Proof', respecting the current indentation depth.
-}
pFormulaSep :: (Parser m) => Int -> m ()
pFormulaSep :: forall (m :: * -> *). Parser m => Int -> m ()
pFormulaSep Int
ind = m Text -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m Text -> m ()) -> (m Text -> m Text) -> m Text -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> m Text -> m Text
forall (m :: * -> *) a. Parser m => Int -> m a -> m a
withIndent Int
ind (m Text -> m ()) -> m Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
"---"

{- | Parses a t'Proof' at the given indentation depth.

The structure is:

1. Zero or more t'Assumption's, collected up to the @---@ separator.
2. One or more t'Derivation's or nested v'SubProof's.
3. The final element must be a t'Derivation'.
-}
pProof :: (FormulaParser m) => Int -> m Proof
pProof :: forall (m :: * -> *). FormulaParser m => Int -> m Proof
pProof Int
ind =
  do
    fs <- m Assumption -> m () -> m [Assumption]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
manyTill (Int -> m Assumption -> m Assumption
forall (m :: * -> *) a. Parser m => Int -> m a -> m a
withIndent Int
ind (m Assumption -> m Assumption
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Assumption
forall (m :: * -> *). FormulaParser m => m Assumption
pAssumption)) (m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Int -> m ()
forall (m :: * -> *). Parser m => Int -> m ()
pFormulaSep Int
ind))
    proofs <-
      some1 . try $
        lexeme
          ( eitherP
              (try $ withIndent ind pDerivation)
              (pProof (ind + 1))
          )

    case last proofs of
      Left Derivation
d -> Proof -> m Proof
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> m Proof) -> Proof -> m Proof
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs (NonEmpty (Either Derivation Proof) -> [Either Derivation Proof]
forall (f :: * -> *) a. IsNonEmpty f a [a] "init" => f a -> [a]
init NonEmpty (Either Derivation Proof)
proofs) Derivation
d
      Right Proof
p -> ErrorItem (Token Text) -> m Proof
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
unexpected (NonEmpty Char -> ErrorItem (Token Text)
forall t. NonEmpty Char -> ErrorItem t
Label (NonEmpty Char -> ErrorItem (Token Text))
-> NonEmpty Char -> ErrorItem (Token Text)
forall a b. (a -> b) -> a -> b
$ [Item (NonEmpty Char)] -> NonEmpty Char
forall l. IsList l => [Item l] -> l
fromList String
[Item (NonEmpty Char)]
"subproof")
    m Proof -> String -> m Proof
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"subproof"

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

-- * Entry points

{- | Parses a single t'Derivation' line from a t'Text'.
Returns 'Left' with a human-readable error message on failure,
or 'Right' with the parsed t'Derivation' on success.
-}
parseLine ::
  -- | List of operators as (alias, operator, arity).
  [(Text, Text, Int)] ->
  -- | List of infix predicates as (alias, predicate).
  [(Text, Text)] ->
  -- | List of quantifiers as (alias, quantifier).
  [(Text, Text)] ->
  -- | Input t'Text' to parse.
  Text ->
  Either Text Derivation
parseLine :: [(Text, Text, Int)]
-> [(Text, Text)]
-> [(Text, Text)]
-> Text
-> Either Text Derivation
parseLine [(Text, Text, Int)]
operators [(Text, Text)]
infixPreds [(Text, Text)]
quantifiers Text
input = case State
  FormulaParserState
  (State Text Void, Either (ParseErrorBundle Text Void) Derivation)
-> FormulaParserState
-> (State Text Void,
    Either (ParseErrorBundle Text Void) Derivation)
forall s a. State s a -> s -> a
evalState
  (ParsecT Void Text (StateT FormulaParserState Identity) Derivation
-> State Text Void
-> State
     FormulaParserState
     (State Text Void, Either (ParseErrorBundle Text Void) Derivation)
forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> State s e -> m (State s e, Either (ParseErrorBundle s e) a)
runParserT' (ParsecT Void Text (StateT FormulaParserState Identity) Derivation
forall (m :: * -> *). FormulaParser m => m Derivation
pDerivation ParsecT Void Text (StateT FormulaParserState Identity) Derivation
-> ParsecT Void Text (StateT FormulaParserState Identity) ()
-> ParsecT
     Void Text (StateT FormulaParserState Identity) Derivation
forall a b.
ParsecT Void Text (StateT FormulaParserState Identity) a
-> ParsecT Void Text (StateT FormulaParserState Identity) b
-> ParsecT Void Text (StateT FormulaParserState Identity) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text (StateT FormulaParserState Identity) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) State Text Void
initialParserState)
  FormulaParserState
initialState of
  (State Text Void
_, Left ParseErrorBundle Text Void
e) -> Text -> Either Text Derivation
forall a b. a -> Either a b
Left (Text -> Either Text Derivation)
-> (String -> Text) -> String -> Either Text Derivation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. ToText a => a -> Text
toText (String -> Either Text Derivation)
-> String -> Either Text Derivation
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 Derivation
d) -> Derivation -> Either Text Derivation
forall a b. b -> Either a b
Right Derivation
d
 where
  initialParserState :: State Text Void
initialParserState =
    Parsec.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 = Pos
pos1
                  , sourceColumn :: Pos
sourceColumn = Pos
pos1
                  }
            , pstateTabWidth :: Pos
pstateTabWidth = Pos
defaultTabWidth
            , pstateLinePrefix :: String
pstateLinePrefix = String
""
            }
      , stateParseErrors :: [ParseError Text Void]
stateParseErrors = []
      }
  initialState :: FormulaParserState
initialState =
    FormulaParserState
      { [(Text, Text, Int)]
operators :: [(Text, Text, Int)]
operators :: [(Text, Text, Int)]
operators
      , [(Text, Text)]
infixPreds :: [(Text, Text)]
infixPreds :: [(Text, Text)]
infixPreds
      , [(Text, Text)]
quantifiers :: [(Text, Text)]
quantifiers :: [(Text, Text)]
quantifiers
      }

{- | Parses a full t'Proof' from a t'Text'.
Returns 'Left' with a human-readable error message on failure,
or 'Right' with the parsed t'Proof' on success.
-}
parseProof ::
  -- | List of operators as (alias, operator, arity).
  [(Text, Text, Int)] ->
  -- | List of infix predicates as (alias, predicate).
  [(Text, Text)] ->
  -- | List of quantifiers as (alias, quantifier).
  [(Text, Text)] ->
  -- | Input t'Text' to parse.
  Text ->
  Either Text Proof
parseProof :: [(Text, Text, Int)]
-> [(Text, Text)] -> [(Text, Text)] -> Text -> Either Text Proof
parseProof [(Text, Text, Int)]
operators [(Text, Text)]
infixPreds [(Text, Text)]
quantifiers Text
input =
  case State
  FormulaParserState
  (State Text Void, Either (ParseErrorBundle Text Void) Proof)
-> FormulaParserState
-> (State Text Void, Either (ParseErrorBundle Text Void) Proof)
forall s a. State s a -> s -> a
evalState
    (ParsecT Void Text (StateT FormulaParserState Identity) Proof
-> State Text Void
-> State
     FormulaParserState
     (State Text Void, Either (ParseErrorBundle Text Void) Proof)
forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> State s e -> m (State s e, Either (ParseErrorBundle s e) a)
runParserT' (Int -> ParsecT Void Text (StateT FormulaParserState Identity) Proof
forall (m :: * -> *). FormulaParser m => Int -> m Proof
pProof Int
1 ParsecT Void Text (StateT FormulaParserState Identity) Proof
-> ParsecT Void Text (StateT FormulaParserState Identity) ()
-> ParsecT Void Text (StateT FormulaParserState Identity) Proof
forall a b.
ParsecT Void Text (StateT FormulaParserState Identity) a
-> ParsecT Void Text (StateT FormulaParserState Identity) b
-> ParsecT Void Text (StateT FormulaParserState Identity) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text (StateT FormulaParserState Identity) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) State Text Void
initialParserState)
    FormulaParserState
initialState of
    (State Text Void
_, Left ParseErrorBundle Text Void
e) -> Text -> Either Text Proof
forall a b. a -> Either a b
Left (Text -> Either Text Proof)
-> (String -> Text) -> String -> Either Text Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. ToText a => a -> Text
toText (String -> Either Text Proof) -> String -> Either Text Proof
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 Proof
p) -> Proof -> Either Text Proof
forall a b. b -> Either a b
Right Proof
p
 where
  initialParserState :: State Text Void
initialParserState =
    Parsec.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 = Pos
pos1
                  , sourceColumn :: Pos
sourceColumn = Pos
pos1
                  }
            , pstateTabWidth :: Pos
pstateTabWidth = Pos
defaultTabWidth
            , pstateLinePrefix :: String
pstateLinePrefix = String
""
            }
      , stateParseErrors :: [ParseError Text Void]
stateParseErrors = []
      }
  initialState :: FormulaParserState
initialState =
    FormulaParserState
      { [(Text, Text, Int)]
operators :: [(Text, Text, Int)]
operators :: [(Text, Text, Int)]
operators
      , [(Text, Text)]
infixPreds :: [(Text, Text)]
infixPreds :: [(Text, Text)]
infixPreds
      , [(Text, Text)]
quantifiers :: [(Text, Text)]
quantifiers :: [(Text, Text)]
quantifiers
      }