1 files changed, 0 insertions, 116 deletions
diff --git a/source/Checking/Exact/Global.hs b/source/Checking/Exact/Global.hs
deleted file mode 100644
index 772a7e2..0000000
--- a/source/Checking/Exact/Global.hs
+++ /dev/null
@@ -1,116 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Exact resolution of source symbols to checked semantic globals.
-module Checking.Exact.Global
-    ( ExactGlobalResolutionError(..)
-    , resolveExactSourceGlobals
-    ) where
-
-import Base
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
-import Syntax.Internal qualified as Internal
-
-import Control.Monad (foldM)
-import Control.Monad.Except
-    ( liftEither
-    , runExceptT
-    , throwError
-    )
-import Control.Monad.Trans.Class (lift)
-import Data.Bifunctor (first)
-import Data.Map.Strict qualified as Map
-import Data.Maybe (catMaybes)
-import Data.Set qualified as Set
-
-
-data ExactGlobalResolutionError
-    = ExactGlobalNotVisible !Internal.Symbol
-    | ExactGlobalAmbiguous !Internal.Symbol
-    | ExactGlobalUnsupported !Internal.Symbol
-    | ExactGlobalContextualUnsupported !Internal.Symbol
-    | ExactGlobalContentInvalid !CoreCheckError
-    deriving stock (Show, Eq)
-
-resolveExactSourceGlobals
-    :: Set.Set Internal.Symbol
-    -> Declaration.LoweringDriver
-        (Either
-            ExactGlobalResolutionError
-            ( Map.Map
-                Internal.Symbol
-                (Typed.SourceGlobal ObjectId)
-            , Map.Map ObjectId CoreType
-            ))
-resolveExactSourceGlobals symbols =
-    runExceptT
-        (foldM resolve (Map.empty, Map.empty)
-            (Set.toAscList symbols))
-  where
-    resolve (resolved, types) symbol =
-        case classifyExactSymbol symbol of
-            ExactClosedLiteral ->
-                pure (resolved, types)
-            ExactFixedPrimitive _meaning ->
-                pure (resolved, types)
-            ExactUnsupportedSymbol ->
-                throwError (ExactGlobalUnsupported symbol)
-            ExactSourceGlobal keys -> do
-                matches <-
-                    catMaybes
-                        <$> traverse
-                            (lift
-                                . Declaration.resolveVisibleGlobalContentLowering)
-                            (toList keys)
-                case matches of
-                    [] ->
-                        throwError (ExactGlobalNotVisible symbol)
-                    [match] -> do
-                        (source, sourceTypes) <-
-                            liftEither (prepareSourceGlobal symbol match)
-                        pure
-                            ( Map.insert symbol source resolved
-                            , Map.union sourceTypes types
-                            )
-                    _ ->
-                        throwError (ExactGlobalAmbiguous symbol)
-
-prepareSourceGlobal
-    :: Internal.Symbol
-    -> ( SemanticGlobalTarget
-       , ObjectContent
-       , Map.Map ObjectId CoreType
-       )
-    -> Either
-        ExactGlobalResolutionError
-        (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
-prepareSourceGlobal symbol (target, content, dependencies) = do
-    body <-
-        case target of
-            GlobalReference _identity ->
-                Right Nothing
-            TransparentExpansion _identity ->
-                case content of
-                    TransparentObjectContent _theory _coreType canonical ->
-                        Just
-                            <$> first ExactGlobalContentInvalid
-                                (checkCanonicalCore
-                                    (`Map.lookup` dependencies)
-                                    canonical)
-                    _ ->
-                        impossible
-                            "validated transparent expansion has opaque content"
-            ContextualTransparentExpansion _identity _requirements ->
-                Left (ExactGlobalContextualUnsupported symbol)
-    let identity = semanticGlobalTargetObject target
-        types =
-            Map.insert
-                identity
-                (objectContentType content)
-                dependencies
-    pure (Typed.SourceGlobal identity body, types)