1 files changed, 0 insertions, 150 deletions
diff --git a/source/Checking/Structure.hs b/source/Checking/Structure.hs
deleted file mode 100644
index ce4a2ac..0000000
--- a/source/Checking/Structure.hs
+++ /dev/null
@@ -1,150 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE RecordWildCards #-}
-
-module Checking.Structure
-    ( CheckedStructDefn
-    , StructurePreparationError(..)
-    , prepareCheckedStructDefn
-    , checkedStructPhrase
-    , checkedStructAncestors
-    , checkedStructInternalSymbols
-    , checkedStructAllSymbols
-    , checkedStructSymbol
-    , checkedStructDependencies
-    , checkedStructSemanticFacts
-    , checkedStructFacts
-    , checkedStructFactRoles
-    , checkedStructMarkers
-    ) where
-
-import Base
-import Checking.Facts
-import Checking.Legacy
-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
-
-checkedStructFactRoles
-    :: CheckedStructDefn
-    -> NonEmpty LegacyStructureFactRole
-checkedStructFactRoles checked =
-    LegacyStructureIntroduction
-        :| ( LegacyStructureInheritance
-                : replicate
-                    (max 0 (factCount - 2))
-                    LegacyStructureAssumption
-           )
-  where
-    factCount =
-        length (checkedStructFacts checked)
-
-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