summaryrefslogtreecommitdiff
path: root/source/Felix
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix')
-rw-r--r--source/Felix/Cache/Codec.hs2
-rw-r--r--source/Felix/Migration.hs284
-rw-r--r--source/Felix/Parse.hs147
-rw-r--r--source/Felix/Prelude.hs200
-rw-r--r--source/Felix/Source.hs20
-rw-r--r--source/Felix/Store.hs189
6 files changed, 418 insertions, 424 deletions
diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs
index 0bfa975..2d81e57 100644
--- a/source/Felix/Cache/Codec.hs
+++ b/source/Felix/Cache/Codec.hs
@@ -75,7 +75,7 @@ newtype CacheEpoch = CacheEpoch Word32
currentCacheEpoch :: CacheEpoch
currentCacheEpoch =
- CacheEpoch 19
+ CacheEpoch 23
cacheEpochValue :: CacheEpoch -> Word32
cacheEpochValue (CacheEpoch value) =
diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs
deleted file mode 100644
index 0fcb05d..0000000
--- a/source/Felix/Migration.hs
+++ /dev/null
@@ -1,284 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Temporary routing data for the content-addressed migration.
---
--- These values select current physical sources. They are not durable module
--- names and must be deleted with the legacy driver.
-module Felix.Migration
- ( MigrationMountRole(..)
- , migrationMountId
- , MigrationModuleRef
- , migrationModuleRefRole
- , migrationModuleRefPath
- , MigrationManifestError(..)
- , migrationModuleCandidatePath
- , ResolvedMigrationSelection
- , resolveMigrationSelection
- , migrationSelectionContains
- , MigrationGraphRoute(..)
- , classifyMigrationGraph
- , activeMigrationRoots
- , protectedMigrationModules
- , phase53LibraryMigrationModules
- , typedMigrationModules
- , PreludeSourceFamily(..)
- , finalPreludeSourceFamilies
- , PreludePublicRole(..)
- , expectedFinalPreludePublicRoles
- ) where
-
-import Base
-import Felix.Parse
-import Felix.Source
-
-import Data.List qualified as List
-import Data.Set qualified as Set
-
-
-data MigrationMountRole
- = MigrationProject
- | MigrationLibrary
- | MigrationDebug
- deriving stock (Show, Eq, Ord, Enum, Bounded)
-
-migrationMountId :: MigrationMountRole -> SourceMountId
-migrationMountId = \case
- MigrationProject ->
- sourceMountId "project"
- MigrationLibrary ->
- sourceMountId "library"
- MigrationDebug ->
- sourceMountId "debug"
-
-
-data MigrationModuleRef = MigrationModuleRef
- !MigrationMountRole
- !SafeRelativePath
- deriving stock (Show, Eq, Ord)
-
-migrationModuleRefRole
- :: MigrationModuleRef
- -> MigrationMountRole
-migrationModuleRefRole (MigrationModuleRef role _path) =
- role
-
-migrationModuleRefPath
- :: MigrationModuleRef
- -> SafeRelativePath
-migrationModuleRefPath (MigrationModuleRef _role path) =
- path
-
-data MigrationManifestError
- = MissingMigrationMountRole !MigrationMountRole
- deriving stock (Show, Eq)
-
-newtype ResolvedMigrationSelection = ResolvedMigrationSelection
- (Set (SourceMountId, CanonicalPath, SafeRelativePath))
-
-resolveMigrationSelection
- :: Foldable references
- => SourceMounts
- -> references MigrationModuleRef
- -> Either MigrationManifestError ResolvedMigrationSelection
-resolveMigrationSelection mounts references =
- ResolvedMigrationSelection . Set.fromList
- <$> traverse resolveOne (toList references)
- where
- resolveOne reference =
- case List.find
- ((== migrationMountId role) . sourceMountIdentifier)
- (sourceMountList mounts) of
- Nothing ->
- Left (MissingMigrationMountRole role)
- Just mount ->
- Right
- ( sourceMountIdentifier mount
- , sourceMountRoot mount
- , migrationModuleRefPath reference
- )
- where
- role = migrationModuleRefRole reference
-
-migrationSelectionContains
- :: ResolvedMigrationSelection
- -> ResolvedSource
- -> Bool
-migrationSelectionContains
- (ResolvedMigrationSelection selected) source =
- ( resolvedSourceMount source
- , resolvedSourceMountRoot source
- , resolvedSourceRelativePath source
- ) `Set.member` selected
-
-data MigrationGraphRoute
- = TypedMigrationGraph
- | LegacyMigrationGraph
- deriving stock (Show, Eq)
-
-classifyMigrationGraph
- :: ResolvedMigrationSelection
- -> ParsedSourceWorkspace
- -> MigrationGraphRoute
-classifyMigrationGraph selected workspace
- | all
- (migrationSelectionContains selected . parsedModuleResolved)
- (parsedWorkspaceModules workspace) =
- TypedMigrationGraph
- | otherwise =
- LegacyMigrationGraph
-
--- | Resolve one routing reference against the current prepared mount table.
---
--- This deliberately returns a physical candidate path, not a logical owner.
-migrationModuleCandidatePath
- :: SourceMounts
- -> MigrationModuleRef
- -> Either MigrationManifestError FilePath
-migrationModuleCandidatePath mounts reference =
- case List.find matchesRole candidates of
- Nothing ->
- Left (MissingMigrationMountRole role)
- Just candidate ->
- Right (sourceCandidatePath candidate)
- where
- role = migrationModuleRefRole reference
- expectedMount = migrationMountId role
- candidates =
- sourceCandidates
- mounts
- (migrationModuleRefPath reference)
- matchesRole candidate =
- sourceCandidateMount candidate == expectedMount
-
-
--- | Current supported verification root.
-activeMigrationRoots :: NonEmpty MigrationModuleRef
-activeMigrationRoots =
- migrationLibraryModule "everything.tex" :| []
-
--- | Dependency-closed set/naturals migration boundary.
-protectedMigrationModules :: NonEmpty MigrationModuleRef
-protectedMigrationModules =
- migrationLibraryModule "set.tex" :|
- [ migrationLibraryModule "set/cons.tex"
- , migrationLibraryModule "set/regularity.tex"
- , migrationLibraryModule "set/suc.tex"
- , migrationLibraryModule "nat.tex"
- ]
-
--- | Phase 5.3 ordinary library modules admitted by the typed driver.
-phase53LibraryMigrationModules :: NonEmpty MigrationModuleRef
-phase53LibraryMigrationModules =
- migrationLibraryModule "set/symdiff.tex" :|
- [ migrationLibraryModule "set/powerset.tex"
- , migrationLibraryModule "set/partition.tex"
- , migrationLibraryModule "set/bipartition.tex"
- , migrationLibraryModule "set/product.tex"
- , migrationLibraryModule "set/filter.tex"
- , migrationLibraryModule "relation.tex"
- , migrationLibraryModule "relation/properties.tex"
- , migrationLibraryModule "relation/uniqueness.tex"
- , migrationLibraryModule "function.tex"
- , migrationLibraryModule "set/cantor.tex"
- , migrationLibraryModule "set/fixpoint.tex"
- ]
-
--- | Sources whose complete graphs may enter the typed driver.
-typedMigrationModules :: NonEmpty MigrationModuleRef
-typedMigrationModules =
- protectedMigrationModules
- <> phase53LibraryMigrationModules
- <> (migrationProjectModule "test/phase3/typed-producer.tex" :|
- [ migrationProjectModule "test/phase3/typed-unsupported.tex"
- , 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"
- , migrationProjectModule "test/phase5/exact-proofs.tex"
- , migrationProjectModule "test/phase5/exact-local-definition.tex"
- , migrationProjectModule "test/phase5/exact-local-definition-failure.tex"
- , migrationProjectModule "test/phase5/exact-contradiction.tex"
- , migrationProjectModule "test/phase5/exact-contradiction-goal.tex"
- , migrationProjectModule "test/phase5/exact-relation-expression.tex"
- , migrationProjectModule "test/phase5/exact-relation-expression-missing-pair.tex"
- , migrationProjectModule "test/phase5/exact-application.tex"
- , migrationProjectModule "test/phase5/exact-application-missing.tex"
- , migrationProjectModule "test/phase5/exact-quantified-subject.tex"
- , migrationProjectModule "test/phase5/exact-quantified-subject-nested.tex"
- , migrationProjectModule "test/phase5/exact-proof-failure.tex"
- , migrationProjectModule "test/phase5/exact-induction-nested.tex"
- , migrationProjectModule "test/phase5/exact-runtime-failure.tex"
- , migrationProjectModule "test/phase5/exact-source-axiom.tex"
- , migrationProjectModule "test/phase5/exact-source-axiom-assumptions.tex"
- , migrationProjectModule "test/phase5/exact-omitted.tex"
- , migrationProjectModule "test/phase5/exact-escape-producer.tex"
- , migrationProjectModule "test/phase5/exact-escape-consumer.tex"
- , migrationProjectModule "test/phase5/exact-separation.tex"
- , migrationProjectModule "test/phase5/exact-replacement.tex"
- , migrationProjectModule "test/phase5/exact-finite-set.tex"
- , migrationProjectModule "test/phase5/exact-datatype.tex"
- , migrationProjectModule "test/phase5/exact-datatype-nested.tex"
- , migrationProjectModule "test/phase5/exact-inductive.tex"
- , migrationProjectModule "test/phase5/exact-inductive-recursive.tex"
- , migrationProjectModule "test/phase5/exact-inductive-nested.tex"
- , migrationProjectModule "test/phase5/unmatched-proof.tex"
- ])
-
-
--- | Source constructs required by the non-authoritative prelude skeleton.
-data PreludeSourceFamily
- = PreludeDefinition
- | PreludeAbbreviation
- | PreludeProposition
- | PreludeProof
- deriving stock (Show, Eq, Ord, Enum, Bounded)
-
-finalPreludeSourceFamilies :: Set PreludeSourceFamily
-finalPreludeSourceFamilies =
- Set.fromList
- [ PreludeDefinition
- , PreludeAbbreviation
- , PreludeProposition
- , PreludeProof
- ]
-
--- | Stable public roles required at final-prelude cutover.
---
--- Helper declarations used to derive these roles are intentionally not
--- frozen by Phase 0.
-data PreludePublicRole
- = PreludeInfinityTheorem
- | PreludeOmegaObject
- | PreludeOmegaDefiningEquation
- | PreludeNaturalsAlias
- | PreludeNaturalsInductiveTheorem
- | PreludeNaturalsMinimalTheorem
- deriving stock (Show, Eq, Ord, Enum, Bounded)
-
-expectedFinalPreludePublicRoles :: Set PreludePublicRole
-expectedFinalPreludePublicRoles =
- Set.fromList [minBound .. maxBound]
-
-
-migrationLibraryModule :: FilePath -> MigrationModuleRef
-migrationLibraryModule =
- MigrationModuleRef MigrationLibrary . checkedRelativePath
-
-migrationProjectModule :: FilePath -> MigrationModuleRef
-migrationProjectModule =
- MigrationModuleRef MigrationProject . checkedRelativePath
-
-checkedRelativePath :: FilePath -> SafeRelativePath
-checkedRelativePath path =
- case safeRelativePath path of
- Left err ->
- impossible
- ("invalid migration path literal "
- <> show path
- <> ": "
- <> show err)
- Right relative ->
- relative
diff --git a/source/Felix/Parse.hs b/source/Felix/Parse.hs
index b9d5c57..751f09c 100644
--- a/source/Felix/Parse.hs
+++ b/source/Felix/Parse.hs
@@ -8,6 +8,7 @@ module Felix.Parse
( ParseException(..)
, ParseWorkspaceError(..)
, renderParseWorkspaceError
+ , renderSyntaxMaterializationError
, ParseExecutionError(..)
, ParsedArtifactIntegrityError(..)
, SyntaxDeclarationError(..)
@@ -89,7 +90,9 @@ module Felix.Parse
, parseMeasurementTargetInspectionCount
, parseSourceWorkspaceMeasured
, parseSourceWorkspaceMeasuredWithSyntaxInputs
+ , parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
, parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
+ , parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
, parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
, parseSourceWorkspaceWith
, parseResolvedSourceGraph
@@ -1149,10 +1152,28 @@ parseSourceWorkspaceMeasuredWithSyntaxInputs
(ParsedSourceWorkspace, ParseMeasurements))
-- Implicit syntax inputs must be self-contained module interfaces.
parseSourceWorkspaceMeasuredWithSyntaxInputs mounts request syntaxInputs =
- parseSourceWorkspaceMeasuredWithSyntaxInputsAndCallback
+ parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
mounts
request
syntaxInputs
+ (const (Right ()))
+
+parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
+ :: SourceMounts
+ -> RootRequest
+ -> (ResolvedSource -> [ModuleSyntaxInterface])
+ -> (ResolvedSourceGraph -> Either SourceError ())
+ -> IO
+ (Either
+ ParseWorkspaceError
+ (ParsedSourceWorkspace, ParseMeasurements))
+parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
+ mounts request syntaxInputs validateGraph =
+ parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidationAndCallback
+ mounts
+ request
+ syntaxInputs
+ validateGraph
(\_source _block -> pure ())
parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
@@ -1166,8 +1187,24 @@ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
(ParsedSourceWorkspace, ParseMeasurements))
parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
store mounts request syntaxInputs =
- parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
- store mounts request syntaxInputs (\_source _block -> pure ())
+ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
+ store mounts request syntaxInputs (const (Right ()))
+
+parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
+ :: Store.Store
+ -> SourceMounts
+ -> RootRequest
+ -> (ResolvedSource -> [ModuleSyntaxInterface])
+ -> (ResolvedSourceGraph -> Either SourceError ())
+ -> IO
+ (Either
+ ParseExecutionError
+ (ParsedSourceWorkspace, ParseMeasurements))
+parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
+ store mounts request syntaxInputs validateGraph =
+ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidationAndCallback
+ store mounts request syntaxInputs validateGraph
+ (\_source _block -> pure ())
parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
:: Store.Store
@@ -1181,6 +1218,22 @@ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
(ParsedSourceWorkspace, ParseMeasurements))
parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
store mounts request syntaxInputs emitBlock = do
+ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidationAndCallback
+ store mounts request syntaxInputs (const (Right ())) emitBlock
+
+parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidationAndCallback
+ :: Store.Store
+ -> SourceMounts
+ -> RootRequest
+ -> (ResolvedSource -> [ModuleSyntaxInterface])
+ -> (ResolvedSourceGraph -> Either SourceError ())
+ -> (ResolvedSource -> Raw.Block -> IO ())
+ -> IO
+ (Either
+ ParseExecutionError
+ (ParsedSourceWorkspace, ParseMeasurements))
+parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidationAndCallback
+ store mounts request syntaxInputs validateGraph emitBlock = do
resolutionStart <- getMonotonicTimeNSec
graphResult <- buildResolvedSourceGraphMeasured mounts request
resolutionEnd <- getMonotonicTimeNSec
@@ -1191,20 +1244,27 @@ parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
(ParseExecutionWorkspaceError
(SourceWorkspaceError err)))
Right (graph, selectionMeasurements) ->
- fmap
- (fmap
- (\(workspace, measurements) ->
- ( workspace
- , withResolutionMeasurements
- measurements
- (resolutionEnd - resolutionStart)
- selectionMeasurements
- )))
- (parseResolvedSourceGraphMeasuredWithArtifacts
- (PersistentParsedArtifacts store)
- graph
- syntaxInputs
- emitBlock)
+ case validateGraph graph of
+ Left err ->
+ pure
+ (Left
+ (ParseExecutionWorkspaceError
+ (SourceWorkspaceError err)))
+ Right () ->
+ fmap
+ (fmap
+ (\(workspace, measurements) ->
+ ( workspace
+ , withResolutionMeasurements
+ measurements
+ (resolutionEnd - resolutionStart)
+ selectionMeasurements
+ )))
+ (parseResolvedSourceGraphMeasuredWithArtifacts
+ (PersistentParsedArtifacts store)
+ graph
+ syntaxInputs
+ emitBlock)
-- | Resolve, strictly load, and parse one source closure with a block
-- callback.
@@ -1250,6 +1310,21 @@ parseSourceWorkspaceMeasuredWithSyntaxInputsAndCallback
(ParsedSourceWorkspace, ParseMeasurements))
parseSourceWorkspaceMeasuredWithSyntaxInputsAndCallback
mounts request syntaxInputs emitBlock = do
+ parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidationAndCallback
+ mounts request syntaxInputs (const (Right ())) emitBlock
+
+parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidationAndCallback
+ :: SourceMounts
+ -> RootRequest
+ -> (ResolvedSource -> [ModuleSyntaxInterface])
+ -> (ResolvedSourceGraph -> Either SourceError ())
+ -> (ResolvedSource -> Raw.Block -> IO ())
+ -> IO
+ (Either
+ ParseWorkspaceError
+ (ParsedSourceWorkspace, ParseMeasurements))
+parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidationAndCallback
+ mounts request syntaxInputs validateGraph emitBlock = do
resolutionStart <- getMonotonicTimeNSec
graphResult <- buildResolvedSourceGraphMeasured mounts request
resolutionEnd <- getMonotonicTimeNSec
@@ -1257,23 +1332,27 @@ parseSourceWorkspaceMeasuredWithSyntaxInputsAndCallback
Left err ->
pure (Left (SourceWorkspaceError err))
Right (graph, selectionMeasurements) ->
- fmap
- (fmap
- (\(workspace, measurements) ->
- let
- -- Resolution includes source loading and import
- -- scanning for graph construction.
- measured =
- withResolutionMeasurements
- measurements
- (resolutionEnd - resolutionStart)
- selectionMeasurements
- in
- (workspace, measured)))
- (parseResolvedSourceGraphMeasuredWith
- graph
- syntaxInputs
- emitBlock)
+ case validateGraph graph of
+ Left err ->
+ pure (Left (SourceWorkspaceError err))
+ Right () ->
+ fmap
+ (fmap
+ (\(workspace, measurements) ->
+ let
+ -- Resolution includes source loading and
+ -- import scanning for graph construction.
+ measured =
+ withResolutionMeasurements
+ measurements
+ (resolutionEnd - resolutionStart)
+ selectionMeasurements
+ in
+ (workspace, measured)))
+ (parseResolvedSourceGraphMeasuredWith
+ graph
+ syntaxInputs
+ emitBlock)
parseResolvedSourceGraph
:: ResolvedSourceGraph
diff --git a/source/Felix/Prelude.hs b/source/Felix/Prelude.hs
index d159b21..28ad961 100644
--- a/source/Felix/Prelude.hs
+++ b/source/Felix/Prelude.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}
--- | The reserved in-memory prelude source used during migration.
+-- | The reserved packaged final-prelude source and its authority-free parser.
module Felix.Prelude
( ReservedPreludeSourceInput
, reservedPreludeSourceInput
@@ -9,11 +9,15 @@ module Felix.Prelude
, emptyBootstrapSourceInput
, reservedPreludeSourceOwner
, reservedPreludeSourceLabel
+ , reservedPreludeSourceCanonicalPath
, reservedPreludeSourceBytes
, reservedPreludeSourceText
+ , rejectOrdinaryPreludeSourceGraph
, preludeDiagnosticLabel
, PreludeLoadError(..)
+ , renderPreludeLoadError
, PreludeParseError(..)
+ , renderPreludeParseError
, ReservedParsedPrelude
, reservedParsedPreludeInput
, reservedParsedPreludeModule
@@ -24,6 +28,8 @@ import Base
import Felix.Module
import Felix.Parse
import Felix.Parsed.Identity qualified as Parsed
+import Felix.Source
+import Felix.Source.Graph
import Report.Location
import Syntax.Adapt (SyntaxMaterializationError)
import Syntax.Interface
@@ -41,6 +47,7 @@ import Paths_felix qualified as Paths
data ReservedPreludeSourceInput = ReservedPreludeSourceInput
!ModuleName
!FilePath
+ !(Maybe CanonicalPath)
!ByteString
!Text
@@ -51,38 +58,76 @@ reservedPreludeSourceInput bytes =
ReservedPreludeSourceInput
preludeModuleName
preludeDiagnosticLabel
+ Nothing
bytes
<$> Text.decodeUtf8' bytes
data PreludeLoadError
= PreludeSourceReadFailed !FilePath !Text
+ | PreludeSourceCanonicalizationFailed !FilePath !SourceError
| PreludeSourceUtf8Failed !UnicodeException
- deriving stock (Show)
+
+instance Show PreludeLoadError where
+ show = Text.unpack . renderPreludeLoadError
+
+renderPreludeLoadError :: PreludeLoadError -> Text
+renderPreludeLoadError = \case
+ PreludeSourceReadFailed path failure ->
+ Text.pack path
+ <> ": unable to read packaged final prelude: "
+ <> failure
+ PreludeSourceCanonicalizationFailed path failure ->
+ Text.pack path
+ <> ": unable to resolve packaged final prelude: "
+ <> renderSourceError failure
+ PreludeSourceUtf8Failed failure ->
+ preludeErrorPrefix
+ <> "malformed UTF-8: "
+ <> Text.pack (displayException failure)
loadReservedPreludeSourceInput
:: IO (Either PreludeLoadError ReservedPreludeSourceInput)
loadReservedPreludeSourceInput = do
path <- Paths.getDataFileName "data/felix-prelude.tex"
- loaded <- try (ByteString.readFile path)
- :: IO (Either IOException ByteString)
- pure case loaded of
+ canonicalized <- canonicalizeExistingSourcePath path
+ case canonicalized of
Left failure ->
- Left
- (PreludeSourceReadFailed
- path
- (Text.pack (displayException failure)))
- Right bytes ->
- case reservedPreludeSourceInput bytes of
+ pure
+ (Left
+ (PreludeSourceCanonicalizationFailed path failure))
+ Right canonical -> do
+ loaded <- try
+ (ByteString.readFile
+ (canonicalPathFilePath canonical))
+ :: IO (Either IOException ByteString)
+ pure case loaded of
Left failure ->
- Left (PreludeSourceUtf8Failed failure)
- Right input ->
- Right input
+ Left
+ (PreludeSourceReadFailed
+ path
+ (Text.pack (displayException failure)))
+ Right bytes ->
+ case Text.decodeUtf8' bytes of
+ Left failure ->
+ Left (PreludeSourceUtf8Failed failure)
+ Right sourceText ->
+ Right
+ (ReservedPreludeSourceInput
+ preludeModuleName
+ preludeDiagnosticLabel
+ (Just canonical)
+ bytes
+ sourceText)
+-- | Empty final-prelude input used only by focused compiler fixtures.
+--
+-- Production verification always calls 'loadReservedPreludeSourceInput'.
emptyBootstrapSourceInput :: ReservedPreludeSourceInput
emptyBootstrapSourceInput =
ReservedPreludeSourceInput
preludeModuleName
preludeDiagnosticLabel
+ Nothing
ByteString.empty
Text.empty
@@ -90,28 +135,58 @@ reservedPreludeSourceOwner
:: ReservedPreludeSourceInput
-> ModuleName
reservedPreludeSourceOwner
- (ReservedPreludeSourceInput owner _label _bytes _text) =
+ (ReservedPreludeSourceInput owner _label _canonical _bytes _text) =
owner
reservedPreludeSourceLabel
:: ReservedPreludeSourceInput
-> FilePath
reservedPreludeSourceLabel
- (ReservedPreludeSourceInput _owner label _bytes _text) =
+ (ReservedPreludeSourceInput _owner label _canonical _bytes _text) =
label
+reservedPreludeSourceCanonicalPath
+ :: ReservedPreludeSourceInput
+ -> Maybe CanonicalPath
+reservedPreludeSourceCanonicalPath
+ (ReservedPreludeSourceInput _owner _label canonical _bytes _text) =
+ canonical
+
reservedPreludeSourceBytes
:: ReservedPreludeSourceInput
-> ByteString
reservedPreludeSourceBytes
- (ReservedPreludeSourceInput _owner _label bytes _text) =
+ (ReservedPreludeSourceInput _owner _label _canonical bytes _text) =
bytes
reservedPreludeSourceText :: ReservedPreludeSourceInput -> Text
reservedPreludeSourceText
- (ReservedPreludeSourceInput _owner _label _bytes sourceText) =
+ (ReservedPreludeSourceInput
+ _owner _label _canonical _bytes sourceText) =
sourceText
+-- | Reject an ordinary source graph containing the physical packaged
+-- prelude. Synthetic reserved inputs deliberately have no physical path.
+rejectOrdinaryPreludeSourceGraph
+ :: ReservedPreludeSourceInput
+ -> ResolvedSourceGraph
+ -> Either SourceError ()
+rejectOrdinaryPreludeSourceGraph sourceInput graph =
+ case reservedPreludeSourceCanonicalPath sourceInput of
+ Nothing ->
+ Right ()
+ Just reservedPath ->
+ case listToMaybe
+ [ source
+ | node <- sourceGraphNodes graph
+ , let source = sourceNodeResolved node
+ , resolvedSourceCanonicalPath source == reservedPath
+ ] of
+ Nothing ->
+ Right ()
+ Just source ->
+ Left (PackagedPreludeSelectedAsOrdinarySource source)
+
preludeDiagnosticLabel :: FilePath
preludeDiagnosticLabel =
"<felix-prelude>"
@@ -130,7 +205,92 @@ data PreludeParseError
| PreludeFreshInputFailed !FreshModuleInputError
| PreludeParsedModuleKeyFailed !Parsed.ParsedModuleKeyError
| PreludeParseInvariantFailed !Text
- deriving stock (Show)
+
+instance Show PreludeParseError where
+ show = Text.unpack . renderPreludeParseError
+
+renderPreludeParseError :: PreludeParseError -> Text
+renderPreludeParseError = \case
+ PreludeLocationRegistrationFailed FileIdSpaceExhausted ->
+ preludeErrorPrefix
+ <> "could not register source locations: file identifier space exhausted"
+ PreludeSyntaxPragmaFailed failure ->
+ renderSyntaxPragmaError failure
+ PreludeImportNotSupported imports ->
+ preludeErrorPrefix
+ <> "imports are not supported"
+ <> case imports of
+ [] -> ""
+ _ ->
+ ": "
+ <> Text.intercalate
+ ", "
+ (Text.pack . show <$> imports)
+ PreludeLexicalScanFailed failure ->
+ Text.pack (show failure)
+ PreludeSyntaxDeclarationFailed failure ->
+ Text.pack (show failure)
+ PreludeLexiconCollision collision ->
+ Text.pack (show collision)
+ PreludeSyntaxDeltaFailed collision ->
+ preludeErrorPrefix
+ <> "syntax delta has conflicting entries for pattern "
+ <> Text.pack (show (canonicalCollisionPattern collision))
+ <> ": "
+ <> Text.pack
+ (show (toList (canonicalCollisionEntries collision)))
+ PreludeSyntaxInterfaceFailed failure ->
+ preludeErrorPrefix <> renderSyntaxInterfaceError failure
+ PreludeSyntaxMaterializationFailed failure ->
+ preludeErrorPrefix <> renderSyntaxMaterializationError failure
+ PreludeParseFailed failure ->
+ preludeErrorPrefix <> Text.pack (show failure)
+ PreludeFreshInputFailed failure ->
+ preludeErrorPrefix <> renderFreshModuleInputError failure
+ PreludeParsedModuleKeyFailed failure ->
+ preludeErrorPrefix <> renderParsedModuleKeyError failure
+ PreludeParseInvariantFailed failure ->
+ preludeErrorPrefix <> "parse invariant failed: " <> failure
+
+preludeErrorPrefix :: Text
+preludeErrorPrefix =
+ Text.pack preludeDiagnosticLabel <> ": "
+
+renderSyntaxInterfaceError :: SyntaxInterfaceError -> Text
+renderSyntaxInterfaceError = \case
+ DuplicateDirectSyntaxInterface duplicate ->
+ "duplicate direct syntax input " <> Text.pack (show duplicate)
+ UnexpectedBaseSyntaxInterface actual expected ->
+ "base syntax interface mismatch: expected "
+ <> Text.pack (show expected)
+ <> ", got "
+ <> Text.pack (show actual)
+ SyntaxInterfaceIdMismatch asserted computed ->
+ "syntax interface identity mismatch: asserted "
+ <> Text.pack (show asserted)
+ <> ", computed "
+ <> Text.pack (show computed)
+
+renderFreshModuleInputError :: FreshModuleInputError -> Text
+renderFreshModuleInputError = \case
+ FreshModuleTextDoesNotMatchBytes ->
+ "decoded source text does not match its source bytes"
+ FreshPhysicalOwnerMismatch expected actual ->
+ "physical source owner mismatch: expected "
+ <> Text.pack (show expected)
+ <> ", got "
+ <> Text.pack (show actual)
+ FreshPhysicalLocationPathMismatch expected actual ->
+ "physical source location mismatch: expected "
+ <> Text.pack (show expected)
+ <> ", got "
+ <> Text.pack (show actual)
+
+renderParsedModuleKeyError :: Parsed.ParsedModuleKeyError -> Text
+renderParsedModuleKeyError = \case
+ Parsed.DuplicateParsedDirectSyntaxInput duplicate ->
+ "parsed module has duplicate direct syntax input "
+ <> Text.pack (show duplicate)
data ReservedParsedPrelude = ReservedParsedPrelude
!FreshModuleInput
@@ -148,7 +308,7 @@ reservedParsedPreludeModule
reservedParsedPreludeModule (ReservedParsedPrelude _input parsed) =
parsed
--- | Parse a reserved migration input through the ordinary fresh-source path.
+-- | Parse reserved final-prelude input through the ordinary fresh-source path.
parseReservedPreludeSource
:: ReservedPreludeSourceInput
-> IO (Either PreludeParseError ReservedParsedPrelude)
diff --git a/source/Felix/Source.hs b/source/Felix/Source.hs
index a30b5f9..64a88cd 100644
--- a/source/Felix/Source.hs
+++ b/source/Felix/Source.hs
@@ -25,6 +25,7 @@ module Felix.Source
, RootRequest
, searchedRoot
, existingRoot
+ , canonicalizeExistingSourcePath
, rootRequestSpelling
, ResolvedSource
, resolvedSourceCanonicalPath
@@ -230,6 +231,21 @@ existingRoot path
fmap (\canonical -> ExistingRoot canonical path) <$>
canonicalize ExistingRootCanonicalizationFailed path
+-- | Validate and canonicalize an existing source path without assigning it
+-- to a source mount.
+canonicalizeExistingSourcePath
+ :: FilePath
+ -> IO (Either SourceError CanonicalPath)
+canonicalizeExistingSourcePath path =
+ fmap extract <$> existingRoot path
+ where
+ extract = \case
+ ExistingRoot canonical _spelling ->
+ canonical
+ SearchedRoot{} ->
+ impossible
+ "canonicalizeExistingSourcePath produced a searched root"
+
-- | The user-facing spelling retained only for diagnostics.
rootRequestSpelling :: RootRequest -> FilePath
rootRequestSpelling = \case
@@ -450,6 +466,7 @@ data SourceError
!ResolvedSource
!LocationRegistrationError
| SourceImportCycle !(NonEmpty SourceCycleStep)
+ | PackagedPreludeSelectedAsOrdinarySource !ResolvedSource
| SourceGraphInvariantViolation !Text
deriving stock (Show, Eq)
@@ -551,6 +568,9 @@ renderSourceError = \case
<> sourceLabel (cycleImported step)
| step <- toList steps
]
+ PackagedPreludeSelectedAsOrdinarySource source ->
+ "the packaged final prelude cannot be used as ordinary source "
+ <> quotePath (resolvedSourceLocationPath source)
SourceGraphInvariantViolation reason ->
"source graph invariant failed: " <> reason
diff --git a/source/Felix/Store.hs b/source/Felix/Store.hs
index 973a172..bf84f6e 100644
--- a/source/Felix/Store.hs
+++ b/source/Felix/Store.hs
@@ -47,6 +47,9 @@ module Felix.Store
, newStoreMemo
, StoreMemoVisits(..)
, storeMemoVisits
+ , StoreCoordinator
+ , newStoreCoordinator
+ , withStoreCoordinator
) where
import Base
@@ -61,6 +64,11 @@ import Felix.Parsed.Identity qualified as Parsed
import Felix.Parsed.Payload qualified as ParsedPayload
import Syntax.Interface qualified as Syntax
+import Control.Concurrent.MVar
+ ( MVar
+ , newMVar
+ , withMVar
+ )
import Control.Exception qualified as Exception
import Control.Monad (foldM, unless)
import Control.Monad.Except qualified as Except
@@ -84,6 +92,18 @@ data Store = Store
!TheoryId
!SQLite.Connection
+-- | The single invocation-local gateway for a store connection and its
+-- ordinary 'IORef'-backed validation memo. Module checkers may run in
+-- parallel, but every SQLite and memo operation remains coordinator-owned.
+newtype StoreCoordinator = StoreCoordinator (MVar ())
+
+newStoreCoordinator :: IO StoreCoordinator
+newStoreCoordinator = StoreCoordinator <$> newMVar ()
+
+withStoreCoordinator :: StoreCoordinator -> IO value -> IO value
+withStoreCoordinator (StoreCoordinator ownership) action =
+ withMVar ownership (const action)
+
-- | A completely validated, inert cached module. Runtime authority is
-- minted only after this value is adopted by 'Checking.Module'.
data CachedModuleInstallation = CachedModuleInstallation
@@ -157,8 +177,6 @@ data StoreMemo = StoreMemo
, memoCheckedObjects :: !(IORef.IORef CheckedObjectClosure)
, memoValidatedPropositions :: !(IORef.IORef
(Map PropositionId CheckedPropositionContent))
- , memoSemanticInventories :: !(IORef.IORef
- (Map SemanticInterfaceId SemanticInventory))
, memoValidatedArtifacts :: !(IORef.IORef (Set ModuleArtifactId))
, memoSyntaxValidationVisits :: !(IORef.IORef Int)
, memoSemanticValidationVisits :: !(IORef.IORef Int)
@@ -167,8 +185,9 @@ data StoreMemo = StoreMemo
, memoArtifactValidationVisits :: !(IORef.IORef Int)
}
--- Complete aggregate inventories keep validation direct for the current
--- walking subset. Measure long chains before adding Phase 6 sharing.
+-- Root-scoped validation carries one flat inventory through a deterministic
+-- visited fold. Immutable rows and their validation results are memoized
+-- above, but complete transitive inventories are not retained per interface.
data SemanticInventory = SemanticInventory
!(Set SemanticFactOccurrenceFingerprint)
!(Map SemanticName SemanticFactOccurrenceFingerprint)
@@ -203,7 +222,6 @@ newStoreMemo (Store _path theory _connection) = do
validatedSemantic <- IORef.newIORef Set.empty
checkedObjects <- IORef.newIORef emptyClosure
validatedPropositions <- IORef.newIORef Map.empty
- semanticInventories <- IORef.newIORef Map.empty
validatedArtifacts <- IORef.newIORef Set.empty
syntaxVisits <- IORef.newIORef 0
semanticVisits <- IORef.newIORef 0
@@ -221,7 +239,6 @@ newStoreMemo (Store _path theory _connection) = do
, memoValidatedSemantic = validatedSemantic
, memoCheckedObjects = checkedObjects
, memoValidatedPropositions = validatedPropositions
- , memoSemanticInventories = semanticInventories
, memoValidatedArtifacts = validatedArtifacts
, memoSyntaxValidationVisits = syntaxVisits
, memoSemanticValidationVisits = semanticVisits
@@ -1654,7 +1671,6 @@ validateModuleArtifactClosure memo store root = do
(moduleArtifactResultSemantic artifact)
void
(validateSemanticInventory
- Set.empty
(moduleArtifactResultSemantic artifact))
case checked of
Left failure ->
@@ -1734,6 +1750,8 @@ validateModuleArtifactClosure memo store root = do
traverse_
(validateSemantic (Set.insert identity path))
(semanticInterfaceDirectInputs interface)
+ operationBindings <-
+ semanticOperationBindings Set.empty identity
validateObjectRoots objects
closure <- Except.liftIO
(IORef.readIORef (memoCheckedObjects memo))
@@ -1745,7 +1763,7 @@ validateModuleArtifactClosure memo store root = do
(semanticGlobalBindingKey binding)
(semanticGlobalBindingTarget binding))
(validateSemanticGlobalBindingTarget
- closure binding)))
+ operationBindings closure binding)))
bindings
traverse_ validateProposition propositions
traverse_ validateOccurrence
@@ -1758,6 +1776,33 @@ validateModuleArtifactClosure memo store root = do
(memoValidatedSemantic memo)
(Set.insert identity))
+ semanticOperationBindings path identity
+ | identity `Set.member` path = pure Set.empty
+ | otherwise = do
+ interface <- requireMemo
+ SemanticInterfaces
+ (cacheDigestBytes
+ (semanticInterfaceIdDigest identity))
+ (memoSemantic memo store identity)
+ inherited <-
+ traverse
+ (semanticOperationBindings
+ (Set.insert identity path))
+ (semanticInterfaceDirectInputs interface)
+ let local =
+ Set.fromList
+ [ ( semanticStructureOperationSymbol operation
+ , semanticStructureOperationObject operation
+ )
+ | declaration <-
+ semanticInterfaceDeclarations interface
+ , descriptor <- semanticEnvironmentStructures
+ (declarationDeltaEnvironment declaration)
+ , operation <-
+ semanticStructureDescriptorOperations descriptor
+ ]
+ pure (Set.unions (local : inherited))
+
validateObjectRoots identities = do
closure <- Except.liftIO
(IORef.readIORef (memoCheckedObjects memo))
@@ -1843,83 +1888,57 @@ validateModuleArtifactClosure memo store root = do
proposition
(semanticFactAuthority occurrence))))
- validateSemanticInventory path identity = do
- inventories <- Except.liftIO
- (IORef.readIORef (memoSemanticInventories memo))
- case Map.lookup identity inventories of
- Just inventory ->
- pure inventory
- Nothing
- | identity `Set.member` path ->
- pure
- (SemanticInventory
- Set.empty Map.empty Map.empty)
- | otherwise -> do
- interface <- requireMemo
- SemanticInterfaces
- (cacheDigestBytes
- (semanticInterfaceIdDigest identity))
- (memoSemantic memo store identity)
- parents <- traverse
- (validateSemanticInventory
- (Set.insert identity path))
- (semanticInterfaceDirectInputs interface)
- SemanticInventory
- parentFacts parentAliases parentGlobals <-
- foldM mergeInventory
- (SemanticInventory
- Set.empty Map.empty Map.empty)
- parents
- let declarations =
- semanticInterfaceDeclarations interface
- localFacts = Set.fromList
- [ semanticFactFingerprint occurrence
- | declaration <- declarations
- , occurrence <- declarationDeltaFacts declaration
- ]
- visibleFacts = parentFacts <> localFacts
- aliases <- foldM
- (insertAlias visibleFacts)
- parentAliases
- [ alias
- | declaration <- declarations
- , alias <- declarationDeltaAliases declaration
- ]
- globals <- foldM
- insertGlobal
- parentGlobals
- [ binding
- | declaration <- declarations
- , binding <- semanticEnvironmentBindings
- (declarationDeltaEnvironment declaration)
- ]
- let inventory =
- SemanticInventory
- visibleFacts aliases globals
- Except.liftIO
- (IORef.modifyIORef'
- (memoSemanticInventories memo)
- (Map.insert identity inventory))
- pure inventory
-
- mergeInventory
- (SemanticInventory facts aliases globals)
- (SemanticInventory moreFacts moreAliases moreGlobals) = do
- merged <- foldM
- (\current (name, target) ->
- insertNamedAlias name target current)
- aliases
- (Map.toAscList moreAliases)
- mergedGlobals <- foldM
- (\current (key, target) ->
- insertGlobalBinding key target current)
- globals
- (Map.toAscList moreGlobals)
- pure
- (SemanticInventory
- (facts <> moreFacts)
- merged
- mergedGlobals)
+ validateSemanticInventory identity =
+ snd
+ <$> foldSemanticInventory
+ Set.empty
+ (SemanticInventory Set.empty Map.empty Map.empty)
+ identity
+
+ foldSemanticInventory visited inventory identity
+ | identity `Set.member` visited =
+ pure (visited, inventory)
+ | otherwise = do
+ interface <- requireMemo
+ SemanticInterfaces
+ (cacheDigestBytes
+ (semanticInterfaceIdDigest identity))
+ (memoSemantic memo store identity)
+ (parentVisited, parentInventory) <-
+ foldM
+ (\(seen, current) parent ->
+ foldSemanticInventory seen current parent)
+ (Set.insert identity visited, inventory)
+ (semanticInterfaceDirectInputs interface)
+ let declarations = semanticInterfaceDeclarations interface
+ SemanticInventory
+ parentFacts parentAliases parentGlobals =
+ parentInventory
+ localFacts = Set.fromList
+ [ semanticFactFingerprint occurrence
+ | declaration <- declarations
+ , occurrence <- declarationDeltaFacts declaration
+ ]
+ visibleFacts = parentFacts <> localFacts
+ aliases <- foldM
+ (insertAlias visibleFacts)
+ parentAliases
+ [ alias
+ | declaration <- declarations
+ , alias <- declarationDeltaAliases declaration
+ ]
+ globals <- foldM
+ insertGlobal
+ parentGlobals
+ [ binding
+ | declaration <- declarations
+ , binding <- semanticEnvironmentBindings
+ (declarationDeltaEnvironment declaration)
+ ]
+ pure
+ ( parentVisited
+ , SemanticInventory visibleFacts aliases globals
+ )
insertGlobal globals binding =
insertGlobalBinding
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 07:35:11 +0000