Make structure registration transactional

11 files changed, 1285 insertions, 407 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 7da9d58..9874a0b 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -10,6 +10,9 @@ module Checking where
 
 
 import Base hiding (locally)
+import Checking.Dependencies qualified as Dependencies
+import Checking.Facts qualified as Facts
+import Checking.Structure qualified as Structure
 import StructGraph
 import Syntax.Internal
 import Syntax.Lexicon
@@ -22,10 +25,9 @@ import Bound.Var (Var(..), unvar)
 import Control.Exception (Exception)
 import Control.Monad.Reader
 import Control.Monad.State
+import Data.Bifunctor (first)
 import Data.HashMap.Strict qualified as HM
 import Data.HashSet qualified as HS
-import Data.InsOrdMap (InsOrdMap)
-import Data.InsOrdMap qualified as InsOrdMap
 import Data.IORef (newIORef, modifyIORef', readIORef)
 import Data.List qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
@@ -60,11 +62,12 @@ initialCheckingState dumpPremselTraining emitTask = CheckingState
     { checkingAssumptions = []
     , checkingDumpPremselTraining = dumpPremselTraining
     , checkingGoals = []
-    , checkingFacts = mempty
+    , checkingFacts = Facts.emptyFactRegistry
     , checkingDirectness = Direct
     , checkingAbbreviations = initAbbreviations
     , checkingPredicateDefinitions = mempty
-    , checkingDefinitionDependencies = mempty
+    , checkingDependencies =
+        Dependencies.fromRootSymbols (Set.fromList builtinSymbols)
     , checkingOwnedSymbols = builtinOwnedSymbols
     , checkingOwnedSymbolMarkers = builtinOwnedSymbolMarkers
     , checkingFrozenSymbols = mempty
@@ -97,13 +100,13 @@ data CheckingState = CheckingState
     { checkingDumpPremselTraining :: WithDumpPremselTraining
 
     , checkingAssumptions :: [Hypothesis]
-    -- ^ Local assumptions (cached encoding).
+    -- ^ Local assumptions.
     --
     , checkingGoals :: [Formula]
     -- ^ The current goals. INVARIANT: these should always be canonicalized and have all abbreviations resolved.
     --
-    , checkingFacts :: InsOrdMap Marker Hypothesis
-    -- ^ Axioms and proven results (cached encoding).
+    , checkingFacts :: Facts.FactRegistry
+    -- ^ Canonical axioms and proven results with separate registration metadata.
     --
     --
     , checkingDirectness :: Directness
@@ -120,12 +123,8 @@ data CheckingState = CheckingState
     -- ^ Definitions of predicate that we can match against in assumptions.
     -- Axioms and theorems that have the shape of a definition can be added as alternate definitions.
     --
-    , checkingDefinitionDependencies :: HashMap Symbol (Set Symbol)
-    -- ^ Symbols mentioned in the expanded assumptions and definiens of each
-    -- ordinary definition.
-    -- INVARIANT: a definition's dependency set never contains its own symbol.
-    -- This is used to reject hidden recursive inductive occurrences and to freeze
-    -- unresolved downstream dependencies of symbols mentioned in inductive blocks.
+    , checkingDependencies :: Dependencies.DependencyRegistry
+    -- ^ Backward-only dependencies of every owned symbol.
     --
     , checkingOwnedSymbols :: HashMap Symbol SymbolOwner
     -- ^ Top-level symbols with an established introducing owner in this document.
@@ -162,6 +161,12 @@ data StructContext = StructContext
     , structContextOps :: HashMap StructSymbol VarSymbol
     }
 
+data BlockContext = BlockContext
+    { blockContextLocation :: !Location
+    , blockContextMarker :: !Marker
+    }
+    deriving (Show, Eq)
+
 data SymbolOwnerKind
     = OwnedByBuiltin
     | OwnedBySignaturePredicate
@@ -194,6 +199,7 @@ initCheckingStructs = StructGraph.insert
     _Onesorted
     mempty -- no parents
     (Set.singleton CarrierSymbol) -- used for casting X -> \carrier[X]
+    (Set.singleton CarrierSymbol)
     mempty -- empty graph
 
 initAbbreviations :: HashMap Symbol (Scope Int ExprOf Void)
@@ -272,6 +278,7 @@ builtinSymbols =
 
 data CheckingError
     = DuplicateMarker Location Marker
+    | UnknownStructureParent StructPhrase Location Marker
     | ByContradictionOnMultipleGoals Location Marker
     | BySetInductionSyntacticMismatch Location Marker
     | ProofWithoutPrecedingTheorem Location Marker
@@ -315,7 +322,7 @@ assumeFormula phi = do
         Top -> skip
         _ -> do
             marker <- nextHypothesisMarker
-            let hypo = encodeHypothesisContracted marker phi' phiContracted
+            let hypo = Hypothesis marker phi'
             modify \st ->
                 st{checkingAssumptions = hypo : checkingAssumptions st}
 
@@ -339,8 +346,11 @@ structContextFromAssertion = \case
 structContextFor :: VarSymbol -> StructPhrase -> CheckingM StructContext
 structContextFor x sp = do
     structGraph <- gets checkingStructs
-    let struct = lookupStruct structGraph sp
-    pure (structContextFromSymbols x (StructGraph.structSymbols struct structGraph))
+    case StructGraph.lookupSymbols sp structGraph of
+        Nothing ->
+            throwWithLocationAndMarker (UnknownStructureParent sp)
+        Just symbols ->
+            pure (structContextFromSymbols x symbols)
 
 structContextFromSymbols :: VarSymbol -> Set StructSymbol -> StructContext
 structContextFromSymbols x symbols =
@@ -382,11 +392,6 @@ asmStructContext = \case
         structContextFor x sp
 
 
-lookupStruct :: StructGraph -> StructPhrase -> Struct
-lookupStruct structGraph struct = case StructGraph.lookup struct structGraph of
-    Just result -> result
-    Nothing -> error $ "lookup of undefined structure: " <> show struct
-
 setLocation :: Location -> Checking
 setLocation loc = modify \st -> st{stepLocation = loc}
 
@@ -542,57 +547,121 @@ symbolOwnerByMarker marker owners =
 
 assertOwnedSymbolsInFormula :: Formula -> Checking
 assertOwnedSymbolsInFormula phi = do
+    assertOwnedDependencies (mentionedSymbols phi)
+
+assertOwnedDependencies :: Set Symbol -> Checking
+assertOwnedDependencies dependencies = do
     owners <- gets checkingOwnedSymbols
     let unknown =
             Set.filter
                 (\symbol -> ownableSymbol symbol && not (HM.member symbol owners))
-                (mentionedSymbols phi)
+                dependencies
     unless (Set.null unknown) do
         throwCheckingError ("top-level fact mentions symbol(s) without prior ownership: " <> formatSymbols unknown)
 
 claimSymbolOwnership :: SymbolOwnerKind -> Symbol -> Checking
 claimSymbolOwnership ownerKind symbol =
+    claimSymbolOwnershipWithDependencies ownerKind symbol mempty
+
+claimSymbolOwnershipWithDependencies
+    :: SymbolOwnerKind
+    -> Symbol
+    -> Set Symbol
+    -> Checking
+claimSymbolOwnershipWithDependencies ownerKind symbol dependencies =
     case objectSymbolMarker symbol of
         Nothing ->
             skip
-        Just marker -> do
-            owners <- gets checkingOwnedSymbols
-            for_ (HM.lookup symbol owners) \owner ->
-                throwCheckingError
-                    ( "symbol "
-                        <> symbolText symbol
-                        <> " is already owned by "
-                        <> symbolOwnerText owner
-                    )
-
-            ownedMarkers <- gets checkingOwnedSymbolMarkers
-            when (marker `HS.member` ownedMarkers) do
-                throwCheckingError
-                    ( "object-symbol marker "
-                        <> markerTextOf marker
-                        <> " is already owned"
-                        <> maybe "" ((" by " <>) . symbolOwnerText) (symbolOwnerByMarker marker owners)
-                    )
-
-            frozen <- gets checkingFrozenSymbols
-            currentMarker <- gets blockLabel
-            case HM.lookup symbol frozen of
-                Just frozenBy | frozenBy /= currentMarker ->
+        Just _marker -> do
+            st <- get
+            let currentMarker = blockLabel st
+            (owners', ownedMarkers') <-
+                either
                     throwCheckingError
-                        ( "symbol "
-                            <> symbolText symbol
-                            <> " is frozen by inductive block "
-                            <> markerTextOf frozenBy
-                            <> " and cannot be defined here"
-                        )
-                _ ->
-                    modify \st ->
-                        st
-                            { checkingOwnedSymbols =
-                                HM.insert symbol (SymbolOwner ownerKind currentMarker) (checkingOwnedSymbols st)
-                            , checkingOwnedSymbolMarkers =
-                                HS.insert marker (checkingOwnedSymbolMarkers st)
-                            }
+                    pure
+                    (validatedOwnership
+                        currentMarker
+                        ownerKind
+                        symbol
+                        st)
+            dependencyRegistry <-
+                either
+                    (throwCheckingError . dependencyRegistrationErrorText symbol)
+                    pure
+                    (Dependencies.registerDependencies
+                        symbol
+                        (Set.filter ownableSymbol dependencies)
+                        (checkingDependencies st))
+            put
+                st
+                    { checkingOwnedSymbols = owners'
+                    , checkingOwnedSymbolMarkers = ownedMarkers'
+                    , checkingDependencies = dependencyRegistry
+                    }
+
+validatedOwnership
+    :: Marker
+    -> SymbolOwnerKind
+    -> Symbol
+    -> CheckingState
+    -> Either Text (HashMap Symbol SymbolOwner, HashSet Marker)
+validatedOwnership currentMarker ownerKind symbol st = do
+    marker <-
+        maybe
+            (Left ("symbol has no object marker: " <> symbolText symbol))
+            Right
+            (objectSymbolMarker symbol)
+    let owners = checkingOwnedSymbols st
+    for_ (HM.lookup symbol owners) \owner ->
+        Left
+            ( "symbol "
+                <> symbolText symbol
+                <> " is already owned by "
+                <> symbolOwnerText owner
+            )
+    let ownedMarkers = checkingOwnedSymbolMarkers st
+    when (marker `HS.member` ownedMarkers) do
+        Left
+            ( "object-symbol marker "
+                <> markerTextOf marker
+                <> " is already owned"
+                <> maybe
+                    ""
+                    ((" by " <>) . symbolOwnerText)
+                    (symbolOwnerByMarker marker owners)
+            )
+    case HM.lookup symbol (checkingFrozenSymbols st) of
+        Just frozenBy | frozenBy /= currentMarker ->
+            Left
+                ( "symbol "
+                    <> symbolText symbol
+                    <> " is frozen by inductive block "
+                    <> markerTextOf frozenBy
+                    <> " and cannot be defined here"
+                )
+        _ ->
+            Right
+                ( HM.insert
+                    symbol
+                    (SymbolOwner ownerKind currentMarker)
+                    owners
+                , HS.insert marker ownedMarkers
+                )
+
+dependencyRegistrationErrorText
+    :: Symbol
+    -> Dependencies.DependencyRegistrationError
+    -> Text
+dependencyRegistrationErrorText owner = \case
+    Dependencies.DependencyOwnerAlreadyRegistered _ ->
+        "dependencies are already registered for symbol " <> symbolText owner
+    Dependencies.SelfDependency _ ->
+        "definition of symbol " <> symbolText owner <> " is self-referential"
+    Dependencies.UnknownDependency unknown ->
+        "definition of symbol "
+            <> symbolText owner
+            <> " depends on unknown symbol "
+            <> symbolText unknown
 
 freezeSymbols :: Set Symbol -> Checking
 freezeSymbols symbols = do
@@ -606,35 +675,6 @@ freezeSymbols symbols = do
     modify \st ->
         st{checkingFrozenSymbols = HM.union (checkingFrozenSymbols st) frozen}
 
-mentionedSymbols :: ExprOf a -> Set Symbol
-mentionedSymbols = \case
-    TermVar{} ->
-        mempty
-    TermSymbol _loc symbol args ->
-        Set.insert symbol (Set.unions (mentionedSymbols <$> args))
-    TermSymbolStruct _symbol expr ->
-        maybe mempty mentionedSymbols expr
-    Apply expr args ->
-        mentionedSymbols expr <> Set.unions (mentionedSymbols <$> toList args)
-    TermSep _x bound scope ->
-        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
-    ReplacePred _y _x bound scope ->
-        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
-    ReplaceFun bounds lhs cond ->
-        Set.unions (mentionedSymbols . snd <$> toList bounds)
-            <> mentionedSymbols (fromScope lhs)
-            <> mentionedSymbols (fromScope cond)
-    Connected _conn left right ->
-        mentionedSymbols left <> mentionedSymbols right
-    Lambda scope ->
-        mentionedSymbols (fromScope scope)
-    Quantified _quant scope ->
-        mentionedSymbols (fromScope scope)
-    PropositionalConstant{} ->
-        mempty
-    Not _loc expr ->
-        mentionedSymbols expr
-
 checkedInductiveMentionedSymbols :: CheckedInductive -> Set Symbol
 checkedInductiveMentionedSymbols CheckedInductive{checkedInductiveSymbol, checkedInductiveDomain, checkedInductiveIntros} =
     Set.insert
@@ -660,38 +700,6 @@ formatSymbolPath :: [Symbol] -> Text
 formatSymbolPath =
     Text.intercalate " -> " . fmap symbolText
 
-definitionDependencyClosure :: HashMap Symbol (Set Symbol) -> Set Symbol -> Set Symbol
-definitionDependencyClosure graph =
-    go Set.empty . Set.toList
-    where
-        go :: Set Symbol -> [Symbol] -> Set Symbol
-        go seen [] =
-            seen
-        go seen (symbol:rest)
-            | symbol `Set.member` seen =
-                go seen rest
-            | otherwise =
-                let directDeps = HM.lookupDefault mempty symbol graph
-                in go (Set.insert symbol seen) (Set.toList directDeps <> rest)
-
-definitionDependencyPath :: HashMap Symbol (Set Symbol) -> Set Symbol -> Symbol -> Maybe [Symbol]
-definitionDependencyPath graph seeds target =
-    firstJust id [go Set.empty seed | seed <- Set.toList seeds]
-    where
-        go :: Set Symbol -> Symbol -> Maybe [Symbol]
-        go seen symbol
-            | symbol == target =
-                Just [symbol]
-            | symbol `Set.member` seen =
-                Nothing
-            | otherwise =
-                let seen' = Set.insert symbol seen
-                    directDeps = HM.lookupDefault mempty symbol graph
-                in firstJust id
-                    [ (symbol :) <$> go seen' dep
-                    | dep <- Set.toList directDeps
-                    ]
-
 definitionParts :: Defn -> (SymbolOwnerKind, Symbol, [Asm], Expr)
 definitionParts = \case
     DefnPredicate asms predicate _vs body ->
@@ -714,14 +722,6 @@ checkedDefinitionDependencies symbol asms definiens = do
             ("definition of symbol " <> symbolText symbol <> " is self-referential")
     pure dependencies
 
-recordDefinitionDependencies :: Symbol -> Set Symbol -> Checking
-recordDefinitionDependencies symbol dependencies =
-    modify \st ->
-        st
-            { checkingDefinitionDependencies =
-                HM.insert symbol dependencies (checkingDefinitionDependencies st)
-            }
-
 checkDatatype :: Datatype -> Checking
 checkDatatype datatype@Datatype{datatypeHead = SymbolPattern datatypeSymbol datatypeArgs, datatypeClauses} = do
     claimSymbolOwnership OwnedByDatatypeHead (SymbolMixfix datatypeSymbol)
@@ -1009,17 +1009,52 @@ tellTasks = do
     directness <- gets checkingDirectness
     loc <- gets stepLocation
     emitTask <- gets checkingEmitTask
-    let hypos = (snd <$> InsOrdMap.toList facts) <> assumptions
+    let hypos = factHypotheses facts <> assumptions
     liftIO (traverse_ emitTask (Task directness hypos m loc <$> goals))
 
+factHypotheses :: Facts.FactRegistry -> [Hypothesis]
+factHypotheses facts =
+    [ Hypothesis marker (Facts.preparedSemanticStatement fact)
+    | (marker, fact) <- Facts.registeredFacts facts
+    ]
+
+prepareFact :: Formula -> CheckingM Facts.PreparedSemanticFact
+prepareFact phi = do
+    assertOwnedSymbolsInFormula phi
+    pure (Facts.prepareSemanticFact phi)
+
+registerPreparedFacts
+    :: NonEmpty Facts.StagedFact
+    -> Checking
+registerPreparedFacts staged = do
+    facts <- gets checkingFacts
+    case Facts.registerStagedFacts staged facts of
+        Left duplicate ->
+            throwWithLocationAndMarker
+                (\loc _blockMarker -> DuplicateMarker loc duplicate)
+        Right facts' ->
+            modify \st -> st{checkingFacts = facts'}
+
+stagePreparedFact
+    :: Location
+    -> Marker
+    -> Marker
+    -> Facts.PreparedSemanticFact
+    -> Facts.StagedFact
+stagePreparedFact loc blockMarker factMarker =
+    Facts.stageFact
+        (factMarker :| [])
+        (Facts.factOrigin loc blockMarker)
+
 -- | Make a fact available to all future paragraphs.
 addFact :: Formula -> Checking
 addFact phi = do
     phi' <- canonicalize phi
-    assertOwnedSymbolsInFormula phi'
-    m <- gets blockLabel
-    let hypo = encodeHypothesis m phi'
-    modify $ \st -> st{checkingFacts = InsOrdMap.insert m hypo (checkingFacts st)}
+    prepared <- prepareFact phi'
+    marker <- gets blockLabel
+    loc <- gets stepLocation
+    registerPreparedFacts
+        (stagePreparedFact loc marker marker prepared :| [])
 
 
 -- | Make a fact available to all future paragraphs.
@@ -1027,31 +1062,47 @@ addFacts :: [(Marker, Formula)] -> Checking
 addFacts phis = do
     loc <- gets stepLocation
     reserveMarkers loc (fst <$> phis)
-    phis' <- forM phis \(m, phi) -> do
+    blockMarker <- gets blockLabel
+    staged <- forM phis \(marker, phi) -> do
         phi' <- canonicalize phi
-        assertOwnedSymbolsInFormula phi'
-        let hypo = encodeHypothesis m phi'
-        pure (m, hypo)
-    modify $ \st -> st{checkingFacts = InsOrdMap.fromList phis' <> (checkingFacts st)}
+        prepared <- prepareFact phi'
+        pure (stagePreparedFact loc blockMarker marker prepared)
+    for_ (NonEmpty.nonEmpty staged) registerPreparedFacts
 
 
 reserveMarkers :: Location -> [Marker] -> Checking
 reserveMarkers loc markers = do
-    existing <- gets definedMarkers
-    case firstDuplicateMarker existing HS.empty markers of
+    st <- get
+    either throwIO (\markers' -> put st{definedMarkers = markers'})
+        (validatedMarkers loc markers st)
+
+validatedMarkers
+    :: Location
+    -> [Marker]
+    -> CheckingState
+    -> Either CheckingError (HashSet Marker)
+validatedMarkers loc markers st =
+    case firstDuplicateMarker (definedMarkers st) HS.empty markers of
         Just marker ->
-            throwIO (DuplicateMarker loc marker)
+            Left (DuplicateMarker loc marker)
         Nothing ->
-            modify \st -> st{definedMarkers = foldr HS.insert (definedMarkers st) markers}
-    where
-        firstDuplicateMarker :: HashSet Marker -> HashSet Marker -> [Marker] -> Maybe Marker
-        firstDuplicateMarker _seenGlobals _seenLocals [] =
-            Nothing
-        firstDuplicateMarker seenGlobals seenLocals (marker:rest)
-            | HS.member marker seenGlobals || HS.member marker seenLocals =
-                Just marker
-            | otherwise =
-                firstDuplicateMarker seenGlobals (HS.insert marker seenLocals) rest
+            Right (foldr HS.insert (definedMarkers st) markers)
+
+firstDuplicateMarker
+    :: HashSet Marker
+    -> HashSet Marker
+    -> [Marker]
+    -> Maybe Marker
+firstDuplicateMarker _seenGlobals _seenLocals [] =
+    Nothing
+firstDuplicateMarker seenGlobals seenLocals (marker:rest)
+    | HS.member marker seenGlobals || HS.member marker seenLocals =
+        Just marker
+    | otherwise =
+        firstDuplicateMarker
+            seenGlobals
+            (HS.insert marker seenLocals)
+            rest
 
 
 
@@ -1069,11 +1120,11 @@ canonicalizedFactWithAsms asms stmt = do
 addFactWithAsms :: [Asm] -> Formula -> Checking
 addFactWithAsms asms stmt = do
     phi <- canonicalizedFactWithAsms asms stmt
-    assertOwnedSymbolsInFormula phi
-    m <- gets blockLabel
-    modify $ \st ->
-        let hypo = encodeHypothesis m phi
-        in st{checkingFacts = InsOrdMap.insert m hypo (checkingFacts st)}
+    prepared <- prepareFact phi
+    marker <- gets blockLabel
+    loc <- gets stepLocation
+    registerPreparedFacts
+        (stagePreparedFact loc marker marker prepared :| [])
 
 
 -- | Mark a proof as indirect. Intended to be used in a @locally do@ block.
@@ -1150,56 +1201,71 @@ mentionsSymbol target = \case
 -- | Unroll supported comprehensions in equations and reject leftover ones.
 -- E.g. /@B = \\{f(a) | a\\in A \\}@/ turns into
 -- /@\\forall b. b\\in B \\iff \\exists a\\in A. b = f(a)@/.
-desugarComprehensionsA :: ExprOf a -> CheckingM (ExprOf a)
-desugarComprehensionsA = \case
+desugarComprehensionsAt
+    :: BlockContext
+    -> ExprOf a
+    -> CheckingM (ExprOf a)
+desugarComprehensionsAt context = go
+  where
+    go :: forall b. ExprOf b -> CheckingM (ExprOf b)
+    go = \case
     -- We only desugar comprehensions directly under equations.
     -- Any remaining comprehension is currently unsupported.
-    e@TermSep{} ->
-        reject e
-    e@ReplacePred{} ->
-        reject e
-    e@ReplaceFun{} ->
-        reject e
-    e@TermVar{} ->
-        pure e
-    e@PropositionalConstant{} ->
-        pure e
-    e@TermSymbolStruct{} ->
-        pure e
+        e@TermSep{} ->
+            reject e
+        e@ReplacePred{} ->
+            reject e
+        e@ReplaceFun{} ->
+            reject e
+        e@TermVar{} ->
+            pure e
+        e@PropositionalConstant{} ->
+            pure e
+        e@TermSymbolStruct{} ->
+            pure e
     --
-    Equals _pos e (TermSep x bound scope) ->
-        pure (desugarSeparation e x bound scope)
-    Equals _pos (TermSep x bound scope) e ->
-        pure (desugarSeparation e x bound scope)
+        Equals _pos e (TermSep x bound scope) ->
+            pure (desugarSeparation e x bound scope)
+        Equals _pos (TermSep x bound scope) e ->
+            pure (desugarSeparation e x bound scope)
     --
-    Equals _pos e (ReplaceFun bounds scope cond) ->
-        pure (makeReplacementIff (F <$> e) bounds scope cond)
-    Equals _pos (ReplaceFun bounds scope cond) e ->
-        pure (makeReplacementIff (F <$> e) bounds scope cond)
+        Equals _pos e (ReplaceFun bounds scope cond) ->
+            pure (makeReplacementIff (F <$> e) bounds scope cond)
+        Equals _pos (ReplaceFun bounds scope cond) e ->
+            pure (makeReplacementIff (F <$> e) bounds scope cond)
     --
-    Apply e es ->
-        Apply <$> desugarComprehensionsA e <*> traverse desugarComprehensionsA es
-    Not loc e ->
-        Not loc <$> desugarComprehensionsA e
-    TermSymbol loc sym es ->
-        TermSymbol loc sym <$> traverse desugarComprehensionsA es
-    Connected conn e1 e2 ->
-        Connected conn <$> desugarComprehensionsA e1 <*> desugarComprehensionsA e2
-    Lambda scope ->
-        Lambda <$> transverseScope desugarComprehensionsA scope
-    Quantified quant scope ->
-        Quantified quant <$> transverseScope desugarComprehensionsA scope
-    where
-        reject :: ExprOf a -> CheckingM b
-        reject _ =
-            throwWithLocationAndMarker (CheckingError "Could not eliminate set comprehensions in this step. Nested comprehensions are not supported yet.")
-
-        desugarSeparation :: ExprOf a -> VarSymbol -> (ExprOf a) -> (Scope () ExprOf a) -> ExprOf a
-        desugarSeparation e x bound scope =
-            let phi = isElementOf (TermVar (B x)) (F <$> e)
-                psi = isElementOf (TermVar (B x)) (F <$> bound)
-                rho = fromScope (mapBound (const x) scope)
-            in  Quantified Universally (toScope (phi `Iff` (psi `And` rho)))
+        Apply e es ->
+            Apply <$> go e <*> traverse go es
+        Not loc e ->
+            Not loc <$> go e
+        TermSymbol loc sym es ->
+            TermSymbol loc sym <$> traverse go es
+        Connected conn e1 e2 ->
+            Connected conn <$> go e1 <*> go e2
+        Lambda scope ->
+            Lambda <$> transverseScope go scope
+        Quantified quant scope ->
+            Quantified quant <$> transverseScope go scope
+
+    reject :: ExprOf a -> CheckingM b
+    reject _ =
+        throwIO
+            (CheckingError
+                "Could not eliminate set comprehensions in this step. Nested comprehensions are not supported yet."
+                (blockContextLocation context)
+                (blockContextMarker context))
+
+    desugarSeparation
+        :: ExprOf a
+        -> VarSymbol
+        -> ExprOf a
+        -> Scope () ExprOf a
+        -> ExprOf a
+    desugarSeparation e x bound scope =
+        let phi = isElementOf (TermVar (B x)) (F <$> e)
+            psi = isElementOf (TermVar (B x)) (F <$> bound)
+            rho = fromScope (mapBound (const x) scope)
+        in Quantified Universally (toScope (phi `Iff` (psi `And` rho)))
 
 
 
@@ -1234,11 +1300,11 @@ checkBlocks = \case
         withLabel loc marker (checkInductive inductiveDefn)
         checkBlocks blocks
     BlockStruct loc marker structDefn : blocks -> do
-        withLabel loc marker (checkStructDefn structDefn)
+        checkStructDefn (BlockContext loc marker) structDefn
         checkBlocks blocks
     [] -> skip
 
--- | Add the given label to the set of in-scope markers and set it as the current label for error reporting.
+-- | Reserve a non-structure block label and make it current.
 withLabel :: Location -> Marker -> CheckingM a -> CheckingM a
 withLabel loc marker ma = do
     reserveMarkers loc [marker]
@@ -1641,25 +1707,35 @@ byRef ms = locally do
     case dumpPremselTraining of
         WithDumpPremselTraining -> dumpTrainingData facts ms
         WithoutDumpPremselTraining -> skip
-    case InsOrdMap.lookupsMap ms facts of
-        Left (Marker str) -> throwWithLocationAndMarker (CheckingError ("unknown marker: " <> str))
+    case Facts.restrictFactRegistry ms facts of
+        Left (Marker str) ->
+            throwWithLocationAndMarker
+                (CheckingError ("unknown marker: " <> str))
         Right facts' -> modify (\st -> st{checkingFacts = facts'}) *> tellTasks
 
 byAssumption :: Checking
 byAssumption = locally do
-    modify (\st -> st{checkingFacts = mempty}) *> tellTasks
+    modify (\st -> st{checkingFacts = Facts.emptyFactRegistry}) *> tellTasks
 
-dumpTrainingData :: InsOrdMap Marker Hypothesis -> NonEmpty Marker -> Checking
+dumpTrainingData :: Facts.FactRegistry -> NonEmpty Marker -> Checking
 dumpTrainingData facts ms = do
-    let (picked, unpicked) = InsOrdMap.pickOutMap ms facts
+    (picked, unpicked) <-
+        case Facts.partitionFactRegistry ms facts of
+            Left (Marker str) ->
+                throwWithLocationAndMarker
+                    (CheckingError ("unknown marker: " <> str))
+            Right partitioned ->
+                pure partitioned
     goals <- gets checkingGoals
     m@(Marker m_) <- gets blockLabel
     let dir = "premseldump"
     let makePath k = dir </> (Text.unpack m_ <> show (k :: Int)) <.> "txt"
-    let dumpTrainingExample goal =
+        dumpTrainingExample goal =
             let conj = encodeConjecture m goal
-                usefuls = encodeWithRole Tptp.AxiomUseful (snd <$> InsOrdMap.toList picked)
-                redundants = encodeWithRole Tptp.AxiomRedundant (snd <$> InsOrdMap.toList unpicked)
+                usefuls =
+                    encodeWithRole Tptp.AxiomUseful (factHypotheses picked)
+                redundants =
+                    encodeWithRole Tptp.AxiomRedundant (factHypotheses unpicked)
                 k = hash goal
                 example = Tptp.toTextNewline (Tptp.Task (conj : (usefuls <> redundants)))
             in do
@@ -1678,10 +1754,10 @@ checkCase (Case split proof) = locally do
 checkDefn :: Location -> Defn -> Checking
 checkDefn loc defn = do
     let (ownerKind, definedSymbol, definitionAsms, definiens) = definitionParts defn
-    claimSymbolOwnership ownerKind definedSymbol
     dependencies <- checkedDefinitionDependencies definedSymbol definitionAsms definiens
+    assertOwnedDependencies dependencies
+    claimSymbolOwnershipWithDependencies ownerKind definedSymbol dependencies
     addDefinitionFact loc defn
-    recordDefinitionDependencies definedSymbol dependencies
 
 addDefinitionFact :: Location -> Defn -> Checking
 addDefinitionFact loc = \case
@@ -1791,8 +1867,22 @@ canonicalize phi = do
 -- | Canonicalize using an explicit structure context instead of the checker state's current one.
 canonicalizeWith :: StructContext -> Formula -> CheckingM Formula
 canonicalizeWith ctx phi = do
+    blockContext <-
+        BlockContext
+            <$> gets stepLocation
+            <*> gets blockLabel
+    canonicalizeWithAt blockContext ctx phi
+
+canonicalizeWithAt
+    :: BlockContext
+    -> StructContext
+    -> Formula
+    -> CheckingM Formula
+canonicalizeWithAt blockContext ctx phi = do
     phi' <- unabbreviate phi
-    desugarComprehensionsA (annotateWithStructContext ctx phi')
+    desugarComprehensionsAt
+        blockContext
+        (annotateWithStructContext ctx phi')
 
 annotateWithStructContext :: StructContext -> Formula -> Formula
 annotateWithStructContext StructContext{..} =
@@ -1862,10 +1952,19 @@ normalizeInductive Inductive{..} = do
 
 ensureInductiveDefinitionIndependence :: CheckedInductive -> Checking
 ensureInductiveDefinitionIndependence checked = do
-    graph <- gets checkingDefinitionDependencies
+    graph <- gets checkingDependencies
     let carrier = SymbolMixfix (checkedInductiveSymbol checked)
-        externalSymbols = Set.delete carrier (checkedInductiveMentionedSymbols checked)
-    case definitionDependencyPath graph externalSymbols carrier of
+        externalSymbols =
+            Set.filter ownableSymbol
+                (Set.delete carrier (checkedInductiveMentionedSymbols checked))
+    path <-
+        either
+            (\unknown ->
+                throwCheckingError
+                    ("inductive specification mentions unknown symbol " <> symbolText unknown))
+            pure
+            (Dependencies.dependencyPath graph externalSymbols carrier)
+    case path of
         Nothing ->
             skip
         Just path ->
@@ -1884,8 +1983,16 @@ ensureInductiveDefinitionIndependence checked = do
 
 checkedInductiveFrozenSymbols :: CheckedInductive -> CheckingM (Set Symbol)
 checkedInductiveFrozenSymbols checked = do
-    graph <- gets checkingDefinitionDependencies
-    pure (definitionDependencyClosure graph (checkedInductiveMentionedSymbols checked))
+    graph <- gets checkingDependencies
+    let seeds =
+            Set.filter ownableSymbol
+                (checkedInductiveMentionedSymbols checked)
+    either
+        (\unknown ->
+            throwCheckingError
+                ("inductive specification mentions unknown symbol " <> symbolText unknown))
+        pure
+        (Dependencies.dependencyClosure graph seeds)
 
 normalizeInductiveIntro :: FunctionSymbol -> [VarSymbol] -> IntroRule -> CheckingM CheckedInductiveIntro
 normalizeInductiveIntro symbol params IntroRule{introConditions, introResult} = do
@@ -2153,32 +2260,153 @@ inductiveUsedVars CheckedInductive{checkedInductiveParams, checkedInductiveIntro
                ]
         )
 
-checkStructDefn :: StructDefn -> Checking
-checkStructDefn StructDefn{..} = do
-    claimSymbolOwnership OwnedByStructureDefinition (SymbolPredicate (PredicateNounStruct structPhrase))
+checkStructDefn :: BlockContext -> StructDefn -> Checking
+checkStructDefn context structDefn@StructDefn{..} = do
+    structGraph <- gets checkingStructs
+    resolvedParents <-
+        forM (Set.toList structParents) \parent ->
+            case StructGraph.lookup parent structGraph of
+                Nothing ->
+                    throwIO
+                        (UnknownStructureParent
+                            parent
+                            (blockContextLocation context)
+                            (blockContextMarker context))
+                Just struct ->
+                    pure struct
+    let ancestors =
+            structParents
+                <> Set.unions (StructGraph.structAncestors <$> resolvedParents)
+        inheritedSymbols =
+            Set.unions (StructGraph.structSymbols <$> resolvedParents)
+        structContext =
+            structContextFromSymbols
+                structDefnLabel
+                (structDefnFixes <> inheritedSymbols)
+    assumptions <-
+        forM structDefnAssumes \(assumptionMarker, assumption) -> do
+            canonical <-
+                canonicalizeWithAt context structContext assumption
+            pure (assumptionMarker, canonical)
+    let canonicalStructDefn =
+            structDefn{structDefnAssumes = assumptions}
+    checked <-
+        either
+            (throwIO . structurePreparationCheckingError context)
+            pure
+            (Structure.prepareCheckedStructDefn
+                (blockContextLocation context)
+                (blockContextMarker context)
+                canonicalStructDefn
+                ancestors
+                inheritedSymbols)
     st <- get
-    let structGraph = checkingStructs st
-    let m@(Marker m_) = blockLabel st
-    let structAncestors = Set.unions (Set.map (`StructGraph.lookupAncestors` structGraph) structParents)
-    let structAncestors' = structParents <> structAncestors
-    let parentSymbols = Set.unions (Set.map (`StructGraph.lookupSymbols` structGraph) structParents)
-    let structContext = structContextFromSymbols structDefnLabel (structDefnFixes <> parentSymbols)
-    let isStruct p = TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct p)) [TermVar structDefnLabel]
-    let intro = if structParents == Set.singleton _Onesorted
-            then makeConjunction (snd <$> structDefnAssumes) `Implies` isStruct structPhrase
-            else makeConjunction ([isStruct parent | parent <- toList structParents] <> (snd <$> structDefnAssumes)) `Implies` isStruct structPhrase
-    let intro' = (m, intro)
-    let inherit' = (Marker (m_ <> "inherit"), isStruct structPhrase `Implies` makeConjunction [isStruct parent | parent <- toList structParents])
-    let elims' = [(marker, isStruct structPhrase `Implies` phi) | (marker, phi) <- structDefnAssumes]
-    rules' <- forM (InsOrdMap.toList (InsOrdMap.fromList (intro' : inherit' : elims'))) \(marker, phi) -> do
-        phi' <- canonicalizeWith structContext phi
-        assertOwnedSymbolsInFormula (forallClosure mempty phi')
-        pure (marker, encodeHypothesis marker (forallClosure mempty phi'))
-    let rules'' = InsOrdMap.fromList rules'
-    put st
-            { checkingStructs = StructGraph.insert structPhrase structAncestors' structDefnFixes (checkingStructs st)
-            , checkingFacts = rules'' <> checkingFacts st
+    either throwIO put (commitCheckedStructDefn context checked st)
+
+structurePreparationCheckingError
+    :: BlockContext
+    -> Structure.StructurePreparationError
+    -> CheckingError
+structurePreparationCheckingError context = \case
+    Structure.SelfReferentialStructure symbol ->
+        CheckingError
+            ( "structure definition of symbol "
+                <> symbolText symbol
+                <> " is self-referential"
+            )
+            (blockContextLocation context)
+            (blockContextMarker context)
+
+-- | Validate and commit every state row introduced by one structure.
+commitCheckedStructDefn
+    :: BlockContext
+    -> Structure.CheckedStructDefn
+    -> CheckingState
+    -> Either CheckingError CheckingState
+commitCheckedStructDefn context checked st = do
+    markers' <-
+        validatedMarkers
+            location
+            (NonEmpty.toList (Structure.checkedStructMarkers checked))
+            st
+    (owners', ownedMarkers') <-
+        first (checkingErrorAt context)
+            (validatedOwnership
+                marker
+                OwnedByStructureDefinition
+                structureSymbol
+                st)
+    dependencies' <-
+        first
+            (checkingErrorAt context . dependencyRegistrationErrorText structureSymbol)
+            (Dependencies.registerDependencies
+                structureSymbol
+                semanticDependencies
+                (checkingDependencies st))
+    traverse_
+        (validatePreparedDependencies dependencies')
+        (Structure.checkedStructSemanticFacts checked)
+    facts' <-
+        first
+            (DuplicateMarker location)
+            (Facts.registerStagedFacts
+                (Structure.checkedStructFacts checked)
+                (checkingFacts st))
+    pure
+        st
+            { checkingFacts = facts'
+            , checkingDependencies = dependencies'
+            , checkingOwnedSymbols = owners'
+            , checkingOwnedSymbolMarkers = ownedMarkers'
+            , checkingStructs =
+                StructGraph.insert
+                    (Structure.checkedStructPhrase checked)
+                    (Structure.checkedStructAncestors checked)
+                    (Structure.checkedStructInternalSymbols checked)
+                    (Structure.checkedStructAllSymbols checked)
+                    (checkingStructs st)
+            , definedMarkers = markers'
+            , blockLabel = marker
+            , stepLocation = location
+            , checkingHypothesisCounter = 0
             }
+  where
+    location = blockContextLocation context
+    marker = blockContextMarker context
+    structureSymbol = Structure.checkedStructSymbol checked
+    semanticDependencies =
+        Set.filter ownableSymbol
+            (Structure.checkedStructDependencies checked)
+
+    validatePreparedDependencies dependencyRegistry prepared =
+        case
+            Set.lookupMin
+                ( Set.filter
+                    (\dependency ->
+                        ownableSymbol dependency
+                            && isNothing
+                                (Dependencies.lookupDependencies
+                                    dependency
+                                    dependencyRegistry))
+                    (Facts.preparedSemanticDependencies prepared)
+                )
+        of
+            Nothing ->
+                Right ()
+            Just unknown ->
+                Left
+                    (checkingErrorAt context
+                        ( "structure fact depends on unknown symbol "
+                            <> symbolText unknown
+                        ))
+
+checkingErrorAt :: BlockContext -> Text -> CheckingError
+checkingErrorAt context message =
+    CheckingError
+        message
+        (blockContextLocation context)
+        (blockContextMarker context)
+
 
 fixing :: NonEmpty VarSymbol -> Checking
 fixing xs = do
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
diff --git a/source/Data/InsOrdMap.hs b/source/Data/InsOrdMap.hs
deleted file mode 100644
index ae75d31..0000000
--- a/source/Data/InsOrdMap.hs
+++ /dev/null
@@ -1,91 +0,0 @@
-{-# LANGUAGE TupleSections #-}
-
-{-
-    Simple "mostly-insert-only" insert-ordered maps.
-
-    There's also OMap from ordered-containers which uses two regular Maps,
-    but this isn't really more efficient for our use case.
-
-    There's also InsOrdHashMap from insert-ordered-containers which tries
-    its best to preserve the insertion order. Alas, this isn't quite enough to have
-    stable ATP proofs. At scale and with some other features helping with proof stability,
-    (i.e. prover guidance, premise selection, etc), it may be worth revisiting InsOrdHashMap.
--}
-
-module Data.InsOrdMap where
-
-import Data.Either
-import Data.Functor
-import Data.Hashable
-import Data.HashMap.Strict (HashMap)
-import Data.HashMap.Strict qualified as HM
-import Data.Int
-import Data.List qualified as List
-import Data.List.NonEmpty (NonEmpty(..))
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Maybe (Maybe, maybe)
-import Data.Maybe qualified as Maybe
-import Data.Monoid
-import Data.Semigroup
-import Prelude (error)
-import Data.Traversable
-import Data.Foldable hiding (toList)
-
-data InsOrdMap k v = InsOrdMap {toList :: [(k, v)], toHashMap :: (HashMap k v)}
-
-instance Hashable k => Semigroup (InsOrdMap k a) where
-    InsOrdMap a b <> InsOrdMap c d = InsOrdMap (a <> c) (b <> d)
-
-instance Hashable k => Monoid (InsOrdMap k a) where
-    mempty = InsOrdMap mempty mempty
-
-instance Functor (InsOrdMap k) where
-    fmap f (InsOrdMap asList asHashMap) = InsOrdMap (fmap (\(k,v) -> (k, f v)) asList) (fmap f asHashMap)
-
-instance Foldable (InsOrdMap k) where
-    foldr f b (InsOrdMap _asList asHashMap) = foldr f b asHashMap
-
-instance Traversable (InsOrdMap k) where
-    traverse f (InsOrdMap _asList asHashMap) = fromHashMap <$> (traverse f asHashMap)
-
-size :: InsOrdMap k v -> Int
-size omap = HM.size (toHashMap omap)
-
-fromList :: Hashable k => [(k, v)] -> InsOrdMap k v
-fromList kvs = InsOrdMap kvs (HM.fromList kvs)
-
-fromHashMap :: HashMap k v -> InsOrdMap k v
-fromHashMap kvs =  InsOrdMap (HM.toList kvs) kvs
-
-insert :: Hashable k => k -> v -> InsOrdMap k v -> InsOrdMap k v
-insert k v (InsOrdMap kvs kvs') = InsOrdMap ((k, v) : kvs) (HM.insert k v kvs')
-
-mapMaybe :: (v1 -> Maybe v) -> InsOrdMap k v1 -> InsOrdMap k v
-mapMaybe f (InsOrdMap kvs kvs') = InsOrdMap (Maybe.mapMaybe (\(k, v) -> (k,) <$> f v) kvs) (HM.mapMaybe f kvs')
-
-lookup :: Hashable k => k -> InsOrdMap k a -> Maybe a
-lookup a (InsOrdMap _ kvs) = HM.lookup a kvs
-
-lookups :: Hashable k => NonEmpty k -> InsOrdMap k v -> Either k (NonEmpty v)
-lookups ks kvs =
-    let lookups' = (\a kvs' -> maybe (Left a) Right (lookup a kvs')) <$> ks
-        flap ff x = (\f -> f x) <$> ff
-    in case partitionEithers (NonEmpty.toList (flap lookups' kvs)) of
-        (missingKey : _, _) -> Left missingKey
-        ([], v : vs) -> Right (v :| vs)
-        ([], []) -> error "IMPOSSIBLE (Data.InsOrdMap.lookups): one of the two result lists must be nonempty as they partition a nonempty list"
-
--- | Only intended for very small nonempty lists of keys!
-lookupsMap :: Hashable k => NonEmpty k -> InsOrdMap k v -> Either k (InsOrdMap k v)
-lookupsMap ks kvs =
-    let lookups' = (\a kvs' -> maybe (Left a) Right (lookup a kvs')) <$> ks
-        flap ff x = (\f -> f x) <$> ff
-    in case partitionEithers (NonEmpty.toList (flap lookups' kvs)) of
-        (missingKey : _, _) -> Left missingKey
-        ([], vs) -> Right (fromList (List.zip (NonEmpty.toList ks) vs))
-
--- | Split an InsOrdMap into an InsOrdMap specified by given "relevant" keys and non-given "irrelevant" keys.
-pickOutMap :: Hashable k => NonEmpty k -> InsOrdMap k v -> (InsOrdMap k v, InsOrdMap k v)
-pickOutMap ks kvs =
-    let (relevants, irrelevants) = List.partition (\(k,_) -> k `List.elem` NonEmpty.toList ks) (toList kvs)
-    in (fromList relevants, fromList irrelevants)
diff --git a/source/Encoding.hs b/source/Encoding.hs
index b0fac23..dc2092c 100644
--- a/source/Encoding.hs
+++ b/source/Encoding.hs
@@ -25,18 +25,6 @@ encodeTask task = Tptp.Task (conjecture' : hypos')
 encodeTaskText :: Task -> Text
 encodeTaskText = Tptp.toText . encodeTask
 
-encodeHypothesis :: Marker -> Formula -> Hypothesis
-encodeHypothesis m phi = encodeHypothesisContracted m phi (contraction phi)
-
-encodeHypothesisContracted :: Marker -> Formula -> Formula -> Hypothesis
-encodeHypothesisContracted m phi phiContracted =
-    let encoded = encodeExpr phiContracted
-    in Hypothesis
-        { hypothesisMarker = m
-        , hypothesisFormula = phi
-        , hypothesisEncoded = encoded
-        }
-
 -- | Boolean contraction of a task.
 contractionTask :: Task -> Task
 contractionTask task = task
@@ -53,24 +41,24 @@ encodeConjecture (Marker str) f =
 
 -- NOTE: E's SInE will only filter out axioms and leave hypotheses fixed.
 encodeHypos :: [Hypothesis] -> [Tptp.FofFormula]
-encodeHypos phis = [makeHypo  (hypothesisMarker h) (hypothesisEncoded h) | h <- phis]
+encodeHypos phis = [makeHypo (hypothesisMarker h) (hypothesisFormula h) | h <- phis]
     where
-        makeHypo :: Marker -> TextBuilder -> Tptp.FofFormula
-        makeHypo (Marker str) f' =
+        makeHypo :: Marker -> Formula -> Tptp.FofFormula
+        makeHypo (Marker str) formula =
             Tptp.FofFormula
                 (Tptp.NameAtomicWord (Tptp.AtomicWord str))
                 Tptp.Axiom
-                f'
+                (encodeExpr (contraction formula))
 
 encodeWithRole :: Tptp.Role -> [Hypothesis] -> [Tptp.FofFormula]
-encodeWithRole role phis = [makeHypo  (hypothesisMarker h) (hypothesisEncoded h) | h <- phis]
+encodeWithRole role phis = [makeHypo (hypothesisMarker h) (hypothesisFormula h) | h <- phis]
     where
-        makeHypo :: Marker -> TextBuilder -> Tptp.FofFormula
-        makeHypo (Marker str) f' =
+        makeHypo :: Marker -> Formula -> Tptp.FofFormula
+        makeHypo (Marker str) formula =
             Tptp.FofFormula
                 (Tptp.NameAtomicWord (Tptp.AtomicWord str))
                 role
-                f'
+                (encodeExpr (contraction formula))
 
 writeTask :: Handle -> Task -> IO ()
 writeTask h =
diff --git a/source/StructGraph.hs b/source/StructGraph.hs
index 35de34f..6e4c928 100644
--- a/source/StructGraph.hs
+++ b/source/StructGraph.hs
@@ -4,7 +4,21 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 
 
-module StructGraph where
+module StructGraph
+    ( Struct
+    , structNoun
+    , structAncestors
+    , structInternalSymbols
+    , structSymbols
+    , StructGraph
+    , lookup
+    , lookupAncestors
+    , lookupInternalSymbols
+    , lookupSymbols
+    , isInternalSymbolIn
+    , isSymbolIn
+    , insert
+    ) where
 
 
 import Base
@@ -18,6 +32,7 @@ data Struct = Struct
     { structNoun :: StructPhrase
     , structAncestors :: Set StructPhrase -- ^ All ancestors, including transitive ancestors.
     , structInternalSymbols :: Set StructSymbol -- ^ Signature.
+    , structSymbols :: Set StructSymbol -- ^ Signature, including inherited symbols.
     } deriving (Show, Eq, Ord)
 
 newtype StructGraph
@@ -29,53 +44,33 @@ newtype StructGraph
 lookup :: StructPhrase -> StructGraph -> Maybe Struct
 lookup str graph = Map.lookup str (unStructGraph graph)
 
--- | Unsafe variant of 'lookup'.
-unsafeLookup :: StructPhrase -> StructGraph -> Struct
-unsafeLookup str graph = lookup str graph ?? error ("not in scope: " <> show str)
-
 -- | Returns the ancestors of the given StructPhrase in the graph.
--- This function fails quietly by returning the empty set if the struct is not present in the graph.
-lookupAncestors :: StructPhrase -> StructGraph -> Set StructPhrase
-lookupAncestors str graph = case lookup str graph of
-    Just struct -> structAncestors struct
-    Nothing -> mempty
-
--- | Unsafe lookup of internal symbols by struct name.
-lookupInternalSymbols :: StructPhrase -> StructGraph -> Set StructSymbol
-lookupInternalSymbols phrase graph = case lookup phrase graph of
-    Nothing -> error ("structure not in scope: " <> show phrase)
-    Just struct -> structInternalSymbols struct
-
--- | Unsafe lookup of symbols of a structure, including those inherited from ancestors.
-lookupSymbols :: StructPhrase -> StructGraph -> Set StructSymbol
-lookupSymbols phrase graph = case lookup phrase graph of
-    Nothing -> error ("structure not in scope: " <> show phrase)
-    Just struct ->
-        let ancestors = Set.map (`unsafeLookup` graph) (structAncestors struct)
-            ancestorSymbols = Set.unions (Set.map structInternalSymbols ancestors)
-        in ancestorSymbols <> structInternalSymbols struct
-
-structSymbols :: Struct -> StructGraph -> Set StructSymbol
-structSymbols struct graph =
-    let ancestors = Set.map (`unsafeLookup` graph) (structAncestors struct)
-        ancestorSymbols = Set.unions (Set.map structInternalSymbols ancestors)
-    in structInternalSymbols struct <> ancestorSymbols
+lookupAncestors :: StructPhrase -> StructGraph -> Maybe (Set StructPhrase)
+lookupAncestors str graph =
+    structAncestors <$> lookup str graph
+
+lookupInternalSymbols :: StructPhrase -> StructGraph -> Maybe (Set StructSymbol)
+lookupInternalSymbols phrase graph =
+    structInternalSymbols <$> lookup phrase graph
+
+-- | Lookup all symbols of a structure, including inherited symbols.
+lookupSymbols :: StructPhrase -> StructGraph -> Maybe (Set StructSymbol)
+lookupSymbols phrase graph =
+    structSymbols <$> lookup phrase graph
 
 isInternalSymbolIn :: StructSymbol -> Struct -> Bool
 isInternalSymbolIn tok struct = Set.member tok (structInternalSymbols struct)
 
-isSymbolIn :: StructSymbol -> Struct -> StructGraph -> Bool
-isSymbolIn tok struct graph =  Set.member tok (structSymbols struct graph)
+isSymbolIn :: StructSymbol -> Struct -> Bool
+isSymbolIn tok struct = Set.member tok (structSymbols struct)
 
 -- | Insert a new struct into the graph.
 insert
     :: StructPhrase
     -> Set StructPhrase
     -> Set StructSymbol
+    -> Set StructSymbol
     -> StructGraph
     -> StructGraph
-insert structNoun ancestors structInternalSymbols graph =
-    let
-        transitiveAncestors anc = lookupAncestors anc graph
-        structAncestors = ancestors `Set.union` Set.unions (Set.map transitiveAncestors ancestors)
-    in  StructGraph (Map.insert structNoun Struct{..} (unStructGraph graph))
+insert structNoun structAncestors structInternalSymbols structSymbols graph =
+    StructGraph (Map.insert structNoun Struct{..} (unStructGraph graph))
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 287eed6..ea07533 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -62,7 +62,6 @@ import Data.HashMap.Strict qualified as HM
 import Data.List qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Set qualified as Set
-import TextBuilder (TextBuilder)
 
 -- | 'Symbol's can be used as function and relation symbols.
 data Symbol
@@ -186,6 +185,35 @@ deriving instance Hashable1 ExprOf
 
 deriving instance Hashable a =>  Hashable (ExprOf a)
 
+mentionedSymbols :: ExprOf a -> Set Symbol
+mentionedSymbols = \case
+    TermVar{} ->
+        mempty
+    TermSymbol _loc symbol args ->
+        Set.insert symbol (Set.unions (mentionedSymbols <$> args))
+    TermSymbolStruct _symbol expr ->
+        maybe mempty mentionedSymbols expr
+    Apply expr args ->
+        mentionedSymbols expr <> Set.unions (mentionedSymbols <$> toList args)
+    TermSep _x bound scope ->
+        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
+    ReplacePred _y _x bound scope ->
+        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
+    ReplaceFun bounds lhs cond ->
+        Set.unions (mentionedSymbols . snd <$> toList bounds)
+            <> mentionedSymbols (fromScope lhs)
+            <> mentionedSymbols (fromScope cond)
+    Connected _conn left right ->
+        mentionedSymbols left <> mentionedSymbols right
+    Lambda scope ->
+        mentionedSymbols (fromScope scope)
+    Quantified _quant scope ->
+        mentionedSymbols (fromScope scope)
+    PropositionalConstant{} ->
+        mempty
+    Not _loc expr ->
+        mentionedSymbols expr
+
 abstractVarSymbol :: VarSymbol -> ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol
 abstractVarSymbol x = abstract (\y -> if x == y then Just x else Nothing)
 
@@ -694,22 +722,23 @@ data Task = Task
 data Hypothesis = Hypothesis
     { hypothesisMarker :: Marker
     , hypothesisFormula :: Formula
-    , hypothesisEncoded :: TextBuilder
     }
 
 instance Show Hypothesis where
-    show (Hypothesis marker formula _) =
+    show (Hypothesis marker formula) =
         "Hypothesis " <> show marker <> " " <> show formula
 
 instance Eq Hypothesis where
-    Hypothesis m f _ == Hypothesis m' f' _ = (m, f) == (m', f')
+    Hypothesis marker formula == Hypothesis marker' formula' =
+        (marker, formula) == (marker', formula')
 
 instance Ord Hypothesis where
-    compare (Hypothesis m f _) (Hypothesis m' f' _) =
-        compare (m, f) (m', f')
+    compare (Hypothesis marker formula) (Hypothesis marker' formula') =
+        compare (marker, formula) (marker', formula')
 
 instance Hashable Hypothesis where
-    hashWithSalt s (Hypothesis m f _) = hashWithSalt s (m, f)
+    hashWithSalt salt (Hypothesis marker formula) =
+        hashWithSalt salt (marker, formula)
 
 
 -- | Indicates whether a given proof is direct or indirect.
diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs
index e458e39..7043ee1 100644
--- a/source/Test/Unit/Checking.hs
+++ b/source/Test/Unit/Checking.hs
@@ -4,6 +4,9 @@ module Test.Unit.Checking (unitTests) where
 
 import Base
 import Checking
+import Checking.Dependencies qualified as Dependencies
+import Checking.Facts qualified as Facts
+import Checking.Structure qualified as Structure
 import Encoding (encodeTaskText)
 import Report.Location
 import Syntax.Internal
@@ -13,7 +16,6 @@ import Bound.Scope (toScope)
 import Bound.Var (Var(..))
 import Control.Exception (try)
 import Data.HashSet qualified as HS
-import Data.InsOrdMap qualified as InsOrdMap
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Test.Tasty
@@ -83,6 +85,7 @@ unitTests = testGroup "Checking"
         text <- encodedTasksText boundStructLabelBlocks
         assertContains "bound carrier label remains raw" "![XA]:elem(fx,XA)" text
         assertNotContains "bound carrier label not rewritten" "![XA]:elem(fx,s__carrier(XA))" text
+    , structureTransactionTests
     , testCase "abbreviations reject direct self-reference" do
         expectCheckingError "self-referential" directSelfReferentialAbbrBlocks
     , testCase "abbreviations reject indirect self-reference after expansion" do
@@ -196,6 +199,137 @@ unitTests = testGroup "Checking"
         expectCheckingError "already owned by signature formula" transitiveFrozenDefinitionBlocks
     ]
 
+structureTransactionTests :: TestTree
+structureTransactionTests =
+    testGroup "structure transactions"
+        [ testCase "reject positive and negative direct self-reference" do
+            for_ [fooStructPredicate "A", Not Nowhere (fooStructPredicate "A")]
+                \assumption ->
+                    expectCheckingError
+                        "self-referential"
+                        [fooStructBlock "self_struct" [("self_rule", assumption)]]
+        , testCase "reject abbreviation-hidden self-reference" do
+            expectCheckingError
+                "self-referential"
+                hiddenSelfReferentialStructBlocks
+        , testCase "report unknown and forward parents as located errors" do
+            expectUnknownStructureParent
+                unknownStruct
+                [testStructBlock "unknown_child" childStruct (Set.singleton unknownStruct) []]
+            expectUnknownStructureParent
+                fooStruct
+                [ testStructBlock "forward_child" childStruct (Set.singleton fooStruct) []
+                , fooStructBlock "forward_parent" []
+                ]
+            expectUnknownStructureParent
+                fooStruct
+                [testStructBlock "self_parent" fooStruct (Set.singleton fooStruct) []]
+        , testCase "reject every local structure marker collision" do
+            for_
+                [ ( "same_marker"
+                  , fooStructBlock "same_marker" [("same_marker", Top)]
+                  )
+                , ( "duplicate_rule"
+                  , fooStructBlock
+                        "duplicate_rules"
+                        [("duplicate_rule", Top), ("duplicate_rule", Top)]
+                  )
+                , ( "inherit_collisioninherit"
+                  , fooStructBlock
+                        "inherit_collision"
+                        [("inherit_collisioninherit", Top)]
+                  )
+                ]
+                \(duplicate, block) ->
+                    expectDuplicateMarker duplicate [block]
+        , testCase "reject collisions before and after a structure" do
+            expectDuplicateMarker
+                "prior_rule"
+                [ BlockAxiom Nowhere "prior_rule" (Axiom [] Top)
+                , fooStructBlock "prior_collision" [("prior_rule", Top)]
+                ]
+            expectDuplicateMarker
+                "later_collisioninherit"
+                [ fooStructBlock "later_collision" []
+                , BlockAxiom
+                    Nowhere
+                    "later_collisioninherit"
+                    (Axiom [] Top)
+                ]
+        , testCase "commit exact prepared facts and backward dependencies" do
+            case preparedFooStructure "prepared_struct" of
+                Left err ->
+                    assertFailure
+                        ("could not prepare structure: " <> show err)
+                Right checked -> do
+                    let context = BlockContext Nowhere "prepared_struct"
+                        initial =
+                            initialCheckingState
+                                WithoutDumpPremselTraining
+                                (\_task -> pure ())
+                    case commitCheckedStructDefn context checked initial of
+                        Left err ->
+                            assertFailure
+                                ("could not commit structure: " <> show err)
+                        Right committed -> do
+                            assertBool
+                                "fact registry invariant"
+                                (Facts.factRegistryInvariant
+                                    (checkingFacts committed))
+                            for_
+                                (zip
+                                    (toList
+                                        (Structure.checkedStructMarkers checked))
+                                    (toList
+                                        (Structure.checkedStructSemanticFacts checked)))
+                                \(factMarker, prepared) ->
+                                    assertEqual
+                                        ("prepared fact " <> show factMarker)
+                                        (Just prepared)
+                                        (Facts.lookupPreparedFact
+                                            factMarker
+                                            (checkingFacts committed))
+                            assertEqual
+                                "structure dependencies"
+                                (Just
+                                    (Set.singleton
+                                        (SymbolPredicate
+                                            (PredicateNounStruct _Onesorted))))
+                                (Dependencies.lookupDependencies
+                                    (Structure.checkedStructSymbol checked)
+                                    (checkingDependencies committed))
+        ]
+
+preparedFooStructure
+    :: Marker
+    -> Either
+        Structure.StructurePreparationError
+        Structure.CheckedStructDefn
+preparedFooStructure marker =
+    Structure.prepareCheckedStructDefn
+        Nowhere
+        marker
+        (fooStructDefn [("prepared_rule", Top)])
+        (Set.singleton _Onesorted)
+        (Set.singleton CarrierSymbol)
+
+expectUnknownStructureParent
+    :: StructPhrase
+    -> [Block]
+    -> Assertion
+expectUnknownStructureParent expected blocks = do
+    result <-
+        try (check WithoutDumpPremselTraining blocks)
+            :: IO (Either CheckingError [Task])
+    case result of
+        Left (UnknownStructureParent actual Nowhere _) ->
+            assertEqual "unknown structure parent" expected actual
+        Left err ->
+            assertFailure
+                ("expected UnknownStructureParent, got " <> show err)
+        Right _ ->
+            assertFailure "expected an unknown structure parent"
+
 assumptionGoalReductionTests :: TestTree
 assumptionGoalReductionTests =
     testGroup "assumption goal reductions"
@@ -350,7 +484,9 @@ expectFactMarkers markers blocks = do
     checkingState <- runCheckingBlocks blocks (initialCheckingState WithoutDumpPremselTraining (\_task -> pure ()))
     let facts = checkingFacts checkingState
     for_ markers \marker ->
-        assertBool ("expected generated fact marker " <> show marker) (isJust (InsOrdMap.lookup marker facts))
+        assertBool
+            ("expected generated fact marker " <> show marker)
+            (isJust (Facts.lookupPreparedFact marker facts))
 
 expectDefinedMarkers :: [Marker] -> [Block] -> Assertion
 expectDefinedMarkers markers blocks = do
@@ -501,7 +637,11 @@ boundStructLabelBlocks =
 
 fooStructBlock :: Marker -> [(Marker, Formula)] -> Block
 fooStructBlock marker assumes =
-    BlockStruct Nowhere marker StructDefn
+    BlockStruct Nowhere marker (fooStructDefn assumes)
+
+fooStructDefn :: [(Marker, Formula)] -> StructDefn
+fooStructDefn assumes =
+    StructDefn
         { structPhrase = fooStruct
         , structParents = Set.singleton _Onesorted
         , structDefnLabel = "A"
@@ -509,10 +649,37 @@ fooStructBlock marker assumes =
         , structDefnAssumes = assumes
         }
 
+testStructBlock
+    :: Marker
+    -> StructPhrase
+    -> Set StructPhrase
+    -> [(Marker, Formula)]
+    -> Block
+testStructBlock marker phrase parents assumes =
+    BlockStruct Nowhere marker StructDefn
+        { structPhrase = phrase
+        , structParents = parents
+        , structDefnLabel = "A"
+        , structDefnFixes = mempty
+        , structDefnAssumes = assumes
+        }
+
 fooStruct :: StructPhrase
 fooStruct =
     mkLexicalItemSgPl (unsafeReadPhraseSgPl "foo[/s]") "foo"
 
+childStruct :: StructPhrase
+childStruct =
+    mkLexicalItemSgPl
+        (unsafeReadPhraseSgPl "child[/s]")
+        "child"
+
+unknownStruct :: StructPhrase
+unknownStruct =
+    mkLexicalItemSgPl
+        (unsafeReadPhraseSgPl "unknown[/s]")
+        "unknown"
+
 fooOp :: StructSymbol
 fooOp =
     StructSymbol "fooop"
@@ -521,6 +688,43 @@ fooStructPredicate :: VarSymbol -> Formula
 fooStructPredicate x =
     TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct fooStruct)) [TermVar x]
 
+hiddenSelfReferentialStructBlocks :: [Block]
+hiddenSelfReferentialStructBlocks =
+    [ BlockAbbr Nowhere "struct_alias_a"
+        ( Abbreviation
+            (SymbolPredicate structAliasA)
+            (toScope
+                (TermSymbol
+                    Nowhere
+                    (SymbolPredicate (PredicateNounStruct fooStruct))
+                    [TermVar (B 0)]))
+        )
+    , BlockAbbr Nowhere "struct_alias_b"
+        ( Abbreviation
+            (SymbolPredicate structAliasB)
+            (toScope
+                (TermSymbol
+                    Nowhere
+                    (SymbolPredicate structAliasA)
+                    [TermVar (B 0)]))
+        )
+    , fooStructBlock
+        "hidden_self_struct"
+        [("hidden_self_rule", structAliasFormula structAliasB (var "A"))]
+    ]
+
+structAliasA :: Predicate
+structAliasA =
+    PredicateSymbol "struct_alias_a"
+
+structAliasB :: Predicate
+structAliasB =
+    PredicateSymbol "struct_alias_b"
+
+structAliasFormula :: Predicate -> Term -> Formula
+structAliasFormula predicate term =
+    TermSymbol Nowhere (SymbolPredicate predicate) [term]
+
 var :: VarSymbol -> Term
 var = TermVar
 
diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs
index 9ed5bee..13f94c3 100644
--- a/source/Test/Unit/Provers.hs
+++ b/source/Test/Unit/Provers.hs
@@ -3,11 +3,11 @@
 module Test.Unit.Provers (unitTests) where
 
 import Base
-import Encoding (encodeHypothesis)
 import Provers
 import Report.Location (pattern Nowhere)
 import Syntax.Internal
     ( Directness(..)
+    , Hypothesis(..)
     , Marker(..)
     , Task(..)
     , pattern Top
@@ -328,5 +328,5 @@ largeTask =
         { taskHypotheses =
             replicate
                 20000
-                (encodeHypothesis (Marker "large") Top)
+                (Hypothesis (Marker "large") Top)
         }
diff --git a/source/Test/Unit/Symdiff.hs b/source/Test/Unit/Symdiff.hs
index 8d40320..bc205f0 100644
--- a/source/Test/Unit/Symdiff.hs
+++ b/source/Test/Unit/Symdiff.hs
@@ -3,7 +3,6 @@ module Test.Unit.Symdiff where
 import Base
 import Bound.Scope
 import Bound.Var
-import Encoding (encodeHypothesis)
 import Syntax.Internal
 import Filter
 import Report.Location
@@ -42,7 +41,6 @@ handlesStructAndApply =
         hypo = Hypothesis
             { hypothesisMarker = Marker "struct_apply"
             , hypothesisFormula = formula
-            , hypothesisEncoded = mempty
             }
     in Map.member hypo (relevantFacts passmark formula (Set.singleton hypo))
 
@@ -58,7 +56,7 @@ symdiff =
         , taskLocation = Nowhere
         , taskConjectureLabel = Marker "symdiff_test"
         , taskHypotheses = zipWith
-            encodeHypothesis
+            Hypothesis
             (Marker . Text.pack . show <$> ([1..] :: [Int]))
             [ Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))], TermVar (B (NamedVar "A"))]))
             , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]]))