Migrate to `Felix` namespaceHEADhotg

1 files changed, 221 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Concrete.hs b/source/Felix/Test/Unit/Concrete.hs
new file mode 100644
index 0000000..7eac7df
--- /dev/null
+++ b/source/Felix/Test/Unit/Concrete.hs
@@ -0,0 +1,221 @@
+{-# 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}"
+            ]