{- |
Module      : Parser.IncompleteProof
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 a compact serialization format for t'Proof's using
ASCII control characters, and a corresponding parser for deserialization.
This format is used for encoding t'Proof's in URLs via
t'App.URLDecoder'.

In contrast to "Parser.Proof" this can also parse incomplete t'Proof's,
i.e. ones with parse errors.
-}
module Parser.IncompleteProof where

import Data.Text qualified as T
import Fitch.Proof
import Parser.Util
import Text.Megaparsec (chunk, eof, manyTill, runParser, try)
import Text.Megaparsec.Char

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

-- * Serialization

{- | Serializes a t'Proof' to a compact t'Text' representation using
ASCII control characters as delimiters, suitable for later re-parsing
with 'parseIncompleteProof'.

Legend of control characters:

* @\\31@ separates a t'Formula' from its t'RuleApplication'
* @\\30@ separates individual lines from each other
* @\\29@ encloses groups: the t'Assumption' list, the t'Derivation' or t'Proof' list,
and the conclusion
* @\\28@ encloses an entire t'Proof'
-}
safeParsePrint :: Proof -> Text
safeParsePrint :: Proof -> Text
safeParsePrint (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  Text
"\28\29"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fsShow
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\29"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
psShow
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\29"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cShow
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\29\28"
 where
  fsShow :: Text
fsShow = [Text] -> Text
T.concat ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Assumption -> Text) -> [Assumption] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Assumption -> Text
assumptionShow [Assumption]
fs
  psShow :: Text
psShow = [Text] -> Text
T.concat ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Either Derivation Proof -> Text)
-> [Either Derivation Proof] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map ((Derivation -> Text)
-> (Proof -> Text) -> Either Derivation Proof -> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Derivation -> Text
derivationShow Proof -> Text
safeParsePrint) [Either Derivation Proof]
ps
  cShow :: Text
cShow = Derivation -> Text
derivationShow Derivation
c
  assumptionShow :: Assumption -> Text
  assumptionShow :: Assumption -> Text
assumptionShow (Wrapper RawAssumption
a, Wrapper RuleApplication
r) = Wrapper RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Wrapper RawAssumption
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\31" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Wrapper RuleApplication -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Wrapper RuleApplication
r Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\30"
  derivationShow :: Derivation -> Text
  derivationShow :: Derivation -> Text
derivationShow (Derivation Formula
f Wrapper RuleApplication
r) = Formula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Formula
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\31" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Wrapper RuleApplication -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Wrapper RuleApplication
r Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\30"

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

-- * Parsers

{- | Parses a single t'Derivation' from the serialization format produced by
'safeParsePrint'.
The t'Formula' and t'RuleApplication' fields are left as v'Unparsed'
wrappers and are re-parsed later by the application.
-}
pIncompleteDerivation :: (Parser m) => m Derivation
pIncompleteDerivation :: forall (m :: * -> *). Parser m => m Derivation
pIncompleteDerivation = do
  f <- m Text
forall (m :: * -> *). Parser m => m Text
pText
  chunk "\31"
  r <- pText
  chunk "\30"
  pure $ Derivation (Unparsed f "") (Unparsed r "")

{- | Parses a single t'Assumption' from the serialization format produced by
'safeParsePrint'.
Both the t'Formula' and t'RuleApplication' fields are left as v'Unparsed' wrappers
and are re-parsed later by the application.
-}
pIncompleteAssumption :: (Parser m) => m Assumption
pIncompleteAssumption :: forall (m :: * -> *). Parser m => m Assumption
pIncompleteAssumption = do
  f <- m Text
forall (m :: * -> *). Parser m => m Text
pText
  chunk "\31"
  r <- pText
  chunk "\30"
  pure (Unparsed f "", Unparsed r "")

-- | Parses a full t'Proof' from the serialization format produced by 'safeParsePrint'.
pIncompleteProof :: (Parser m) => m Proof
pIncompleteProof :: forall (m :: * -> *). Parser m => m Proof
pIncompleteProof = do
  Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Tokens Text
"\28\29"
  fs <- m Assumption -> m (Tokens Text) -> m [Assumption]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
manyTill m Assumption
forall (m :: * -> *). Parser m => m Assumption
pIncompleteAssumption (Tokens Text -> m (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
chunk Tokens Text
"\29")
  ps <-
    manyTill
      (try (Right <$> pIncompleteProof) <|> (Left <$> pIncompleteDerivation))
      (chunk "\29")
  c <- pIncompleteDerivation
  chunk "\29\28"
  pure $ SubProof fs ps c

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

-- * Entry point

{- | Deserializes a t'Proof' from a t'Text' produced by 'safeParsePrint'.
Returns 'Nothing' if parsing fails.
-}
parseIncompleteProof :: Text -> Maybe Proof
parseIncompleteProof :: Text -> Maybe Proof
parseIncompleteProof = Either (ParseErrorBundle Text Void) Proof -> Maybe Proof
forall l r. Either l r -> Maybe r
rightToMaybe (Either (ParseErrorBundle Text Void) Proof -> Maybe Proof)
-> (Text -> Either (ParseErrorBundle Text Void) Proof)
-> Text
-> Maybe Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parsec Void Text Proof
-> String -> Text -> Either (ParseErrorBundle Text Void) Proof
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
runParser (Parsec Void Text Proof
forall (m :: * -> *). Parser m => m Proof
pIncompleteProof Parsec Void Text Proof
-> ParsecT Void Text Identity () -> Parsec Void Text Proof
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) String
""