diff options
| -rw-r--r-- | source/Checking/Exact.hs | 19 | ||||
| -rw-r--r-- | source/Checking/Module.hs | 52 | ||||
| -rw-r--r-- | source/Felix/Migration.hs | 5 | ||||
| -rw-r--r-- | source/Test/Unit/Module.hs | 400 | ||||
| -rw-r--r-- | test/phase5/exact-failure.tex | 7 | ||||
| -rw-r--r-- | test/phase5/exact-importer.tex | 5 | ||||
| -rw-r--r-- | test/phase5/exact-producer.tex | 12 |
7 files changed, 491 insertions, 9 deletions
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index ccb7665..b76e1c3 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -15,6 +15,7 @@ module Checking.Exact , prepareExactDeclaration , commitPreparedExactBinding , ExactCompileError(..) + , exactCompileErrorLocation , renderExactCompileError ) where @@ -128,6 +129,24 @@ data ExactCompileError | ExactObjectTypeMismatch !Location !CoreType !CoreType deriving stock (Show, Eq) +exactCompileErrorLocation :: ExactCompileError -> Location +exactCompileErrorLocation = \case + ExactUnsupportedDeclaration location -> location + ExactUnsupportedDeclarationBody location -> location + ExactDeclarationOccurrenceMissing location -> location + ExactDeclarationOccurrenceAmbiguous location -> location + ExactDeclarationHeadMismatch location -> location + ExactGlobalAlreadyVisible location _key -> location + ExactGlobalNotVisible location _key -> location + ExactDuplicateParameter location _parameter -> location + ExactFreeVariable location _variable -> location + ExactApplicationExpectedFunction location _actual -> location + ExactApplicationArgumentMismatch location _expected _actual -> location + ExactExpressionExpectedSet location _actual -> location + ExactFormulaExpectedProposition location _actual -> location + ExactCoreCheckFailed location _failure -> location + ExactObjectTypeMismatch location _expected _actual -> location + renderExactCompileError :: ExactCompileError -> Text renderExactCompileError = \case ExactUnsupportedDeclaration location -> diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs index dca77d3..a308926 100644 --- a/source/Checking/Module.hs +++ b/source/Checking/Module.hs @@ -43,6 +43,7 @@ module Checking.Module import Base import Checking.Declaration qualified as Declaration +import Checking.Exact qualified as Exact import Checking.Foundation import Checking.Identity import Checking.Semantic @@ -53,8 +54,9 @@ import Felix.Source import Felix.Store qualified as Store import Report.Location import Syntax.Interface +import Syntax.Abstract qualified as Raw -import Control.Monad (unless) +import Control.Monad (foldM, unless) import Data.Bifunctor (first) import Data.Text qualified as Text @@ -371,6 +373,7 @@ typedModuleInput data TypedPathError = TypedUnsupportedBlock !Location + | TypedExactCompileFailed !Exact.ExactCompileError deriving stock (Show, Eq) data TypedModuleFailure @@ -383,6 +386,8 @@ typedModuleFailureLocation :: TypedModuleFailure -> Maybe Location typedModuleFailureLocation = \case TypedActionFailed (TypedUnsupportedBlock location) -> Just location + TypedActionFailed (TypedExactCompileFailed failure) -> + Just (Exact.exactCompileErrorLocation failure) TypedDeclarationFailed{} -> Nothing TypedSealFailed{} -> @@ -395,6 +400,8 @@ renderTypedModuleFailure = \case TypedActionFailed (TypedUnsupportedBlock location) -> locationToText location <> ": this source block is not yet supported by the typed checker" + TypedActionFailed (TypedExactCompileFailed failure) -> + Exact.renderExactCompileError failure TypedSealFailed failure -> renderSemanticInterfaceError failure @@ -416,12 +423,13 @@ runTypedModule (Declaration.importSealedModuleDriver . sealedTypedModuleEvidence) effectiveDirect - case identifiedParsedModuleBlocks - (identifiedModuleParsed identified) of - [] -> pure () - block : _ -> - Declaration.failModuleDriver - (TypedUnsupportedBlock (locate block)) + void + (foldM + compileBlock + Exact.initialExactCompilerState + (zip [0 ..] + (identifiedParsedModuleBlocks + (identifiedModuleParsed identified)))) semanticDirect = semanticInterfaceAssertedId (sealedTypedModuleSemantic prelude) @@ -431,6 +439,36 @@ runTypedModule ) effectiveDirect = prelude : direct + occurrences = + identifiedParsedModuleSyntaxOccurrences + (identifiedModuleParsed identified) + compileBlock compilerState (blockIndex, block) = + case block of + Raw.BlockSig{} -> compileSelected + Raw.BlockAbbr{} -> compileSelected + Raw.BlockDefn{} -> compileSelected + _ -> + Declaration.failModuleDriver + (TypedUnsupportedBlock (locate block)) + where + compileSelected = do + prepared <- + Exact.prepareExactDeclaration + compilerState + block + [ parsedSyntaxOccurrenceEntry occurrence + | occurrence <- occurrences + , parsedSyntaxOccurrenceBlockIndex occurrence + == blockIndex + ] + case prepared of + Left failure -> + Declaration.failModuleDriver + (TypedExactCompileFailed failure) + Right (compilerState', declaration) -> do + void + (Exact.commitPreparedExactBinding declaration) + pure compilerState' result <- Declaration.runModuleDriver foundation diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs index d6af939..0496d84 100644 --- a/source/Felix/Migration.hs +++ b/source/Felix/Migration.hs @@ -166,7 +166,7 @@ protectedMigrationModules = , migrationLibraryModule "nat.tex" ] --- | Phase 3 source fixtures whose complete graphs may enter the typed driver. +-- | Source fixtures whose complete graphs may enter the typed driver. typedMigrationModules :: NonEmpty MigrationModuleRef typedMigrationModules = migrationProjectModule "test/phase3/typed-producer.tex" :| @@ -174,6 +174,9 @@ typedMigrationModules = , migrationProjectModule "test/phase3/typed-shared-a.tex" , migrationProjectModule "test/phase3/typed-shared-b.tex" , migrationProjectModule "test/phase3/typed-shared-root.tex" + , migrationProjectModule "test/phase5/exact-producer.tex" + , migrationProjectModule "test/phase5/exact-importer.tex" + , migrationProjectModule "test/phase5/exact-failure.tex" ] diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index bc634ac..9d36641 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -4,6 +4,7 @@ module Test.Unit.Module (unitTests) where import Base import Api qualified +import Checking.Authority qualified as Authority import Checking.Core qualified as Core import Checking.Declaration qualified as Declaration import Checking.Foundation qualified as Foundation @@ -26,11 +27,14 @@ import Syntax.Interface qualified as Syntax import Bound.Scope (fromScope) import Bound.Var (Var(..)) +import Control.Monad (foldM) import Data.ByteString qualified as ByteString import Data.Text qualified as StrictText import Data.Text.Encoding qualified as Text import Control.Monad.Logger (runNoLoggingT) -import System.Directory (getCurrentDirectory) +import Data.IORef (modifyIORef', newIORef, readIORef) +import Data.Map.Strict qualified as Map +import System.Directory (createDirectoryIfMissing, getCurrentDirectory) import System.FilePath.Posix qualified as Posix import System.IO.Temp qualified as Temp import Test.Tasty @@ -52,6 +56,14 @@ unitTests = resetsGlossStatePerModule , testCase "makes selected unsupported syntax terminal" rejectsUnsupportedTypedSource + , testCase "compiles exact declarations across an import" + compilesExactDeclarationGraph + , testCase "keeps exact semantics independent of fixity" + keepsExactSemanticsIndependentOfFixity + , testCase "loads a cached exact producer for a fresh importer" + loadsCachedExactProducerForFreshImporter + , testCase "retains the exact prefix before a later failure" + retainsExactPrefixBeforeFailure , testCase "routes production verification by complete graph" routesProductionVerification , testCase "installs nonempty implicit prelude evidence" @@ -346,6 +358,241 @@ rejectsUnsupportedTypedSource = do Right{} -> assertFailure "unsupported typed source was admitted" +compilesExactDeclarationGraph :: Assertion +compilesExactDeclarationGraph = do + (_foundation, _bootstrap, workspace, sealedModules) <- + compileExactFixture "test/phase5/exact-importer.tex" + assertEqual "dependency-closed module count" 2 (length sealedModules) + assertEqual "imported-before-importer source order" + [ "test/phase5/exact-producer.tex" + , "test/phase5/exact-importer.tex" + ] + [ safeRelativePathFilePath + (resolvedSourceRelativePath + (Parse.parsedModuleResolved parsed)) + | parsed <- toList + (Parse.parsedWorkspaceImportedBeforeImporter workspace) + ] + case sealedModules of + [producer, importer] -> do + let producerPrefix = Module.sealedTypedModulePrefix producer + importerPrefix = Module.sealedTypedModulePrefix importer + producerBatches = + Declaration.pendingModulePrefixBatches producerPrefix + importerBatches = + Declaration.pendingModulePrefixBatches importerPrefix + assertEqual "producer declaration batches" 3 + (length producerBatches) + assertEqual "importer declaration batches" 1 + (length importerBatches) + assertEqual "producer declaration order" + [0, 1, 2] + [ localDeclarationOrdinalValue + (Semantic.declarationSlotOrdinal + (Declaration.committedBatchSlot batch)) + | batch <- producerBatches + ] + + let producerDeltas = + Semantic.semanticInterfaceDeclarations + (Module.sealedTypedModuleSemantic producer) + importerDeltas = + Semantic.semanticInterfaceDeclarations + (Module.sealedTypedModuleSemantic importer) + assertEqual "one exact binding per producer declaration" + [1, 1, 1] + (bindingCount <$> producerDeltas) + assertEqual "one exact importer binding" + [1] + (bindingCount <$> importerDeltas) + assertEqual "producer object families" + ["opaque", "transparent", "transparent"] + [ objectFamilyName + (Identity.assertedObjectContent object) + | batch <- producerBatches + , object <- Declaration.committedBatchObjects batch + ] + + definitionDelta <- sole "producer definition delta" + (drop 2 producerDeltas) + definitionBinding <- sole "producer definition binding" + (bindings definitionDelta) + definitionFact <- sole "producer definition fact" + (Semantic.declarationDeltaFacts definitionDelta) + definitionAlias <- sole "producer definition alias" + (Semantic.declarationDeltaAliases definitionDelta) + assertEqual "definition alias" + (Semantic.semanticName "phase5_definition") + (Semantic.semanticAliasName definitionAlias) + assertEqual "definition is proof-search eligible" + Semantic.SearchEligible + (Semantic.semanticFactSearchEligibility definitionFact) + assertEqual "definition authority is clean" + Authority.cleanAuthoritySafety + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority definitionFact)) + definitionBatch <- sole "producer definition batch" + (drop 2 producerBatches) + validation <- + maybe + (assertFailure "definition declaration validation is absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + definitionBatch) + certificate <- sole "definition validation certificate" + (Semantic.declarationValidationRecordCertificates validation) + assertEqual "direct defining-equation authority" + (Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation + (Semantic.semanticGlobalBindingTarget + definitionBinding))) + (Authority.validationDirectAuthorization + certificate) + + aliasDelta <- sole "producer abbreviation delta" + (take 1 (drop 1 producerDeltas)) + aliasBinding <- sole "producer abbreviation binding" + (bindings aliasDelta) + definitionObject <- sole "producer definition object" + (Declaration.committedBatchObjects definitionBatch) + case Identity.assertedObjectContent definitionObject of + Identity.TransparentObjectContent _theory _coreType body -> + assertBool "definition resolves the producer alias" + (Semantic.semanticGlobalBindingTarget aliasBinding + `elem` canonicalGlobals body) + content -> + assertFailure + ("definition object is not transparent: " + <> show content) + importerBatch <- sole "importer declaration batch" importerBatches + importerDelta <- sole "importer semantic delta" importerDeltas + importerBinding <- sole "importer binding" + (bindings importerDelta) + assertEqual "equal transparent content reuses the producer object" + (Semantic.semanticGlobalBindingTarget definitionBinding) + (Semantic.semanticGlobalBindingTarget importerBinding) + assertEqual "reused transparent content adds no object" + [] + (Declaration.committedBatchObjects importerBatch) + modules -> + assertFailure + ("unexpected exact module count: " <> show (length modules)) + where + bindingCount = length . bindings + + bindings = + Semantic.semanticEnvironmentBindings + . Semantic.declarationDeltaEnvironment + + objectFamilyName :: Identity.ObjectContent -> String + objectFamilyName = \case + Identity.OpaqueObjectContent{} -> "opaque" + Identity.TransparentObjectContent{} -> "transparent" + Identity.IntrinsicObjectContent{} -> "intrinsic" + +keepsExactSemanticsIndependentOfFixity :: Assertion +keepsExactSemanticsIndependentOfFixity = + Temp.withSystemTempDirectory "felix-exact-fixity" \root -> do + let relative = "test/phase5/exact-producer.tex" + path = root Posix.</> relative + createDirectoryIfMissing True (Posix.takeDirectory path) + original <- ByteString.readFile relative + let changed = + Text.encodeUtf8 + (StrictText.replace + "infixl 2" + "infixr 6" + (Text.decodeUtf8 original)) + ByteString.writeFile path original + first <- compileExactRootAt root relative + ByteString.writeFile path changed + second <- compileExactRootAt root relative + let firstParsed = Parse.parsedWorkspaceRootModule (fst first) + secondParsed = Parse.parsedWorkspaceRootModule (fst second) + firstSealed = snd first + secondSealed = snd second + assertBool "fixity changes syntax identity" + (Syntax.moduleSyntaxAssertedId + (Parse.parsedModuleSyntaxInterface firstParsed) + /= Syntax.moduleSyntaxAssertedId + (Parse.parsedModuleSyntaxInterface secondParsed)) + assertBool "fixity changes parsed identity" + (Parse.parsedModuleId firstParsed + /= Parse.parsedModuleId secondParsed) + assertEqual "fixity preserves semantic interface" + (Module.sealedTypedModuleSemantic firstSealed) + (Module.sealedTypedModuleSemantic secondSealed) + assertEqual "fixity preserves semantic prefix" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix firstSealed)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix secondSealed)) + +loadsCachedExactProducerForFreshImporter :: Assertion +loadsCachedExactProducerForFreshImporter = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-exact-cache" \root -> do + let path = root Posix.</> "store.sqlite" + (_startup, store) <- + Store.openStore path (Identity.theoryId foundation) + >>= expectRight + observed <- newIORef (0 :: Int) + let observer = Api.verificationRequestObserver \_ordinal _request -> + modifyIORef' observed (+ 1) + prover = + Provers.vampire + "phase5-fixture-must-not-run-vampire" + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + verify mode source = + runNoLoggingT + (Api.verifyWithObserverAndStoreMode + store mode observer prover source) + >>= expectRight + producer <- + verify Api.FreshStoreValidation + "test/phase5/exact-producer.tex" + importer <- + verify Api.WarmStoreValidation + "test/phase5/exact-importer.tex" + assertTypedSuccess "fresh producer" producer + assertTypedSuccess "warm producer/fresh importer" importer + assertEqual "exact declarations issue no Vampire requests" + 0 + =<< readIORef observed + Store.closeStore store + +retainsExactPrefixBeforeFailure :: Assertion +retainsExactPrefixBeforeFailure = do + result <- + runNoLoggingT + (Api.verifyMeasured + (Provers.vampire + "phase5-fixture-must-not-run-vampire" + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + "test/phase5/exact-failure.tex") + case result of + Left + (Api.VerificationTypedModuleError + source + (Module.TypedActionFailed + (Module.TypedUnsupportedBlock location)) + prefix) -> do + assertEqual "failed exact source" + "test/phase5/exact-failure.tex" + (safeRelativePathFilePath + (resolvedSourceRelativePath source)) + assertEqual "unsupported declaration line" 5 (locLine location) + assertEqual "earlier exact declaration remains committed" + 1 + (length (Declaration.pendingModulePrefixBatches prefix)) + Left err -> + assertFailure ("unexpected exact failure: " <> show err) + Right{} -> + assertFailure "unsupported declaration was admitted" + routesProductionVerification :: Assertion routesProductionVerification = do producer <- verifyFixture "test/phase3/typed-producer.tex" @@ -551,6 +798,157 @@ unusedResolver = Declaration.vampireResolver \_prepared -> fail "empty bootstrap invoked Vampire" +compileExactFixture + :: FilePath + -> IO + ( Foundation.CheckedFoundation + , Module.MigrationPreludeSession + , Parse.ParsedSourceWorkspace + , [Module.SealedTypedModule] + ) +compileExactFixture relative = do + root <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeSession + foundation + unusedResolver + mounts <- exactFixtureMounts root + workspace <- parseExactWorkspace bootstrap mounts relative + sealed <- compileParsedWorkspace foundation bootstrap workspace + pure (foundation, bootstrap, workspace, sealed) + +compileExactRootAt + :: FilePath + -> FilePath + -> IO (Parse.ParsedSourceWorkspace, Module.SealedTypedModule) +compileExactRootAt projectRoot relative = do + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeSession + foundation + unusedResolver + mounts <- exactFixtureMounts projectRoot + workspace <- parseExactWorkspace bootstrap mounts relative + sealed <- compileParsedWorkspace foundation bootstrap workspace + rootModule <- sole "exact root module" (reverse sealed) + pure (workspace, rootModule) + +exactFixtureMounts :: FilePath -> IO SourceMounts +exactFixtureMounts projectRoot = do + repository <- getCurrentDirectory + expectRight + =<< prepareSourceMounts + [ (sourceMountId "project", projectRoot) + , (sourceMountId "library", repository Posix.</> "library") + , (sourceMountId "debug", repository Posix.</> "debug") + ] + +parseExactWorkspace + :: Module.MigrationPreludeSession + -> SourceMounts + -> FilePath + -> IO Parse.ParsedSourceWorkspace +parseExactWorkspace bootstrap mounts relative = do + request <- expectRight (searchedRoot relative) + let preludeSyntax = + Module.sealedTypedModuleSyntax + (Module.migrationPreludeModule bootstrap) + fst + <$> (expectRight + =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs + mounts + request + (const [preludeSyntax])) + +compileParsedWorkspace + :: Foundation.CheckedFoundation + -> Module.MigrationPreludeSession + -> Parse.ParsedSourceWorkspace + -> IO [Module.SealedTypedModule] +compileParsedWorkspace foundation bootstrap workspace = + snd + <$> foldM + compileOne + (Map.empty, []) + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + where + compileOne (admitted, ordered) parsed = do + direct <- + traverse + (\address -> + maybe + (assertFailure + ("missing exact direct module: " <> show address) + >> fail "unreachable") + pure + (Map.lookup address admitted)) + (nubOrd + (Parse.parsedImportedAddress + <$> Parse.parsedModuleImports parsed)) + input <- + expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapWalkingReadiness bootstrap) + unusedResolver + Declaration.FreshValidation + parsed + direct) + sealed <- + Module.runTypedModule input >>= \case + Module.TypedModuleSucceeded module' -> pure module' + Module.TypedModuleOpenFailed failure -> + assertFailure + ("exact module did not open: " <> show failure) + >> fail "unreachable" + Module.TypedModuleFailed failure _prefix -> + assertFailure + ("exact module did not seal: " <> show failure) + >> fail "unreachable" + pure + ( Map.insert (Parse.parsedModuleAddress parsed) sealed admitted + , ordered <> [sealed] + ) + +canonicalGlobals :: Core.CanonicalTerm Identity.ObjectId -> [Identity.ObjectId] +canonicalGlobals = \case + Core.CBound{} -> [] + Core.CGlobal identity -> [identity] + Core.CIntrinsic{} -> [] + Core.COpaqueInteger{} -> [] + Core.CApp function argument -> + canonicalGlobals function <> canonicalGlobals argument + Core.CLam _type body -> canonicalGlobals body + Core.CFalsum -> [] + Core.CImp premise conclusion -> + canonicalGlobals premise <> canonicalGlobals conclusion + Core.CEq _type left right -> + canonicalGlobals left <> canonicalGlobals right + Core.CForall _type body -> canonicalGlobals body + +assertTypedSuccess :: String -> Api.VerificationResult -> Assertion +assertTypedSuccess label = \case + Api.VerifiedWithTrustedVampire report -> + assertEqual label Api.TypedVerificationRoute + (Api.verificationRoute report) + Api.CompletedWithExplicitGaps report -> + assertFailure + (label <> " completed with gaps via " + <> show (Api.verificationRoute report)) + Api.VerificationFailure failure -> + assertFailure (label <> " failed: " <> show failure) + +sole :: String -> [value] -> IO value +sole label = \case + [value] -> pure value + values -> + assertFailure + (label <> ": expected one value, found " <> show (length values)) + >> fail "unreachable" + expectRight :: Show error => Either error value -> IO value expectRight = \case Left err -> assertFailure (show err) >> fail "unreachable" diff --git a/test/phase5/exact-failure.tex b/test/phase5/exact-failure.tex new file mode 100644 index 0000000..692433c --- /dev/null +++ b/test/phase5/exact-failure.tex @@ -0,0 +1,7 @@ +\begin{signature}\label{phase5_before_failure} + $\phasefivebeforefailure{X}$ is a set. +\end{signature} + +\begin{axiom}\label{phase5_unsupported_axiom} + $X = X$. +\end{axiom} diff --git a/test/phase5/exact-importer.tex b/test/phase5/exact-importer.tex new file mode 100644 index 0000000..8365ffd --- /dev/null +++ b/test/phase5/exact-importer.tex @@ -0,0 +1,5 @@ +\import{test/phase5/exact-producer.tex} + +\begin{definition}\label{phase5_imported_definition} + $\phasefiveimporter{X}{Y} = \phasefivealias{X}{Y}$. +\end{definition} diff --git a/test/phase5/exact-producer.tex b/test/phase5/exact-producer.tex new file mode 100644 index 0000000..0148d35 --- /dev/null +++ b/test/phase5/exact-producer.tex @@ -0,0 +1,12 @@ +\begin{signature}\label{phase5_seed} + %! infixl 2 + $X \phasefiveseed Y$ is a set. +\end{signature} + +\begin{abbreviation}\label{phase5_alias} + $\phasefivealias{X}{Y} = X \phasefiveseed Y$. +\end{abbreviation} + +\begin{definition}\label{phase5_definition} + $\phasefivedefinition{X}{Y} = \phasefivealias{X}{Y}$. +\end{definition} |