diff options
Diffstat (limited to 'source/Test/Unit/Checking.hs')
| -rw-r--r-- | source/Test/Unit/Checking.hs | 1982 |
1 files changed, 0 insertions, 1982 deletions
diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs deleted file mode 100644 index 13499a3..0000000 --- a/source/Test/Unit/Checking.hs +++ /dev/null @@ -1,1982 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Test.Unit.Checking (unitTests) where - -import Base -import Checking -import Checking.Dependencies qualified as Dependencies -import Checking.Facts qualified as Facts -import Checking.Legacy -import Checking.Obligation -import Checking.Structure qualified as Structure -import Encoding (contractionTask, encodeTaskText) -import Report.Location -import Syntax.Internal -import Syntax.Lexicon (_Onesorted, pattern ApplySymbol) - -import Bound.Scope (bindings, fromScope, toScope) -import Bound.Var (Var(..)) -import Control.Exception (try) -import Control.Monad.State (runStateT) -import Data.HashSet qualified as HS -import Data.IORef (modifyIORef', newIORef, readIORef) -import Data.Set qualified as Set -import Data.Text qualified as Text -import Test.Tasty -import Test.Tasty.HUnit - -unitTests :: TestTree -unitTests = testGroup "Checking" - [ testCase "renders checking context without constructors" do - let rendered = - renderCheckingError - (DuplicateMarker Nowhere (Marker "labelled")) - assertEqual - "checking diagnostic" - "<nowhere> -1:-1 in labelled: marker is already registered" - rendered - assertBool - "internal Marker constructor is absent" - (not ("Marker" `Text.isInfixOf` rendered)) - , testCase "TPTP encoding excludes task provenance" do - registration <- - registerFilePathWithDisplay - "/tmp/f24-source.tex" - "quote\"\nfof(injected,axiom,$false).\nλ.tex" - fileId <- either - (assertFailure . ("location registration failed: " <>) . show) - pure - registration - let expected = "fof(zf_q0,conjecture,$true)." - plainTask = Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "provenance_test" - , taskLocation = Nowhere - , taskConjecture = PropositionalConstant IsTop - } - adversarialTask = plainTask - { taskDirectness = - Indirect (PropositionalConstant IsBottom) - , taskLocation = mkLocation fileId 12 34 - } - assertEqual "three-argument TPTP" expected (encodeTaskText plainTask) - assertEqual - "path, span, and directness do not affect proof bytes" - (encodeTaskText plainTask) - (encodeTaskText adversarialTask) - , testCase "prepares complete ordered obligation batches" - preparesCompleteObligationBatches - , testCase "replacement conditions remain existentially scoped" do - let x = NamedVar "x" - y = NamedVar "y" - replacement = - makeReplacementIff - (TermVar (F (NamedVar "image"))) - ((x, TermVar (NamedVar "X")) - :| [(y, TermVar (NamedVar "Y"))]) - (abstractVarSymbols [x, y] (TermVar x)) - (abstractVarSymbols - [x, y] - (Equals Nowhere (TermVar x) (TermVar y))) - case replacement of - Quantified Universally outerScope -> do - assertEqual - "outer binders" - [NamedVar "frv"] - (nubOrd (bindings outerScope)) - case fromScope outerScope of - Connected - Equivalence - _ - (Quantified Existentially innerScope) -> - case fromScope innerScope of - And _ (And _ (Equals _ left right)) -> do - assertEqual - "condition left operand" - (TermVar (B x)) - left - assertEqual - "condition right operand" - (TermVar (B y)) - right - body -> - assertFailure - ( "expected replacement condition equality, got " - <> show body - ) - body -> - assertFailure - ("expected replacement equivalence, got " - <> show body) - formula -> - assertFailure - ("expected replacement universal, got " <> show formula) - , testCase "fix rejects shadowing theorem-local variables" do - expectCheckingError "already in scope" (lemmaBlocks "bad_fix" badFixLemma badFixProof) - , testCase "define rejects shadowing local variables" do - expectCheckingError "already in scope" (lemmaBlocks "bad_define" badDefineLemma badDefineProof) - , testCase "take rejects shadowing theorem-local variables" do - expectCheckingError "already in scope" (lemmaBlocks "bad_take" badTakeLemma badTakeProof) - , testCase "have rejects new free variables" do - expectCheckingError "not in scope" (lemmaBlocks "bad_have" badHaveLemma badHaveProof) - , testCase "define function rejects shadowing function name" do - expectCheckingError "already in scope" (lemmaBlocks "bad_define_function_name" badDefineFunctionNameLemma badDefineFunctionNameProof) - , testCase "define function rejects shadowing argument name" do - expectCheckingError "shadow local variable" (lemmaBlocks "bad_define_function_arg" badDefineFunctionArgLemma badDefineFunctionArgProof) - , testCase "free theorem goal variables are local in proofs" do - expectChecks (lemmaBlocks "free_goal_local" freeGoalLocalLemma freeGoalLocalProof) - , testCase "fix accepts fresh local variables" do - expectChecks (lemmaBlocks "fresh_fix" freshFixLemma freshFixProof) - , testCase "take accepts fresh witnesses" do - expectChecks (lemmaBlocks "fresh_take" freshTakeLemma freshTakeProof) - , testCase "assume rejects disjunctive goals" do - expectMismatchedAssume unsoundDisjunctionAssumeBlocks - , assumptionGoalReductionTests - , proofShapeErrorTests - , testCase "struct axioms recursively rewrite carrier labels" do - text <- encodedTasksText structCarrierRewriteBlocks - assertContains "rewritten struct-rule carrier" "zf_u0(zf_f1,zf_s0(zf_f0))" text - assertNotContains "raw struct-rule carrier" "zf_u0(zf_f1,zf_f0)" text - , testCase "struct axioms annotate operations from the same structure" do - text <- encodedTasksText structOperationRewriteBlocks - assertContains "annotated struct operation in rule" "zf_u0(zf_s1(zf_f0),zf_s0(zf_f0))" text - , testCase "structure terms fail before task encoding" do - unresolved <- - try - (check - WithoutDumpPremselTraining - unresolvedStructOperationBlocks) - :: IO (Either CheckingError [Task]) - case unresolved of - Left - (UnresolvedStructureOperation - actualSymbol - actualLocation - actualMarker) -> do - assertEqual - "structure operation" - fooOp - actualSymbol - assertEqual - "block location" - structureTermErrorLocation - actualLocation - assertEqual - "block marker" - "unresolved_structure_operation" - actualMarker - Left err -> - assertFailure - ("expected unresolved structure operation, got " - <> show err) - Right _ -> - assertFailure - "expected unresolved structure operation to fail" - expectCheckingError - "Nested comprehensions are not supported" - nestedStructComprehensionBlocks - , testCase "exact structure claims introduce carrier labels for continuations" do - text <- encodedTasksText structClaimIntroducesContextBlocks - assertContains "claim continuation carrier" "conjecture,zf_u0(zf_f1,zf_s0(zf_f0))" text - , testCase "bound variables do not inherit outer carrier labels" do - text <- encodedTasksText boundStructLabelBlocks - assertContains "bound carrier label remains raw" "![V0]:zf_u0(zf_f1,V0)" text - assertNotContains "bound carrier label not rewritten" "![V0]:zf_u0(zf_f1,zf_s0(V0))" text - , structureTransactionTests - , testCase "abbreviations reject direct self-reference" do - expectCheckingError "self-referential" directSelfReferentialAbbrBlocks - , testCase "abbreviations reject indirect self-reference after expansion" do - expectCheckingError "self-referential" indirectSelfReferentialAbbrBlocks - , testCase "predicate definitions reject direct self-reference" do - expectCheckingError "self-referential" directSelfReferentialPredicateDefinitionBlocks - , testCase "function definitions reject direct self-reference" do - expectCheckingError "self-referential" directSelfReferentialFunctionDefinitionBlocks - , testCase "operator definitions reject direct self-reference" do - expectCheckingError "self-referential" directSelfReferentialOperatorDefinitionBlocks - , testCase "definitions reject abbreviation-hidden self-reference" do - expectCheckingError "self-referential" abbreviationHiddenSelfReferentialDefinitionBlocks - , testCase "definitions reject abbreviation-hidden self-reference in assumptions" do - expectCheckingError "self-referential" assumptionHiddenSelfReferentialDefinitionBlocks - , testCase "ordinary definitions accept non-recursive bodies" do - expectChecks nonRecursiveDefinitionBlocks - , testCase "definitions reject builtin mixfix marker collisions" do - expectCheckingError "object-symbol marker pow is already owned by builtin" [builtinMixfixMarkerCollisionBlock] - , testCase "definitions reject builtin predicate marker collisions" do - expectCheckingError "object-symbol marker elem is already owned by builtin" [builtinPredicateMarkerCollisionBlock] - , testCase "abbreviations reject builtin marker collisions" do - expectCheckingError "object-symbol marker pow is already owned by builtin" [builtinAbbreviationMarkerCollisionBlock] - , testCase "builtin object markers do not reserve proof labels" do - expectChecks [builtinMarkerProofLabelBlock] - , testCase "subseteq remains user-definable" do - expectChecks [subseteqDefinitionBlock] - , testCase "datatype accepts bootstrap propositional fragment" do - expectChecks [goodDatatypeBlock] - , testCase "datatype treats a carrier alias as direct recursion" do - directFacts <- - datatypePreparedFacts [goodDatatypeBlock] - aliasedFacts <- - datatypePreparedFacts directRecursionAliasDatatypeBlocks - assertEqual - "generated datatype facts" - directFacts - aliasedFacts - , testCase "datatype rejects powerset recursion through aliases" do - for_ - [ oneHopPowersetAliasDatatypeBlocks - , multiHopPowersetAliasDatatypeBlocks - ] - (expectCheckingError "recursive premise must be direct") - , testCase "datatype rejects nested recursive premise" do - expectCheckingError "recursive premise must be direct" [badNestedRecursiveDatatypeBlock] - , testCase "datatype rejects missing constructor premise" do - expectCheckingError "missing premise" [badMissingPremiseDatatypeBlock] - , testCase "datatype rejects duplicate constructor patterns" do - expectCheckingError "constructor patterns must be distinct" [badDuplicateConstructorDatatypeBlock] - , testCase "datatype rejects open premise domains" do - expectCheckingError "closed terms" [badOpenDomainDatatypeBlock] - , testCase "datatype rejects application-shaped constructors" do - expectCheckingError "function application" [badApplyConstructorDatatypeBlock] - , testCase "datatype generates trusted fact markers" do - expectFactMarkers datatypeGeneratedMarkers [goodDatatypeBlock] - , testCase "datatype generated fact markers are reserved globally" do - expectDefinedMarkers datatypeGeneratedMarkers [goodDatatypeBlock] - , testCase "datatype generated intro facts are usable by reference" do - expectChecks datatypeIntroReferenceBlocks - , testCase "datatype generated distinctness fact is usable by reference" do - expectChecks datatypeDistinctReferenceBlocks - , testCase "datatype generated injective fact is usable by reference" do - expectChecks datatypeInjectiveReferenceBlocks - , testCase "datatype generated fact markers cannot be reused by later blocks" do - expectDuplicateMarker "propform_cases" datatypeGeneratedMarkerReuseBlocks - , testCase "datatype rejects duplicate constructor markers" do - expectCheckingError "object-symbol marker dup is already owned by datatype constructor" [badDuplicateConstructorMarkerDatatypeBlock] - , testCase "signature predicate declares symbols for later facts" do - expectChecks signaturePredicateUsageBlocks - , testCase "signature formula declares symbolic operators for later facts" do - expectChecks signatureFormulaUsageBlocks - , testCase "signature formula rejects unrecoverable declarations" do - expectCheckingError "could not recover the declared symbol" [badSignatureFormulaBlock] - , testCase "inductive accepts bounded fin fragment" do - expectChecks goodInductiveBlocks - , testCase "inductive generates trusted fact markers" do - expectFactMarkers inductiveGeneratedMarkers goodInductiveBlocks - , testCase "inductive generated fact markers are reserved globally" do - expectDefinedMarkers inductiveGeneratedMarkers goodInductiveBlocks - , testCase "inductive generated intro and domain facts are usable by reference" do - expectChecks inductiveIntroAndDomainReferenceBlocks - , testCase "inductive generated cases fact is usable by reference" do - expectChecks inductiveCasesReferenceBlocks - , testCase "inductive generated induction fact is usable by reference" do - expectChecks inductiveInductReferenceBlocks - , testCase "inductive generates monotonicity obligations for recursive carriers" do - text <- encodedTasksText goodMonotoneInductiveBlocks - assertContains "monotonicity antecedent expands subset" "zf_u1(V2,V0)=>zf_u1(V2,V1)" text - assertContains "monotonicity conclusion expands subset" "zf_u1(V3,zf_u0(V0))=>zf_u1(V3,zf_u0(V1))" text - , testCase "inductive rejects recursive premises outside carrier positions" do - expectCheckingError "carrier of a membership premise" [badRecursiveTermInductiveBlock] - , testCase "inductive rejects malformed recursive premises" do - expectCheckingError "direct membership condition" [badRecursiveFormulaInductiveBlock] - , testCase "inductive rejects malformed results" do - expectCheckingError "form t \\in F(args)" [badInductiveResultBlock] - , testCase "inductive rejects recursive occurrences with the wrong arguments" do - expectCheckingError "wrong arguments" [badInductiveWrongArgsBlock] - , testCase "inductive validates generated markers before emitting obligations" do - tasksRef <- newIORef [] - result <- - try - (runCheckingBlocks - [ BlockAxiom - Nowhere - "fin_cases" - (Axiom [] Top) - , goodInductiveBlock - ] - ( initialCheckingState - WithoutDumpPremselTraining - (\task -> modifyIORef' tasksRef (task :)) - )) - :: IO (Either CheckingError CheckingState) - case result of - Left (DuplicateMarker _ actualMarker) -> - assertEqual - "duplicate marker" - "fin_cases" - actualMarker - Left err -> - assertFailure - ("expected DuplicateMarker, got " <> show err) - Right _ -> - assertFailure - "expected generated marker validation to fail" - tasks <- readIORef tasksRef - assertBool - "failed inductive obligations" - (null tasks) - , testCase "inductive rejects duplicate carrier ownership" do - expectCheckingError "already owned" duplicateInductiveCarrierBlocks - , testCase "inductive rejects operator definitions with the same carrier symbol" do - expectCheckingError "already owned" operatorThenInductiveBlocks - , testCase "inductive rejects prior axiom mentions of the carrier" do - expectCheckingError "without prior ownership" priorInductiveCarrierAxiomBlocks - , testCase "inductive rejects direct recursive domains" do - expectCheckingError "independent of the inductive symbol" [badInductiveSelfDomainBlock] - , testCase "inductive rejects abbreviation-hidden recursive domains" do - expectCheckingError "independent of the inductive symbol" hiddenSelfDomainBlocks - , testCase "inductive rejects prior ordinary-definition mentions of the carrier via domains" do - expectCheckingError "without prior ownership" hiddenDefinitionDomainBlocks - , testCase "inductive rejects prior ordinary-definition mentions of the carrier via side-condition aliases" do - expectCheckingError "without prior ownership" hiddenCarrierSideConditionBlocks - , testCase "datatype rejects prior signature mentions of the datatype head" do - expectCheckingError "already owned" priorDatatypeHeadSignatureBlocks - , testCase "datatype rejects prior theorem mentions of constructors" do - expectCheckingError "without prior ownership" priorDatatypeConstructorLemmaBlocks - , testCase "datatype constructor ownership blocks later operator definitions" do - expectCheckingError "already owned" datatypeConstructorThenOperatorBlocks - , testCase "inductive freezes mentioned symbols against later definitions" do - expectCheckingError "already owned by signature formula" frozenSymbolDefinitionBlocks - , testCase "inductive freezes symbols from canonicalized domains" do - expectCheckingError "already owned by signature formula" canonicalizedDomainFreezeBlocks - , testCase "inductive freezes transitive definition dependencies" do - expectCheckingError "already owned by signature formula" transitiveFrozenDefinitionBlocks - ] - -preparesCompleteObligationBatches :: Assertion -preparesCompleteObligationBatches = do - registry <- - case - Facts.registerStagedFacts - ( Facts.stageFact - ("known_fact" :| []) - (Facts.factOrigin Nowhere "known_block") - (Facts.prepareSemanticFact Top) - :| [] - ) - Facts.emptyFactRegistry of - Left marker -> - assertFailure - ("could not register premise " <> show marker) - Right preparedRegistry -> - pure preparedRegistry - batchesRef <- newIORef [] - let initial = - ( initialCheckingStateWithTaskPreparation - WithoutDumpPremselTraining - contractionTask - (\batch -> - modifyIORef' batchesRef (batch :)) - ) - { checkingFacts = registry - , checkingGoals = [Top `Iff` Top, Bottom] - , blockLabel = "batch_claim" - , stepLocation = Nowhere - } - (_result, afterGoals) <- runStateT tellTasks initial - (_emptyResult, afterEmpty) <- - runStateT - tellTasks - afterGoals{checkingGoals = []} - batches <- reverse <$> readIORef batchesRef - case batches of - [goalBatch, emptyBatch] -> do - assertEqual "batch marker" - "batch_claim" - (preparedBatchMarker goalBatch) - assertEqual "batch location" - Nowhere - (preparedBatchLocation goalBatch) - assertEqual "stable declaration-local ordinals" - [0, 1] - ( legacyObligationOrdinalValue - . preparedObligationOrdinal - <$> toList - (preparedBatchObligations goalBatch) - ) - assertEqual "prepared contracted goals" - [Top, Bottom] - ( taskConjecture - . preparedObligationTask - <$> toList - (preparedBatchObligations goalBatch) - ) - case toList (preparedBatchPremises goalBatch) of - [premise] -> do - assertEqual "premise marker" - "known_fact" - (hypothesisMarker - (preparedPremiseHypothesis premise)) - assertEqual "premise provenance" - (RegisteredFactPremise - (Facts.factOrigin - Nowhere - "known_block")) - (preparedPremiseOrigin premise) - premises -> - assertFailure - ("expected one premise, got " - <> show (length premises)) - assertBool "empty batch callback" - (null (preparedBatchObligations emptyBatch)) - assertEqual "empty batch does not consume an ordinal" - 2 - (legacyObligationOrdinalValue - (checkingNextObligationOrdinal afterEmpty)) - _ -> - assertFailure - ("expected one goal batch and one empty batch, got " - <> show (length batches)) - -structureTransactionTests :: TestTree -structureTransactionTests = - testGroup "structure transactions" - [ testCase "reject positive and negative direct self-reference" do - for_ [fooStructPredicate "A", Not Nowhere (fooStructPredicate "A")] - \assumption -> - expectCheckingError - "self-referential" - [fooStructBlock "self_struct" [("self_rule", assumption)]] - , testCase "reject abbreviation-hidden self-reference" do - expectCheckingError - "self-referential" - hiddenSelfReferentialStructBlocks - , testCase "report unknown and forward parents as located errors" do - expectUnknownStructureParent - unknownStruct - [testStructBlock "unknown_child" childStruct (Set.singleton unknownStruct) []] - expectUnknownStructureParent - fooStruct - [ testStructBlock "forward_child" childStruct (Set.singleton fooStruct) [] - , fooStructBlock "forward_parent" [] - ] - expectUnknownStructureParent - fooStruct - [testStructBlock "self_parent" fooStruct (Set.singleton fooStruct) []] - , testCase "reject every local structure marker collision" do - for_ - [ ( "same_marker" - , fooStructBlock "same_marker" [("same_marker", Top)] - ) - , ( "duplicate_rule" - , fooStructBlock - "duplicate_rules" - [("duplicate_rule", Top), ("duplicate_rule", Top)] - ) - , ( "inherit_collisioninherit" - , fooStructBlock - "inherit_collision" - [("inherit_collisioninherit", Top)] - ) - ] - \(duplicate, block) -> - expectDuplicateMarker duplicate [block] - , testCase "reject collisions before and after a structure" do - expectDuplicateMarker - "prior_rule" - [ BlockAxiom Nowhere "prior_rule" (Axiom [] Top) - , fooStructBlock "prior_collision" [("prior_rule", Top)] - ] - expectDuplicateMarker - "later_collisioninherit" - [ fooStructBlock "later_collision" [] - , BlockAxiom - Nowhere - "later_collisioninherit" - (Axiom [] Top) - ] - , testCase "commit exact prepared facts and backward dependencies" do - case preparedFooStructure "prepared_struct" of - Left err -> - assertFailure - ("could not prepare structure: " <> show err) - Right checked -> do - let context = BlockContext Nowhere "prepared_struct" - initial = - initialCheckingState - WithoutDumpPremselTraining - (\_task -> pure ()) - case commitCheckedStructDefn context checked initial of - Left err -> - assertFailure - ("could not commit structure: " <> show err) - Right committed -> do - assertBool - "fact registry invariant" - (Facts.factRegistryInvariant - (checkingFacts committed)) - for_ - (zip - (toList - (Structure.checkedStructMarkers checked)) - (toList - (Structure.checkedStructSemanticFacts checked))) - \(factMarker, prepared) -> - assertEqual - ("prepared fact " <> show factMarker) - (Just prepared) - (Facts.lookupPreparedFact - factMarker - (checkingFacts committed)) - assertEqual - "structure dependencies" - (Just - (Set.singleton - (SymbolPredicate - (PredicateNounStruct _Onesorted)))) - (Dependencies.lookupDependencies - (Structure.checkedStructSymbol checked) - (checkingDependencies committed)) - ] - -preparedFooStructure - :: Marker - -> Either - Structure.StructurePreparationError - Structure.CheckedStructDefn -preparedFooStructure marker = - Structure.prepareCheckedStructDefn - Nowhere - marker - (fooStructDefn [("prepared_rule", Top)]) - (Set.singleton _Onesorted) - (Set.singleton CarrierSymbol) - -expectUnknownStructureParent - :: StructPhrase - -> [Block] - -> Assertion -expectUnknownStructureParent expected blocks = do - result <- - try (check WithoutDumpPremselTraining blocks) - :: IO (Either CheckingError [Task]) - case result of - Left (UnknownStructureParent actual Nowhere _) -> - assertEqual "unknown structure parent" expected actual - Left err -> - assertFailure - ("expected UnknownStructureParent, got " <> show err) - Right _ -> - assertFailure "expected an unknown structure parent" - -assumptionGoalReductionTests :: TestTree -assumptionGoalReductionTests = - testGroup "assumption goal reductions" - [ testCase "introduces an implication antecedent" do - assertGoalReduction - (ImplicationIntroduction propositionA propositionC) - propositionA - (propositionA `Implies` propositionC) - propositionC - , testCase "curries an assumed left conjunct" do - assertGoalReduction - (CurryLeftConjunct propositionA propositionB propositionC) - propositionA - ((propositionA `And` propositionB) `Implies` propositionC) - (propositionB `Implies` propositionC) - , testCase "curries an assumed right conjunct" do - assertGoalReduction - (CurryRightConjunct propositionA propositionB propositionC) - propositionB - ((propositionA `And` propositionB) `Implies` propositionC) - (propositionA `Implies` propositionC) - , testCase "does not reduce a disjunction" do - assertEqual "disjunction reduction" - Nothing - (reduceGoalWithAssumption - propositionA - (propositionA `Or` propositionB)) - ] - -proofShapeErrorTests :: TestTree -proofShapeErrorTests = - testCase "malformed proof shapes return located errors" do - for_ cases \(label, expectedError, action) -> do - result <- try action :: IO (Either CheckingError ()) - assertEqual label (Left expectedError) result - where - cases = - [ ( "ordinal induction goal" - , ByOrdInductionSyntacticMismatch - proofShapeLocation - "bad_ordinal_induction" - , checkAsUnit - (proofBlocks - "bad_ordinal_induction" - Top - (ByOrdInduction - proofShapeLocation - (Omitted proofShapeLocation))) - ) - , ( "set extensionality with take" - , SetExtensionalityWithTake - proofShapeLocation - "bad_take_setext" - , checkAsUnit - (proofBlocks - "bad_take_setext" - Top - (Take - proofShapeLocation - ("witness" :| []) - Top - JustificationSetExt - (Omitted proofShapeLocation))) - ) - ] - - checkAsUnit = - void . check WithoutDumpPremselTraining - - proofBlocks marker goal proof = - [ BlockLemma - proofShapeLocation - marker - (Lemma [] goal) - , BlockProof - proofShapeLocation - proofShapeLocation - proof - ] - - proofShapeLocation = - mkLocation (FileId 47) 6 11 - -assertGoalReduction - :: GoalReduction - -> Formula - -> Formula - -> Formula - -> Assertion -assertGoalReduction expected assumption original residual = - case reduceGoalWithAssumption assumption original of - Nothing -> - assertFailure "expected a goal reduction" - Just reduction -> do - assertEqual "trusted rule" expected reduction - assertEqual "introduced assumption" - assumption - (goalReductionAssumption reduction) - assertEqual "residual goal" - residual - (goalReductionResidual reduction) - assertReductionSound original reduction - -assertReductionSound :: Formula -> GoalReduction -> Assertion -assertReductionSound original reduction = - for_ propositionAssignments \assignment -> do - let discharged = - goalReductionAssumption reduction - `Implies` goalReductionResidual reduction - soundness = discharged `Implies` original - assertBool - ( "reduction is not sound under " - <> show assignment - <> ": " - <> show reduction - ) - (evaluateProposition assignment soundness) - -type PropositionAssignment = (Bool, Bool, Bool) - -evaluateProposition :: PropositionAssignment -> Formula -> Bool -evaluateProposition assignment@(a, b, c) = \case - Atomic _location (PredicateSymbol name) [] -> - case name of - "A" -> a - "B" -> b - "C" -> c - _ -> error ("missing proposition value for " <> show name) - left `And` right -> - evaluateProposition assignment left - && evaluateProposition assignment right - left `Or` right -> - evaluateProposition assignment left - || evaluateProposition assignment right - left `Implies` right -> - not (evaluateProposition assignment left) - || evaluateProposition assignment right - Not _location formula -> - not (evaluateProposition assignment formula) - Top -> - True - Bottom -> - False - formula -> - error - ( "not a propositional test formula under " - <> show assignment - <> ": " - <> show formula - ) - -propositionAssignments :: [PropositionAssignment] -propositionAssignments = - [ (a, b, c) - | a <- [False, True] - , b <- [False, True] - , c <- [False, True] - ] - -propositionA, propositionB, propositionC :: Formula -propositionA = proposition "A" -propositionB = proposition "B" -propositionC = proposition "C" - -proposition :: Text -> Formula -proposition name = - Atomic Nowhere (PredicateSymbol name) [] - -expectChecks :: [Block] -> Assertion -expectChecks blocks = do - _tasks <- check WithoutDumpPremselTraining blocks - pure () - -encodedTasksText :: [Block] -> IO Text -encodedTasksText blocks = do - tasks <- check WithoutDumpPremselTraining blocks - if null tasks - then assertFailure "expected at least one generated task" - else pure () - pure (Text.intercalate "\n------------------\n" (encodeTaskText <$> tasks)) - -expectCheckingError :: Text -> [Block] -> Assertion -expectCheckingError fragment blocks = do - result <- try (check WithoutDumpPremselTraining blocks) :: IO (Either CheckingError [Task]) - case result of - Right _ -> - assertFailure "expected a CheckingError, but checking succeeded" - Left err@(CheckingError msg _ _) -> - assertBool ("expected error containing " <> show fragment <> ", got " <> show err) (fragment `Text.isInfixOf` msg) - Left err -> - assertFailure ("expected generic CheckingError, got " <> show err) - -expectMismatchedAssume :: [Block] -> Assertion -expectMismatchedAssume blocks = do - result <- try (check WithoutDumpPremselTraining blocks) :: IO (Either CheckingError [Task]) - case result of - Right _ -> - assertFailure "expected a MismatchedAssume error, but checking succeeded" - Left (MismatchedAssume _assumption _goal _location _marker) -> - pure () - Left err -> - assertFailure ("expected MismatchedAssume, got " <> show err) - -expectFactMarkers :: [Marker] -> [Block] -> Assertion -expectFactMarkers markers blocks = do - checkingState <- runCheckingBlocks blocks (initialCheckingState WithoutDumpPremselTraining (\_task -> pure ())) - let facts = checkingFacts checkingState - for_ markers \marker -> - assertBool - ("expected generated fact marker " <> show marker) - (isJust (Facts.lookupPreparedFact marker facts)) - -datatypePreparedFacts - :: [Block] - -> IO [Facts.PreparedSemanticFact] -datatypePreparedFacts blocks = do - checkingState <- - runCheckingBlocks - blocks - ( initialCheckingState - WithoutDumpPremselTraining - (\_task -> pure ()) - ) - traverse - (lookupFact (checkingFacts checkingState)) - datatypeGeneratedMarkers - where - lookupFact facts marker = - case Facts.lookupPreparedFact marker facts of - Just fact -> - pure fact - Nothing -> do - assertFailure - ("missing generated datatype fact " <> show marker) - pure - (impossible - "assertFailure returned while looking up a datatype fact") - -expectDefinedMarkers :: [Marker] -> [Block] -> Assertion -expectDefinedMarkers markers blocks = do - checkingState <- runCheckingBlocks blocks (initialCheckingState WithoutDumpPremselTraining (\_task -> pure ())) - let reserved = definedMarkers checkingState - for_ markers \marker -> - assertBool ("expected reserved marker " <> show marker) (HS.member marker reserved) - -expectDuplicateMarker :: Marker -> [Block] -> Assertion -expectDuplicateMarker expectedMarker blocks = do - result <- try (check WithoutDumpPremselTraining blocks) :: IO (Either CheckingError [Task]) - case result of - Right _ -> - assertFailure "expected a DuplicateMarker error, but checking succeeded" - Left (DuplicateMarker _ actualMarker) -> - assertEqual "duplicate marker" expectedMarker actualMarker - Left err -> - assertFailure ("expected DuplicateMarker, got " <> show err) - -assertContains :: String -> Text -> Text -> Assertion -assertContains label needle haystack = - assertBool (label <> ": expected to find " <> show needle <> " in " <> Text.unpack haystack) (needle `Text.isInfixOf` haystack) - -assertNotContains :: String -> Text -> Text -> Assertion -assertNotContains label needle haystack = - assertBool (label <> ": expected not to find " <> show needle <> " in " <> Text.unpack haystack) (not (needle `Text.isInfixOf` haystack)) - -lemmaBlocks :: Marker -> Lemma -> Proof -> [Block] -lemmaBlocks marker lemma proof = - [BlockLemma Nowhere marker lemma, BlockProof Nowhere Nowhere proof] - -badFixLemma :: Lemma -badFixLemma = - Lemma [Asm (var "a" `eq` var "b")] (makeForall ["x"] (var "x" `eq` var "b")) - -badFixProof :: Proof -badFixProof = - Fix Nowhere ("a" :| []) Top (Qed (Just Nowhere) JustificationLocal) - -badDefineLemma :: Lemma -badDefineLemma = - Lemma [] (makeForall ["x"] (var "x" `eq` emptySet)) - -badDefineProof :: Proof -badDefineProof = - Fix Nowhere ("x" :| []) Top (Define Nowhere "x" emptySet (Qed (Just Nowhere) JustificationLocal)) - -badTakeLemma :: Lemma -badTakeLemma = - Lemma [Asm (makeExists ["x"] (var "x" `neq` var "b"))] (var "a" `neq` var "b") - -badTakeProof :: Proof -badTakeProof = - Take Nowhere ("a" :| []) (var "a" `neq` var "b") JustificationLocal (Qed (Just Nowhere) JustificationLocal) - -badHaveLemma :: Lemma -badHaveLemma = - Lemma [] Top - -badHaveProof :: Proof -badHaveProof = - Have Nowhere (var "c" `eq` var "c") JustificationEmpty (Qed (Just Nowhere) JustificationEmpty) - -badDefineFunctionNameLemma :: Lemma -badDefineFunctionNameLemma = - Lemma [] (var "f" `eq` var "f") - -badDefineFunctionNameProof :: Proof -badDefineFunctionNameProof = - DefineFunction Nowhere "f" "x" (var "x") emptySet (Qed (Just Nowhere) JustificationLocal) - -badDefineFunctionArgLemma :: Lemma -badDefineFunctionArgLemma = - Lemma [] (var "x" `eq` var "x") - -badDefineFunctionArgProof :: Proof -badDefineFunctionArgProof = - DefineFunction Nowhere "f" "x" (var "x") emptySet (Qed (Just Nowhere) JustificationLocal) - -freeGoalLocalLemma :: Lemma -freeGoalLocalLemma = - Lemma [] (var "b" `eq` var "b") - -freeGoalLocalProof :: Proof -freeGoalLocalProof = - Qed (Just Nowhere) JustificationEmpty - -freshFixLemma :: Lemma -freshFixLemma = - Lemma [] (makeForall ["x"] (var "x" `eq` var "x")) - -freshFixProof :: Proof -freshFixProof = - Fix Nowhere ("x" :| []) Top (Qed (Just Nowhere) JustificationEmpty) - -freshTakeLemma :: Lemma -freshTakeLemma = - Lemma [Asm (makeExists ["x"] (var "x" `eq` var "b"))] (var "b" `eq` var "b") - -freshTakeProof :: Proof -freshTakeProof = - Take Nowhere ("y" :| []) (var "y" `eq` var "b") JustificationLocal (Qed (Just Nowhere) JustificationEmpty) - -unsoundDisjunctionAssumeBlocks :: [Block] -unsoundDisjunctionAssumeBlocks = - [ BlockAxiom Nowhere "membership_asymmetry" - (Axiom [] (membershipXY `Implies` Not Nowhere membershipYX)) - , BlockLemma Nowhere "membership_totality" - (Lemma [] (membershipXY `Or` membershipYX)) - , BlockProof Nowhere Nowhere - (Assume Nowhere membershipXY - (Qed (Just Nowhere) - (JustificationRef ("membership_asymmetry" :| [])))) - ] - where - membershipXY = var "x" `isElementOf` var "y" - membershipYX = var "y" `isElementOf` var "x" - -structCarrierRewriteBlocks :: [Block] -structCarrierRewriteBlocks = - [ fooStructBlock "foo_struct" [("foo_rule", makeForall ["x"] ((var "x" `isElementOf` var "A") `Implies` (var "x" `isElementOf` var "A")))] - , BlockLemma Nowhere "foo_test" (Lemma [AsmStruct "A" fooStruct, Asm (var "x" `isElementOf` var "A")] (var "x" `isElementOf` var "A")) - , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("foo_rule" :| []))) - ] - -structOperationRewriteBlocks :: [Block] -structOperationRewriteBlocks = - [ fooStructBlock "foo_op_struct" [("foo_op_rule", TermSymbolStruct fooOp Nothing `isElementOf` var "A")] - , BlockLemma Nowhere "foo_op_test" (Lemma [AsmStruct "A" fooStruct] (TermSymbolStruct fooOp Nothing `isElementOf` var "A")) - , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("foo_op_rule" :| []))) - ] - -unresolvedStructOperationBlocks :: [Block] -unresolvedStructOperationBlocks = - [ fooStructBlock "unresolved_structure_definition" [] - , BlockAxiom - structureTermErrorLocation - "unresolved_structure_operation" - (Axiom [] - (TermSymbolStruct fooOp Nothing - `eq` TermSymbolStruct fooOp Nothing)) - ] - -nestedStructComprehensionBlocks :: [Block] -nestedStructComprehensionBlocks = - [ fooStructBlock "nested_structure_definition" [] - , BlockAxiom - structureTermErrorLocation - "nested_structure_comprehension" - (Axiom [] - (nestedOperation `eq` nestedOperation)) - ] - where - nestedOperation = - TermSymbolStruct - fooOp - (Just - (TermSep - "x" - emptySet - (toScope Top))) - -structureTermErrorLocation :: Location -structureTermErrorLocation = - mkLocation (FileId 50) 7 1 - -structClaimIntroducesContextBlocks :: [Block] -structClaimIntroducesContextBlocks = - [ fooStructBlock "foo_claim_struct" [] - , BlockLemma Nowhere "foo_claim_test" (Lemma [] ((var "A" `eq` var "A") `And` (var "x" `eq` var "x"))) - , BlockProof Nowhere Nowhere $ - Have Nowhere (fooStructPredicate "A") JustificationEmpty $ - Have Nowhere (var "x" `isElementOf` var "A") JustificationEmpty (Omitted Nowhere) - ] - -boundStructLabelBlocks :: [Block] -boundStructLabelBlocks = - [ fooStructBlock "foo_bound_struct" [] - , BlockLemma Nowhere "foo_bound_test" (Lemma [AsmStruct "A" fooStruct] (makeForall ["A"] (var "x" `isElementOf` var "A"))) - , BlockProof Nowhere Nowhere (Qed (Just Nowhere) JustificationEmpty) - ] - -fooStructBlock :: Marker -> [(Marker, Formula)] -> Block -fooStructBlock marker assumes = - BlockStruct Nowhere marker (fooStructDefn assumes) - -fooStructDefn :: [(Marker, Formula)] -> StructDefn -fooStructDefn assumes = - StructDefn - { structPhrase = fooStruct - , structParents = Set.singleton _Onesorted - , structDefnLabel = "A" - , structDefnFixes = Set.singleton fooOp - , structDefnAssumes = assumes - } - -testStructBlock - :: Marker - -> StructPhrase - -> Set StructPhrase - -> [(Marker, Formula)] - -> Block -testStructBlock marker phrase parents assumes = - BlockStruct Nowhere marker StructDefn - { structPhrase = phrase - , structParents = parents - , structDefnLabel = "A" - , structDefnFixes = mempty - , structDefnAssumes = assumes - } - -fooStruct :: StructPhrase -fooStruct = - mkLexicalItemSgPl (unsafeReadPhraseSgPl "foo[/s]") "foo" - -childStruct :: StructPhrase -childStruct = - mkLexicalItemSgPl - (unsafeReadPhraseSgPl "child[/s]") - "child" - -unknownStruct :: StructPhrase -unknownStruct = - mkLexicalItemSgPl - (unsafeReadPhraseSgPl "unknown[/s]") - "unknown" - -fooOp :: StructSymbol -fooOp = - StructSymbol "fooop" - -fooStructPredicate :: VarSymbol -> Formula -fooStructPredicate x = - TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct fooStruct)) [TermVar x] - -hiddenSelfReferentialStructBlocks :: [Block] -hiddenSelfReferentialStructBlocks = - [ BlockAbbr Nowhere "struct_alias_a" - ( Abbreviation - (SymbolPredicate structAliasA) - (toScope - (TermSymbol - Nowhere - (SymbolPredicate (PredicateNounStruct fooStruct)) - [TermVar (B 0)])) - ) - , BlockAbbr Nowhere "struct_alias_b" - ( Abbreviation - (SymbolPredicate structAliasB) - (toScope - (TermSymbol - Nowhere - (SymbolPredicate structAliasA) - [TermVar (B 0)])) - ) - , fooStructBlock - "hidden_self_struct" - [("hidden_self_rule", structAliasFormula structAliasB (var "A"))] - ] - -structAliasA :: Predicate -structAliasA = - PredicateSymbol "struct_alias_a" - -structAliasB :: Predicate -structAliasB = - PredicateSymbol "struct_alias_b" - -structAliasFormula :: Predicate -> Term -> Formula -structAliasFormula predicate term = - TermSymbol Nowhere (SymbolPredicate predicate) [term] - -var :: VarSymbol -> Term -var = TermVar - -emptySet :: Term -emptySet = EmptySet Nowhere - -eq :: Term -> Term -> Formula -eq = Equals Nowhere - -neq :: Term -> Term -> Formula -neq = NotEquals Nowhere - -directSelfReferentialAbbrBlocks :: [Block] -directSelfReferentialAbbrBlocks = - [ BlockAbbr Nowhere "bad_abbr_direct" (Abbreviation abbrSymbolA (toScope (TermSymbol Nowhere abbrSymbolA []))) - ] - -indirectSelfReferentialAbbrBlocks :: [Block] -indirectSelfReferentialAbbrBlocks = - [ BlockAbbr Nowhere "bad_abbr_indirect_a" (Abbreviation abbrSymbolA (toScope (TermSymbol Nowhere abbrSymbolB []))) - , BlockAbbr Nowhere "bad_abbr_indirect_b" (Abbreviation abbrSymbolB (toScope (TermSymbol Nowhere abbrSymbolA []))) - ] - -directSelfReferentialPredicateDefinitionBlocks :: [Block] -directSelfReferentialPredicateDefinitionBlocks = - [ BlockDefn Nowhere "bad_predicate_definition_direct" - ( DefnPredicate - [] - definitionTestPredicate - ("x" :| []) - (Not Nowhere (definitionTestPredicateFormula (var "x"))) - ) - ] - -directSelfReferentialFunctionDefinitionBlocks :: [Block] -directSelfReferentialFunctionDefinitionBlocks = - [ BlockDefn Nowhere "bad_function_definition_direct" - ( DefnFun - [] - definitionTestFunction - ["x"] - (definitionTestFunctionTerm (var "x")) - ) - ] - -directSelfReferentialOperatorDefinitionBlocks :: [Block] -directSelfReferentialOperatorDefinitionBlocks = - [ BlockDefn Nowhere "bad_operator_definition_direct" - (DefnOp definitionTestOperator ["x"] (termSymbol definitionTestOperator [var "x"])) - ] - -abbreviationHiddenSelfReferentialDefinitionBlocks :: [Block] -abbreviationHiddenSelfReferentialDefinitionBlocks = - [ BlockAbbr Nowhere "bad_definition_body_alias" - ( Abbreviation - (SymbolMixfix selfDefinitionBodyAlias) - (toScope (TermSymbol Nowhere (SymbolMixfix definitionTestOperator) [TermVar (B 0)])) - ) - , BlockDefn Nowhere "bad_definition_body_target" - (DefnOp definitionTestOperator ["x"] (termSymbol selfDefinitionBodyAlias [var "x"])) - ] - -assumptionHiddenSelfReferentialDefinitionBlocks :: [Block] -assumptionHiddenSelfReferentialDefinitionBlocks = - [ BlockAbbr Nowhere "bad_definition_assumption_alias" - ( Abbreviation - (SymbolPredicate selfDefinitionAssumptionAlias) - (toScope (TermSymbol Nowhere (SymbolPredicate definitionTestPredicate) [TermVar (B 0)])) - ) - , BlockDefn Nowhere "bad_definition_assumption_target" - ( DefnPredicate - [Asm (selfDefinitionAssumptionAliasFormula (var "x"))] - definitionTestPredicate - ("x" :| []) - (var "x" `eq` var "x") - ) - ] - -nonRecursiveDefinitionBlocks :: [Block] -nonRecursiveDefinitionBlocks = - [ BlockDefn Nowhere "good_predicate_definition" - (DefnPredicate [] definitionTestPredicate ("x" :| []) (var "x" `eq` var "x")) - , BlockDefn Nowhere "good_function_definition" - (DefnFun [] definitionTestFunction ["x"] emptySet) - , BlockDefn Nowhere "good_operator_definition" - (DefnOp definitionTestOperator ["x"] emptySet) - ] - -definitionTestPredicate :: Predicate -definitionTestPredicate = - PredicateSymbol "definition_test_predicate" - -definitionTestPredicateFormula :: Term -> Formula -definitionTestPredicateFormula expr = - TermSymbol Nowhere (SymbolPredicate definitionTestPredicate) [expr] - -definitionTestFunction :: LexicalItemSgPl -definitionTestFunction = - mkLexicalItemSgPl - (unsafeReadPhraseSgPl "definition test function[/s] of ?") - "definition_test_function" - -definitionTestFunctionTerm :: Term -> Term -definitionTestFunctionTerm expr = - TermSymbol Nowhere (SymbolFun definitionTestFunction) [expr] - -definitionTestOperator :: FunctionSymbol -definitionTestOperator = - unarySymbol "definition_test_operator" - -selfDefinitionBodyAlias :: FunctionSymbol -selfDefinitionBodyAlias = - unarySymbol "self_definition_body_alias" - -selfDefinitionAssumptionAlias :: Predicate -selfDefinitionAssumptionAlias = - PredicateSymbol "self_definition_assumption_alias" - -selfDefinitionAssumptionAliasFormula :: Term -> Formula -selfDefinitionAssumptionAliasFormula expr = - TermSymbol Nowhere (SymbolPredicate selfDefinitionAssumptionAlias) [expr] - -builtinMixfixMarkerCollisionBlock :: Block -builtinMixfixMarkerCollisionBlock = - BlockDefn Nowhere "pow" (DefnOp powHijackSym ["A"] emptySet) - -powHijackSym :: FunctionSymbol -powHijackSym = - mkMixfixItem - [Just (Command "powhijack"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] - "pow" - NonAssoc - -builtinPredicateMarkerCollisionBlock :: Block -builtinPredicateMarkerCollisionBlock = - BlockDefn Nowhere "elem" - ( DefnPredicate - [] - (PredicateRelation - (RelationSymbol - (Command "elemhijack") - zeroParameterArity - "elem")) - ("A" :| ["B"]) - (var "A" `eq` var "B") - ) - -builtinAbbreviationMarkerCollisionBlock :: Block -builtinAbbreviationMarkerCollisionBlock = - BlockAbbr Nowhere "pow" - ( Abbreviation - (SymbolMixfix (constSymbolWithMarker "powabbr" "pow")) - (toScope (TermSymbol Nowhere (SymbolInteger 0) [])) - ) - -builtinMarkerProofLabelBlock :: Block -builtinMarkerProofLabelBlock = - BlockAxiom Nowhere "pow" (Axiom [] (emptySet `eq` emptySet)) - -subseteqDefinitionBlock :: Block -subseteqDefinitionBlock = - BlockDefn Nowhere "subseteq" - ( DefnPredicate - [] - (PredicateRelation SubseteqSymbol) - ("A" :| ["B"]) - (var "A" `eq` var "B") - ) - -goodDatatypeBlock :: Block -goodDatatypeBlock = - datatypeBlock "good_datatype" goodDatatypeClauses - -directRecursionAliasDatatypeBlocks :: [Block] -directRecursionAliasDatatypeBlocks = - [ closedDatatypeAliasBlock - "direct_recursion_alias" - directRecursionAliasSym - (closedTermSymbol propformSym []) - , datatypeBlock - "aliased_recursive_datatype" - ( DatatypeClause - (SymbolPattern propbotSym []) - [] - :| [ DatatypeClause - (SymbolPattern propvarSym ["n"]) - [("n", naturalsTerm)] - , DatatypeClause - (SymbolPattern proptoSym ["p", "q"]) - [ ("p", termSymbol directRecursionAliasSym []) - , ("q", termSymbol directRecursionAliasSym []) - ] - ] - ) - ] - -oneHopPowersetAliasDatatypeBlocks :: [Block] -oneHopPowersetAliasDatatypeBlocks = - [ closedDatatypeAliasBlock - "powerset_recursion_alias" - powersetRecursionAliasSym - ( closedTermSymbol - powSym - [closedTermSymbol propformSym []] - ) - , datatypeBlock - "one_hop_powerset_recursive_datatype" - ( DatatypeClause - (SymbolPattern propvarSym ["n"]) - [("n", termSymbol powersetRecursionAliasSym [])] - :| [] - ) - ] - -multiHopPowersetAliasDatatypeBlocks :: [Block] -multiHopPowersetAliasDatatypeBlocks = - [ closedDatatypeAliasBlock - "powerset_recursion_alias" - powersetRecursionAliasSym - ( closedTermSymbol - powSym - [closedTermSymbol propformSym []] - ) - , closedDatatypeAliasBlock - "indirect_powerset_recursion_alias" - indirectPowersetRecursionAliasSym - (closedTermSymbol powersetRecursionAliasSym []) - , datatypeBlock - "multi_hop_powerset_recursive_datatype" - ( DatatypeClause - (SymbolPattern propvarSym ["n"]) - [("n", termSymbol indirectPowersetRecursionAliasSym [])] - :| [] - ) - ] - -closedDatatypeAliasBlock - :: Marker - -> FunctionSymbol - -> ExprOf (Var Int Void) - -> Block -closedDatatypeAliasBlock marker symbol body = - BlockAbbr - Nowhere - marker - (Abbreviation (SymbolMixfix symbol) (toScope body)) - -closedTermSymbol - :: FunctionSymbol - -> [ExprOf (Var Int Void)] - -> ExprOf (Var Int Void) -closedTermSymbol symbol = - TermSymbol Nowhere (SymbolMixfix symbol) - -datatypeGeneratedMarkers :: [Marker] -datatypeGeneratedMarkers = - [ "propform_propbot_intro" - , "propform_propvar_intro" - , "propform_propto_intro" - , "propform_propbot_propvar_distinct" - , "propform_propbot_propto_distinct" - , "propform_propvar_propto_distinct" - , "propform_propvar_injective" - , "propform_propto_injective" - , "propform_cases" - , "propform_induct" - ] - -datatypeIntroReferenceBlocks :: [Block] -datatypeIntroReferenceBlocks = - [ goodDatatypeBlock - , BlockLemma Nowhere "datatype_propbot_intro_ref" - (Lemma [] (propbotTerm `isElementOf` propformTerm)) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("propform_propbot_intro" :| []))) - , BlockLemma Nowhere "datatype_propvar_intro_ref" - (Lemma [Asm (var "n" `isElementOf` naturalsTerm)] (termSymbol propvarSym [var "n"] `isElementOf` propformTerm)) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("propform_propvar_intro" :| []))) - , BlockLemma Nowhere "datatype_propto_intro_ref" - (Lemma [Asm (propbotTerm `isElementOf` propformTerm)] (proptoTerm propbotTerm propbotTerm `isElementOf` propformTerm)) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("propform_propto_intro" :| []))) - ] - -datatypeDistinctReferenceBlocks :: [Block] -datatypeDistinctReferenceBlocks = - [ goodDatatypeBlock - , BlockLemma Nowhere "datatype_distinct_ref" - (Lemma [] (propbotTerm `neq` proptoTerm propbotTerm propbotTerm)) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("propform_propbot_propto_distinct" :| []))) - ] - -datatypeInjectiveReferenceBlocks :: [Block] -datatypeInjectiveReferenceBlocks = - [ goodDatatypeBlock - , BlockLemma Nowhere "datatype_injective_ref" - (Lemma [] (makeForall ["m", "n"] ((termSymbol propvarSym [var "m"] `eq` termSymbol propvarSym [var "n"]) `Implies` (var "m" `eq` var "n")))) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("propform_propvar_injective" :| []))) - ] - -datatypeGeneratedMarkerReuseBlocks :: [Block] -datatypeGeneratedMarkerReuseBlocks = - [ goodDatatypeBlock - , BlockLemma Nowhere "propform_cases" (Lemma [] Top) - ] - -badDuplicateConstructorMarkerDatatypeBlock :: Block -badDuplicateConstructorMarkerDatatypeBlock = - datatypeBlock "propform" - ( DatatypeClause (SymbolPattern (unarySymbol "dup") ["n"]) [("n", naturalsTerm)] :| - [ DatatypeClause (SymbolPattern (infixSymbol "dup") ["p", "q"]) [("p", propformTerm), ("q", propformTerm)] - ] - ) - -badNestedRecursiveDatatypeBlock :: Block -badNestedRecursiveDatatypeBlock = - datatypeBlock "bad_nested_recursive_datatype" - (DatatypeClause (SymbolPattern proptoSym ["p", "q"]) [("p", wrapPropformTerm), ("q", propformTerm)] :| []) - -badMissingPremiseDatatypeBlock :: Block -badMissingPremiseDatatypeBlock = - datatypeBlock "bad_missing_premise_datatype" - (DatatypeClause (SymbolPattern propvarSym ["n"]) [] :| []) - -badDuplicateConstructorDatatypeBlock :: Block -badDuplicateConstructorDatatypeBlock = - datatypeBlock "bad_duplicate_constructor_datatype" - ( DatatypeClause (SymbolPattern propbotSym []) [] :| - [ DatatypeClause (SymbolPattern propbotSym []) [] - ] - ) - -badOpenDomainDatatypeBlock :: Block -badOpenDomainDatatypeBlock = - datatypeBlock "bad_open_domain_datatype" - (DatatypeClause (SymbolPattern propvarSym ["n"]) [("n", TermVar "A")] :| []) - -badApplyConstructorDatatypeBlock :: Block -badApplyConstructorDatatypeBlock = - datatypeBlock "bad_apply_constructor_datatype" - (DatatypeClause (SymbolPattern ApplySymbol ["f", "x"]) [("f", naturalsTerm), ("x", naturalsTerm)] :| []) - -goodInductiveBlock :: Block -goodInductiveBlock = - BlockInductive Nowhere "fin" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` finTerm (var "A")) :| - [ IntroRule - [ var "a" `isElementOf` var "A" - , var "B" `isElementOf` finTerm (var "A") - ] - (consTerm (var "a") (var "B") `isElementOf` finTerm (var "A")) - ] - } - -goodInductiveBlocks :: [Block] -goodInductiveBlocks = - [ goodInductiveBlock - ] - -goodMonotoneInductiveBlock :: Block -goodMonotoneInductiveBlock = - BlockInductive Nowhere "acc" Inductive - { inductiveSymbol = accSym - , inductiveParams = ["R"] - , inductiveDomain = wrapTerm (var "R") - , inductiveIntros = - IntroRule - [ var "x" `isElementOf` wrapTerm (accTerm (var "R")) ] - (var "x" `isElementOf` accTerm (var "R")) - :| [] - } - -goodMonotoneInductiveBlocks :: [Block] -goodMonotoneInductiveBlocks = - [ wrapSignatureBlock - , goodMonotoneInductiveBlock - ] - -inductiveGeneratedMarkers :: [Marker] -inductiveGeneratedMarkers = - [ "fin_intro_1" - , "fin_intro_2" - , "fin_dom_subset" - , "fin_cases" - , "fin_induct" - ] - -inductiveIntroAndDomainReferenceBlocks :: [Block] -inductiveIntroAndDomainReferenceBlocks = - goodInductiveBlocks - <> [ BlockLemma Nowhere "inductive_intro_ref" - (Lemma [] (makeForall ["A"] (emptySet `isElementOf` finTerm (var "A")))) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("fin_intro_1" :| []))) - , BlockLemma Nowhere "inductive_dom_subset_ref" - (Lemma [] $ - makeForall ["A"] $ - semanticSubsetFormula (Set.fromList ["A"]) (finTerm (var "A")) (powTerm (var "A"))) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("fin_dom_subset" :| []))) - ] - -inductiveCasesReferenceBlocks :: [Block] -inductiveCasesReferenceBlocks = - goodInductiveBlocks - <> [ BlockLemma Nowhere "inductive_cases_ref" - (Lemma [] finCasesFormula) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("fin_cases" :| []))) - ] - -inductiveInductReferenceBlocks :: [Block] -inductiveInductReferenceBlocks = - goodInductiveBlocks - <> [ BlockLemma Nowhere "inductive_induct_ref" - (Lemma [] finInductFormula) - , BlockProof Nowhere Nowhere - (Qed (Just Nowhere) (JustificationRef ("fin_induct" :| []))) - ] - -duplicateInductiveCarrierBlocks :: [Block] -duplicateInductiveCarrierBlocks = - goodInductiveBlocks - <> [ BlockInductive Nowhere "fin_again" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = wrapTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` finTerm (var "A")) :| [] - } - ] - -operatorThenInductiveBlocks :: [Block] -operatorThenInductiveBlocks = - [ BlockDefn Nowhere "fin_operator_definition" (DefnOp finSym ["A"] emptySet) - , goodInductiveBlock - ] - -signaturePredicateUsageBlocks :: [Block] -signaturePredicateUsageBlocks = - [ BlockSig Nowhere "sig_predicate" [] (SignaturePredicate signaturePredicate ("x" :| [])) - , BlockLemma Nowhere "sig_predicate_use" - (Lemma [] (makeForall ["x"] (signaturePredicateFormula (var "x") `Implies` signaturePredicateFormula (var "x")))) - ] - -signatureFormulaUsageBlocks :: [Block] -signatureFormulaUsageBlocks = - [ BlockSig Nowhere "sig_formula" [] (SignatureFormula recoverableSignatureFormula) - , BlockLemma Nowhere "sig_formula_use" - (Lemma [] (makeForall ["A"] (signatureDeclaredTerm (var "A") `eq` signatureDeclaredTerm (var "A")))) - ] - -badSignatureFormulaBlock :: Block -badSignatureFormulaBlock = - BlockSig Nowhere "bad_signature_formula" [] (SignatureFormula Top) - -priorInductiveCarrierAxiomBlocks :: [Block] -priorInductiveCarrierAxiomBlocks = - [ BlockAxiom Nowhere "pre_fin_axiom" (Axiom [] (emptySet `isElementOf` finTerm emptySet)) - , goodInductiveBlock - ] - -badInductiveSelfDomainBlock :: Block -badInductiveSelfDomainBlock = - BlockInductive Nowhere "bad_inductive_self_domain" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = finTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` finTerm (var "A")) :| [] - } - -hiddenSelfDomainBlocks :: [Block] -hiddenSelfDomainBlocks = - [ BlockAbbr Nowhere "hidden_self_domain_abbr" - (Abbreviation - (SymbolMixfix hiddenSelfDomainSym) - (toScope (TermSymbol Nowhere (SymbolMixfix finSym) [TermVar (B 0)]))) - , BlockInductive Nowhere "hidden_self_domain_inductive" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = hiddenSelfDomainTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` finTerm (var "A")) :| [] - } - ] - -hiddenDefinitionDomainBlocks :: [Block] -hiddenDefinitionDomainBlocks = - [ BlockDefn Nowhere "ordinary_domain_alias_definition" (DefnOp ordinaryDomainAliasSym ["A"] (finTerm (var "A"))) - , BlockInductive Nowhere "ordinary_definition_hidden_domain_inductive" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = ordinaryDomainAliasTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` finTerm (var "A")) :| [] - } - ] - -hiddenCarrierSideConditionBlocks :: [Block] -hiddenCarrierSideConditionBlocks = - [ BlockDefn Nowhere "hidden_carrier_definition" (DefnOp hiddenCarrierSym ["A"] (finTerm (var "A"))) - , BlockInductive Nowhere "ordinary_definition_hidden_side_condition_inductive" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ var "x" `isElementOf` hiddenCarrierTerm (var "A") ] - (emptySet `isElementOf` finTerm (var "A")) - :| [] - } - ] - -priorDatatypeHeadSignatureBlocks :: [Block] -priorDatatypeHeadSignatureBlocks = - [ BlockSig Nowhere "pre_propform_signature" [] (SignatureFormula propformSignatureFormula) - , goodDatatypeBlock - ] - -priorDatatypeConstructorLemmaBlocks :: [Block] -priorDatatypeConstructorLemmaBlocks = - [ BlockLemma Nowhere "pre_propbot_lemma" (Lemma [] (propbotTerm `eq` propbotTerm)) - , goodDatatypeBlock - ] - -datatypeConstructorThenOperatorBlocks :: [Block] -datatypeConstructorThenOperatorBlocks = - [ goodDatatypeBlock - , BlockDefn Nowhere "propbot_operator_definition" (DefnOp propbotSym [] emptySet) - ] - -frozenSymbolDefinitionBlocks :: [Block] -frozenSymbolDefinitionBlocks = - [ laterSignatureBlock - , freezingInductiveBlock - , BlockDefn Nowhere "later_operator_definition" (DefnOp laterSym ["A"] emptySet) - ] - -freezingInductiveBlock :: Block -freezingInductiveBlock = - BlockInductive Nowhere "freeze_inductive" Inductive - { inductiveSymbol = freezeCarrierSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ var "x" `eq` laterTerm (var "A") ] - (emptySet `isElementOf` freezeCarrierTerm (var "A")) - :| [] - } - -canonicalizedDomainFreezeBlocks :: [Block] -canonicalizedDomainFreezeBlocks = - [ laterSignatureBlock - , BlockAbbr Nowhere "domain_alias_abbr" - (Abbreviation - (SymbolMixfix domainAliasSym) - (toScope (TermSymbol Nowhere (SymbolMixfix laterSym) [TermVar (B 0)]))) - , BlockInductive Nowhere "canonicalized_domain_freeze_inductive" Inductive - { inductiveSymbol = freezeCarrierSym - , inductiveParams = ["A"] - , inductiveDomain = domainAliasTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` freezeCarrierTerm (var "A")) :| [] - } - , BlockDefn Nowhere "later_operator_definition_after_canonicalized_domain" (DefnOp laterSym ["A"] emptySet) - ] - -transitiveFrozenDefinitionBlocks :: [Block] -transitiveFrozenDefinitionBlocks = - [ laterSignatureBlock - , BlockDefn Nowhere "middle_later_alias_definition" (DefnOp middleLaterAliasSym ["A"] (laterTerm (var "A"))) - , BlockDefn Nowhere "indirect_later_alias_definition" (DefnOp indirectLaterAliasSym ["A"] (middleLaterAliasTerm (var "A"))) - , BlockInductive Nowhere "transitive_freeze_inductive" Inductive - { inductiveSymbol = freezeCarrierSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ var "x" `isElementOf` indirectLaterAliasTerm (var "A") ] - (emptySet `isElementOf` freezeCarrierTerm (var "A")) - :| [] - } - , BlockDefn Nowhere "later_operator_definition_after_transitive_freeze" (DefnOp laterSym ["A"] emptySet) - ] - -badRecursiveTermInductiveBlock :: Block -badRecursiveTermInductiveBlock = - BlockInductive Nowhere "bad_recursive_term_inductive" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ finTerm (var "A") `isElementOf` powTerm (var "A") ] - (emptySet `isElementOf` finTerm (var "A")) - :| [] - } - -badRecursiveFormulaInductiveBlock :: Block -badRecursiveFormulaInductiveBlock = - BlockInductive Nowhere "bad_recursive_formula_inductive" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ Not Nowhere (emptySet `isElementOf` finTerm (var "A")) ] - (emptySet `isElementOf` finTerm (var "A")) - :| [] - } - -badInductiveResultBlock :: Block -badInductiveResultBlock = - BlockInductive Nowhere "bad_inductive_result" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule [] (emptySet `isElementOf` powTerm (var "A")) :| [] - } - -badInductiveWrongArgsBlock :: Block -badInductiveWrongArgsBlock = - BlockInductive Nowhere "bad_inductive_wrong_args" Inductive - { inductiveSymbol = finSym - , inductiveParams = ["A"] - , inductiveDomain = powTerm (var "A") - , inductiveIntros = - IntroRule - [ var "B" `isElementOf` finTerm (var "B") ] - (emptySet `isElementOf` finTerm (var "A")) - :| [] - } - -finCasesFormula :: Formula -finCasesFormula = - makeForall ["A", "x"] - ((var "x" `isElementOf` finTerm (var "A")) `Implies` makeDisjunction - [ var "x" `eq` emptySet - , makeExists ["a", "B"] - (makeConjunction - [ var "a" `isElementOf` var "A" - , var "B" `isElementOf` finTerm (var "A") - , var "x" `eq` consTerm (var "a") (var "B") - ]) - ]) - -finInductFormula :: Formula -finInductFormula = - makeForall ["A", "S"] - (makeConjunction - [ emptySet `isElementOf` var "S" - , makeForall ["a", "B"] - ((makeConjunction - [ var "a" `isElementOf` var "A" - , var "B" `isElementOf` var "S" - ]) - `Implies` - (consTerm (var "a") (var "B") `isElementOf` var "S")) - ] - `Implies` - semanticSubsetFormula - (Set.fromList ["A", "S"]) - (finTerm (var "A")) - (var "S")) - -goodDatatypeClauses :: NonEmpty DatatypeClause -goodDatatypeClauses = - DatatypeClause (SymbolPattern propbotSym []) [] :| - [ DatatypeClause (SymbolPattern propvarSym ["n"]) [("n", naturalsTerm)] - , DatatypeClause (SymbolPattern proptoSym ["p", "q"]) [("p", propformTerm), ("q", propformTerm)] - ] - -datatypeBlock :: Marker -> NonEmpty DatatypeClause -> Block -datatypeBlock marker clauses = - BlockData Nowhere marker (Datatype (SymbolPattern propformSym []) clauses) - -propformTerm :: Term -propformTerm = - termSymbol propformSym [] - -propbotTerm :: Term -propbotTerm = - termSymbol propbotSym [] - -naturalsTerm :: Term -naturalsTerm = - termSymbol naturalsSym [] - -wrapPropformTerm :: Term -wrapPropformTerm = - termSymbol wrapSym [propformTerm] - -powTerm :: Term -> Term -powTerm expr = - termSymbol powSym [expr] - -finTerm :: Term -> Term -finTerm expr = - termSymbol finSym [expr] - -accTerm :: Term -> Term -accTerm expr = - termSymbol accSym [expr] - -wrapTerm :: Term -> Term -wrapTerm expr = - termSymbol wrapSym [expr] - -laterTerm :: Term -> Term -laterTerm expr = - termSymbol laterSym [expr] - -freezeCarrierTerm :: Term -> Term -freezeCarrierTerm expr = - termSymbol freezeCarrierSym [expr] - -domainAliasTerm :: Term -> Term -domainAliasTerm expr = - termSymbol domainAliasSym [expr] - -hiddenSelfDomainTerm :: Term -> Term -hiddenSelfDomainTerm expr = - termSymbol hiddenSelfDomainSym [expr] - -ordinaryDomainAliasTerm :: Term -> Term -ordinaryDomainAliasTerm expr = - termSymbol ordinaryDomainAliasSym [expr] - -hiddenCarrierTerm :: Term -> Term -hiddenCarrierTerm expr = - termSymbol hiddenCarrierSym [expr] - -middleLaterAliasTerm :: Term -> Term -middleLaterAliasTerm expr = - termSymbol middleLaterAliasSym [expr] - -indirectLaterAliasTerm :: Term -> Term -indirectLaterAliasTerm expr = - termSymbol indirectLaterAliasSym [expr] - -signatureDeclaredTerm :: Term -> Term -signatureDeclaredTerm expr = - termSymbol signatureDeclaredSym [expr] - -signaturePredicateFormula :: Term -> Formula -signaturePredicateFormula expr = - TermSymbol Nowhere (SymbolPredicate signaturePredicate) [expr] - -recoverableSignatureFormula :: Formula -recoverableSignatureFormula = - makeForall ["z"] - ((var "z" `eq` signatureDeclaredTerm (var "A")) `Implies` (var "z" `eq` var "z")) - -propformSignatureFormula :: Formula -propformSignatureFormula = - makeForall ["z"] - ((var "z" `eq` propformTerm) `Implies` (var "z" `eq` var "z")) - -wrapSignatureBlock :: Block -wrapSignatureBlock = - mixfixSignatureBlock "wrap_signature" wrapSym ["A"] - -laterSignatureBlock :: Block -laterSignatureBlock = - mixfixSignatureBlock "later_signature" laterSym ["A"] - -mixfixSignatureBlock :: Marker -> FunctionSymbol -> [VarSymbol] -> Block -mixfixSignatureBlock marker symbol args = - BlockSig Nowhere marker [] (SignatureFormula (recoverableMixfixSignatureFormula symbol args)) - -recoverableMixfixSignatureFormula :: FunctionSymbol -> [VarSymbol] -> Formula -recoverableMixfixSignatureFormula symbol args = - makeForall ["z"] - ((var "z" `eq` termSymbol symbol (var <$> args)) `Implies` (var "z" `eq` var "z")) - -consTerm :: Term -> Term -> Term -consTerm left right = - termSymbol consSym [left, right] - -termSymbol :: FunctionSymbol -> [Term] -> Term -termSymbol sym args = - TermSymbol Nowhere (SymbolMixfix sym) args - -proptoTerm :: Term -> Term -> Term -proptoTerm left right = - termSymbol proptoSym [left, right] - -propformSym :: FunctionSymbol -propformSym = - constSymbol "propform" - -propbotSym :: FunctionSymbol -propbotSym = - constSymbol "propbot" - -propvarSym :: FunctionSymbol -propvarSym = - unarySymbol "propvar" - -proptoSym :: FunctionSymbol -proptoSym = - infixSymbol "propto" - -directRecursionAliasSym :: FunctionSymbol -directRecursionAliasSym = - constSymbol "directrecursionalias" - -powersetRecursionAliasSym :: FunctionSymbol -powersetRecursionAliasSym = - constSymbol "powersetrecursionalias" - -indirectPowersetRecursionAliasSym :: FunctionSymbol -indirectPowersetRecursionAliasSym = - constSymbol "indirectpowersetrecursionalias" - -naturalsSym :: FunctionSymbol -naturalsSym = - constSymbol "naturals" - -powSym :: FunctionSymbol -powSym = - unarySymbol "pow" - -finSym :: FunctionSymbol -finSym = - unarySymbol "fin" - -accSym :: FunctionSymbol -accSym = - unarySymbol "acc" - -consSym :: FunctionSymbol -consSym = - ConsSymbol - -wrapSym :: FunctionSymbol -wrapSym = - unarySymbol "wrap" - -laterSym :: FunctionSymbol -laterSym = - unarySymbol "later" - -freezeCarrierSym :: FunctionSymbol -freezeCarrierSym = - unarySymbol "freezecarrier" - -domainAliasSym :: FunctionSymbol -domainAliasSym = - unarySymbol "domainalias" - -hiddenSelfDomainSym :: FunctionSymbol -hiddenSelfDomainSym = - unarySymbol "hiddenselfdomain" - -ordinaryDomainAliasSym :: FunctionSymbol -ordinaryDomainAliasSym = - unarySymbol "ordinarydomainalias" - -hiddenCarrierSym :: FunctionSymbol -hiddenCarrierSym = - unarySymbol "hiddencarrier" - -middleLaterAliasSym :: FunctionSymbol -middleLaterAliasSym = - unarySymbol "middlelateralias" - -indirectLaterAliasSym :: FunctionSymbol -indirectLaterAliasSym = - unarySymbol "indirectlateralias" - -signatureDeclaredSym :: FunctionSymbol -signatureDeclaredSym = - unarySymbol "signaturedeclared" - -signaturePredicate :: Predicate -signaturePredicate = - PredicateSymbol "signaturepredicate" - -constSymbol :: Text -> FunctionSymbol -constSymbol name = - mkMixfixItem [Just (Command name)] (Marker name) NonAssoc - -constSymbolWithMarker :: Text -> Marker -> FunctionSymbol -constSymbolWithMarker name marker = - mkMixfixItem [Just (Command name)] marker NonAssoc - -unarySymbol :: Text -> FunctionSymbol -unarySymbol name = - mkMixfixItem [Just (Command name), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] (Marker name) NonAssoc - -infixSymbol :: Text -> FunctionSymbol -infixSymbol name = - mkMixfixItem [Nothing, Just (Command name), Nothing] (Marker name) NonAssoc - -abbrSymbolA :: Symbol -abbrSymbolA = abbrSymbol "unit_test_abbr_a" - -abbrSymbolB :: Symbol -abbrSymbolB = abbrSymbol "unit_test_abbr_b" - -abbrSymbol :: Text -> Symbol -abbrSymbol name = - SymbolMixfix (MixfixItem (TokenCons (Command name) End) (Marker name) NonAssoc) |