diff options
Diffstat (limited to 'source/Test/Unit/Source.hs')
| -rw-r--r-- | source/Test/Unit/Source.hs | 1930 |
1 files changed, 46 insertions, 1884 deletions
diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs index 3f6703e..73eaef5 100644 --- a/source/Test/Unit/Source.hs +++ b/source/Test/Unit/Source.hs @@ -5,35 +5,24 @@ module Test.Unit.Source (unitTests) where import Base -import Checking qualified -import Checking.Backend.Problem qualified as Backend -import Checking.Backend.Reconstruction qualified as Reconstruction -import Checking.Core qualified as Core -import Checking.Facts qualified as Facts import Checking.Foundation qualified as Foundation import Checking.Identity qualified as Identity -import Checking.Kernel.Derivation qualified as Derivation -import Checking.Legacy qualified as Legacy -import Checking.Obligation qualified as Obligation import Checking.Semantic qualified as Semantic -import Checking.Transition qualified as Transition import Felix.Cache.Codec qualified as Cache import Felix.Module qualified as Module import Felix.Parse qualified as Parse import Felix.Parsed.Identity qualified as ParsedIdentity import Felix.Parsed.Payload qualified as Parsed +import Felix.Prelude qualified as Prelude import Felix.Source import Felix.Source.Content qualified as Content import Felix.Source.Graph import Felix.Store qualified as Store -import Meaning qualified -import Provers qualified import Report.Location ( FileId(..) , FileIdAllocator(..) , Location(..) , LocationRegistrationError(..) - , pattern Nowhere , allocateFileId , locColumn , locFile @@ -44,21 +33,14 @@ import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Adapt qualified as Adapt import Syntax.Interface qualified as Interface -import Syntax.Internal import Syntax.Token (runLexer) -import Bound.Scope (toScope) -import Control.Exception (bracket, evaluate, try) -import Control.Monad (foldM) -import Control.Monad.Logger (runNoLoggingT) +import Control.Exception (bracket, evaluate) import Data.ByteString qualified as ByteString -import Data.HashMap.Strict qualified as HashMap import Data.IORef import Data.List qualified as List import Data.List.NonEmpty qualified as NonEmpty -import Data.Set qualified as Set import Data.Text qualified as Text -import Data.Vector qualified as Vector import Data.Word (Word8, Word16) import Database.SQLite.Simple qualified as SQLite import System.Directory qualified as Directory @@ -89,6 +71,8 @@ unitTests = testGroup "Source resolution" , testCase "reserves the all-ones file identifier" preservesReservedFileId , testCase "builds an imported-before-importer source graph" buildsSourceGraph + , testCase "rejects the packaged prelude as ordinary source" + rejectsPackagedPreludeAsOrdinarySource , testCase "orders sibling imports by textual occurrence" ordersSiblingImports , testCase "orders shared dependencies before their importers" @@ -114,20 +98,6 @@ unitTests = testGroup "Source resolution" , testCase "rejects a corrupted cached declaration anchor" rejectsCorruptedCachedDeclarationAnchor , testCase "parses source-local blocks in graph order" parsesSourceGraph - , testCase "assigns and reserves dense legacy module positions" - reservesLegacyModulePositions - , testCase "admits complete legacy declaration batches" - admitsLegacyDeclarations - , testCase "publishes deterministic legacy import views" - publishesLegacyImportViews - , testCase "publishes typed signatures and facts through transition modules" - publishesTransitionSignatures - , testCase "rejects cached global types from another builder" - rejectsForeignCachedGlobalType - , testCase "authorizes exact typed Vampire requests" - authorizesTypedVampireRequests - , testCase "enforces and replays direct inductive guards" - publishesTypedInductive , testCase "does not leak syntax between sibling imports" rejectsSiblingSyntaxLeakage , testCase "parses source fixity levels and grouping" @@ -154,10 +124,8 @@ unitTests = testGroup "Source resolution" reportsMalformedLexicalDeclaration , testCase "validates inductive function patterns during scanning" rejectsMalformedInductivePattern - , testCase "scans, parses, and checks adjective signatures" + , testCase "scans and parses adjective signatures" acceptsAdjectiveSignature - , testCase "rejects unresolved quantified symbolic-signature terms" - rejectsQuantifiedSymbolicSignatureTerm , testCase "rejects malformed math-led signature heads" rejectsMalformedSignatureHead , testCase "locates conflicting declarations within one environment" @@ -166,8 +134,6 @@ unitTests = testGroup "Source resolution" acceptsBuiltinSourceDeclaration , testCase "keeps the built-in marker for a prefix predicate declaration" acceptsBuiltinPrefixPredicateDeclaration - , testCase "rejects duplicate fixed-base semantics during checking" - rejectsDuplicateFixedBaseSemantics , testCase "does not rescan repeated canonical imports" avoidsAliasImportLexiconCollision , testCase "parses loaded sources without rereading files" parsesWithoutRereading @@ -275,6 +241,47 @@ rootFormsShareIdentity = (resolvedSourceRelativePath (loadedSource searchedLoaded)) (resolvedSourceRelativePath (loadedSource exactLoaded)) +rejectsPackagedPreludeAsOrdinarySource :: Assertion +rejectsPackagedPreludeAsOrdinarySource = do + packaged <- expectRight =<< Prelude.loadReservedPreludeSourceInput + canonical <- expectJust "packaged canonical path" + (Prelude.reservedPreludeSourceCanonicalPath packaged) + let path = canonicalPathFilePath canonical + mounts <- oneMount "packaged" (Posix.takeDirectory path) + request <- expectRight (searchedRoot (Posix.takeFileName path)) + let validate = Prelude.rejectOrdinaryPreludeSourceGraph packaged + syntaxInputs = const [] + Parse.parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation + mounts request syntaxInputs validate >>= \case + Left + (Parse.SourceWorkspaceError + (PackagedPreludeSelectedAsOrdinarySource source)) -> + assertEqual "authority-free rejected path" + canonical + (resolvedSourceCanonicalPath source) + other -> + assertFailure + ("unexpected authority-free result: " <> show other) + + withTemporaryDirectory "felix-reserved-parse-store" \temp -> do + foundation <- expectRight Foundation.checkedFoundation + store <- openTestStore + (temp Posix.</> "store.sqlite") + (Identity.theoryId foundation) + Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation + store mounts request syntaxInputs validate >>= \case + Left + (Parse.ParseExecutionWorkspaceError + (Parse.SourceWorkspaceError + (PackagedPreludeSelectedAsOrdinarySource source))) -> + assertEqual "typed rejected path" + canonical + (resolvedSourceCanonicalPath source) + other -> + assertFailure + ("unexpected typed result: " <> show other) + Store.closeStore store + attributesNestedSources :: Assertion attributesNestedSources = withTemporaryDirectory "felix-source-nested-mount" \temp -> do @@ -682,46 +689,6 @@ buildsEmptyModules = (Parse.parsedModuleSyntaxInterface (Parse.parsedWorkspaceRootModule workspace))))) - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - assignment <- - case toList assignments of - [only] -> - pure only - actual -> - assertFailure - ("expected one empty module assignment, got " - <> show (length actual)) - >> fail "unreachable" - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - builder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - []) - checked <- - Checking.runCheckingBlocks - [] - (Checking.initialTransitionCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - builder - (\_batch -> - assertFailure - "empty module emitted an obligation")) - finalBuilder <- - expectJust - "empty transition builder" - (Checking.checkingTransitionModuleBuilder checked) - void - (expectRight - (Transition.sealTransitionModule - (Checking.checkingStateEnvironment checked) - finalBuilder)) identifiesOwnerIndependentParsedModules :: Assertion identifiesOwnerIndependentParsedModules = @@ -1235,1613 +1202,6 @@ parsesSourceGraph = ["shared.tex", "entry.tex"] emitted -reservesLegacyModulePositions :: Assertion -reservesLegacyModulePositions = - withTemporaryDirectory "felix-legacy-module-stage" \temp -> do - writeTheory (temp Posix.</> "shared.tex") [] "shared" - writeTheory - (temp Posix.</> "entry.tex") - ["shared.tex"] - "entry" - graph <- buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - assertEqual "dense imported-first module ordinals" - [0, 1] - ( Legacy.legacyModuleOrdinalValue - . Legacy.assignedLegacyModuleOrdinal - <$> toList assignments - ) - assertEqual "assigned source order" - ["shared.tex", "entry.tex"] - ( safeRelativePathFilePath - . sourceAddressRelativePath - . Parse.parsedModuleAddress - . Legacy.assignedParsedModule - <$> toList assignments - ) - - let firstAssignment :| _remainingAssignments = - assignments - stage = - Legacy.openLegacyModuleStage - firstAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - origin = Facts.factOrigin (Location 0) "declaration" - firstFact = - Facts.stageFact - ("first" :| ["first_alias"]) - origin - (Facts.prepareSemanticFact Top) - secondFact = - Facts.stageFact - ("second" :| []) - origin - (Facts.prepareSemanticFact Bottom) - reservation <- - expectRight - (Legacy.reserveLegacyDeclaration - (firstFact :| [secondFact]) - stage) - assertEqual "dense local fact ordinals" - [0, 1] - ( Legacy.legacyLocalFactOrdinalValue - . Legacy.legacyFactLocalOrdinal - . Legacy.legacyReservedFactReference - <$> toList (Legacy.legacyReservedFacts reservation) - ) - - let duplicateAliasFact = - Facts.stageFact - ("first_alias" :| []) - origin - (Facts.prepareSemanticFact Bottom) - case Legacy.reserveLegacyDeclaration - (firstFact :| [duplicateAliasFact]) - stage of - Left Legacy.LegacyAliasAlreadyBound{} -> - pure () - Left err -> - assertFailure - ("expected alias rejection, got " <> show err) - Right _ -> - assertFailure "expected duplicate legacy alias rejection" - -admitsLegacyDeclarations :: Assertion -admitsLegacyDeclarations = - withTemporaryDirectory "felix-legacy-admission" \temp -> do - writeTheory (temp Posix.</> "entry.tex") [] "entry" - graph <- buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignment :| _ <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - let stage = - Legacy.openLegacyModuleStage - assignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - blocks = - [ BlockAxiom - Nowhere - "declared" - (Axiom [] Top) - , BlockLemma - Nowhere - "omitted" - (Lemma [] Bottom) - , BlockProof - Nowhere - Nowhere - (Omitted Nowhere) - ] - resolveGapBatch batch = do - resolved <- - traverse - (either - (ioError . userError . show) - pure - . Obligation.resolveObligationAsGap) - (Obligation.preparedBatchObligations batch) - either - (ioError . userError . show) - pure - (Obligation.resolveObligationBatch - batch - resolved) - initial = - Checking.initialLegacyCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - stage - resolveGapBatch - checked <- - Checking.runCheckingBlocks blocks initial - admittedStage <- - maybe - (assertFailure - "authoritative checking lost the legacy stage" - >> pure stage) - pure - (Checking.checkingLegacyModuleStage checked) - admittedModule <- - expectRight - (Legacy.sealLegacyModuleStage - (Checking.checkingStateEnvironment checked) - admittedStage) - assertEqual "two sealed local facts" - 2 - (Vector.length - (Legacy.legacyAdmittedLocalFacts admittedModule)) - assertEqual "one sealed declared assumption" - 1 - (Vector.length - (Legacy.legacyAdmittedDirectAxiomManifest - admittedModule)) - let finalTrust = - Legacy.legacyFactEntryTrustDependencies - (Vector.last - (Legacy.legacyAdmittedLocalFacts - admittedModule)) - assertEqual "one explicit gap" - 1 - (Set.size - (Legacy.legacyExplicitGaps finalTrust)) - assertEqual "direct gap needs no legacy finalization rule" - 0 - (Set.size - (Legacy.trustedLegacyRuleUses finalTrust)) - -publishesTransitionSignatures :: Assertion -publishesTransitionSignatures = - withTemporaryDirectory "felix-transition-signatures" \temp -> do - writeTheory (temp Posix.</> "shared.tex") [] "shared" - writeTheory - (temp Posix.</> "entry.tex") - ["shared.tex"] - "entry" - graph <- buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - case toList assignments of - [sharedAssignment, entryAssignment] -> do - shared <- - admit - checkedFoundationValue - sharedAssignment - [] - [ BlockSig - Nowhere - "shared_signature" - [] - (SignaturePredicate - sharedPredicate - ("x" :| [])) - , BlockAxiom - Nowhere - "shared_atomic_axiom" - (Axiom [] sharedAtomicFormula) - ] - let sharedGlobals = - Transition.transitionAdmittedGlobals - shared - assertEqual - "one shared typed declaration" - 1 - (Vector.length sharedGlobals) - case Vector.toList sharedGlobals of - [(symbol, reference, _origin)] -> do - assertEqual - "shared symbol" - (SymbolPredicate sharedPredicate) - symbol - assertEqual - "shared declaration ordinal" - 0 - (Transition.localDeclarationOrdinalValue - (Transition.opaqueDeclarationOrdinal - (Transition.checkedGlobalReference - reference))) - assertEqual - "shared predicate type" - (Core.TySet - `Core.TyArrow` - Core.TyProp) - (Transition.checkedGlobalType reference) - _ -> - assertFailure - "expected one shared typed declaration" - let sharedFacts = - Vector.toList - (Transition.transitionAdmittedFacts - shared) - sharedManifest = - Vector.toList - (Transition.transitionAdmittedTypedDirectAxiomManifest - shared) - (sharedReference, sharedStatement) <- - case (sharedFacts, sharedManifest) of - ([assumption], [manifestEntry]) -> do - assertBool - "typed axiom is not a kernel proof" - (not - (Transition.admittedFactIsKernelProof - assumption)) - assertEqual - "manifest kind" - Legacy.DeclaredUserAxiom - (Transition.typedDirectAssumptionKind - manifestEntry) - assertEqual - "manifest fact reference" - (Just - (Transition.typedDirectAssumptionFact - manifestEntry)) - (Transition.transitionTypedFactReference - (Transition.admittedFactReference - assumption)) - pure - ( Transition.admittedFactReference - assumption - , Transition.typedDirectAssumptionStatement - manifestEntry - ) - _ -> - fail - "expected one manifest-backed typed axiom" - - hiddenBuilder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - entryAssignment - []) - hiddenTarget <- - expectRight - (Core.checkCanonicalCore - (const Nothing) - (Core.CImp - Core.CFalsum - Core.CFalsum)) - hiddenImport <- - expectRight - (Transition.transitionDerivationImport - sharedReference - hiddenTarget) - case Transition.commitTransitionKernelFactWithImports - ("hidden_import" :| []) - (Transition.origin - Nowhere - Nothing - (Just "hidden_import")) - (Vector.singleton hiddenImport) - hiddenTarget - (Derivation.importedFactDerivation - (Derivation.importIx 0)) - hiddenBuilder of - Left - (Transition.TransitionKernelImportNotVisible - actualReference) -> - assertEqual - "unimported fact reference" - sharedReference - actualReference - Left err -> - assertFailure - ("expected hidden typed import failure, got " - <> show err) - Right _ -> - assertFailure - "an unimported typed row authorized replay" - - entryBuilder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - entryAssignment - [shared]) - assertBool - "direct import exposes the typed global" - (isJust - (Transition.lookupTransitionGlobal - (SymbolPredicate sharedPredicate) - entryBuilder)) - entry <- - admitWithBuilder - entryBuilder - [ BlockAxiom - Nowhere - "legacy_axiom" - (Axiom [] Top) - , BlockSig - Nowhere - "entry_signature" - [] - (SignaturePredicate - entryPredicate - ("z" :| [])) - , BlockLemma - Nowhere - "typed_import_reuse" - (Lemma [] sharedAtomicFormula) - , BlockLemma - Nowhere - "typed_reflexivity" - (Lemma - [] - (Equals - Nowhere - (EmptySet Nowhere) - (EmptySet Nowhere))) - ] - case Vector.toList - (Transition.transitionAdmittedGlobals - entry) of - [(_symbol, reference, _origin)] -> - assertEqual - "legacy declaration occupies its source ordinal" - 1 - (Transition.localDeclarationOrdinalValue - (Transition.opaqueDeclarationOrdinal - (Transition.checkedGlobalReference - reference))) - _ -> - assertFailure - "expected one local entry declaration" - let facts = - Vector.toList - (Transition.transitionAdmittedFacts - entry) - assertEqual - "imported and local rows retain declaration order" - [False, False, True, True] - (Transition.admittedFactIsKernelProof - <$> facts) - case facts of - [_assumption, _legacy, reused, reflexivity] -> do - case Transition.transitionTypedFactReference - (Transition.admittedFactReference - reused) of - Nothing -> - assertFailure - "expected a typed fact reference" - Just reference -> - assertEqual - "first typed fact ordinal" - 0 - (Transition.localFactOrdinalValue - (Transition.factReferenceOrdinal - reference)) - case Transition.transitionTypedFactReference - (Transition.admittedFactReference - reflexivity) of - Nothing -> - assertFailure - "expected a typed reflexivity reference" - Just reference -> - assertEqual - "second typed fact ordinal" - 1 - (Transition.localFactOrdinalValue - (Transition.factReferenceOrdinal - reference)) - _ -> - assertFailure - "expected imported assumption and three local facts" - let inheritedAssumptions = - Set.toList - (Transition.typedDeclaredAssumptionUses - (Transition.transitionAdmittedTypedTrustDependencies - entry)) - case inheritedAssumptions of - [assumption] -> do - assertEqual - "the importer retains the owner fact" - (Transition.transitionTypedFactReference - sharedReference) - (Just - (Transition.sessionTypedAssumptionFact - assumption)) - assertEqual - "the owner assumption ordinal" - 0 - (Transition.localAssumptionOrdinalValue - (Transition.sessionTypedAssumptionOrdinal - assumption)) - assertEqual - "the imported assumption statement" - sharedStatement - (Transition.sessionTypedAssumptionStatement - assumption) - _ -> - assertFailure - "expected one inherited typed declared assumption" - assertEqual - "two local replayed kernel proofs" - 2 - (Transition.transitionAdmittedKernelProofCount - entry) - actual -> - assertFailure - ("expected two module assignments, got " - <> show (length actual)) - where - sharedPredicate = - PredicateSymbol "typed_shared_predicate" - entryPredicate = - PredicateSymbol "typed_entry_predicate" - sharedAtomicFormula = - Atomic - Nowhere - sharedPredicate - [EmptySet Nowhere] - - admit checkedFoundationValue assignment imports blocks = do - builder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - imports) - admitWithBuilder builder blocks - - admitWithBuilder builder blocks = do - checked <- - Checking.runCheckingBlocks - blocks - (Checking.initialTransitionCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - builder - (\_batch -> - assertFailure - "typed transition emitted an obligation")) - finalBuilder <- - maybe - (assertFailure - "checking lost its transition builder") - pure - (Checking.checkingTransitionModuleBuilder - checked) - expectRight - (Transition.sealTransitionModule - (Checking.checkingStateEnvironment checked) - finalBuilder) - -rejectsForeignCachedGlobalType :: Assertion -rejectsForeignCachedGlobalType = - withTemporaryDirectory "felix-transition-global-types" \temp -> do - writeTheory - (temp Posix.</> "entry.tex") - [] - "entry" - graph <- - buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - assignment <- - case toList assignments of - [only] -> - pure only - actual -> - assertFailure - ("expected one module assignment, got " - <> show (length actual)) - >> fail "unreachable" - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - builderA0 <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - []) - builderB0 <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - []) - let symbol = - SymbolPredicate - (PredicateSymbol - "same_nominal_global") - declarationOrigin = - Transition.origin - Nowhere - Nothing - (Just "same_nominal_global") - builderA <- - expectRight - (Transition.commitTransitionOpaqueGlobal - symbol - Core.TySet - declarationOrigin - (Transition.beginTransitionDeclaration - builderA0)) - builderB <- - expectRight - (Transition.commitTransitionOpaqueGlobal - symbol - Core.TyProp - declarationOrigin - (Transition.beginTransitionDeclaration - builderB0)) - globalA <- - maybe - (assertFailure "builder A lost its global" - >> fail "unreachable") - pure - (Transition.lookupTransitionGlobal - symbol - builderA) - globalB <- - maybe - (assertFailure "builder B lost its global" - >> fail "unreachable") - pure - (Transition.lookupTransitionGlobal - symbol - builderB) - operand <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - (Core.CGlobal globalA)) - statement <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - (Core.CEq - Core.TySet - (Core.CGlobal globalA) - (Core.CGlobal globalA))) - case Transition.commitTransitionKernelFact - ("foreign_global_type" :| []) - (Transition.origin - Nowhere - Nothing - (Just "foreign_global_type")) - statement - (Derivation.equalityReflexivityDerivation - operand) - (Transition.beginTransitionDeclaration - builderB) of - Left - (Transition.TransitionGlobalReferenceTypeMismatch - actual - authoritativeType) -> do - assertEqual - "cached global reference" - globalA - actual - assertEqual - "builder B authoritative type" - Core.TyProp - authoritativeType - Left err -> - assertFailure - ("expected cached global type rejection, got " - <> show err) - Right _ -> - assertFailure - "builder B admitted builder A's cached type" - let remappedOperand = - Core.mapFrozenGlobals - (const globalB) - operand - remappedStatement = - Core.mapFrozenGlobals - (const globalB) - statement - case Transition.commitTransitionKernelFact - ("stale_term_annotation" :| []) - (Transition.origin - Nowhere - Nothing - (Just "stale_term_annotation")) - remappedStatement - (Derivation.equalityReflexivityDerivation - remappedOperand) - (Transition.beginTransitionDeclaration - builderB) of - Left - (Transition.TransitionCoreCheckError - (Core.EqualityOperandTypeMismatch - Core.TySet - Core.TyProp)) -> - pure () - Left err -> - assertFailure - ("expected fresh builder-relative core check, got " - <> show err) - Right _ -> - assertFailure - "builder B admitted a stale term annotation" - -authorizesTypedVampireRequests :: Assertion -authorizesTypedVampireRequests = - withTemporaryDirectory "felix-typed-vampire" \temp -> do - let sourcePath = - temp Posix.</> "entry.tex" - executablePath = - temp Posix.</> "vampire" - writeTheory sourcePath [] "entry" - graph <- - buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals - workspace) - assignment <- - case toList assignments of - [only] -> - pure only - actual -> - assertFailure - ("expected one module assignment, got " - <> show (length actual)) - >> fail "unreachable" - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - baseBuilder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - []) - let legacyStage = - Transition.transitionBuilderLegacyStage - baseBuilder - legacyStaged = - Facts.stageFact - ("legacy_input" :| []) - (Facts.factOrigin - (Location 0) - "legacy_input") - (Facts.prepareSemanticFact Top) - legacyReservation <- - expectRight - (Legacy.reserveLegacyDeclaration - (legacyStaged :| []) - legacyStage) - let legacyReserved = - NonEmpty.head - (Legacy.legacyReservedFacts - legacyReservation) - legacyAdmitted = - Legacy.authorizeLegacyDeclaredAssumption - legacyStage - Legacy.DeclaredUserAxiom - legacyReserved - legacyStage' <- - expectRight - (Legacy.appendEstablishedLegacyDeclaration - legacyReservation - (legacyAdmitted :| []) - legacyStage) - builderWithLegacy <- - expectRight - (Transition.transitionBuilderWithLegacyStage - legacyStage' - baseBuilder) - target <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - (Core.CImp - Core.CFalsum - Core.CFalsum)) - claim <- - expectRight - (Backend.supportedProposition - (Vector.empty - :: Vector.Vector - (Void, Core.CoreType)) - (Core.embedClosedCore [] target)) - builderWithFof <- - expectRight - (Transition.commitTransitionTypedDeclaredAssumption - ("fof_input" :| []) - (Transition.origin - Nowhere - Nothing - (Just "fof_input")) - Legacy.DeclaredUserAxiom - target - (Transition.beginTransitionDeclaration - builderWithLegacy)) - let higherOrderTarget = - Core.mapFrozenGlobals - absurd - (Foundation.foundationAxiomFrozen - checkedFoundationValue - Foundation.DoubleNegationElim) - builderWithTh0 <- - expectRight - (Transition.commitTransitionTypedDeclaredAssumption - ("th0_input" :| []) - (Transition.origin - Nowhere - Nothing - (Just "th0_input")) - Legacy.DeclaredUserAxiom - higherOrderTarget - (Transition.beginTransitionDeclaration - builderWithFof)) - builder <- - expectRight - (Transition.commitTransitionTypedDeclaredAssumption - ("second_fof_input" :| []) - (Transition.origin - Nowhere - Nothing - (Just "second_fof_input")) - Legacy.DeclaredUserAxiom - target - (Transition.beginTransitionDeclaration - builderWithTh0)) - implicitProblem <- - expectRight - (Transition.planTransitionTypedProblem - builder - claim - [] - [] - Transition.ImplicitFofFacts - Backend.FirstOrderLocals) - let selected = - Vector.toList - (Backend.typedProblemGlobalPremises - implicitProblem) - references <- - traverse - ( maybe - (assertFailure - "implicit planning selected a legacy row" - >> fail "unreachable") - pure - . Transition.transitionTypedFactReference - . Backend.typedBackendFactReference - ) - selected - assertEqual - "implicit planning preserves FOF admission order" - [0, 2] - ( Transition.localFactOrdinalValue - . Transition.factReferenceOrdinal - <$> references - ) - assertEqual - "implicit admitted-fact route" - Backend.RouteFof - (Backend.typedProblemRoute - implicitProblem) - explicitHigherOrder <- - expectRight - (Transition.planTransitionTypedProblem - builder - claim - [] - [] - (Transition.ExplicitFacts - ("th0_input" :| ["th0_input"])) - Backend.FirstOrderLocals) - assertEqual - "explicit higher-order admitted fact selects TH0" - Backend.RouteTh0 - (Backend.typedProblemRoute - explicitHigherOrder) - assertEqual - "repeated explicit aliases select one fact" - 1 - (Vector.length - (Backend.typedProblemGlobalPremises - explicitHigherOrder)) - case Transition.planTransitionTypedProblem - builder - claim - [] - [] - (Transition.ExplicitFacts - ("legacy_input" :| [])) - Backend.FirstOrderLocals of - Left - (Transition.TransitionTypedProblemDependencyNotMigrated - reference) -> - assertEqual - "legacy dependency stays legacy" - Nothing - (Transition.transitionTypedFactReference - reference) - result' -> - assertFailure - ("expected legacy dependency rejection, got " - <> case result' of - Left err -> - "Left " <> show err - Right _problem -> - "Right problem") - problem <- - expectRight - (Transition.planTransitionTypedProblem - builder - claim - [] - [Backend.typedFoundationAuxiliaryInput - checkedFoundationValue - Foundation.DoubleNegationElim] - Transition.NoGlobalFacts - Backend.AllLocals) - prepared <- - expectRight - (Provers.prepareTypedProverTask - Provers.DirectTask - problem) - mismatched <- - expectRight - (Provers.prepareTypedProverTask - Provers.IndirectTask - problem) - assertEqual - "higher-order foundation input selects TH0" - Provers.VerificationTh0 - (Provers.preparedVerificationDialect - (Provers.preparedTypedProverRequest - prepared)) - writeFile executablePath - (unlines - [ "#!/bin/sh" - , "cat >/dev/null" - , "printf '%s\\n' '% SZS status Theorem for typed'" - ]) - permissions <- - Directory.getPermissions executablePath - Directory.setPermissions executablePath - (Directory.setOwnerExecutable - True - permissions) - result <- - runNoLoggingT - (Provers.runPreparedTypedProver - (Provers.vampire - executablePath - Provers.defaultTimeLimit - Provers.defaultMemoryLimit) - prepared) - accepted <- - case result of - Right answer - | Just run <- - Provers.provedVampireRun answer -> - pure run - _ -> - assertFailure - ("expected accepted typed Vampire run, got " - <> show result) - >> fail "unreachable" - let factOrigin = - Transition.origin - Nowhere - Nothing - (Just "typed_vampire") - commit task = - Transition.commitTransitionTypedVampireFact - Reconstruction.defaultReconstructionPolicy - ("typed_vampire" :| []) - factOrigin - target - task - accepted - builder - case commit mismatched of - Left Transition.TransitionTypedVampireRequestMismatch -> - pure () - result' -> - assertFailure - ("expected exact-request mismatch, got " - <> showResult result') - committed <- - expectRight (commit prepared) - admitted <- - expectRight - (Transition.sealTransitionModule - Checking.initialLegacyCheckingEnvironment - committed) - let trust = - Transition.transitionAdmittedTypedTrustDependencies - admitted - assertEqual - "one typed trusted Vampire row" - 1 - (Transition.transitionAdmittedTypedTrustedVampireCount - admitted) - assertEqual - "one typed Vampire trust occurrence" - 1 - (Set.size - (Transition.typedTrustedVampireUses - trust)) - assertEqual - "mandatory lowering assumptions" - Legacy.mandatoryVampireLoweringAssumptions - (Transition.typedVampireLoweringUses - trust) - assertEqual - "exact foundation input" - (Set.singleton - Foundation.DoubleNegationElim) - (Transition.typedFoundationUses - trust) - let atom argument = - Core.CApp - (Core.CApp - (Core.CIntrinsic Core.Member) - (Core.CIntrinsic Core.Empty)) - argument - atomP = - atom (Core.CIntrinsic Core.Empty) - atomQ = - atom (Core.COpaqueInteger 1) - atomR = - atom (Core.COpaqueInteger 2) - declareTyped alias statement current = - expectRight - (Transition.commitTransitionTypedDeclaredAssumption - (alias :| []) - (Transition.origin - Nowhere - Nothing - (Just alias)) - Legacy.DeclaredUserAxiom - statement - (Transition.beginTransitionDeclaration - current)) - premiseP <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - atomP) - premisePtoQ <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - (Core.CImp atomP atomQ)) - premiseQtoR <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - (Core.CImp atomQ atomR)) - reconstructedTarget <- - expectRight - (Core.checkCanonicalCore - (Just . Transition.checkedGlobalType) - atomR) - builderWithP <- - declareTyped - "horn_p" - premiseP - builder - builderWithPtoQ <- - declareTyped - "horn_p_to_q" - premisePtoQ - builderWithP - builderWithHornInputs <- - declareTyped - "horn_q_to_r" - premiseQtoR - builderWithPtoQ - reconstructedClaim <- - expectRight - (Backend.supportedProposition - (Vector.empty - :: Vector.Vector - (Void, Core.CoreType)) - (Core.embedClosedCore - [] - reconstructedTarget)) - reconstructedProblem <- - expectRight - (Transition.planTransitionTypedProblem - builderWithHornInputs - reconstructedClaim - [] - [] - (Transition.ExplicitFacts - ("horn_p" - :| [ "horn_p_to_q" - , "horn_q_to_r" - ])) - Backend.FirstOrderLocals) - reconstructedPrepared <- - expectRight - (Provers.prepareTypedProverTask - Provers.DirectTask - reconstructedProblem) - reconstructedResult <- - runNoLoggingT - (Provers.runPreparedTypedProver - (Provers.vampire - executablePath - Provers.defaultTimeLimit - Provers.defaultMemoryLimit) - reconstructedPrepared) - reconstructedAccepted <- - case reconstructedResult of - Right answer - | Just run <- - Provers.provedVampireRun answer -> - pure run - _ -> - assertFailure - ("expected accepted Horn Vampire run, got " - <> show reconstructedResult) - >> fail "unreachable" - reconstructedBuilder <- - expectRight - (Transition.commitTransitionTypedVampireFact - Reconstruction.defaultReconstructionPolicy - ("horn_result" :| []) - (Transition.origin - Nowhere - Nothing - (Just "horn_result")) - reconstructedTarget - reconstructedPrepared - reconstructedAccepted - builderWithHornInputs) - reconstructedModule <- - expectRight - (Transition.sealTransitionModule - Checking.initialLegacyCheckingEnvironment - reconstructedBuilder) - reconstructedFact <- - case Vector.unsnoc - (Transition.transitionAdmittedFacts - reconstructedModule) of - Just (_earlier, finalFact) -> - pure finalFact - Nothing -> - assertFailure - "expected a reconstructed admitted fact" - >> fail "unreachable" - assertBool - "supported accepted task becomes a reconstructed kernel proof" - (Transition.admittedFactIsReconstructedKernelProof - reconstructedFact) - reconstructedTrust <- - maybe - (assertFailure - "expected typed reconstructed trust") - pure - (Transition.admittedFactTypedTrustDependencies - reconstructedFact) - assertEqual - "reconstruction inherits its three exact assumptions" - 3 - (Set.size - (Transition.typedDeclaredAssumptionUses - reconstructedTrust)) - assertEqual - "reconstructed run adds no trusted Vampire leaf" - Set.empty - (Transition.typedTrustedVampireUses - reconstructedTrust) - assertEqual - "reconstructed run adds no Vampire lowering trust" - Set.empty - (Transition.typedVampireLoweringUses - reconstructedTrust) - tinyKernelLimits <- - expectRight - (Derivation.kernelReplayLimits 1 10) - let tinyKernelPolicy = - Reconstruction.reconstructionPolicy - (Reconstruction.reconstructionPolicyConnectionLimits - Reconstruction.defaultReconstructionPolicy) - tinyKernelLimits - fallbackBuilder <- - expectRight - (Transition.commitTransitionTypedVampireFact - tinyKernelPolicy - ("horn_fallback" :| []) - (Transition.origin - Nowhere - Nothing - (Just "horn_fallback")) - reconstructedTarget - reconstructedPrepared - reconstructedAccepted - builderWithHornInputs) - fallbackModule <- - expectRight - (Transition.sealTransitionModule - Checking.initialLegacyCheckingEnvironment - fallbackBuilder) - fallbackFact <- - case Vector.unsnoc - (Transition.transitionAdmittedFacts - fallbackModule) of - Just (_earlier, finalFact) -> - pure finalFact - Nothing -> - assertFailure - "expected a kernel-exhaustion fallback fact" - >> fail "unreachable" - assertBool - "kernel exhaustion retains accepted Vampire authority" - (Transition.admittedFactIsTrustedVampire - fallbackFact) - where - showResult = \case - Left err -> - "Left " <> show err - Right _builder -> - "Right builder" - -publishesTypedInductive :: Assertion -publishesTypedInductive = - withTemporaryDirectory "felix-transition-inductive" \temp -> do - writeTheory - (temp Posix.</> "entry.tex") - [] - "entry" - graph <- buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals - workspace) - assignment <- - case toList assignments of - [only] -> - pure only - actual -> - assertFailure - ("expected one module assignment, got " - <> show (length actual)) - >> fail "unreachable" - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - builder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - assignment - []) - let unprovedCarrier = - TermOp Nowhere unprovedInductiveSymbol [] - unprovedBlocks = - [ BlockInductive - Nowhere - "unproved_inductive" - Inductive - { inductiveSymbol = - unprovedInductiveSymbol - , inductiveParams = [] - , inductiveDomain = - EmptySet Nowhere - , inductiveIntros = - IntroRule - [] - ( EmptySet Nowhere - `isElementOf` - unprovedCarrier - ) - :| [] - } - ] - unproved <- - try - (Checking.runCheckingBlocks - unprovedBlocks - (Checking.initialTransitionCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - builder - (\_batch -> - assertFailure - "unproved inductive emitted a legacy obligation"))) - :: IO - (Either - Checking.CheckingError - Checking.CheckingState) - case unproved of - Left checkingError -> - assertBool - "missing exact guard is reported" - ("has no authorized typed fact" - `Text.isInfixOf` - Text.pack (show checkingError)) - Right _checked -> - assertFailure - "inductive with an unproved domain guard was admitted" - unchanged <- - expectRight - (Transition.sealTransitionModule - Checking.initialLegacyCheckingEnvironment - builder) - assertEqual - "failed inductive publishes no global" - 0 - (Vector.length - (Transition.transitionAdmittedGlobals - unchanged)) - assertEqual - "failed inductive publishes no fact" - 0 - (Vector.length - (Transition.transitionAdmittedFacts - unchanged)) - let parameter = - NamedVar "domain" - domain = - TermOp - Nowhere - cumulSymbol - [TermVar parameter] - carrier = - TermOp - Nowhere - typedInductiveSymbol - [TermVar parameter] - blocks = - [ BlockInductive - Nowhere - "typed_inductive" - Inductive - { inductiveSymbol = - typedInductiveSymbol - , inductiveParams = [parameter] - , inductiveDomain = domain - , inductiveIntros = - IntroRule - [] - (TermVar parameter - `isElementOf` - carrier) - :| [] - } - ] - checked <- - Checking.runCheckingBlocks - blocks - (Checking.initialTransitionCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - builder - (\_batch -> - assertFailure - "typed inductive emitted a legacy obligation")) - finalBuilder <- - maybe - (assertFailure - "checking lost its transition builder" - >> fail "unreachable") - pure - (Checking.checkingTransitionModuleBuilder - checked) - admitted <- - expectRight - (Transition.sealTransitionModule - (Checking.checkingStateEnvironment - checked) - finalBuilder) - assertEqual - "one transparent carrier" - 1 - (Vector.length - (Transition.transitionAdmittedGlobals - admitted)) - assertEqual - "four derived facts" - [True, True, True, True] - ( Transition.admittedFactIsKernelProof - <$> Vector.toList - (Transition.transitionAdmittedFacts - admitted) - ) - assertEqual - "four replayed inductive facts" - 4 - (Transition.transitionAdmittedKernelProofCount - admitted) - assertBool - "foundation guard dependency is retained" - (Foundation.UnivOfContains - `Set.member` - Transition.typedFoundationUses - (Transition.transitionAdmittedTypedTrustDependencies - admitted)) - where - typedInductiveSymbol = - mkMixfixItem - [ Just (Command "typedfin") - , Just InvisibleBraceL - , Nothing - , Just InvisibleBraceR - ] - "typed_inductive" - NonAssoc - - cumulSymbol = - mkMixfixItem - [ Just (Command "cumul") - , Just InvisibleBraceL - , Nothing - , Just InvisibleBraceR - ] - "cumul" - NonAssoc - - unprovedInductiveSymbol = - mkMixfixItem - [Just (Command "unprovedfin")] - "unproved_inductive" - NonAssoc - -publishesLegacyImportViews :: Assertion -publishesLegacyImportViews = - withTemporaryDirectory "felix-legacy-import-view" \temp -> do - writeTheory (temp Posix.</> "shared.tex") [] "shared" - writeTheory - (temp Posix.</> "a.tex") - ["shared.tex"] - "a" - writeTheory - (temp Posix.</> "b.tex") - ["shared.tex"] - "b" - writeTheory - (temp Posix.</> "entry.tex") - ["a.tex", "b.tex"] - "entry" - graph <- buildSearchedGraph temp "entry.tex" - workspace <- - expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - case toList assignments of - [ sharedAssignment - , aAssignment - , bAssignment - , entryAssignment - ] -> do - shared <- - admitOne - sharedAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - "shared_fact" - Bottom - (Location 1) - sharedView <- - expectRight - (Legacy.legacyImportedView - Checking.initialLegacyCheckingEnvironment - [shared]) - a <- - admitOne - aAssignment - sharedView - "a_fact" - Top - (Location 2) - b <- - admitOne - bAssignment - sharedView - "b_fact" - Top - (Location 3) - diamondView <- - expectRight - (Legacy.legacyImportedView - Checking.initialLegacyCheckingEnvironment - [a, b]) - entry <- - expectRight - (Legacy.sealLegacyModuleStage - (Legacy.legacyImportedCheckingEnvironment - diamondView) - (Legacy.openLegacyModuleStage - entryAssignment - diamondView)) - assertEqual - "direct imports retain textual order" - [1, 2] - ( Legacy.legacyModuleOrdinalValue - <$> Vector.toList - (Legacy.legacyAdmittedDirectImports - entry) - ) - assertEqual - "diamond facts retain imported source order" - [0, 1, 2] - ( Legacy.legacyModuleOrdinalValue - . Legacy.legacyFactModule - . Legacy.legacyFactEntryReference - <$> Vector.toList - (Legacy.legacyAdmittedVisibleFacts - entry) - ) - assertEqual - "equal statements at different references remain" - 3 - (Vector.length - (Legacy.legacyAdmittedVisibleFacts entry)) - let environmentSymbol = - SymbolMixfix - (mkMixfixItem - [Just - (Command - "module_environment")] - "module_environment" - NonAssoc) - environmentWith body = - Legacy.legacyCheckingEnvironment - (HashMap.insert - environmentSymbol - (toScope body) - (Legacy.legacyEnvironmentAbbreviations - Checking.initialLegacyCheckingEnvironment)) - (Legacy.legacyEnvironmentPredicateDefinitions - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentDependencies - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentOwnedSymbols - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentOwnedSymbolMarkers - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentFrozenSymbols - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentStructs - Checking.initialLegacyCheckingEnvironment) - (Legacy.legacyEnvironmentDefinedMarkers - Checking.initialLegacyCheckingEnvironment) - environmentA <- - admitEnvironment - aAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - (environmentWith Top) - environmentView <- - expectRight - (Legacy.legacyImportedView - Checking.initialLegacyCheckingEnvironment - [environmentA]) - assertEqual - "admitted semantic environment is imported" - (Just (toScope Top)) - (HashMap.lookup - environmentSymbol - (Legacy.legacyEnvironmentAbbreviations - (Legacy.legacyImportedCheckingEnvironment - environmentView))) - environmentB <- - admitEnvironment - bAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - (environmentWith Bottom) - case Legacy.legacyImportedView - Checking.initialLegacyCheckingEnvironment - [environmentA, environmentB] of - Left Legacy.LegacyImportedEnvironmentConflict{} -> - pure () - Left err -> - assertFailure - ("expected imported environment conflict, got " - <> show err) - Right _ -> - assertFailure - "expected imported environment conflict" - - conflictingA <- - admitOne - aAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - "conflicting" - Top - (Location 4) - conflictingB <- - admitOne - bAssignment - (Legacy.emptyLegacyImportedView - Checking.initialLegacyCheckingEnvironment) - "conflicting" - Bottom - (Location 5) - case Legacy.legacyImportedView - Checking.initialLegacyCheckingEnvironment - [conflictingA, conflictingB] of - Left Legacy.LegacyImportedAliasConflict{} -> - pure () - Left err -> - assertFailure - ("expected imported alias conflict, got " - <> show err) - Right _ -> - assertFailure - "expected imported alias conflict" - actual -> - assertFailure - ("expected four module assignments, got " - <> show (length actual)) - where - admitOne assignment imported alias statement location = do - let stage = - Legacy.openLegacyModuleStage - assignment - imported - staged = - Facts.stageFact - (alias :| []) - (Facts.factOrigin location alias) - (Facts.prepareSemanticFact statement) - reservation <- - expectRight - (Legacy.reserveLegacyDeclaration - (staged :| []) - stage) - let reserved = - NonEmpty.head - (Legacy.legacyReservedFacts reservation) - admitted = - Legacy.authorizeLegacyDeclaredAssumption - stage - Legacy.DeclaredUserAxiom - reserved - stage' <- - expectRight - (Legacy.appendEstablishedLegacyDeclaration - reservation - (admitted :| []) - stage) - expectRight - (Legacy.sealLegacyModuleStage - (Legacy.legacyImportedCheckingEnvironment imported) - stage') - - admitEnvironment assignment imported finalEnvironment = - expectRight - (Legacy.sealLegacyModuleStage - finalEnvironment - (Legacy.openLegacyModuleStage assignment imported)) - rejectsSiblingSyntaxLeakage :: Assertion rejectsSiblingSyntaxLeakage = withTemporaryDirectory "felix-source-syntax-world" \temp -> do @@ -3667,48 +2027,6 @@ acceptsAdjectiveSignature = _ -> assertFailure ("unexpected adjective-signature blocks: " <> show blocks) - semanticBlocks <- expectRight (Meaning.meaning blocks) - void - (Checking.check - Checking.WithoutDumpPremselTraining - semanticBlocks) - -rejectsQuantifiedSymbolicSignatureTerm :: Assertion -rejectsQuantifiedSymbolicSignatureTerm = - withTemporaryDirectory "felix-source-signature-quantified-term" \temp -> do - writeFile - (temp Posix.</> "entry.tex") - (unlines - [ "\\begin{definition}\\label{bridge}" - , " $z$ is a bridge from $A$ to $B$ iff $z = z$ and $A = A$ and $B = B$." - , "\\end{definition}" - , "\\begin{signature}\\label{bridge_signature}" - , " $\\foo{A}$ is a bridge from every set $x$ to $x$." - , "\\end{signature}" - ]) - graph <- buildSearchedGraph temp "entry.tex" - workspace <- expectRight - =<< Parse.parseResolvedSourceGraph graph - case Meaning.meaning - (Parse.importedBeforeImporterBlocks workspace) of - Left (Meaning.QuantifiedTermRequiresResolvedContext location) -> do - assertEqual "quantified term file" - "entry.tex" - (locFile location) - assertEqual "quantified term line" - 5 - (locLine location) - assertEqual "quantified term column" - 30 - (locColumn location) - Left err -> - assertFailure - ("expected quantified-term context error, got " - <> show err) - Right blocks -> - assertFailure - ("expected quantified-term context rejection, got " - <> show blocks) rejectsMalformedSignatureHead :: Assertion rejectsMalformedSignatureHead = do @@ -3902,162 +2220,6 @@ acceptsBuiltinPrefixPredicateDeclaration = ("unexpected built-in prefix declaration parse: " <> show blocks) -rejectsDuplicateFixedBaseSemantics :: Assertion -rejectsDuplicateFixedBaseSemantics = - withTemporaryDirectory "felix-source-builtin-collision" \temp -> do - writeBuiltinZeroDefinition - (temp Posix.</> "a.tex") - "source_zero_a" - writeFile - (temp Posix.</> "entry.tex") - ("\\import{a.tex}\n" - <> builtinZeroDefinition "source_zero_b") - graph <- buildSearchedGraph temp "entry.tex" - workspace <- expectRight - =<< Parse.parseResolvedSourceGraph graph - assignments <- - expectRight - (Legacy.assignLegacyModuleOrdinals workspace) - case toList assignments of - [acceptedAssignment, collidingAssignment] -> do - let acceptedParsed = - Legacy.assignedParsedModule acceptedAssignment - collidingParsed = - Legacy.assignedParsedModule collidingAssignment - acceptedLocation <- - onlySyntaxOccurrenceLocation acceptedParsed - collidingLocation <- - onlySyntaxOccurrenceLocation collidingParsed - assertLocation - "accepted declaration" - "a.tex" - 1 - acceptedLocation - assertLocation - "colliding declaration" - "entry.tex" - 2 - collidingLocation - assertEqual - "fixed reuses emit no syntax delta" - [[], []] - [ Interface.canonicalSyntaxDeltaEntries - (Interface.moduleSyntaxLocalDelta - (Parse.parsedModuleSyntaxInterface parsed)) - | parsed <- [acceptedParsed, collidingParsed] - ] - - checkedFoundationValue <- - expectRight Foundation.checkedFoundation - (acceptedBlocks, glossState) <- - glossParsedBlocks - Meaning.initialGlossState - acceptedParsed - acceptedBuilder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - acceptedAssignment - []) - acceptedState <- - Checking.runCheckingBlocks - acceptedBlocks - (checkingState acceptedBuilder) - finalAcceptedBuilder <- - expectJust - "accepted transition builder" - (Checking.checkingTransitionModuleBuilder - acceptedState) - acceptedModule <- - expectRight - (Transition.sealTransitionModule - (Checking.checkingStateEnvironment - acceptedState) - finalAcceptedBuilder) - - (collidingBlocks, _finalGlossState) <- - glossParsedBlocks glossState collidingParsed - collidingBuilder <- - expectRight - (Transition.openTransitionModuleBuilder - checkedFoundationValue - Checking.initialLegacyCheckingEnvironment - collidingAssignment - [acceptedModule]) - result <- - try - (Checking.runCheckingBlocks - collidingBlocks - (checkingState collidingBuilder)) - :: IO - (Either - Checking.CheckingError - Checking.CheckingState) - case result of - Left - (Checking.CheckingError - message - location - marker) -> do - assertEqual - "semantic collision location" - collidingLocation - location - assertEqual - "semantic collision marker" - "source_zero_b" - marker - assertBool - "accepted owner is identified" - ("already owned by abbreviation source_zero_a" - `Text.isInfixOf` message) - Left err -> - assertFailure - ("expected located ownership collision, got " - <> show err) - Right _checked -> - assertFailure - "duplicate fixed-base semantics were accepted" - actual -> - assertFailure - ("expected two module assignments, got " - <> show (length actual)) - where - checkingState builder = - Checking.initialTransitionCheckingStateWithTaskPreparation - Checking.WithoutDumpPremselTraining - id - builder - (\_batch -> - assertFailure - "fixed-base abbreviation emitted an obligation") - - glossParsedBlocks initialState parsed = - fmap - (\(reversed, finalState) -> - (reverse reversed, finalState)) - (foldM - glossOne - ([], initialState) - (Parse.parsedModuleBlocks parsed)) - - glossOne (reversed, state) raw = do - (block, nextState) <- - expectRight (Meaning.glossStep state raw) - pure (block : reversed, nextState) - - onlySyntaxOccurrenceLocation parsed = - case Parse.parsedModuleSyntaxOccurrences parsed of - [occurrence] -> - pure - (Parse.parsedSyntaxOccurrenceLocation - occurrence) - occurrences -> - assertFailure - ("expected one fixed-base occurrence, got " - <> show occurrences) - avoidsAliasImportLexiconCollision :: Assertion avoidsAliasImportLexiconCollision = withTemporaryDirectory "felix-source-alias-lexicon" \temp -> do |