Correct exact semantic resolution

1 files changed, 206 insertions, 31 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 82ee35e..224c1cd 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -7,6 +7,7 @@ import Api qualified
 import Checking.Authority qualified as Authority
 import Checking.Core qualified as Core
 import Checking.Declaration qualified as Declaration
+import Checking.Exact qualified as Exact
 import Checking.Foundation qualified as Foundation
 import Checking.Identity qualified as Identity
 import Checking.Module qualified as Module
@@ -22,6 +23,7 @@ import Felix.Source.Content qualified as Content
 import Felix.Store qualified as Store
 import Report.Location
 import Provers qualified
+import Syntax.Abstract qualified as Raw
 import Syntax.Internal qualified as Internal
 import Syntax.Interface qualified as Syntax
 
@@ -34,6 +36,7 @@ import Data.Text.Encoding qualified as Text
 import Control.Monad.Logger (runNoLoggingT)
 import Data.IORef (modifyIORef', newIORef, readIORef)
 import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
 import System.Directory (createDirectoryIfMissing, getCurrentDirectory)
 import System.FilePath.Posix qualified as Posix
 import System.IO.Temp qualified as Temp
@@ -58,6 +61,8 @@ unitTests =
             rejectsUnsupportedTypedSource
         , testCase "compiles exact declarations across an import"
             compilesExactDeclarationGraph
+        , testCase "rejects declarations of fixed semantics"
+            rejectsFixedSemanticDeclaration
         , testCase "keeps exact semantics independent of fixity"
             keepsExactSemanticsIndependentOfFixity
         , testCase "loads a cached exact producer for a fresh importer"
@@ -406,7 +411,7 @@ compilesExactDeclarationGraph = do
                 [1]
                 (bindingCount <$> importerDeltas)
             assertEqual "producer object families"
-                ["opaque", "transparent", "transparent"]
+                ["opaque", "transparent"]
                 [ objectFamilyName
                     (Identity.assertedObjectContent object)
                 | batch <- producerBatches
@@ -455,29 +460,46 @@ compilesExactDeclarationGraph = do
                 (take 1 (drop 1 producerDeltas))
             aliasBinding <- sole "producer abbreviation binding"
                 (bindings aliasDelta)
+            seedDelta <- sole "producer signature delta"
+                (take 1 producerDeltas)
+            seedBinding <- sole "producer signature binding"
+                (bindings seedDelta)
+            let seedTarget =
+                    Semantic.semanticGlobalTargetObject
+                        (Semantic.semanticGlobalBindingTarget seedBinding)
+                aliasTarget =
+                    Semantic.semanticGlobalTargetObject
+                        (Semantic.semanticGlobalBindingTarget aliasBinding)
+                definitionTarget =
+                    Semantic.semanticGlobalTargetObject
+                        (Semantic.semanticGlobalBindingTarget
+                            definitionBinding)
             assertEqual "abbreviation expands transparently"
                 (Semantic.TransparentExpansion
-                    (Semantic.semanticGlobalTargetObject
-                        (Semantic.semanticGlobalBindingTarget aliasBinding)))
+                    aliasTarget)
                 (Semantic.semanticGlobalBindingTarget aliasBinding)
             assertEqual "definition remains a named global"
-                (Semantic.GlobalReference
-                    (Semantic.semanticGlobalTargetObject
-                        (Semantic.semanticGlobalBindingTarget
-                            definitionBinding)))
+                (Semantic.GlobalReference definitionTarget)
                 (Semantic.semanticGlobalBindingTarget definitionBinding)
-            definitionObject <- sole "producer definition object"
+            assertEqual "definition content coalesces with its expansion"
+                aliasTarget
+                definitionTarget
+            assertEqual "coalesced definition adds no object"
+                []
                 (Declaration.committedBatchObjects definitionBatch)
-            let aliasTarget =
-                    Semantic.semanticGlobalTargetObject
-                        (Semantic.semanticGlobalBindingTarget aliasBinding)
-            case Identity.assertedObjectContent definitionObject of
+            aliasBatch <- sole "producer abbreviation batch"
+                (take 1 (drop 1 producerBatches))
+            aliasObject <- sole "producer abbreviation object"
+                (Declaration.committedBatchObjects aliasBatch)
+            case Identity.assertedObjectContent aliasObject of
                 Identity.TransparentObjectContent _theory _coreType body ->
-                    assertBool "definition resolves the producer alias"
-                        (aliasTarget `elem` canonicalGlobals body)
+                    assertEqual
+                        "expanded body retains only the opaque seed"
+                        (Set.singleton seedTarget)
+                        (Core.canonicalTermGlobals body)
                 content ->
                     assertFailure
-                        ("definition object is not transparent: "
+                        ("abbreviation object is not transparent: "
                             <> show content)
             importerBatch <- sole "importer declaration batch" importerBatches
             importerDelta <- sole "importer semantic delta" importerDeltas
@@ -505,6 +527,64 @@ compilesExactDeclarationGraph = do
         Identity.TransparentObjectContent{} -> "transparent"
         Identity.IntrinsicObjectContent{} -> "intrinsic"
 
+rejectsFixedSemanticDeclaration :: Assertion
+rejectsFixedSemanticDeclaration =
+    Temp.withSystemTempDirectory "felix-fixed-semantic" \root -> do
+        let relative = "entry.tex"
+            path = root Posix.</> relative
+            source =
+                "\\begin{signature}\\label{source_unions}\n"
+                    <> "    $\\unions{X}$ is a set.\n"
+                    <> "\\end{signature}\n"
+        ByteString.writeFile path
+            (Text.encodeUtf8 (StrictText.pack source))
+        foundation <- expectRight Foundation.checkedFoundation
+        bootstrap <-
+            expectRight
+                =<< Module.buildBootstrapPreludeSession
+                    foundation unusedResolver
+        mounts <- exactFixtureMounts root
+        workspace <- parseExactWorkspace bootstrap mounts relative
+        let parsed = Parse.parsedWorkspaceRootModule workspace
+        input <- expectRight
+            (Module.typedModuleInput
+                foundation
+                (Module.bootstrapWalkingReadiness bootstrap)
+                unusedResolver
+                Declaration.FreshValidation
+                parsed
+                [])
+        Module.runTypedModule input >>= \case
+            Module.TypedModuleFailed
+                    (Module.TypedActionFailed
+                        (Module.TypedExactCompileFailed
+                            (Exact.ExactFixedSemanticCollision
+                                location key)))
+                    prefix -> do
+                assertEqual "fixed collision line" 1 (locLine location)
+                assertEqual "fixed collision key"
+                    (Semantic.SemanticExpressionFunction
+                        (Raw.TokenCons (Raw.Command "unions")
+                            (Raw.TokenCons Raw.InvisibleBraceL
+                                (Raw.HoleCons
+                                    (Raw.TokenCons
+                                        Raw.InvisibleBraceR Raw.End)))))
+                    key
+                assertEqual "fixed collision commits no prefix"
+                    0
+                    (length
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Module.TypedModuleSucceeded{} ->
+                assertFailure "fixed semantic declaration was accepted"
+            Module.TypedModuleOpenFailed failure ->
+                assertFailure
+                    ("fixed semantic module did not open: "
+                        <> show failure)
+            Module.TypedModuleFailed failure _prefix ->
+                assertFailure
+                    ("unexpected fixed semantic failure: "
+                        <> show failure)
+
 keepsExactSemanticsIndependentOfFixity :: Assertion
 keepsExactSemanticsIndependentOfFixity =
     Temp.withSystemTempDirectory "felix-exact-fixity" \root -> do
@@ -575,6 +655,117 @@ loadsCachedExactProducerForFreshImporter = do
         assertEqual "exact declarations issue no Vampire requests"
             0
             =<< readIORef observed
+        bootstrap <-
+            expectRight
+                =<< Module.buildBootstrapPreludeSession
+                    foundation unusedResolver
+        repository <- getCurrentDirectory
+        mounts <- exactFixtureMounts repository
+        workspace <- parseExactWorkspace
+            bootstrap mounts "test/phase5/exact-importer.tex"
+        let parsedModules =
+                toList
+                    (Parse.parsedWorkspaceImportedBeforeImporter workspace)
+            preludeSemantic =
+                Module.sealedTypedModuleSemantic
+                    (Module.migrationPreludeModule bootstrap)
+            preludeId =
+                Semantic.semanticInterfaceAssertedId preludeSemantic
+            theory = Identity.theoryId foundation
+            loadInstallation memo parsed direct = do
+                key <- expectRight
+                    (Semantic.moduleArtifactKey
+                        (moduleName (Parse.parsedModuleAddress parsed))
+                        (Parse.parsedModuleId parsed)
+                        direct
+                        theory)
+                loaded <- expectRight
+                    =<< Store.loadCachedModuleInstallation
+                        memo
+                        store
+                        key
+                        (Syntax.moduleSyntaxAssertedId
+                            (Parse.parsedModuleSyntaxInterface parsed))
+                maybe
+                    (assertFailure "exact cached installation is absent"
+                        >> fail "unreachable")
+                    pure
+                    loaded
+            environmentBindings installation =
+                [ binding
+                | delta <- Semantic.semanticInterfaceDeclarations
+                    (Store.cachedInstallationSemantic installation)
+                , binding <- Semantic.semanticEnvironmentBindings
+                    (Semantic.declarationDeltaEnvironment delta)
+                ]
+        case parsedModules of
+            [producerParsed, importerParsed] -> do
+                memo <- Store.newStoreMemo store
+                producerInstallation <-
+                    loadInstallation memo producerParsed [preludeId]
+                let producerSemanticId =
+                        Semantic.semanticInterfaceAssertedId
+                            (Store.cachedInstallationSemantic
+                                producerInstallation)
+                importerInstallation <-
+                    loadInstallation
+                        memo importerParsed [preludeId, producerSemanticId]
+                case ( environmentBindings producerInstallation
+                     , environmentBindings importerInstallation
+                     ) of
+                    (seedBinding : aliasBinding : _definitionBinding : [],
+                     [importerBinding]) -> do
+                        let seedTarget =
+                                Semantic.semanticGlobalTargetObject
+                                    (Semantic.semanticGlobalBindingTarget
+                                        seedBinding)
+                            aliasTarget =
+                                Semantic.semanticGlobalTargetObject
+                                    (Semantic.semanticGlobalBindingTarget
+                                        aliasBinding)
+                            importerTarget =
+                                Semantic.semanticGlobalTargetObject
+                                    (Semantic.semanticGlobalBindingTarget
+                                        importerBinding)
+                        assertEqual "cached importer reuses expanded content"
+                            aliasTarget importerTarget
+                        assertEqual "cached importer adds no object"
+                            []
+                            (Store.cachedInstallationObjects
+                                importerInstallation)
+                        expandedObject <-
+                            maybe
+                                (assertFailure
+                                    "cached expanded object is absent"
+                                    >> fail "unreachable")
+                                pure
+                                (find
+                                    ((== aliasTarget)
+                                        . Identity.assertedObjectId)
+                                    (Store.cachedInstallationObjects
+                                        producerInstallation))
+                        case Identity.assertedObjectContent expandedObject of
+                            Identity.TransparentObjectContent
+                                    _identity _coreType body ->
+                                assertEqual
+                                    "cached expansion retains the opaque seed"
+                                    (Set.singleton seedTarget)
+                                    (Core.canonicalTermGlobals body)
+                            content ->
+                                assertFailure
+                                    ("cached expansion is not transparent: "
+                                        <> show content)
+                    (producerBindings, importerBindings) ->
+                        assertFailure
+                            ("unexpected cached exact bindings: "
+                                <> show
+                                    ( length producerBindings
+                                    , length importerBindings
+                                    ))
+            modules ->
+                assertFailure
+                    ("unexpected cached exact module count: "
+                        <> show (length modules))
         Store.closeStore store
 
 retainsExactPrefixBeforeFailure :: Assertion
@@ -927,22 +1118,6 @@ compileParsedWorkspace foundation bootstrap workspace =
             , 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 ->