diff options
Diffstat (limited to 'source/Checking/Facts.hs')
| -rw-r--r-- | source/Checking/Facts.hs | 340 |
1 files changed, 0 insertions, 340 deletions
diff --git a/source/Checking/Facts.hs b/source/Checking/Facts.hs deleted file mode 100644 index b365e1e..0000000 --- a/source/Checking/Facts.hs +++ /dev/null @@ -1,340 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Checking.Facts - ( PreparedSemanticFact - , prepareSemanticFact - , preparedSemanticStatement - , preparedSemanticDependencies - , FactOrigin - , factOrigin - , factOriginLocation - , factOriginBlock - , StagedFact - , stageFact - , stagedFactAliases - , stagedFactOrigin - , stagedFactSemantic - , FactRegistry - , emptyFactRegistry - , registerStagedFacts - , lookupPreparedFact - , lookupFactOrigin - , registeredFacts - , registeredFactsWithOrigins - , factRegistryExtension - , restrictFactRegistry - , partitionFactRegistry - , factRegistryInvariant - ) where - -import Base -import Report.Location -import Syntax.Internal - -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set - - --- | A checked fact before aliases and diagnostic provenance are attached. --- This is the complete long-lived semantic row. -data PreparedSemanticFact = PreparedSemanticFact - { preparedSemanticStatement :: !Formula - , preparedSemanticDependencies :: !(Set Symbol) - } - deriving (Show, Eq) - -prepareSemanticFact :: Formula -> PreparedSemanticFact -prepareSemanticFact statement = - PreparedSemanticFact - { preparedSemanticStatement = statement - , preparedSemanticDependencies = mentionedSymbols statement - } - -data FactOrigin = FactOrigin - { factOriginLocation :: !Location - , factOriginBlock :: !Marker - } - deriving (Show, Eq) - -factOrigin :: Location -> Marker -> FactOrigin -factOrigin = FactOrigin - --- | Registration data for one semantic fact. -data StagedFact = StagedFact - { stagedFactAliases :: !(NonEmpty Marker) - , stagedFactOrigin :: !FactOrigin - , stagedFactSemantic :: !PreparedSemanticFact - } - deriving (Show, Eq) - -stageFact - :: NonEmpty Marker - -> FactOrigin - -> PreparedSemanticFact - -> StagedFact -stageFact = StagedFact - -newtype FactHandle = FactHandle - { unFactHandle :: Int - } - deriving (Show, Eq, Ord) - -data FactRegistration = FactRegistration - { factRegistrationAliases :: !(NonEmpty Marker) - , factRegistrationOrigin :: !FactOrigin - } - deriving (Show, Eq) - --- | Semantic rows and their registration sidecars share only a private handle. -data FactRegistry = FactRegistry - { factOrder :: ![FactHandle] - , factRows :: !(Map FactHandle PreparedSemanticFact) - , factRegistrations :: !(Map FactHandle FactRegistration) - , factAliases :: !(Map Marker FactHandle) - , nextFactHandle :: !Int - } - deriving (Show, Eq) - -emptyFactRegistry :: FactRegistry -emptyFactRegistry = - FactRegistry - { factOrder = [] - , factRows = mempty - , factRegistrations = mempty - , factAliases = mempty - , nextFactHandle = 0 - } - -registerStagedFacts - :: NonEmpty StagedFact - -> FactRegistry - -> Either Marker FactRegistry -registerStagedFacts staged registry = - case firstDuplicateAlias (Map.keysSet (factAliases registry)) aliases of - Just duplicate -> - Left duplicate - Nothing -> - Right - registry - { factOrder = handles <> factOrder registry - , factRows = - Map.union - (Map.fromList - [ (handle, stagedFactSemantic fact) - | (handle, fact) <- registrations - ]) - (factRows registry) - , factRegistrations = - Map.union - (Map.fromList - [ ( handle - , FactRegistration - { factRegistrationAliases = - stagedFactAliases fact - , factRegistrationOrigin = - stagedFactOrigin fact - } - ) - | (handle, fact) <- registrations - ]) - (factRegistrations registry) - , factAliases = - Map.union - (Map.fromList - [ (alias, handle) - | (handle, fact) <- registrations - , alias <- - NonEmpty.toList (stagedFactAliases fact) - ]) - (factAliases registry) - , nextFactHandle = - nextFactHandle registry + length stagedList - } - where - stagedList = NonEmpty.toList staged - handles = - FactHandle <$> - [ nextFactHandle registry - .. nextFactHandle registry + length stagedList - 1 - ] - registrations = zip handles stagedList - aliases = - concatMap - (NonEmpty.toList . stagedFactAliases) - stagedList - -lookupPreparedFact :: Marker -> FactRegistry -> Maybe PreparedSemanticFact -lookupPreparedFact marker registry = do - handle <- Map.lookup marker (factAliases registry) - Map.lookup handle (factRows registry) - -lookupFactOrigin :: Marker -> FactRegistry -> Maybe FactOrigin -lookupFactOrigin marker registry = do - handle <- Map.lookup marker (factAliases registry) - factRegistrationOrigin - <$> Map.lookup handle (factRegistrations registry) - --- | Facts in checker premise order, paired with their primary aliases. -registeredFacts :: FactRegistry -> [(Marker, PreparedSemanticFact)] -registeredFacts registry = - [ (marker, semantic) - | (marker, semantic, _origin) <- - registeredFactsWithOrigins registry - ] - --- | Facts in checker premise order with their registration provenance. -registeredFactsWithOrigins - :: FactRegistry - -> [(Marker, PreparedSemanticFact, FactOrigin)] -registeredFactsWithOrigins registry = - [ (primaryAlias registration, semantic, factRegistrationOrigin registration) - | handle <- factOrder registry - , Just registration <- [Map.lookup handle (factRegistrations registry)] - , Just semantic <- [Map.lookup handle (factRows registry)] - ] - where - primaryAlias = - NonEmpty.head . factRegistrationAliases - --- | Recover the source-ordered facts appended to one registry. --- --- The first registry must be an unchanged prefix of the second. -factRegistryExtension - :: FactRegistry - -> FactRegistry - -> Either Text [StagedFact] -factRegistryExtension previous current - | nextFactHandle current < nextFactHandle previous = - Left "fact registry handle counter moved backwards" - | Map.restrictKeys - (factRows current) - previousHandles - /= factRows previous = - Left "fact registry changed an existing semantic row" - | Map.restrictKeys - (factRegistrations current) - previousHandles - /= factRegistrations previous = - Left "fact registry changed an existing registration" - | Map.restrictKeys - (factAliases current) - previousAliases - /= factAliases previous = - Left "fact registry changed an existing alias" - | factOrder current - /= extensionHandles <> factOrder previous = - Left "fact registry extension changed premise order" - | otherwise = - traverse staged extensionHandles - where - previousHandles = - Map.keysSet (factRows previous) - previousAliases = - Map.keysSet (factAliases previous) - extensionHandles = - FactHandle <$> - [ nextFactHandle previous - .. nextFactHandle current - 1 - ] - - staged handle = do - semantic <- - maybe - (Left "fact registry extension is missing a semantic row") - Right - (Map.lookup handle (factRows current)) - registration <- - maybe - (Left "fact registry extension is missing a registration") - Right - (Map.lookup handle (factRegistrations current)) - pure - (StagedFact - (factRegistrationAliases registration) - (factRegistrationOrigin registration) - semantic) - -restrictFactRegistry - :: NonEmpty Marker - -> FactRegistry - -> Either Marker FactRegistry -restrictFactRegistry markers registry = do - handles <- traverse resolveHandle markers - pure (registryForHandles (orderedUnique (NonEmpty.toList handles)) registry) - where - resolveHandle marker = - maybe (Left marker) Right (Map.lookup marker (factAliases registry)) - -partitionFactRegistry - :: NonEmpty Marker - -> FactRegistry - -> Either Marker (FactRegistry, FactRegistry) -partitionFactRegistry markers registry = do - selected <- restrictFactRegistry markers registry - let selectedHandles = Set.fromList (factOrder selected) - selectedInRegistryOrder = - List.filter (`Set.member` selectedHandles) (factOrder registry) - unselectedHandles = - List.filter (`Set.notMember` selectedHandles) (factOrder registry) - pure - ( registryForHandles selectedInRegistryOrder registry - , registryForHandles unselectedHandles registry - ) - -factRegistryInvariant :: FactRegistry -> Bool -factRegistryInvariant registry = - length order == Set.size orderSet - && orderSet == Map.keysSet (factRows registry) - && orderSet == Map.keysSet (factRegistrations registry) - && aliasCount == Map.size expectedAliases - && expectedAliases == factAliases registry - && all ((< nextFactHandle registry) . unFactHandle) order - where - order = factOrder registry - orderSet = Set.fromList order - aliasPairs = - [ (alias, handle) - | (handle, registration) <- - Map.toList (factRegistrations registry) - , alias <- - NonEmpty.toList (factRegistrationAliases registration) - ] - aliasCount = length aliasPairs - expectedAliases = Map.fromList aliasPairs - -registryForHandles :: [FactHandle] -> FactRegistry -> FactRegistry -registryForHandles handles registry = - registry - { factOrder = handles - , factRows = Map.restrictKeys (factRows registry) handleSet - , factRegistrations = - Map.restrictKeys (factRegistrations registry) handleSet - , factAliases = - Map.filter (`Set.member` handleSet) (factAliases registry) - } - where - handleSet = Set.fromList handles - -firstDuplicateAlias :: Set Marker -> [Marker] -> Maybe Marker -firstDuplicateAlias existing = - go mempty - where - go _seen [] = - Nothing - go seen (marker:rest) - | marker `Set.member` existing || marker `Set.member` seen = - Just marker - | otherwise = - go (Set.insert marker seen) rest - -orderedUnique :: Ord a => [a] -> [a] -orderedUnique = - reverse . snd . foldl' step (mempty, []) - where - step (seen, acc) value - | value `Set.member` seen = - (seen, acc) - | otherwise = - (Set.insert value seen, value : acc) |