{- |
Module      : Parser.Formula
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'RawFormula's, t'Term's and t'RawAssumption's.
-}
module Parser.Formula where

import Control.Monad.Combinators.Expr (makeExprParser)
import Fitch.Proof
import Parser.Util
import Text.Megaparsec (
  MonadParsec (..),
  PosState (..),
  SourcePos (..),
  State (..),
  chunk,
  defaultTabWidth,
  errorBundlePretty,
  mkPos,
  pos1,
  runParserT',
  sepBy,
  (<?>),
 )

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

-- * Parser state

-- | State for a t'Formula' parser.
data FormulaParserState = FormulaParserState
  { FormulaParserState -> [(Text, Text, Int)]
operators :: [(Text, Text, Int)]
  -- ^ List of operators as (alias, operator, arity).
  , FormulaParserState -> [(Text, Text)]
infixPreds :: [(Text, Text)]
  -- ^ List of infix predicates as (alias, predicate).
  , FormulaParserState -> [(Text, Text)]
quantifiers :: [(Text, Text)]
  -- ^ List of quantifiers as (alias, quantifier).
  }

{- | Constraint alias combining a t'Parser' with a 'MonadState'
over t'FormulaParserState'.
-}
type FormulaParser m = (MonadParsec Void Text m, MonadState FormulaParserState m)

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

-- * Term parsers

{- | Parses a function application: a lowercase name followed by a parenthesised,
comma-separated argument list, e.g. @f(x, y)@.

__Note:__ the parser cannot distinguish between function constants and variables.
This does not matter for this application — constants are treated as variables.
-}
pFun :: (FormulaParser m) => m Term
pFun :: forall (m :: * -> *). FormulaParser m => m Term
pFun =
  m Term -> m Term
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme
    ( (Text -> [Term] -> Term) -> m Text -> m [Term] -> m Term
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 -> [Term] -> Term
Fun m Text
forall (m :: * -> *). Parser m => m Text
pLowerName (m [Term] -> m [Term]
forall (m :: * -> *) a. Parser m => m a -> m a
parens (m Term
forall (m :: * -> *). FormulaParser m => m Term
pTerm m Term -> m Text -> m [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` m Text
forall (m :: * -> *). Parser m => m Text
comma))
        m Term -> String -> m Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function symbol"
    )

-- | Parses a variable: a single lowercase name.
pVar :: (FormulaParser m) => m Term
pVar :: forall (m :: * -> *). FormulaParser m => m Term
pVar = m Term -> m Term
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme (Text -> Term
Var (Text -> Term) -> m Text -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Text
forall (m :: * -> *). Parser m => m Text
pLowerName m Term -> String -> m Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"variable")

-- | Parses a t'Term': tries 'pFun' first, then falls back to 'pVar'.
pTerm :: (FormulaParser m) => m Term
pTerm :: forall (m :: * -> *). FormulaParser m => m Term
pTerm = m Term -> m Term
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try m Term
forall (m :: * -> *). FormulaParser m => m Term
pFun m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Term
forall (m :: * -> *). FormulaParser m => m Term
pVar m Term -> String -> m Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"term"

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

-- * Formula parsers

{- | Parses a predicate: an uppercase name followed by an optional parenthesised argument list.
Thus also capturing propositional atoms.
-}
pPredicate :: (FormulaParser m) => m RawFormula
pPredicate :: forall (m :: * -> *). FormulaParser m => m RawFormula
pPredicate =
  m RawFormula -> m RawFormula
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme
    ( (Text -> [Term] -> RawFormula)
-> m Text -> m [Term] -> m RawFormula
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 -> [Term] -> RawFormula
Pred m Text
forall (m :: * -> *). Parser m => m Text
pUpperName (m [Term] -> m [Term]
forall (m :: * -> *) a. Parser m => m a -> m a
parens (m Term
forall (m :: * -> *). FormulaParser m => m Term
pTerm m Term -> m Text -> m [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` m Text
forall (m :: * -> *). Parser m => m Text
comma) m [Term] -> m [Term] -> m [Term]
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> m [Term]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
        m RawFormula -> String -> m RawFormula
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"predicate symbol"
    )

{- | Parses a quantifier name from the current t'FormulaParserState',
accepting both the actual symbol and the alias.
-}
pQuantifierName :: (FormulaParser m) => m Name
pQuantifierName :: forall (m :: * -> *). FormulaParser m => m Text
pQuantifierName = do
  symbols <- (FormulaParserState -> [(Text, Text)]) -> m [(Text, Text)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FormulaParserState -> [(Text, Text)]
quantifiers
  foldr (\(Text
alias, Text
s) m Text
p -> Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
s 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
<|> (Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
alias m (Tokens Text) -> m Text -> m Text
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Text -> m Text
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
s) 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
<|> m Text
p) empty symbols

{- | Parses a constant, i.e. a nullary 'Opr' like @⊥@
 from the current t'FormulaParserState'.
-}
pConstant :: (FormulaParser m) => m RawFormula
pConstant :: forall (m :: * -> *). FormulaParser m => m RawFormula
pConstant = do
  ops <- (FormulaParserState -> [(Text, Text, Int)])
-> m [(Text, Text, Int)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FormulaParserState -> [(Text, Text, Int)]
operators
  op <-
    foldr
      (\(Text
alias, Text
o, Int
n) m Text
p -> if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
alias 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
<|> Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
o 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
<|> m Text
p else m Text
p)
      empty
      ops
  lexeme . pure $ Opr op []

-- | Parses a quantified t'RawFormula' of the form @quantifier variable . formula@.
pQuantifier :: (FormulaParser m) => m RawFormula
pQuantifier :: forall (m :: * -> *). FormulaParser m => m RawFormula
pQuantifier =
  m RawFormula -> m RawFormula
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme (m RawFormula -> m RawFormula) -> m RawFormula -> m RawFormula
forall a b. (a -> b) -> a -> b
$
    (Text -> Text -> RawFormula -> RawFormula)
-> m Text -> m Text -> m RawFormula -> m RawFormula
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3
      Text -> Text -> RawFormula -> RawFormula
Quantifier
      (m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Text
forall (m :: * -> *). FormulaParser m => m Text
pQuantifierName)
      (m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme (m Text
forall (m :: * -> *). Parser m => m Text
pLowerName m Text -> String -> m Text
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"variable"))
      (m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme (Text -> m Text
forall (m :: * -> *). Parser m => Text -> m Text
symbol Text
".") m Text -> m RawFormula -> m RawFormula
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m RawFormula -> m RawFormula
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula)

{- | Parses an infix predicate name from the current t'FormulaParserState',
accepting both the actual symbol and the alias.
-}
pInfixPredName :: (FormulaParser m) => m Name
pInfixPredName :: forall (m :: * -> *). FormulaParser m => m Text
pInfixPredName = do
  tops <- (FormulaParserState -> [(Text, Text)]) -> m [(Text, Text)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FormulaParserState -> [(Text, Text)]
infixPreds
  foldr (\(Text
alias, Text
s) m Text
p -> Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
s 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
<|> (Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Text
Tokens Text
alias m (Tokens Text) -> m Text -> m Text
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Text -> m Text
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
s) 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
<|> m Text
p) empty tops

-- | Parses an infix predicate of the form @term predicate term@, e.g. @x = y@.
pInfixPred :: (FormulaParser m) => m RawFormula
pInfixPred :: forall (m :: * -> *). FormulaParser m => m RawFormula
pInfixPred = do
  t1 <- m Term -> m Term
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme m Term
forall (m :: * -> *). FormulaParser m => m Term
pTerm
  op <- lexeme pInfixPredName
  t2 <- lexeme pTerm
  pure $ InfixPred op t1 t2

{- | Parses an atomic t'RawFormula': a quantifier, infix predicate,
parenthesised formula, constant, or predicate.
-}
pFormulaAtomic :: (FormulaParser m) => m RawFormula
pFormulaAtomic :: forall (m :: * -> *). FormulaParser m => m RawFormula
pFormulaAtomic =
  (m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pQuantifier m RawFormula -> m RawFormula -> m RawFormula
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m RawFormula -> m RawFormula
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pInfixPred m RawFormula -> m RawFormula -> m RawFormula
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m RawFormula -> m RawFormula
forall (m :: * -> *) a. Parser m => m a -> m a
parens m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula m RawFormula -> m RawFormula -> m RawFormula
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pConstant m RawFormula -> m RawFormula -> m RawFormula
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pPredicate)
    m RawFormula -> String -> m RawFormula
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"formula"

{- | Parses a full t'RawFormula', using 'makeExprParser'
to handle operator precedence and associativity.
-}
pRawFormula :: (FormulaParser m) => m RawFormula
pRawFormula :: forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula = do
  ops <- (FormulaParserState -> [(Text, Text, Int)])
-> m [(Text, Text, Int)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FormulaParserState -> [(Text, Text, Int)]
operators
  let operatorTable =
        ( ((Text, Text, Int) -> [Operator m RawFormula])
-> [(Text, Text, Int)] -> [[Operator m RawFormula]]
forall a b. (a -> b) -> [a] -> [b]
map
            ( \(Text
alias, Text
u, Int
arity) ->
                if Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
                  then
                    [ Text -> (RawFormula -> RawFormula) -> Operator m RawFormula
forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a) -> Operator m a
prefix Text
alias (\RawFormula
f -> Text -> [RawFormula] -> RawFormula
Opr Text
u [Item [RawFormula]
RawFormula
f])
                    , Text -> (RawFormula -> RawFormula) -> Operator m RawFormula
forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a) -> Operator m a
prefix Text
u (\RawFormula
f -> Text -> [RawFormula] -> RawFormula
Opr Text
u [Item [RawFormula]
RawFormula
f])
                    ]
                  else []
            )
            [(Text, Text, Int)]
ops
            [[Operator m RawFormula]]
-> [[Operator m RawFormula]] -> [[Operator m RawFormula]]
forall a. Semigroup a => a -> a -> a
<> ((Text, Text, Int) -> [Operator m RawFormula])
-> [(Text, Text, Int)] -> [[Operator m RawFormula]]
forall a b. (a -> b) -> [a] -> [b]
map
              ( \(Text
alias, Text
b, Int
arity) ->
                  if Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
                    then
                      [ Text
-> (RawFormula -> RawFormula -> RawFormula)
-> Operator m RawFormula
forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a -> a) -> Operator m a
binary Text
alias (\RawFormula
f1 RawFormula
f2 -> Text -> [RawFormula] -> RawFormula
Opr Text
b [Item [RawFormula]
RawFormula
f1, Item [RawFormula]
RawFormula
f2])
                      , Text
-> (RawFormula -> RawFormula -> RawFormula)
-> Operator m RawFormula
forall (m :: * -> *) a.
Parser m =>
Text -> (a -> a -> a) -> Operator m a
binary Text
b (\RawFormula
f1 RawFormula
f2 -> Text -> [RawFormula] -> RawFormula
Opr Text
b [Item [RawFormula]
RawFormula
f1, Item [RawFormula]
RawFormula
f2])
                      ]
                    else []
              )
              [(Text, Text, Int)]
ops
        )
   in makeExprParser pFormulaAtomic operatorTable <?> "formula"

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

-- * Assumption parsers

{- | Parses a fresh-variable marker: a lowercase name enclosed in square brackets,
e.g. @[x]@.
-}
pFreshVariable :: (FormulaParser m) => m RawAssumption
pFreshVariable :: forall (m :: * -> *). FormulaParser m => m RawAssumption
pFreshVariable = m RawAssumption -> m RawAssumption
forall (m :: * -> *) a. Parser m => m a -> m a
lexeme (m RawAssumption -> m RawAssumption)
-> m RawAssumption -> m RawAssumption
forall a b. (a -> b) -> a -> b
$ Text -> RawAssumption
FreshVar (Text -> RawAssumption) -> m Text -> m RawAssumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Text -> m Text
forall (m :: * -> *) a. Parser m => m a -> m a
brackets m Text
forall (m :: * -> *). Parser m => m Text
pLowerName

-- | Parses a t'RawAssumption': either a fresh-variable marker or a plain t'RawFormula'.
pRawAssumption :: (FormulaParser m) => m RawAssumption
pRawAssumption :: forall (m :: * -> *). FormulaParser m => m RawAssumption
pRawAssumption = (m RawAssumption
forall (m :: * -> *). FormulaParser m => m RawAssumption
pFreshVariable m RawAssumption -> m RawAssumption -> m RawAssumption
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (RawFormula -> RawAssumption
RawAssumption (RawFormula -> RawAssumption) -> m RawFormula -> m RawAssumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula)) m RawAssumption -> String -> m RawAssumption
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"assumption"

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

-- * Entry points

{- | Constructs an initial Megaparsec t'Text.Megaparsec.State' positioned at the
given line number, so that parse errors report the correct source location.
-}
initialParserState ::
  -- | Line number at which parsing begins.
  Int ->
  -- | Input t'Text' to parse.
  Text ->
  Text.Megaparsec.State Text e
initialParserState :: forall e. Int -> Text -> State Text e
initialParserState Int
lineNo Text
input =
  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 e]
stateParseErrors = []
    }

{- | Parses a t'RawFormula' from a t'Text'.
Returns 'Left' with a human-readable error message on failure,
or 'Right' with the parsed t'RawFormula' on success.
-}
parseFormula ::
  -- | Initial parser state.
  FormulaParserState ->
  -- | Line number.
  Int ->
  -- | Input t'Text' to parse.
  Text ->
  Either Text RawFormula
parseFormula :: FormulaParserState -> Int -> Text -> Either Text RawFormula
parseFormula FormulaParserState
initialState Int
lineNo Text
input =
  case State
  FormulaParserState
  (State Text Void, Either (ParseErrorBundle Text Void) RawFormula)
-> FormulaParserState
-> (State Text Void,
    Either (ParseErrorBundle Text Void) RawFormula)
forall s a. State s a -> s -> a
evalState
    (ParsecT Void Text (StateT FormulaParserState Identity) RawFormula
-> State Text Void
-> State
     FormulaParserState
     (State Text Void, Either (ParseErrorBundle Text Void) RawFormula)
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) RawFormula
forall (m :: * -> *). FormulaParser m => m RawFormula
pRawFormula ParsecT Void Text (StateT FormulaParserState Identity) RawFormula
-> ParsecT Void Text (StateT FormulaParserState Identity) ()
-> ParsecT
     Void Text (StateT FormulaParserState Identity) RawFormula
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) (Int -> Text -> State Text Void
forall e. Int -> Text -> State Text e
initialParserState Int
lineNo Text
input))
    FormulaParserState
initialState of
    (State Text Void
_, Left ParseErrorBundle Text Void
e) -> Text -> Either Text RawFormula
forall a b. a -> Either a b
Left (Text -> Either Text RawFormula)
-> (String -> Text) -> String -> Either Text RawFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. ToText a => a -> Text
toText (String -> Either Text RawFormula)
-> String -> Either Text RawFormula
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 RawFormula
f) -> RawFormula -> Either Text RawFormula
forall a b. b -> Either a b
Right RawFormula
f

{- | Parses a t'RawAssumption' from a t'Text'.
Returns 'Left' with a human-readable error message on failure,
or 'Right' with the parsed t'RawAssumption' on success.
-}
parseAssumption ::
  -- | Initial parser state.
  FormulaParserState ->
  -- | Line number.
  Int ->
  -- | Input t'Text' to parse.
  Text ->
  Either Text RawAssumption
parseAssumption :: FormulaParserState -> Int -> Text -> Either Text RawAssumption
parseAssumption FormulaParserState
initialState Int
lineNo Text
input =
  case State
  FormulaParserState
  (State Text Void,
   Either (ParseErrorBundle Text Void) RawAssumption)
-> FormulaParserState
-> (State Text Void,
    Either (ParseErrorBundle Text Void) RawAssumption)
forall s a. State s a -> s -> a
evalState
    (ParsecT
  Void Text (StateT FormulaParserState Identity) RawAssumption
-> State Text Void
-> State
     FormulaParserState
     (State Text Void,
      Either (ParseErrorBundle Text Void) RawAssumption)
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) RawAssumption
forall (m :: * -> *). FormulaParser m => m RawAssumption
pRawAssumption ParsecT
  Void Text (StateT FormulaParserState Identity) RawAssumption
-> ParsecT Void Text (StateT FormulaParserState Identity) ()
-> ParsecT
     Void Text (StateT FormulaParserState Identity) RawAssumption
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) (Int -> Text -> State Text Void
forall e. Int -> Text -> State Text e
initialParserState Int
lineNo Text
input))
    FormulaParserState
initialState of
    (State Text Void
_, Left ParseErrorBundle Text Void
e) -> Text -> Either Text RawAssumption
forall a b. a -> Either a b
Left (Text -> Either Text RawAssumption)
-> (String -> Text) -> String -> Either Text RawAssumption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. ToText a => a -> Text
toText (String -> Either Text RawAssumption)
-> String -> Either Text RawAssumption
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 RawAssumption
a) -> RawAssumption -> Either Text RawAssumption
forall a b. b -> Either a b
Right RawAssumption
a