Support contextual exact abbreviations

2 files changed, 190 insertions, 2 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index c6237b8..e5b8a4f 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -88,6 +88,8 @@ unitTests =
             compilesExactDeclarationGraph
         , testCase "compiles and imports exact structures"
             compilesExactStructures
+        , testCase "compiles and caches contextual abbreviations"
+            compilesContextualAbbreviations
         , testCase "rejects an unknown exact structure parent atomically"
             rejectsUnknownExactStructureParent
         , testCase "compiles exact relation expressions"
@@ -1630,6 +1632,186 @@ compilesExactStructures = do
                     . Declaration.committedBatchDelta)
                 batches)
 
+compilesContextualAbbreviations :: Assertion
+compilesContextualAbbreviations = do
+    foundation <- expectRight Foundation.checkedFoundation
+    repository <- getCurrentDirectory
+    Temp.withSystemTempDirectory "felix-contextual-abbreviation" \directory -> do
+        let storePath = directory Posix.</> "store.sqlite"
+            executable = directory Posix.</> "vampire"
+            relative = "test/phase5/exact-contextual-abbreviation.tex"
+        writeAcceptedFixtureVampire executable
+        runs <- newIORef (0 :: Int)
+        let resolver = countingAcceptedResolver executable runs
+        (_startup, store) <-
+            Store.openStore storePath (Identity.theoryId foundation)
+                >>= expectRight
+        bracket (pure store) Store.closeStore \opened -> do
+            prelude <-
+                expectRight
+                    =<< Module.buildFinalPreludeSession
+                        opened foundation resolver
+            mounts <- exactFixtureMounts repository
+            workspace <- parseFinalExactWorkspace prelude mounts relative
+            sealed <- sole "contextual abbreviation module"
+                =<< compileFinalParsedWorkspaceWithResolver
+                    foundation prelude resolver workspace
+            let deltas =
+                    Semantic.semanticInterfaceDeclarations
+                        (Module.sealedTypedModuleSemantic sealed)
+                contextualTargets =
+                    [ (identity, requirements)
+                    | delta <- deltas
+                    , binding <- Semantic.semanticEnvironmentBindings
+                        (Semantic.declarationDeltaEnvironment delta)
+                    , Semantic.ContextualTransparentExpansion
+                            identity requirements <-
+                        [Semantic.semanticGlobalBindingTarget binding]
+                    ]
+            assertEqual "contextual target count" 2
+                (length contextualTargets)
+            requirements <-
+                sole "canonical contextual requirement set"
+                    (nubOrd (snd <$> contextualTargets))
+            assertEqual "one structure operation requirement" 1
+                (Map.size requirements)
+            let batches =
+                    Declaration.pendingModulePrefixBatches
+                        (Module.sealedTypedModulePrefix sealed)
+            traverse_
+                (assertReflexiveFact batches)
+                [ "phase5_context_dot_explicit"
+                , "phase5_context_inherited"
+                , "phase5_context_nested"
+                , "phase5_context_explicit_unique"
+                ]
+
+            parsed <- pure (Parse.parsedWorkspaceRootModule workspace)
+            let syntax = Module.sealedTypedModuleSyntax sealed
+                semantic = Module.sealedTypedModuleSemantic sealed
+            key <- expectRight
+                (Semantic.moduleArtifactKey
+                    (moduleName (Parse.parsedModuleAddress parsed))
+                    (Parse.parsedModuleId parsed)
+                    (Semantic.semanticInterfaceDirectInputs semantic)
+                    (Identity.theoryId foundation))
+            let artifact =
+                    Semantic.moduleArtifactResult
+                        key
+                        (Syntax.moduleSyntaxAssertedId syntax)
+                        (Semantic.semanticInterfaceAssertedId semantic)
+            void
+                (expectRight
+                    =<< Store.writeSealedModule
+                        opened
+                        (Module.sealedTypedModulePrefix sealed)
+                        [syntax]
+                        [semantic]
+                        artifact)
+            memo <- Store.newStoreMemo opened
+            loaded <- expectRight
+                =<< Store.loadCachedModuleInstallation
+                    memo opened key
+                    (Syntax.moduleSyntaxAssertedId
+                        (Parse.parsedModuleSyntaxInterface parsed))
+            installation <- maybe
+                (assertFailure "contextual cached installation is absent"
+                    >> fail "unreachable")
+                pure
+                loaded
+            cached <- expectRight
+                (Module.cachedSealedTypedModule
+                    foundation
+                    [Module.migrationPreludeModule prelude]
+                    installation)
+            assertEqual "cached contextual semantic target"
+                semantic
+                (Module.sealedTypedModuleSemantic cached)
+
+            verifyFailure foundation resolver prelude mounts sealed
+                "test/phase5/exact-contextual-abbreviation-missing.tex"
+                (\case
+                    Exact.ExactContextualExpansionNotAvailable location _key ->
+                        assertEqual "missing context line" 5 (locLine location)
+                    failure ->
+                        assertFailure
+                            ("unexpected missing-context failure: "
+                                <> show failure))
+            verifyFailure foundation resolver prelude mounts sealed
+                "test/phase5/exact-contextual-abbreviation-ambiguous.tex"
+                (\case
+                    Exact.ExactStructureOperationAmbiguous
+                            location _symbol objects -> do
+                        assertEqual "ambiguous operation line" 16
+                            (locLine location)
+                        assertEqual "two distinct operation objects" 2
+                            (length objects)
+                    failure ->
+                        assertFailure
+                            ("unexpected operation ambiguity failure: "
+                                <> show failure))
+  where
+    assertReflexiveFact batches marker = do
+        batch <- maybe
+            (assertFailure ("missing contextual fact " <> marker)
+                >> fail "unreachable")
+            pure
+            (find
+                (elem (Semantic.semanticName (StrictText.pack marker))
+                    . fmap Semantic.semanticAliasName
+                    . Semantic.declarationDeltaAliases
+                    . Declaration.committedBatchDelta)
+                batches)
+        proposition <- sole (marker <> " proposition")
+            (Declaration.committedBatchPropositions batch)
+        let body = stripClaimEnvelope
+                (Core.frozenCoreTerm
+                    (Identity.checkedPropositionTerm proposition))
+        case body of
+            Core.CEq _ left right ->
+                assertEqual (marker <> " canonical sides") left right
+            _ ->
+                assertFailure
+                    (marker <> " did not elaborate to reflexive equality: "
+                        <> show body)
+
+    stripClaimEnvelope = \case
+        Core.CForall _ body -> stripClaimEnvelope body
+        Core.CImp _ body -> stripClaimEnvelope body
+        term -> term
+
+    verifyFailure foundation resolver prelude mounts imported relative checkFailure = do
+        workspace <- parseFinalExactWorkspace prelude mounts relative
+        let parsed = Parse.parsedWorkspaceRootModule workspace
+        input <- expectRight
+            (Module.typedModuleInput
+                foundation
+                (Module.finalPreludeReadiness prelude)
+                resolver
+                Declaration.FreshValidation
+                parsed
+                [imported])
+        Module.runTypedModule input >>= \case
+            Module.TypedModuleFailed
+                    (Module.TypedActionFailed
+                        (Module.TypedExactCompileFailed failure))
+                    _prefix ->
+                checkFailure failure
+            Module.TypedModuleFailed
+                    (Module.TypedActionFailed
+                        (Module.TypedExactProofFailed
+                            (ExactProof.ExactProofElaborationFailed failure)))
+                    _prefix ->
+                checkFailure failure
+            Module.TypedModuleSucceeded{} ->
+                assertFailure (relative <> " was unexpectedly accepted")
+            Module.TypedModuleOpenFailed failure ->
+                assertFailure
+                    (relative <> " did not open: " <> show failure)
+            Module.TypedModuleFailed failure _prefix ->
+                assertFailure
+                    (relative <> " failed unexpectedly: " <> show failure)
+
 rejectsUnknownExactStructureParent :: Assertion
 rejectsUnknownExactStructureParent =
     Temp.withSystemTempDirectory "felix-exact-structure-parent" \root -> do
@@ -3439,7 +3621,8 @@ assertExactDatatypeModule label sealed = do
             (\binding ->
                 case Semantic.semanticGlobalBindingTarget binding of
                     Semantic.GlobalReference{} -> True
-                    Semantic.TransparentExpansion{} -> False)
+                    Semantic.TransparentExpansion{} -> False
+                    Semantic.ContextualTransparentExpansion{} -> False)
             bindings)
     assertEqual (label <> " datatype global targets")
         (Set.fromList objectIds)
diff --git a/source/Test/Unit/Semantic.hs b/source/Test/Unit/Semantic.hs
index 4affb41..160735c 100644
--- a/source/Test/Unit/Semantic.hs
+++ b/source/Test/Unit/Semantic.hs
@@ -19,6 +19,7 @@ import Syntax.Abstract qualified as Raw
 
 import Data.ByteString (ByteString)
 import Data.List qualified as List
+import Data.Map.Strict qualified as Map
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -104,7 +105,11 @@ roundTripsSemanticGlobalKeys = do
                     first : rest ->
                         Semantic.semanticGlobalBinding
                             first
-                            (Semantic.TransparentExpansion target)
+                            (Semantic.ContextualTransparentExpansion
+                                target
+                                (Map.singleton
+                                    (Raw.StructSymbol "operation")
+                                    target))
                             : [ Semantic.semanticGlobalBinding
                                     key
                                     (Semantic.GlobalReference target)