Migrate to `Felix` namespaceHEADhotg

1 files changed, 116 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact/Global.hs b/source/Felix/Checking/Exact/Global.hs
new file mode 100644
index 0000000..d4040e6
--- /dev/null
+++ b/source/Felix/Checking/Exact/Global.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact resolution of source symbols to checked semantic globals.
+module Felix.Checking.Exact.Global
+    ( ExactGlobalResolutionError(..)
+    , resolveExactSourceGlobals
+    ) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
+import Felix.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)