diff options
Diffstat (limited to 'source/Test/Unit/Concrete.hs')
| -rw-r--r-- | source/Test/Unit/Concrete.hs | 221 |
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}" - ] |