diff options
Diffstat (limited to 'source/Checking/Legacy')
| -rw-r--r-- | source/Checking/Legacy/Environment.hs | 279 |
1 files changed, 0 insertions, 279 deletions
diff --git a/source/Checking/Legacy/Environment.hs b/source/Checking/Legacy/Environment.hs deleted file mode 100644 index 7b94d53..0000000 --- a/source/Checking/Legacy/Environment.hs +++ /dev/null @@ -1,279 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Immutable legacy declaration environment carried by admitted modules. -module Checking.Legacy.Environment - ( SymbolOwnerKind(..) - , SymbolOwner(..) - , LegacyCheckingEnvironment - , legacyCheckingEnvironment - , legacyEnvironmentAbbreviations - , legacyEnvironmentPredicateDefinitions - , legacyEnvironmentDependencies - , legacyEnvironmentOwnedSymbols - , legacyEnvironmentOwnedSymbolMarkers - , legacyEnvironmentFrozenSymbols - , legacyEnvironmentStructs - , legacyEnvironmentDefinedMarkers - , LegacyCheckingEnvironmentDelta - , legacyCheckingEnvironmentExtension - , applyLegacyCheckingEnvironmentDelta - ) where - -import Base -import Checking.Dependencies qualified as Dependencies -import StructGraph qualified -import Syntax.Internal - -import Bound.Scope (Scope) -import Data.HashMap.Strict qualified as HashMap -import Data.HashSet qualified as HashSet - - -data SymbolOwnerKind - = OwnedByBuiltin - | OwnedBySignaturePredicate - | OwnedBySignatureFormula - | OwnedByAbbreviation - | OwnedByPredicateDefinition - | OwnedByFunctionDefinition - | OwnedByOperatorDefinition - | OwnedByDatatypeHead - | OwnedByDatatypeConstructor - | OwnedByInductiveDefinition - | OwnedByStructureDefinition - deriving stock (Show, Eq) - -data SymbolOwner = SymbolOwner - { symbolOwnerKind :: !SymbolOwnerKind - , symbolOwnerMarker :: !Marker - } - deriving stock (Show, Eq) - - -data LegacyCheckingEnvironment = LegacyCheckingEnvironment - { legacyEnvironmentAbbreviations - :: !(HashMap Symbol (Scope Int ExprOf Void)) - , legacyEnvironmentPredicateDefinitions - :: !(HashMap Predicate [Scope Int ExprOf Void]) - , legacyEnvironmentDependencies - :: !Dependencies.DependencyRegistry - , legacyEnvironmentOwnedSymbols - :: !(HashMap Symbol SymbolOwner) - , legacyEnvironmentOwnedSymbolMarkers - :: !(HashSet Marker) - , legacyEnvironmentFrozenSymbols - :: !(HashMap Symbol Marker) - , legacyEnvironmentStructs - :: !StructGraph.StructGraph - , legacyEnvironmentDefinedMarkers - :: !(HashSet Marker) - } - deriving stock (Show, Eq) - -legacyCheckingEnvironment - :: HashMap Symbol (Scope Int ExprOf Void) - -> HashMap Predicate [Scope Int ExprOf Void] - -> Dependencies.DependencyRegistry - -> HashMap Symbol SymbolOwner - -> HashSet Marker - -> HashMap Symbol Marker - -> StructGraph.StructGraph - -> HashSet Marker - -> LegacyCheckingEnvironment -legacyCheckingEnvironment = - LegacyCheckingEnvironment - - -data LegacyCheckingEnvironmentDelta = - LegacyCheckingEnvironmentDelta - !(HashMap Symbol (Scope Int ExprOf Void)) - !(HashMap Predicate [Scope Int ExprOf Void]) - !Dependencies.DependencyRegistryDelta - !(HashMap Symbol SymbolOwner) - !(HashSet Marker) - !(HashMap Symbol Marker) - !StructGraph.StructGraphDelta - !(HashSet Marker) - deriving stock (Show, Eq) - -legacyCheckingEnvironmentExtension - :: LegacyCheckingEnvironment - -> LegacyCheckingEnvironment - -> Either Text LegacyCheckingEnvironmentDelta -legacyCheckingEnvironmentExtension previous current = do - abbreviations <- - hashMapExtension - "abbreviation" - (legacyEnvironmentAbbreviations previous) - (legacyEnvironmentAbbreviations current) - predicateDefinitions <- - hashMapExtension - "predicate definition" - (legacyEnvironmentPredicateDefinitions previous) - (legacyEnvironmentPredicateDefinitions current) - dependencies <- - Dependencies.dependencyRegistryExtension - (legacyEnvironmentDependencies previous) - (legacyEnvironmentDependencies current) - ownedSymbols <- - hashMapExtension - "symbol owner" - (legacyEnvironmentOwnedSymbols previous) - (legacyEnvironmentOwnedSymbols current) - ownedMarkers <- - hashSetExtension - "owned symbol marker" - (legacyEnvironmentOwnedSymbolMarkers previous) - (legacyEnvironmentOwnedSymbolMarkers current) - frozenSymbols <- - hashMapExtension - "frozen symbol" - (legacyEnvironmentFrozenSymbols previous) - (legacyEnvironmentFrozenSymbols current) - structures <- - StructGraph.structGraphExtension - (legacyEnvironmentStructs previous) - (legacyEnvironmentStructs current) - definedMarkers <- - hashSetExtension - "defined marker" - (legacyEnvironmentDefinedMarkers previous) - (legacyEnvironmentDefinedMarkers current) - pure - (LegacyCheckingEnvironmentDelta - abbreviations - predicateDefinitions - dependencies - ownedSymbols - ownedMarkers - frozenSymbols - structures - definedMarkers) - -applyLegacyCheckingEnvironmentDelta - :: LegacyCheckingEnvironmentDelta - -> LegacyCheckingEnvironment - -> Either Text LegacyCheckingEnvironment -applyLegacyCheckingEnvironmentDelta - (LegacyCheckingEnvironmentDelta - abbreviations - predicateDefinitions - dependencies - ownedSymbols - ownedMarkers - frozenSymbols - structures - definedMarkers) - environment = do - abbreviations' <- - disjointHashMapUnion - "abbreviation" - (legacyEnvironmentAbbreviations environment) - abbreviations - predicateDefinitions' <- - disjointHashMapUnion - "predicate definition" - (legacyEnvironmentPredicateDefinitions environment) - predicateDefinitions - dependencies' <- - Dependencies.applyDependencyRegistryDelta - dependencies - (legacyEnvironmentDependencies environment) - ownedSymbols' <- - disjointHashMapUnion - "symbol owner" - (legacyEnvironmentOwnedSymbols environment) - ownedSymbols - ownedMarkers' <- - disjointHashSetUnion - "owned symbol marker" - (legacyEnvironmentOwnedSymbolMarkers environment) - ownedMarkers - structures' <- - StructGraph.applyStructGraphDelta - structures - (legacyEnvironmentStructs environment) - definedMarkers' <- - disjointHashSetUnion - "defined marker" - (legacyEnvironmentDefinedMarkers environment) - definedMarkers - pure - LegacyCheckingEnvironment - { legacyEnvironmentAbbreviations = abbreviations' - , legacyEnvironmentPredicateDefinitions = - predicateDefinitions' - , legacyEnvironmentDependencies = dependencies' - , legacyEnvironmentOwnedSymbols = ownedSymbols' - , legacyEnvironmentOwnedSymbolMarkers = ownedMarkers' - , legacyEnvironmentFrozenSymbols = - HashMap.union - (legacyEnvironmentFrozenSymbols environment) - frozenSymbols - , legacyEnvironmentStructs = structures' - , legacyEnvironmentDefinedMarkers = definedMarkers' - } - -hashMapExtension - :: (Hashable key, Eq value) - => Text - -> HashMap key value - -> HashMap key value - -> Either Text (HashMap key value) -hashMapExtension label previous current - | all - (\(key, value) -> - HashMap.lookup key current == Just value) - (HashMap.toList previous) = - Right (HashMap.difference current previous) - | otherwise = - Left - ("legacy environment changed an imported " - <> label) - -hashSetExtension - :: Hashable value - => Text - -> HashSet value - -> HashSet value - -> Either Text (HashSet value) -hashSetExtension label previous current - | previous `HashSet.isSubsetOf` current = - Right (current `HashSet.difference` previous) - | otherwise = - Left - ("legacy environment removed an imported " - <> label) - -disjointHashMapUnion - :: Hashable key - => Text - -> HashMap key value - -> HashMap key value - -> Either Text (HashMap key value) -disjointHashMapUnion label previous additions - | HashSet.null duplicateKeys = - Right (HashMap.union previous additions) - | otherwise = - Left - ("imported modules define the same " - <> label) - where - duplicateKeys = - HashMap.keysSet previous - `HashSet.intersection` HashMap.keysSet additions - -disjointHashSetUnion - :: Hashable value - => Text - -> HashSet value - -> HashSet value - -> Either Text (HashSet value) -disjointHashSetUnion label previous additions - | HashSet.null (previous `HashSet.intersection` additions) = - Right (previous <> additions) - | otherwise = - Left - ("imported modules define the same " - <> label) |