Make structure registration transactional

3 files changed, 527 insertions, 0 deletions

diff --git a/source/Checking/Dependencies.hs b/source/Checking/Dependencies.hs
new file mode 100644
index 0000000..cf5c0f3
--- /dev/null
+++ b/source/Checking/Dependencies.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Checking.Dependencies
+    ( DependencyRegistry
+    , DependencyRegistrationError(..)
+    , fromRootSymbols
+    , registerDependencies
+    , lookupDependencies
+    , dependencyClosure
+    , dependencyPath
+    ) where
+
+import Base
+import Syntax.Internal
+
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+
+
+newtype DependencyRegistry = DependencyRegistry
+    { dependencyRows :: Map Symbol (Set Symbol)
+    }
+    deriving (Show, Eq)
+
+data DependencyRegistrationError
+    = DependencyOwnerAlreadyRegistered !Symbol
+    | SelfDependency !Symbol
+    | UnknownDependency !Symbol
+    deriving (Show, Eq)
+
+fromRootSymbols :: Set Symbol -> DependencyRegistry
+fromRootSymbols roots =
+    DependencyRegistry
+        (Map.fromSet (const mempty) roots)
+
+registerDependencies
+    :: Symbol
+    -> Set Symbol
+    -> DependencyRegistry
+    -> Either DependencyRegistrationError DependencyRegistry
+registerDependencies owner dependencies registry
+    | Map.member owner rows =
+        Left (DependencyOwnerAlreadyRegistered owner)
+    | owner `Set.member` dependencies =
+        Left (SelfDependency owner)
+    | Just unknown <- Set.lookupMin (dependencies `Set.difference` Map.keysSet rows) =
+        Left (UnknownDependency unknown)
+    | otherwise =
+        Right
+            (DependencyRegistry
+                (Map.insert owner dependencies rows))
+  where
+    rows = dependencyRows registry
+
+lookupDependencies
+    :: Symbol
+    -> DependencyRegistry
+    -> Maybe (Set Symbol)
+lookupDependencies symbol =
+    Map.lookup symbol . dependencyRows
+
+dependencyClosure
+    :: DependencyRegistry
+    -> Set Symbol
+    -> Either Symbol (Set Symbol)
+dependencyClosure registry =
+    go mempty . Set.toList
+  where
+    go seen [] =
+        Right seen
+    go seen (symbol:rest)
+        | symbol `Set.member` seen =
+            go seen rest
+        | otherwise =
+            case lookupDependencies symbol registry of
+                Nothing ->
+                    Left symbol
+                Just direct ->
+                    go
+                        (Set.insert symbol seen)
+                        (Set.toList direct <> rest)
+
+dependencyPath
+    :: DependencyRegistry
+    -> Set Symbol
+    -> Symbol
+    -> Either Symbol (Maybe [Symbol])
+dependencyPath registry seeds target =
+    firstPath (Set.toList seeds)
+  where
+    firstPath [] =
+        Right Nothing
+    firstPath (seed:rest) = do
+        path <- go mempty seed
+        case path of
+            Just _ ->
+                pure path
+            Nothing ->
+                firstPath rest
+
+    go seen symbol
+        | symbol == target =
+            Right (Just [symbol])
+        | symbol `Set.member` seen =
+            Right Nothing
+        | otherwise =
+            case lookupDependencies symbol registry of
+                Nothing ->
+                    Left symbol
+                Just direct ->
+                    prependFirst
+                        symbol
+                        (Set.toList direct)
+                        (Set.insert symbol seen)
+
+    prependFirst _prefix [] _seen =
+        Right Nothing
+    prependFirst prefix (dependency:rest) seen = do
+        path <- go seen dependency
+        case path of
+            Just found ->
+                Right (Just (prefix : found))
+            Nothing ->
+                prependFirst prefix rest seen
diff --git a/source/Checking/Facts.hs b/source/Checking/Facts.hs
new file mode 100644
index 0000000..410c05d
--- /dev/null
+++ b/source/Checking/Facts.hs
@@ -0,0 +1,269 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Checking.Facts
+    ( PreparedSemanticFact
+    , prepareSemanticFact
+    , preparedSemanticStatement
+    , preparedSemanticDependencies
+    , FactOrigin
+    , factOrigin
+    , factOriginLocation
+    , factOriginBlock
+    , StagedFact
+    , stageFact
+    , stagedFactAliases
+    , stagedFactSemantic
+    , FactRegistry
+    , emptyFactRegistry
+    , registerStagedFacts
+    , lookupPreparedFact
+    , lookupFactOrigin
+    , registeredFacts
+    , 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 =
+    [ (primaryAlias registration, semantic)
+    | handle <- factOrder registry
+    , Just registration <- [Map.lookup handle (factRegistrations registry)]
+    , Just semantic <- [Map.lookup handle (factRows registry)]
+    ]
+  where
+    primaryAlias =
+        NonEmpty.head . factRegistrationAliases
+
+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)
diff --git a/source/Checking/Structure.hs b/source/Checking/Structure.hs
new file mode 100644
index 0000000..a4ca5db
--- /dev/null
+++ b/source/Checking/Structure.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Checking.Structure
+    ( CheckedStructDefn
+    , StructurePreparationError(..)
+    , prepareCheckedStructDefn
+    , checkedStructPhrase
+    , checkedStructAncestors
+    , checkedStructInternalSymbols
+    , checkedStructAllSymbols
+    , checkedStructSymbol
+    , checkedStructDependencies
+    , checkedStructSemanticFacts
+    , checkedStructFacts
+    , checkedStructMarkers
+    ) where
+
+import Base
+import Checking.Facts
+import Report.Location
+import Syntax.Internal
+import Syntax.Lexicon
+
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Set qualified as Set
+
+
+-- | A structure declaration whose formulas have been fully prepared.
+data CheckedStructDefn = CheckedStructDefn
+    { checkedStructPhrase :: !StructPhrase
+    , checkedStructAncestors :: !(Set StructPhrase)
+    , checkedStructInternalSymbols :: !(Set StructSymbol)
+    , checkedStructAllSymbols :: !(Set StructSymbol)
+    , checkedStructSymbol :: !Symbol
+    , checkedStructDependencies :: !(Set Symbol)
+    , checkedStructFacts :: !(NonEmpty StagedFact)
+    }
+    deriving (Show, Eq)
+
+checkedStructSemanticFacts
+    :: CheckedStructDefn
+    -> NonEmpty PreparedSemanticFact
+checkedStructSemanticFacts =
+    fmap stagedFactSemantic . checkedStructFacts
+
+checkedStructMarkers :: CheckedStructDefn -> NonEmpty Marker
+checkedStructMarkers =
+    (>>= stagedFactAliases) . checkedStructFacts
+
+data StructurePreparationError
+    = SelfReferentialStructure !Symbol
+    deriving (Show, Eq)
+
+prepareCheckedStructDefn
+    :: Location
+    -> Marker
+    -> StructDefn
+    -> Set StructPhrase
+    -> Set StructSymbol
+    -> Either StructurePreparationError CheckedStructDefn
+prepareCheckedStructDefn location marker StructDefn{..} ancestors inheritedSymbols
+    | prospectiveSymbol `Set.member` assumptionDependencies =
+        Left (SelfReferentialStructure prospectiveSymbol)
+    | otherwise =
+        Right
+            CheckedStructDefn
+                { checkedStructPhrase = structPhrase
+                , checkedStructAncestors = ancestors
+                , checkedStructInternalSymbols = structDefnFixes
+                , checkedStructAllSymbols = structDefnFixes <> inheritedSymbols
+                , checkedStructSymbol = prospectiveSymbol
+                , checkedStructDependencies =
+                    parentSymbols <> assumptionDependencies
+                , checkedStructFacts = stagedFacts
+                }
+  where
+    prospectiveSymbol =
+        SymbolPredicate (PredicateNounStruct structPhrase)
+    parentSymbols =
+        Set.map
+            (SymbolPredicate . PredicateNounStruct)
+            structParents
+    assumptionDependencies =
+        Set.unions
+            [ preparedSemanticDependencies (prepareSemanticFact formula)
+            | (_assumptionMarker, formula) <- structDefnAssumes
+            ]
+    isStruct phrase =
+        TermSymbol
+            Nowhere
+            (SymbolPredicate (PredicateNounStruct phrase))
+            [TermVar structDefnLabel]
+    parentPremises
+        | structParents == Set.singleton _Onesorted =
+            []
+        | otherwise =
+            isStruct <$> Set.toList structParents
+    intro =
+        makeConjunction
+            (parentPremises <> (snd <$> structDefnAssumes))
+            `Implies` isStruct structPhrase
+    inherit =
+        isStruct structPhrase
+            `Implies` makeConjunction
+                [ isStruct parent
+                | parent <- Set.toList structParents
+                ]
+    generated =
+        (marker, intro)
+            :| ( (inheritMarker, inherit)
+               : [ (assumptionMarker, isStruct structPhrase `Implies` formula)
+                 | (assumptionMarker, formula) <- structDefnAssumes
+                 ]
+               )
+    inheritMarker =
+        case marker of
+            Marker text ->
+                Marker (text <> "inherit")
+    origin =
+        factOrigin location marker
+    semanticFacts =
+        fmap
+            (prepareSemanticFact . forallClosure mempty . snd)
+            generated
+    stagedFacts =
+        NonEmpty.zipWith
+            (\(factMarker, _formula) semantic ->
+                stageFact
+                    (factMarker :| [])
+                    origin
+                    semantic)
+            generated
+            semanticFacts