{-# 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)