Support contextual exact abbreviations

13 files changed, 723 insertions, 95 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 ->
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs
index 5d7ed52..9c34eed 100644
--- a/source/Checking/Exact.hs
+++ b/source/Checking/Exact.hs
@@ -244,7 +244,7 @@ data PreparedExactDeclaration = PreparedExactDeclaration
     !Location
     !ExactDeclarationFamily
     !SemanticGlobalKey
-    !ObjectId
+    !SemanticGlobalTarget
     !(Maybe AssertedObject)
     !(Maybe SemanticName)
     !DeclarationSyntaxId
@@ -262,7 +262,7 @@ preparedExactGlobalKey
 preparedExactObjectId :: PreparedExactDeclaration -> ObjectId
 preparedExactObjectId
         (PreparedExactDeclaration _location _family _key target _object _alias _syntax) =
-    target
+    semanticGlobalTargetObject target
 
 preparedExactObject
     :: PreparedExactDeclaration
@@ -288,11 +288,8 @@ preparedExactGlobalTarget
     -> SemanticGlobalTarget
 preparedExactGlobalTarget
         (PreparedExactDeclaration
-            _location family _key target _object _alias _syntax) =
-    case family of
-        ExactSignature -> GlobalReference target
-        ExactAbbreviation -> TransparentExpansion target
-        ExactDefinition -> GlobalReference target
+            _location _family _key target _object _alias _syntax) =
+    target
 
 preparedDefinitionAlias
     :: PreparedExactDeclaration
@@ -347,8 +344,13 @@ data ExactCompileError
     | ExactStructureNotVisible !Location !SemanticStructurePhrase
     | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase
     | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol
-    | ExactStructureArgumentNotAnnotated !Location
     | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol
+    | ExactStructureOperationAmbiguous
+        !Location !Raw.StructSymbol ![ObjectId]
+    | ExactContextualExpansionNotAvailable
+        !Location !SemanticGlobalKey
+    | ExactContextualRequirementConflict
+        !Location !Raw.StructSymbol !ObjectId !ObjectId
     | ExactStructureOccurrenceMismatch !Location
     | ExactStructureSelfParent !Location !SemanticStructurePhrase
     | ExactStructureDuplicateParent !Location !SemanticStructurePhrase
@@ -388,8 +390,10 @@ exactCompileErrorLocation = \case
     ExactStructureNotVisible location _phrase -> location
     ExactBaseStructureNotAssertable location _phrase -> location
     ExactDuplicateStructureAnnotation location _variable -> location
-    ExactStructureArgumentNotAnnotated location -> location
     ExactStructureOperationNotAvailable location _symbol -> location
+    ExactStructureOperationAmbiguous location _symbol _objects -> location
+    ExactContextualExpansionNotAvailable location _key -> location
+    ExactContextualRequirementConflict location _symbol _first _second -> location
     ExactStructureOccurrenceMismatch location -> location
     ExactStructureSelfParent location _phrase -> location
     ExactStructureDuplicateParent location _phrase -> location
@@ -455,11 +459,19 @@ renderExactCompileError = \case
     ExactDuplicateStructureAnnotation location variable ->
         at location <> "the structure binder " <> shown variable
             <> " is annotated more than once"
-    ExactStructureArgumentNotAnnotated location ->
-        at location <> "the structure operation argument has no active structure annotation"
     ExactStructureOperationNotAvailable location symbol ->
         at location <> "the structure operation " <> shown symbol
             <> " is not available in the active structure scope"
+    ExactStructureOperationAmbiguous location symbol objects ->
+        at location <> "the structure operation " <> shown symbol
+            <> " is ambiguous between " <> shown objects
+    ExactContextualExpansionNotAvailable location key ->
+        at location <> "the contextual abbreviation " <> shown key
+            <> " has no compatible active structure"
+    ExactContextualRequirementConflict location symbol firstObject secondObject ->
+        at location <> "the contextual abbreviation requires incompatible "
+            <> shown symbol <> " operations " <> shown firstObject
+            <> " and " <> shown secondObject
     ExactStructureOccurrenceMismatch location ->
         at location <> "the structure syntax occurrences do not match the declaration"
     ExactStructureSelfParent location structurePhrase ->
@@ -498,6 +510,9 @@ data ElaborationState = ElaborationState
     { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural)
     , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation)
     , elaborationGlobals :: !(Map.Map ObjectId CoreType)
+    , elaborationContextualBinder :: !(Maybe Natural)
+    , elaborationContextualRequirements
+        :: !(Map.Map Raw.StructSymbol ObjectId)
     }
 
 type Elaborate failure =
@@ -513,6 +528,9 @@ data PreparedHead = PreparedHead
 data PreparedBody
     = OpaqueBody
     | TransparentBody !(CanonicalTerm ObjectId)
+    | ContextualTransparentBody
+        !(Map.Map Raw.StructSymbol ObjectId)
+        !(CanonicalTerm ObjectId)
 
 prepareExactProposition
     :: ExactBinderContext
@@ -785,6 +803,8 @@ initialElaborationState context =
         (binderIndices context)
         (binderStructures context)
         mempty
+        Nothing
+        mempty
 
 annotateBinderContext
     :: Map.Map Natural ExactStructureAnnotation
@@ -1024,13 +1044,23 @@ prepareExactDeclaration block entries =
                 Nothing -> pure (OpaqueBody, Map.empty)
                 Just buildBody -> do
                     let initialElaboration =
-                            ElaborationState mempty mempty mempty
+                            ElaborationState
+                                mempty mempty mempty Nothing mempty
                     (canonical, finalElaboration) <-
                         State.runStateT buildBody initialElaboration
-                    pure
-                        ( TransparentBody canonical
-                        , elaborationGlobals finalElaboration
-                        )
+                    let requirements =
+                            elaborationContextualRequirements finalElaboration
+                        body
+                            | Map.null requirements =
+                                TransparentBody canonical
+                            | family == ExactAbbreviation =
+                                ContextualTransparentBody
+                                    requirements
+                                    (CLam TySet canonical)
+                            | otherwise =
+                                impossible
+                                    "a non-abbreviation acquired contextual requirements"
+                    pure (body, elaborationGlobals finalElaboration)
         let PreparedHead semanticKey _parameters coreType = head'
         unless (semanticKey == key)
             (Except.throwError
@@ -1046,8 +1076,8 @@ prepareExactDeclaration block entries =
                                 (generatedObjectSlot 0)
                         content' =
                             OpaqueObjectContent theory seed coreType
-                    pure
-                        (opaqueObjectId theory seed coreType, content')
+                        identity = opaqueObjectId theory seed coreType
+                    pure (GlobalReference identity, content')
                 TransparentBody canonical -> do
                     checked <-
                         either
@@ -1069,15 +1099,54 @@ prepareExactDeclaration block entries =
                                 theory
                                 coreType
                                 canonical
+                    let identity =
+                            transparentObjectId theory coreType canonical
+                        semanticTarget =
+                            case family of
+                                ExactAbbreviation ->
+                                    TransparentExpansion identity
+                                ExactDefinition -> GlobalReference identity
+                                ExactSignature ->
+                                    impossible
+                                        "a signature acquired a transparent body"
+                    pure (semanticTarget, content')
+                ContextualTransparentBody requirements canonical -> do
+                    let contextualType = TyArrow TySet coreType
+                    checked <-
+                        either
+                            (Except.throwError
+                                . ExactCoreCheckFailed (locate block))
+                            pure
+                            (checkCanonicalCore
+                                (`Map.lookup` globals)
+                                canonical)
+                    unless
+                        (frozenCoreType checked == contextualType)
+                        (Except.throwError
+                            (ExactObjectTypeMismatch
+                                (locate block)
+                                contextualType
+                                (frozenCoreType checked)))
+                    let content' =
+                            TransparentObjectContent
+                                theory
+                                contextualType
+                                canonical
+                        identity =
+                            transparentObjectId
+                                theory contextualType canonical
                     pure
-                        ( transparentObjectId theory coreType canonical
+                        ( ContextualTransparentExpansion
+                            identity requirements
                         , content'
                         )
-        available <- Except.lift (Declaration.objectAvailableDriver target)
+        let targetObject = semanticGlobalTargetObject target
+        available <-
+            Except.lift (Declaration.objectAvailableDriver targetObject)
         let alias = definitionAlias block
             asserted
                 | available = Nothing
-                | otherwise = Just (assertedObject target content)
+                | otherwise = Just (assertedObject targetObject content)
             syntax =
                 declarationSyntaxId
                     (encodePreparedSyntax family head' body alias)
@@ -1542,32 +1611,32 @@ prepareAbbreviation
 prepareAbbreviation location key = \case
     Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do
         ensureExpressionKey location symbol key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key parameters TySet
             (compileExpressionAsSet expression)
     Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do
         ensureFunctionPhraseKey location item key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key parameters TySet
             (compileTermAsSet term)
     Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do
         ensureAdjectiveKey location item key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key (subject : arguments) TyProp
             (compileStatement statement)
     Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do
         ensureVerbKey location item key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key (subject : arguments) TyProp
             (compileStatement statement)
     Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do
         ensureNounKey location item key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key (subject : arguments) TyProp
             (compileStatement statement)
     Raw.AbbreviationRel left relation parameters right statement -> do
         ensureRelationKey location relation key
-        makeTransparentHead
+        makeContextualTransparentHead
             location key (parameters <> [left, right]) TyProp
             (compileStatement statement)
 
@@ -1666,6 +1735,32 @@ makeTransparentHead location key parameters resultType body = do
             pure (foldr (const (CLam TySet)) body' parameters)
     pure (prepared, close)
 
+makeContextualTransparentHead
+    :: Location
+    -> SemanticGlobalKey
+    -> [Raw.VarSymbol]
+    -> CoreType
+    -> Elaborate failure (CanonicalTerm ObjectId)
+    -> ExceptT
+        ExactCompileError
+        (Declaration.ModuleDriver failure)
+        ( PreparedHead
+        , Elaborate failure (CanonicalTerm ObjectId)
+        )
+makeContextualTransparentHead location key parameters resultType body = do
+    (prepared, binders) <-
+        prepareParameters location key parameters resultType
+    let close = do
+            State.modify' \state ->
+                state
+                    { elaborationBinders = binders
+                    , elaborationContextualBinder =
+                        Just (fromIntegral (length parameters))
+                    }
+            body' <- body
+            pure (foldr (const (CLam TySet)) body' parameters)
+    pure (prepared, close)
+
 makePreparedHead
     :: Location
     -> SemanticGlobalKey
@@ -1812,42 +1907,99 @@ compileStructureOperation
     -> Maybe Raw.Expr
     -> Elaborate failure (CanonicalTerm ObjectId, CoreType)
 compileStructureOperation location symbol maybeArgument = do
-    (argument, annotation) <-
+    (argument, object) <-
         case maybeArgument of
             Just expression -> do
                 term <- compileExpressionAsSet expression
                 structures <- State.gets elaborationStructures
-                case term of
-                    CBound index ->
-                        case Map.lookup index structures of
-                            Just structure -> pure (term, structure)
-                            Nothing ->
-                                Except.throwError
-                                    (ExactStructureArgumentNotAnnotated
-                                        location)
-                    _ ->
-                        Except.throwError
-                            (ExactStructureArgumentNotAnnotated location)
+                case termStructureAnnotation term structures of
+                    Just annotation -> do
+                        object <-
+                            maybe
+                                (Except.throwError
+                                    (ExactStructureOperationNotAvailable
+                                        location symbol))
+                                pure
+                                (structureAnnotationOperation
+                                    symbol annotation)
+                        pure (term, object)
+                    Nothing -> do
+                        object <-
+                            resolveUniqueStructureOperation location symbol
+                        pure (term, object)
             Nothing -> do
                 structures <- State.gets elaborationStructures
                 case
-                    [ (CBound index, structure)
+                    [ (CBound index, object)
                     | (index, structure) <- Map.toAscList structures
-                    , isJust (structureAnnotationOperation symbol structure)
+                    , Just object <-
+                        [structureAnnotationOperation symbol structure]
                     ] of
                     firstMatch : _ -> pure firstMatch
-                    [] ->
-                        Except.throwError
-                            (ExactStructureOperationNotAvailable
-                                location symbol)
-    object <-
-        maybe
-            (Except.throwError
-                (ExactStructureOperationNotAvailable location symbol))
-            pure
-            (structureAnnotationOperation symbol annotation)
+                    [] -> do
+                        contextual <- State.gets elaborationContextualBinder
+                        case contextual of
+                            Nothing ->
+                                Except.throwError
+                                    (ExactStructureOperationNotAvailable
+                                        location symbol)
+                            Just index -> do
+                                object <-
+                                    resolveUniqueStructureOperation
+                                        location symbol
+                                recordContextualRequirement
+                                    location symbol object
+                                pure (CBound index, object)
     recordExactGlobal object (TyArrow TySet TySet)
     pure (CApp (CGlobal object) argument, TySet)
+  where
+    termStructureAnnotation term structures =
+        case term of
+            CBound index -> Map.lookup index structures
+            _ -> Nothing
+
+resolveUniqueStructureOperation
+    :: Location
+    -> Raw.StructSymbol
+    -> Elaborate failure ObjectId
+resolveUniqueStructureOperation location symbol = do
+    objects <-
+        State.lift
+            (Except.lift
+                (Declaration.resolveVisibleStructureOperationObjectsDriver
+                    symbol))
+    case objects of
+        [] ->
+            Except.throwError
+                (ExactStructureOperationNotAvailable location symbol)
+        [object] -> pure object
+        _ ->
+            Except.throwError
+                (ExactStructureOperationAmbiguous location symbol objects)
+
+recordContextualRequirement
+    :: Location
+    -> Raw.StructSymbol
+    -> ObjectId
+    -> Elaborate failure ()
+recordContextualRequirement location symbol object = do
+    existing <-
+        State.gets
+            (Map.lookup symbol . elaborationContextualRequirements)
+    case existing of
+        Nothing ->
+            State.modify' \state ->
+                state
+                    { elaborationContextualRequirements =
+                        Map.insert symbol object
+                            (elaborationContextualRequirements state)
+                    }
+        Just actual
+            | actual == object -> pure ()
+            | otherwise ->
+                Except.throwError
+                    (ExactContextualRequirementConflict
+                        location symbol actual object)
 
 structureCarrierCast
     :: Location
@@ -2698,6 +2850,54 @@ applyResolvedTyped location key arguments = do
                 _ ->
                     impossible
                         "validated transparent expansion has opaque content"
+        ContextualTransparentExpansion _identity requirements ->
+            case content of
+                TransparentObjectContent _theory coreType body -> do
+                    State.modify' \state ->
+                        state
+                            { elaborationGlobals =
+                                Map.union
+                                    dependencies
+                                    (elaborationGlobals state)
+                            }
+                    contextArgument <-
+                        resolveContextualExpansionArgument
+                            location key requirements
+                    applyExpandedTyped
+                        location body coreType
+                        ((contextArgument, TySet) : arguments)
+                _ ->
+                    impossible
+                        "validated contextual expansion has opaque content"
+
+resolveContextualExpansionArgument
+    :: Location
+    -> SemanticGlobalKey
+    -> Map.Map Raw.StructSymbol ObjectId
+    -> Elaborate failure (CanonicalTerm ObjectId)
+resolveContextualExpansionArgument location key requirements = do
+    contextual <- State.gets elaborationContextualBinder
+    case contextual of
+        Just index -> do
+            traverse_
+                (uncurry (recordContextualRequirement location))
+                (Map.toAscList requirements)
+            pure (CBound index)
+        Nothing -> do
+            structures <- State.gets elaborationStructures
+            case
+                [ CBound index
+                | (index, structure) <- Map.toAscList structures
+                , all
+                    (\(symbol, object) ->
+                        structureAnnotationOperation symbol structure
+                            == Just object)
+                    (Map.toAscList requirements)
+                ] of
+                firstMatch : _ -> pure firstMatch
+                [] ->
+                    Except.throwError
+                        (ExactContextualExpansionNotAvailable location key)
 
 applyExpandedTyped
     :: Location
@@ -2861,6 +3061,13 @@ encodePreparedSyntax
             TransparentBody canonical -> do
                 putCacheTag 0x01
                 putCanonicalTermCache putObjectIdCache canonical
+            ContextualTransparentBody requirements canonical -> do
+                putCacheTag 0x02
+                putCanonicalCacheMap
+                    (\(Raw.StructSymbol symbol) -> putCacheText symbol)
+                    putObjectIdCache
+                    requirements
+                putCanonicalTermCache putObjectIdCache canonical
         putCacheMaybe
             (putCacheText . semanticNameText)
             alias
diff --git a/source/Checking/Exact/Global.hs b/source/Checking/Exact/Global.hs
index 848b600..094255e 100644
--- a/source/Checking/Exact/Global.hs
+++ b/source/Checking/Exact/Global.hs
@@ -33,6 +33,7 @@ data ExactGlobalResolutionError
     = ExactGlobalNotVisible !Internal.Symbol
     | ExactGlobalAmbiguous !Internal.Symbol
     | ExactGlobalUnsupported !Internal.Symbol
+    | ExactGlobalContextualUnsupported !Internal.Symbol
     | ExactGlobalContentInvalid !CoreCheckError
     deriving stock (Show, Eq)
 
@@ -71,7 +72,7 @@ resolveExactSourceGlobals symbols =
                         throwError (ExactGlobalNotVisible symbol)
                     [match] -> do
                         (source, sourceTypes) <-
-                            liftEither (prepareSourceGlobal match)
+                            liftEither (prepareSourceGlobal symbol match)
                         pure
                             ( Map.insert symbol source resolved
                             , Map.union sourceTypes types
@@ -80,14 +81,15 @@ resolveExactSourceGlobals symbols =
                         throwError (ExactGlobalAmbiguous symbol)
 
 prepareSourceGlobal
-    :: ( SemanticGlobalTarget
+    :: Internal.Symbol
+    -> ( SemanticGlobalTarget
        , ObjectContent
        , Map.Map ObjectId CoreType
        )
     -> Either
         ExactGlobalResolutionError
         (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
-prepareSourceGlobal (target, content, dependencies) = do
+prepareSourceGlobal symbol (target, content, dependencies) = do
     body <-
         case target of
             GlobalReference _identity ->
@@ -103,6 +105,8 @@ prepareSourceGlobal (target, content, dependencies) = do
                     _ ->
                         impossible
                             "validated transparent expansion has opaque content"
+            ContextualTransparentExpansion _identity _requirements ->
+                Left (ExactGlobalContextualUnsupported symbol)
     let identity = semanticGlobalTargetObject target
         types =
             Map.insert
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
index c3f281c..e873f0c 100644
--- a/source/Checking/Exact/Inductive.hs
+++ b/source/Checking/Exact/Inductive.hs
@@ -500,6 +500,8 @@ exactGlobalError location = \case
         ExactInductiveGlobalAmbiguous location symbol
     ExactGlobal.ExactGlobalUnsupported symbol ->
         ExactInductiveUnsupportedSymbol location symbol
+    ExactGlobal.ExactGlobalContextualUnsupported symbol ->
+        ExactInductiveUnsupportedSymbol location symbol
     ExactGlobal.ExactGlobalContentInvalid failure ->
         ExactInductiveGlobalContentInvalid location failure
 
diff --git a/source/Checking/Semantic.hs b/source/Checking/Semantic.hs
index 1aa27b3..7a05f39 100644
--- a/source/Checking/Semantic.hs
+++ b/source/Checking/Semantic.hs
@@ -35,6 +35,7 @@ module Checking.Semantic
     , semanticGlobalKeyType
     , SemanticGlobalTarget(..)
     , semanticGlobalTargetObject
+    , semanticGlobalTargetRequirements
     , SemanticGlobalBinding
     , semanticGlobalBinding
     , semanticGlobalBindingKey
@@ -164,6 +165,7 @@ import Control.DeepSeq (NFData)
 import Control.Monad (unless, when)
 import Data.ByteString (ByteString)
 import Data.List qualified as List
+import Data.Map.Strict qualified as Map
 import Numeric.Natural (Natural)
 import Data.Set qualified as Set
 import Data.Text qualified as Text
@@ -406,6 +408,9 @@ semanticGlobalKeyFromLexicalEntry = \case
 data SemanticGlobalTarget
     = GlobalReference !ObjectId
     | TransparentExpansion !ObjectId
+    | ContextualTransparentExpansion
+        !ObjectId
+        !(Map.Map StructSymbol ObjectId)
     deriving stock (Show, Eq, Ord, Generic)
     deriving anyclass (NFData)
 
@@ -413,6 +418,15 @@ semanticGlobalTargetObject :: SemanticGlobalTarget -> ObjectId
 semanticGlobalTargetObject = \case
     GlobalReference identity -> identity
     TransparentExpansion identity -> identity
+    ContextualTransparentExpansion identity _requirements -> identity
+
+semanticGlobalTargetRequirements
+    :: SemanticGlobalTarget
+    -> Map.Map StructSymbol ObjectId
+semanticGlobalTargetRequirements = \case
+    GlobalReference{} -> Map.empty
+    TransparentExpansion{} -> Map.empty
+    ContextualTransparentExpansion _identity requirements -> requirements
 
 data SemanticGlobalBinding = SemanticGlobalBinding
     !SemanticGlobalKey
@@ -445,13 +459,22 @@ data SemanticGlobalTargetError
     | SemanticGlobalTargetIsIntrinsic !ObjectId
     | SemanticGlobalTargetTypeMismatch !ObjectId !CoreType !CoreType
     | SemanticGlobalExpansionNotTransparent !ObjectId
+    | SemanticGlobalContextualRequirementsEmpty !ObjectId
+    | SemanticGlobalContextualRequirementMissing !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementIsIntrinsic !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementTypeMismatch
+        !StructSymbol !ObjectId !CoreType !CoreType
+    | SemanticGlobalContextualRequirementNotProvided
+        !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementNotReferenced !StructSymbol !ObjectId
     deriving stock (Show, Eq)
 
 validateSemanticGlobalBindingTarget
-    :: CheckedObjectClosure
+    :: Set.Set (StructSymbol, ObjectId)
+    -> CheckedObjectClosure
     -> SemanticGlobalBinding
     -> Either SemanticGlobalTargetError ()
-validateSemanticGlobalBindingTarget closure binding = do
+validateSemanticGlobalBindingTarget operationBindings closure binding = do
     expected <-
         maybe
             (Left (SemanticGlobalKeyHasInconsistentArity key))
@@ -465,26 +488,70 @@ validateSemanticGlobalBindingTarget closure binding = do
     when
         (objectIdFamily identity == IntrinsicObject)
         (Left (SemanticGlobalTargetIsIntrinsic identity))
-    let actual = objectContentType content
+    let targetExpected =
+            case target of
+                ContextualTransparentExpansion{} ->
+                    TyArrow TySet expected
+                _ -> expected
+        actual = objectContentType content
     unless
-        (actual == expected)
+        (actual == targetExpected)
         (Left
             (SemanticGlobalTargetTypeMismatch
-                identity expected actual))
+                identity targetExpected actual))
     case target of
         GlobalReference{} -> pure ()
         TransparentExpansion{} ->
-            case content of
-                TransparentObjectContent{} -> pure ()
-                _ ->
-                    Left
-                        (SemanticGlobalExpansionNotTransparent
-                            identity)
+            validateTransparent content
+        ContextualTransparentExpansion _ requirements -> do
+            validateTransparent content
+            when
+                (Map.null requirements)
+                (Left (SemanticGlobalContextualRequirementsEmpty identity))
+            traverse_ (validateRequirement content) (Map.toAscList requirements)
   where
     key = semanticGlobalBindingKey binding
     target = semanticGlobalBindingTarget binding
     identity = semanticGlobalTargetObject target
 
+    validateTransparent = \case
+        TransparentObjectContent{} -> pure ()
+        _ -> Left (SemanticGlobalExpansionNotTransparent identity)
+
+    validateRequirement content (symbol, object) = do
+        operationContent <-
+            maybe
+                (Left
+                    (SemanticGlobalContextualRequirementMissing
+                        symbol object))
+                Right
+                (lookupCheckedObjectContent object closure)
+        when
+            (objectIdFamily object == IntrinsicObject)
+            (Left
+                (SemanticGlobalContextualRequirementIsIntrinsic
+                    symbol object))
+        let expectedOperation = TyArrow TySet TySet
+            actualOperation = objectContentType operationContent
+        unless
+            (actualOperation == expectedOperation)
+            (Left
+                (SemanticGlobalContextualRequirementTypeMismatch
+                    symbol object expectedOperation actualOperation))
+        unless
+            ((symbol, object) `Set.member` operationBindings)
+            (Left
+                (SemanticGlobalContextualRequirementNotProvided
+                    symbol object))
+        case content of
+            TransparentObjectContent _theory _coreType body ->
+                unless
+                    (object `Set.member` canonicalTermGlobals body)
+                    (Left
+                        (SemanticGlobalContextualRequirementNotReferenced
+                            symbol object))
+            _ -> impossible "a contextual expansion was not transparent"
+
 data SemanticEnvironmentDelta
     = EmptySemanticEnvironmentDelta
     | SemanticGlobalBindings ![SemanticGlobalBinding]
@@ -1339,6 +1406,13 @@ putSemanticGlobalBindingCache (SemanticGlobalBinding key target) = do
         TransparentExpansion identity -> do
             putCacheTag 0x01
             putObjectIdCache identity
+        ContextualTransparentExpansion identity requirements -> do
+            putCacheTag 0x02
+            putObjectIdCache identity
+            putCanonicalCacheMap
+                (\(StructSymbol symbol) -> putCacheText symbol)
+                putObjectIdCache
+                requirements
 
 getSemanticGlobalBindingCache :: CacheGet SemanticGlobalBinding
 getSemanticGlobalBindingCache =
@@ -1347,6 +1421,12 @@ getSemanticGlobalBindingCache =
         <*> (getCacheTag >>= \case
                 0x00 -> GlobalReference <$> getObjectIdCache
                 0x01 -> TransparentExpansion <$> getObjectIdCache
+                0x02 ->
+                    ContextualTransparentExpansion
+                        <$> getObjectIdCache
+                        <*> getCanonicalCacheMap
+                            (StructSymbol <$> getCacheText)
+                            getObjectIdCache
                 tag ->
                     fail
                         ("unknown semantic global target tag "
diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs
index cd00138..aa8cd88 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 21
+    CacheEpoch 22
 
 cacheEpochValue :: CacheEpoch -> Word32
 cacheEpochValue (CacheEpoch value) =
diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs
index 8a202fd..4782f31 100644
--- a/source/Felix/Migration.hs
+++ b/source/Felix/Migration.hs
@@ -213,6 +213,9 @@ typedMigrationModules =
         , 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-contextual-abbreviation.tex"
+        , migrationProjectModule "test/phase5/exact-contextual-abbreviation-missing.tex"
+        , migrationProjectModule "test/phase5/exact-contextual-abbreviation-ambiguous.tex"
         , migrationProjectModule "test/phase5/exact-quantified-subject.tex"
         , migrationProjectModule "test/phase5/exact-quantified-subject-nested.tex"
         , migrationProjectModule "test/phase5/exact-proof-failure.tex"
diff --git a/source/Felix/Store.hs b/source/Felix/Store.hs
index 973a172..3a5816d 100644
--- a/source/Felix/Store.hs
+++ b/source/Felix/Store.hs
@@ -1734,6 +1734,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 +1747,7 @@ validateModuleArtifactClosure memo store root = do
                                     (semanticGlobalBindingKey binding)
                                     (semanticGlobalBindingTarget binding))
                                 (validateSemanticGlobalBindingTarget
-                                    closure binding)))
+                                    operationBindings closure binding)))
                     bindings
                 traverse_ validateProposition propositions
                 traverse_ validateOccurrence
@@ -1758,6 +1760,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))
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)
diff --git a/test/phase5/exact-contextual-abbreviation-ambiguous.tex b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
new file mode 100644
index 0000000..c8fd94c
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
@@ -0,0 +1,17 @@
+\import{test/phase5/exact-contextual-abbreviation.tex}
+
+\begin{struct}\label{phase5_context_other_magma}
+    A phase five context other magma $A$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\phasefivecombine$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{phase5_context_other_refl} $A = A$.
+    \end{enumerate}
+\end{struct}
+
+\begin{proposition}\label{phase5_context_ambiguous}
+    Let $A,a,b$ be sets.
+    Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
+\end{proposition}
diff --git a/test/phase5/exact-contextual-abbreviation-missing.tex b/test/phase5/exact-contextual-abbreviation-missing.tex
new file mode 100644
index 0000000..cecbbf2
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-missing.tex
@@ -0,0 +1,6 @@
+\import{test/phase5/exact-contextual-abbreviation.tex}
+
+\begin{proposition}\label{phase5_context_missing}
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = b\phasefivedot a$.
+\end{proposition}
diff --git a/test/phase5/exact-contextual-abbreviation.tex b/test/phase5/exact-contextual-abbreviation.tex
new file mode 100644
index 0000000..9b4387e
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation.tex
@@ -0,0 +1,56 @@
+\begin{signature}\label{phase5_context_apply}
+    $\apply{f}{x}$ is a set.
+\end{signature}
+
+\begin{signature}\label{phase5_context_pair}
+    $(a,b)$ is a set.
+\end{signature}
+
+\begin{struct}\label{phase5_context_magma}
+    A phase five context magma $A$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\phasefivecombine$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{phase5_context_refl} $A = A$.
+    \end{enumerate}
+\end{struct}
+
+\begin{struct}\label{phase5_context_unital_magma}
+    A phase five context unital magma $A$ is a phase five context magma.
+\end{struct}
+
+\begin{abbreviation}\label{phase5_context_dot}
+    %! infixl 4
+    $a\phasefivedot b = \phasefivecombine(a,b)$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{phase5_context_commutes}
+    $a$ phase five commutes with $b$ iff
+    $a\phasefivedot b = b\phasefivedot a$.
+\end{abbreviation}
+
+\begin{proposition}\label{phase5_context_dot_explicit}
+    Let $A$ be a phase five context magma.
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_inherited}
+    Let $A$ be a phase five context unital magma.
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_nested}
+    Let $A$ be a phase five context magma.
+    Let $a,b$ be sets.
+    Then $a$ phase five commutes with $b$ iff
+        $\phasefivecombine[A](a,b) = \phasefivecombine[A](b,a)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_explicit_unique}
+    Let $A,a,b$ be sets.
+    Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
+\end{proposition}