{-# LANGUAGE OverloadedStrings #-}

module Felix.Test.Unit.Concrete (unitTests) where

import Base
import Felix.Report.Location
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Concrete (grammar)
import Felix.Syntax.Lexicon (builtins)
import Felix.Syntax.Token (runLexer)

import Data.Text qualified as Text
import Test.Tasty
import Test.Tasty.HUnit
import Text.Earley (fullParses, parser)
import Text.Megaparsec (errorBundlePretty)

unitTests :: TestTree
unitTests =
    testGroup "Parser"
        [ testCase
            "textual connectives follow symbolic precedence"
            textualConnectivePrecedence
        , testCase
            "transfinite induction precedes its continuation"
            transfiniteInductionContinuation
        ]

data StatementShape
    = Truth
    | Falsity
    | Connected Raw.Connective StatementShape StatementShape
    | Scoped StatementShape
    deriving (Show, Eq)

textualConnectivePrecedence :: Assertion
textualConnectivePrecedence = do
    for_ cases \(label, statement, expected) ->
        assertEqual label (Right expected) (statementShape =<< parseStatement statement)

    assertBool
        "chained iff is rejected"
        (case parseStatement "$\\top$ iff $\\bot$ iff $\\top$" of
            Left _ -> True
            Right _ -> False)

    assertEqual
        "textual and symbolic connective trees agree"
        (statementShape
            =<< parseStatement
                "$\\top \\land \\bot \\lor \\top$")
        (statementShape
            =<< parseStatement
                "$\\top$ and $\\bot$ or $\\top$")
  where
    cases =
        [ ( "and binds tighter than following or"
          , "$\\top$ and $\\bot$ or $\\top$"
          , Connected Raw.Disjunction
                (Connected Raw.Conjunction Truth Falsity)
                Truth
          )
        , ( "and binds tighter than preceding or"
          , "$\\top$ or $\\bot$ and $\\top$"
          , Connected Raw.Disjunction
                Truth
                (Connected Raw.Conjunction Falsity Truth)
          )
        , ( "and associates left"
          , "$\\top$ and $\\bot$ and $\\top$"
          , Connected Raw.Conjunction
                (Connected Raw.Conjunction Truth Falsity)
                Truth
          )
        , ( "or associates left"
          , "$\\top$ or $\\bot$ or $\\top$"
          , Connected Raw.Disjunction
                (Connected Raw.Disjunction Truth Falsity)
                Truth
          )
        , ( "either is accepted after ordinary or"
          , "$\\top$ or either $\\bot$ or $\\top$"
          , Connected Raw.Disjunction
                Truth
                (Connected Raw.ExclusiveOr Falsity Truth)
          )
        , ( "implication associates right"
          , "if $\\top$ then if $\\bot$ then $\\top$"
          , Connected Raw.Implication
                Truth
                (Connected Raw.Implication Falsity Truth)
          )
        , ( "a quantified implication antecedent ends at then"
          , "if for all $x$ we have $\\top$ then $\\bot$"
          , Connected Raw.Implication
                (Scoped Truth)
                Falsity
          )
        , ( "parentheses override precedence"
          , "($\\top$ or $\\bot$) and $\\top$"
          , Connected Raw.Conjunction
                (Connected Raw.Disjunction Truth Falsity)
                Truth
          )
        , ( "a quantified right operand scopes over its continuation"
          , "$\\top$ iff there exists $x$ such that $\\bot$ and $\\top$"
          , Connected Raw.Equivalence
                Truth
                (Scoped
                    (Connected Raw.Conjunction Falsity Truth))
          )
        ]

parseStatement :: Text -> Either String Raw.Stmt
parseStatement statement = do
    chunks <- case runLexer
        (FileId 46)
        "textual-connectives.tex"
        (Text.unlines
            [ "\\begin{axiom}\\label{textual_connectives}"
            , statement <> "."
            , "\\end{axiom}"
            ]) of
        Left err ->
            Left (errorBundlePretty err)
        Right (_imports, chunks') ->
            Right chunks'
    tokens <- case chunks of
        [tokens'] ->
            Right tokens'
        _ ->
            Left ("expected one source chunk, got " <> show (length chunks))
    case fullParses (parser (grammar builtins)) tokens of
        ( [Raw.BlockAxiom
                _location
                _title
                _marker
                (Raw.Axiom [] statement')]
            , _report
            ) ->
                Right statement'
        (blocks, report) ->
            Left
                ( "expected one axiom, got "
                    <> show blocks
                    <> " with "
                    <> show report
                )

statementShape :: Raw.Stmt -> Either String StatementShape
statementShape = \case
    Raw.StmtConnected conn _ left right ->
        Connected conn
            <$> statementShape left
            <*> statementShape right
    Raw.StmtFormula formula ->
        formulaShape formula
    Raw.SymbolicQuantified _ _ _ _ _ statement ->
        Scoped <$> statementShape statement
    statement ->
        Left ("unsupported statement in precedence test: " <> show statement)

formulaShape :: Raw.Formula -> Either String StatementShape
formulaShape = \case
    Raw.PropositionalConstant _ Raw.IsTop ->
        Right Truth
    Raw.PropositionalConstant _ Raw.IsBottom ->
        Right Falsity
    Raw.Connected _ conn left right ->
        Connected conn
            <$> formulaShape left
            <*> formulaShape right
    formula ->
        Left ("unsupported formula in precedence test: " <> show formula)

transfiniteInductionContinuation :: Assertion
transfiniteInductionContinuation =
    case runLexer
        (FileId 45)
        "transfinite-induction.tex"
        sourceText of
        Left err ->
            assertFailure (errorBundlePretty err)
        Right (_imports, [tokens]) ->
            case fullParses (parser (grammar builtins)) tokens of
                ( [ Raw.BlockProof
                        _start
                        (Raw.ByOrdInduction methodLocation
                            (Raw.Qed
                                (Just continuationLocation)
                                Raw.JustificationEmpty))
                        _end
                  ]
                    , _report
                    ) -> do
                        assertEqual
                            "method header line"
                            2
                            (locLine methodLocation)
                        assertEqual
                            "continuation line"
                            3
                            (locLine continuationLocation)
                (blocks, report) ->
                    assertFailure
                        ( "expected one transfinite-induction proof, got "
                            <> show blocks
                            <> " with "
                            <> show report
                        )
        Right (_imports, chunks) ->
            assertFailure
                ("expected one proof chunk, got " <> show (length chunks))
  where
    sourceText =
        Text.unlines
            [ "\\begin{proof}"
            , "[proof by transfinite induction]"
            , "Trivial."
            , "\\end{proof}"
            ]