diff options
| -rw-r--r-- | source/Checking/Declaration.hs | 88 | ||||
| -rw-r--r-- | source/Checking/Exact.hs | 309 | ||||
| -rw-r--r-- | source/Checking/Exact/Global.hs | 10 | ||||
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 2 | ||||
| -rw-r--r-- | source/Checking/Semantic.hs | 102 | ||||
| -rw-r--r-- | source/Felix/Cache/Codec.hs | 2 | ||||
| -rw-r--r-- | source/Felix/Migration.hs | 3 | ||||
| -rw-r--r-- | source/Felix/Store.hs | 31 | ||||
| -rw-r--r-- | source/Test/Unit/Module.hs | 185 | ||||
| -rw-r--r-- | source/Test/Unit/Semantic.hs | 7 | ||||
| -rw-r--r-- | test/phase5/exact-contextual-abbreviation-ambiguous.tex | 17 | ||||
| -rw-r--r-- | test/phase5/exact-contextual-abbreviation-missing.tex | 6 | ||||
| -rw-r--r-- | test/phase5/exact-contextual-abbreviation.tex | 56 |
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} |