Support contextual exact abbreviations

1 files changed, 62 insertions, 26 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index afedbe9..dcefe5d 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -28,6 +28,7 @@ module Checking.Declaration
     , resolvedStructureOperation
     , resolvedStructureOperations
     , resolveVisibleStructureDriver
+    , resolveVisibleStructureOperationObjectsDriver
     , objectAvailableDriver
     , objectTypeDriver
     , runModuleDriver
@@ -135,7 +136,7 @@ import Data.ByteString qualified as ByteString
 import Data.List qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
-import Data.Maybe (catMaybes)
+import Data.Maybe (catMaybes, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Unique (Unique, newUnique)
@@ -264,6 +265,17 @@ resolvedStructureOperations (ResolvedStructure _ _ operations) =
   where
     operationObject (ResolvedStructureOperation object _origin) = object
 
+structureOperationBindings
+    :: Map SemanticStructurePhrase ResolvedStructure
+    -> Set (StructSymbol, ObjectId)
+structureOperationBindings structures =
+    Set.fromList
+        [ (symbol, object)
+        | structure <- Map.elems structures
+        , (symbol, object) <-
+            Map.toAscList (resolvedStructureOperations structure)
+        ]
+
 
 data CommittedDeclarationBatch = CommittedDeclarationBatch
     !ModuleName
@@ -647,9 +659,11 @@ validateEvidenceInventory
     -> ImportedModuleEvidence
     -> Either DeclarationError ()
 validateEvidenceInventory theory closure evidence =
-    void (foldEvidence Set.empty Map.empty Map.empty evidence)
-        *> void (foldGlobals Set.empty Map.empty evidence)
-        *> void (foldStructures Set.empty Map.empty evidence)
+    do
+        void (foldEvidence Set.empty Map.empty Map.empty evidence)
+        (_seen, structures) <-
+            foldStructures Set.empty Map.empty evidence
+        void (foldGlobals structures Set.empty Map.empty evidence)
   where
     foldEvidence seen facts aliases current
         | identity `Set.member` seen =
@@ -731,19 +745,20 @@ validateEvidenceInventory theory closure evidence =
                         (ImportedAliasCollision
                             name existingOrigin origin)
 
-    foldGlobals seen globals current
+    foldGlobals structures seen globals current
         | identity `Set.member` seen =
             Right (seen, globals)
         | otherwise = do
             (parentsSeen, parentGlobals) <-
                 foldM
                     (\(seen', globals') parent ->
-                        foldGlobals seen' globals' parent)
+                        foldGlobals structures seen' globals' parent)
                     (seen, globals)
                     parents
             globals' <-
                 foldM
-                    (insertGlobal current)
+                    (insertGlobal
+                        (structureOperationBindings structures))
                     parentGlobals
                     [ binding
                     | delta <- semanticInterfaceDeclarations interface
@@ -755,13 +770,15 @@ validateEvidenceInventory theory closure evidence =
         ImportedModuleEvidence interface parents _entries _objects = current
         identity = semanticInterfaceAssertedId interface
 
-    insertGlobal _current globals binding = do
+    insertGlobal operationBindings globals binding = do
         let key = semanticGlobalBindingKey binding
             target = semanticGlobalBindingTarget binding
         _ <-
             first
                 (ImportedGlobalTargetInvalid key target)
-                (validateSemanticGlobalBindingTarget closure binding)
+                (validateSemanticGlobalBindingTarget
+                    operationBindings
+                    closure binding)
         case Map.lookup key globals of
             Nothing -> Right (Map.insert key target globals)
             Just existing
@@ -967,8 +984,12 @@ resolveVisibleGlobalDriver
 resolveVisibleGlobalDriver key = ModuleDriver do
     DriverState _resolver builder _prefix _validation <- State.get
     pure
-        ( (\(target, content, _dependencies) ->
-                (target, objectContentType content))
+        ( (\(target, _content, _dependencies) ->
+                ( target
+                , fromMaybe
+                    (impossible "visible semantic key has no source type")
+                    (semanticGlobalKeyType key)
+                ))
             <$> resolveVisibleGlobalContent builder key
         )
 
@@ -991,6 +1012,19 @@ resolveVisibleStructureDriver structurePhrase = ModuleDriver do
     DriverState _resolver builder _prefix _validation <- State.get
     pure (Map.lookup structurePhrase (logicalBuilderStructures builder))
 
+resolveVisibleStructureOperationObjectsDriver
+    :: StructSymbol
+    -> ModuleDriver failure [ObjectId]
+resolveVisibleStructureOperationObjectsDriver symbol = ModuleDriver do
+    DriverState _resolver builder _prefix _validation <- State.get
+    pure
+        ( Set.toAscList
+            (Set.fromList
+                (mapMaybe
+                    (resolvedStructureOperation symbol)
+                    (Map.elems (logicalBuilderStructures builder))))
+        )
+
 resolveVisibleGlobalContent
     :: LogicalBuilder
     -> SemanticGlobalKey
@@ -1193,10 +1227,7 @@ resolveVisibleGlobal key = Declaration do
     let builder = declarationBuilder state
     pure do
         target <- Map.lookup key (logicalBuilderGlobals builder)
-        coreType <-
-            lookupCheckedObjectType
-                (semanticGlobalTargetObject target)
-                (logicalBuilderObjectClosure builder)
+        coreType <- semanticGlobalKeyType key
         pure (target, coreType)
 
 stageSemanticGlobalBinding
@@ -2200,14 +2231,6 @@ foldImportedEvidence evidence builder
             | delta <- semanticInterfaceDeclarations interface
             , alias <- declarationDeltaAliases delta
             ]
-        importedGlobals <- foldM
-            (insertImportedGlobal objectClosure)
-            (logicalBuilderGlobals withParents)
-            [ binding
-            | delta <- semanticInterfaceDeclarations interface
-            , binding <- semanticEnvironmentBindings
-                (declarationDeltaEnvironment delta)
-            ]
         importedStructures <- foldM
             (insertSemanticStructure objectClosure)
             (logicalBuilderStructures withParents)
@@ -2216,6 +2239,14 @@ foldImportedEvidence evidence builder
             , descriptor <- semanticEnvironmentStructures
                 (declarationDeltaEnvironment delta)
             ]
+        importedGlobals <- foldM
+            (insertImportedGlobal objectClosure importedStructures)
+            (logicalBuilderGlobals withParents)
+            [ binding
+            | delta <- semanticInterfaceDeclarations interface
+            , binding <- semanticEnvironmentBindings
+                (declarationDeltaEnvironment delta)
+            ]
         pure
             withParents
                 { logicalBuilderFacts = importedFacts
@@ -2291,13 +2322,15 @@ foldImportedEvidence evidence builder
                         (ImportedAliasCollision
                             name existingOrigin origin)
 
-    insertImportedGlobal closure globals binding = do
+    insertImportedGlobal closure structures globals binding = do
         let key = semanticGlobalBindingKey binding
             target = semanticGlobalBindingTarget binding
         _ <-
             first
                 (ImportedGlobalTargetInvalid key target)
-                (validateSemanticGlobalBindingTarget closure binding)
+                (validateSemanticGlobalBindingTarget
+                    (structureOperationBindings structures)
+                    closure binding)
         case Map.lookup key globals of
             Nothing -> pure (Map.insert key target globals)
             Just existing
@@ -3665,7 +3698,10 @@ appendDeclaration mode declaration = do
                 (DeclarationGlobalTargetInvalid
                     (semanticGlobalBindingKey binding)
                     (semanticGlobalBindingTarget binding))
-                (validateSemanticGlobalBindingTarget closure binding))
+                (validateSemanticGlobalBindingTarget
+                    (structureOperationBindings
+                        (logicalBuilderStructures builder))
+                    closure binding))
         bindings
     traverse_
         (\descriptor ->