diff options
Diffstat (limited to 'source/Checking/Semantic.hs')
| -rw-r--r-- | source/Checking/Semantic.hs | 333 |
1 files changed, 319 insertions, 14 deletions
diff --git a/source/Checking/Semantic.hs b/source/Checking/Semantic.hs index 3deaa65..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 @@ -44,7 +45,24 @@ module Checking.Semantic , SemanticEnvironmentDelta , emptySemanticEnvironmentDelta , semanticEnvironmentDelta + , semanticEnvironmentWithStructures , semanticEnvironmentBindings + , semanticEnvironmentStructures + , SemanticStructurePhrase + , semanticStructurePhrase + , semanticStructurePhraseSingular + , semanticStructurePhrasePlural + , semanticStructurePhraseMarker + , SemanticStructureOperation + , semanticStructureOperation + , semanticStructureOperationSymbol + , semanticStructureOperationObject + , SemanticStructureDescriptor + , semanticStructureDescriptor + , semanticStructureDescriptorPhrase + , semanticStructureDescriptorPredicate + , semanticStructureDescriptorParents + , semanticStructureDescriptorOperations , SemanticEnvironmentError(..) , DeclarationInterfaceDelta , declarationInterfaceDelta @@ -147,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 @@ -389,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) @@ -396,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 @@ -428,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)) @@ -448,35 +488,193 @@ 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] + | SemanticGlobalBindingsAndStructures + ![SemanticGlobalBinding] + ![SemanticStructureDescriptor] + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +data SemanticStructurePhrase = SemanticStructurePhrase + !Pattern + !Pattern + !Marker deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) +semanticStructurePhrase :: LexicalItemSgPl -> SemanticStructurePhrase +semanticStructurePhrase (LexicalItemSgPl forms marker) = + SemanticStructurePhrase (sg forms) (pl forms) marker + +semanticStructurePhraseSingular :: SemanticStructurePhrase -> Pattern +semanticStructurePhraseSingular (SemanticStructurePhrase singular _ _) = + singular + +semanticStructurePhrasePlural :: SemanticStructurePhrase -> Pattern +semanticStructurePhrasePlural (SemanticStructurePhrase _ plural _) = + plural + +semanticStructurePhraseMarker :: SemanticStructurePhrase -> Marker +semanticStructurePhraseMarker (SemanticStructurePhrase _ _ marker) = + marker + +data SemanticStructureOperation = SemanticStructureOperation + !StructSymbol + !ObjectId + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +semanticStructureOperation + :: StructSymbol + -> ObjectId + -> SemanticStructureOperation +semanticStructureOperation = + SemanticStructureOperation + +semanticStructureOperationSymbol + :: SemanticStructureOperation + -> StructSymbol +semanticStructureOperationSymbol (SemanticStructureOperation symbol _) = + symbol + +semanticStructureOperationObject + :: SemanticStructureOperation + -> ObjectId +semanticStructureOperationObject (SemanticStructureOperation _ object) = + object + +data SemanticStructureDescriptor = SemanticStructureDescriptor + !SemanticStructurePhrase + !(Maybe ObjectId) + ![SemanticStructurePhrase] + ![SemanticStructureOperation] + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +semanticStructureDescriptor + :: SemanticStructurePhrase + -> Maybe ObjectId + -> [SemanticStructurePhrase] + -> [SemanticStructureOperation] + -> Either SemanticEnvironmentError SemanticStructureDescriptor +semanticStructureDescriptor structurePhrase predicate parents operations = do + case firstDuplicate parents of + Just duplicate -> + Left (DuplicateSemanticStructureParent duplicate) + Nothing -> pure () + when + (structurePhrase `elem` parents) + (Left (SelfSemanticStructureParent structurePhrase)) + case firstDuplicate (semanticStructureOperationSymbol <$> operations) of + Just duplicate -> + Left (DuplicateSemanticStructureOperation duplicate) + Nothing -> pure () + pure + (SemanticStructureDescriptor + structurePhrase predicate parents operations) + +semanticStructureDescriptorPhrase + :: SemanticStructureDescriptor + -> SemanticStructurePhrase +semanticStructureDescriptorPhrase + (SemanticStructureDescriptor structurePhrase _ _ _) = + structurePhrase + +semanticStructureDescriptorPredicate + :: SemanticStructureDescriptor + -> Maybe ObjectId +semanticStructureDescriptorPredicate + (SemanticStructureDescriptor _ predicate _ _) = + predicate + +semanticStructureDescriptorParents + :: SemanticStructureDescriptor + -> [SemanticStructurePhrase] +semanticStructureDescriptorParents + (SemanticStructureDescriptor _ _ parents _) = + parents + +semanticStructureDescriptorOperations + :: SemanticStructureDescriptor + -> [SemanticStructureOperation] +semanticStructureDescriptorOperations + (SemanticStructureDescriptor _ _ _ operations) = + operations + data SemanticEnvironmentError = DuplicateSemanticGlobalKey !SemanticGlobalKey | NonCanonicalSemanticGlobalBindingOrder + | DuplicateSemanticStructure !SemanticStructurePhrase + | NonCanonicalSemanticStructureOrder + | DuplicateSemanticStructureParent !SemanticStructurePhrase + | SelfSemanticStructureParent !SemanticStructurePhrase + | DuplicateSemanticStructureOperation !StructSymbol deriving stock (Show, Eq) emptySemanticEnvironmentDelta :: SemanticEnvironmentDelta @@ -486,9 +684,16 @@ emptySemanticEnvironmentDelta = semanticEnvironmentDelta :: [SemanticGlobalBinding] -> Either SemanticEnvironmentError SemanticEnvironmentDelta -semanticEnvironmentDelta [] = +semanticEnvironmentDelta bindings = + semanticEnvironmentWithStructures bindings [] + +semanticEnvironmentWithStructures + :: [SemanticGlobalBinding] + -> [SemanticStructureDescriptor] + -> Either SemanticEnvironmentError SemanticEnvironmentDelta +semanticEnvironmentWithStructures [] [] = Right EmptySemanticEnvironmentDelta -semanticEnvironmentDelta bindings = do +semanticEnvironmentWithStructures bindings structures = do case firstDuplicate (semanticGlobalBindingKey <$> bindings) of Just duplicate -> Left (DuplicateSemanticGlobalKey duplicate) @@ -497,7 +702,19 @@ semanticEnvironmentDelta bindings = do unless (bindings == List.sortOn semanticGlobalBindingKey bindings) (Left NonCanonicalSemanticGlobalBindingOrder) - pure (SemanticGlobalBindings bindings) + case firstDuplicate (semanticStructureDescriptorPhrase <$> structures) of + Just duplicate -> + Left (DuplicateSemanticStructure duplicate) + Nothing -> pure () + unless + ( structures + == List.sortOn semanticStructureDescriptorPhrase structures + ) + (Left NonCanonicalSemanticStructureOrder) + pure + (case structures of + [] -> SemanticGlobalBindings bindings + _ -> SemanticGlobalBindingsAndStructures bindings structures) semanticEnvironmentBindings :: SemanticEnvironmentDelta @@ -505,6 +722,15 @@ semanticEnvironmentBindings semanticEnvironmentBindings = \case EmptySemanticEnvironmentDelta -> [] SemanticGlobalBindings bindings -> bindings + SemanticGlobalBindingsAndStructures bindings _ -> bindings + +semanticEnvironmentStructures + :: SemanticEnvironmentDelta + -> [SemanticStructureDescriptor] +semanticEnvironmentStructures = \case + EmptySemanticEnvironmentDelta -> [] + SemanticGlobalBindings{} -> [] + SemanticGlobalBindingsAndStructures _ structures -> structures data DeclarationInterfaceDelta = DeclarationInterfaceDelta @@ -1079,6 +1305,11 @@ putSemanticEnvironmentDeltaCache EmptySemanticEnvironmentDelta = putSemanticEnvironmentDeltaCache (SemanticGlobalBindings bindings) = do putCacheTag 0x01 putCacheList putSemanticGlobalBindingCache bindings +putSemanticEnvironmentDeltaCache + (SemanticGlobalBindingsAndStructures bindings structures) = do + putCacheTag 0x02 + putCacheList putSemanticGlobalBindingCache bindings + putCacheList putSemanticStructureDescriptorCache structures getSemanticEnvironmentDeltaCache :: CacheGet SemanticEnvironmentDelta @@ -1092,6 +1323,13 @@ getSemanticEnvironmentDeltaCache = (fail . ("invalid semantic environment delta: " <>) . show) pure (semanticEnvironmentDelta bindings) + 0x02 -> do + bindings <- getCacheList getSemanticGlobalBindingCache + structures <- getCacheList getSemanticStructureDescriptorCache + either + (fail . ("invalid semantic environment delta: " <>) . show) + pure + (semanticEnvironmentWithStructures bindings structures) tag -> fail ("unknown semantic environment delta tag " @@ -1168,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 = @@ -1176,11 +1421,71 @@ getSemanticGlobalBindingCache = <*> (getCacheTag >>= \case 0x00 -> GlobalReference <$> getObjectIdCache 0x01 -> TransparentExpansion <$> getObjectIdCache + 0x02 -> + ContextualTransparentExpansion + <$> getObjectIdCache + <*> getCanonicalCacheMap + (StructSymbol <$> getCacheText) + getObjectIdCache tag -> fail ("unknown semantic global target tag " <> show tag)) +putSemanticStructureDescriptorCache + :: SemanticStructureDescriptor + -> CachePut +putSemanticStructureDescriptorCache + (SemanticStructureDescriptor structurePhrase predicate parents operations) = do + putSemanticStructurePhraseCache structurePhrase + putCacheMaybe putObjectIdCache predicate + putCacheList putSemanticStructurePhraseCache parents + putCacheList putSemanticStructureOperationCache operations + +getSemanticStructureDescriptorCache + :: CacheGet SemanticStructureDescriptor +getSemanticStructureDescriptorCache = do + structurePhrase <- getSemanticStructurePhraseCache + predicate <- getCacheMaybe getObjectIdCache + parents <- getCacheList getSemanticStructurePhraseCache + operations <- getCacheList getSemanticStructureOperationCache + either + (fail . ("invalid semantic structure descriptor: " <>) . show) + pure + (semanticStructureDescriptor structurePhrase predicate parents operations) + +putSemanticStructurePhraseCache + :: SemanticStructurePhrase + -> CachePut +putSemanticStructurePhraseCache + (SemanticStructurePhrase singular plural (Marker marker)) = do + putPatternCache singular + putPatternCache plural + putCacheText marker + +getSemanticStructurePhraseCache + :: CacheGet SemanticStructurePhrase +getSemanticStructurePhraseCache = + SemanticStructurePhrase + <$> getPatternCache + <*> getPatternCache + <*> (Marker <$> getCacheText) + +putSemanticStructureOperationCache + :: SemanticStructureOperation + -> CachePut +putSemanticStructureOperationCache + (SemanticStructureOperation (StructSymbol symbol) object) = do + putCacheText symbol + putObjectIdCache object + +getSemanticStructureOperationCache + :: CacheGet SemanticStructureOperation +getSemanticStructureOperationCache = + SemanticStructureOperation + <$> (StructSymbol <$> getCacheText) + <*> getObjectIdCache + putDeclarationInterfaceDeltaCache :: DeclarationInterfaceDelta -> CachePut |