Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 221 deletions

diff --git a/source/Test/Unit/Concrete.hs b/source/Test/Unit/Concrete.hs
deleted file mode 100644
index 7776552..0000000
--- a/source/Test/Unit/Concrete.hs
+++ /dev/null
@@ -1,221 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Test.Unit.Concrete (unitTests) where
-
-import Base
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Concrete (grammar)
-import Syntax.Lexicon (builtins)
-import 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}"
-            ]