
-- | Name resolution via the type checker context.
--
--   The general process is
      1 ) First try to lookup a name from the type checker context of
--        the module currently being checked.
--     2) Look in the oracle cache for things imported from other modules
--        that we've used before.
      3 ) Get the oracle to ask the interface store to see if the thing
--        is visibly imported from another module, perhaps transitively.
--
module DDC.Core.Check.Context.Resolve
        ( TyConThing(..)
        , resolveTyConThing
        , lookupTypeSyn
        , lookupDataType
        , lookupDataCtor
        , lookupTypeOfValueName)
where
import DDC.Core.Check.State
import DDC.Core.Check.Context.Base
import DDC.Core.Check.Error
import DDC.Core.Interface.Oracle                (TyConThing(..))
import DDC.Type.Exp
import DDC.Type.DataDef
import qualified DDC.Core.Interface.Oracle      as Oracle
import qualified DDC.Core.Module                as C
import qualified DDC.Core.Env.EnvT              as EnvT
import qualified DDC.Core.Env.EnvX              as EnvX
import qualified Data.Map.Strict                as Map


---------------------------------------------------------------------------------------------------
-- | Resolve the name of a data type, type synonym, for foreign type.
--
--   These are all named after a type constructor, but they have different
--   sorts of declarations.
--
--   If we can't find one then throw an error in the `CheckM` monad.
--
resolveTyConThing
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (TyConThing n, Kind n)

resolveTyConThing ctx n
 = lookupTyConThing ctx n
 >>= \case
        Nothing -> throw  $ ErrorType $ ErrorTypeUndefinedTypeCtor (UName n)
        Just tk -> return tk


-- | Lookup the name of a data type, type synonym, for foreign type.
--
--   If we can't find it then `Nothing`.
--
lookupTyConThing
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (TyConThing n, Kind n))

lookupTyConThing ctx n
 -- Look for a primitive type of the same name.
 | Just k        <- EnvT.envtPrimFun (contextEnvT ctx) n
 = return $ Just (TyConThingPrim n k, k)

 -- Look for a data type defined in the current module.
 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataType <- Map.lookup n (dataDefsTypes dataDefs)
 = return $ Just ( TyConThingData n dataType
                 , kindOfDataType dataType)

 -- Look for a type synonym defined in the current module.
 | Just tBind    <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx
 , Just kBind    <- Map.lookup n $ EnvT.envtMap $ contextEnvT ctx
 = return $ Just  ( TyConThingSyn n kBind tBind
                  , kBind)

 -- Look for a foreign type defined in the current module.
 | Just it      <- Map.lookup n $ EnvT.envtForeignTypes $ contextEnvT ctx
 = return $ Just  ( TyConThingForeign n it
                  , C.kindOfImportType it )

 -- Look for a data type, synonym or foreign type in an imported module.
 | Just oracle  <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err           -> throw $ checkOfResolveError n err
        Right Nothing      -> return Nothing
        Right (Just thing) -> return $ Just (thing, Oracle.kindOfTyConThing thing)

 -- It's just not there.
 | otherwise
 = return Nothing


---------------------------------------------------------------------------------------------------
-- | Lookup the definition of a type synonym from its name.
--
--   If we can't find it then `Nothing`.
--
lookupTypeSyn
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (Type n))

lookupTypeSyn ctx n
 -- Look for synonyom in the current module.
 | Just tR  <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx
 = return $ Just tR

 -- Look for synonym in imported modules.
 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right (Just (TyConThingSyn _ _ t))
                        -> return $ Just t
        Right (Just _)  -> return Nothing
        Right Nothing   -> return Nothing

 -- It's just not there.
 | otherwise    = return Nothing


---------------------------------------------------------------------------------------------------
-- | Lookup the definition of a data type.
--
--   If we can't find it then `Nothing`.
--
lookupDataType
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (DataType n))

lookupDataType ctx n
 -- Look for data type definition in the current module.
 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataType <- Map.lookup n (dataDefsTypes dataDefs)
 = return $ Just dataType

 -- Look for data type definition in an imported module.
 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right Nothing   -> return Nothing
        Right (Just (TyConThingData _ dataType))
                        -> return $ Just dataType
        Right (Just _)  -> return Nothing

 -- It's just not there.
 | otherwise    = return Nothing


---------------------------------------------------------------------------------------------------
-- | Lookup the definition of a data constructor.
--
--   If we can't find it then `Nothing`.
--
lookupDataCtor
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (DataCtor n))

lookupDataCtor ctx n

 -- Look for data ctor in the current module, or as a primitive.
 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataCtor <- Map.lookup n (dataDefsCtors dataDefs)
 = return $ Just dataCtor

 -- Look for data ctor in imported modules.
 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveDataCtor oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right mc        -> return mc

 -- It's just not there.
 | otherwise    = return Nothing


---------------------------------------------------------------------------------------------------
-- | Lookup the type of a value.
--
--   If we can't find then `Nothing`.
--
lookupTypeOfValueName
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (Type n))

lookupTypeOfValueName ctx n
 -- Look for value on the context stack.
 | Just t       <- lookupType (UName n) ctx
 = return $ Just t

 -- Look for value at the top level of the current module,
 -- or as a primitive.
 | Just t       <- EnvX.lookupX (UName n) $ contextEnvX ctx
 = return $ Just t

 -- Look for value in imported modules.
 | Just oracle  <- contextOracle ctx
 = (liftIO $ Oracle.resolveValueName oracle n)
 >>= \case
        Left err         -> throw  $ checkOfResolveError n err
        Right (Just ivs) -> return $ Just $ C.typeOfImportValue ivs
        Right Nothing    -> return Nothing

 -- Its just not there.
 | otherwise    = return Nothing



 | Name resolution via the type checker context.

   The general process is
        the module currently being checked.
     2) Look in the oracle cache for things imported from other modules
        that we've used before.
        is visibly imported from another module, perhaps transitively.

-------------------------------------------------------------------------------------------------
 | Resolve the name of a data type, type synonym, for foreign type.

   These are all named after a type constructor, but they have different
   sorts of declarations.

   If we can't find one then throw an error in the `CheckM` monad.

 | Lookup the name of a data type, type synonym, for foreign type.

   If we can't find it then `Nothing`.

 Look for a primitive type of the same name.
 Look for a data type defined in the current module.
 Look for a type synonym defined in the current module.
 Look for a foreign type defined in the current module.
 Look for a data type, synonym or foreign type in an imported module.
 It's just not there.
-------------------------------------------------------------------------------------------------
 | Lookup the definition of a type synonym from its name.

   If we can't find it then `Nothing`.

 Look for synonyom in the current module.
 Look for synonym in imported modules.
 It's just not there.
-------------------------------------------------------------------------------------------------
 | Lookup the definition of a data type.

   If we can't find it then `Nothing`.

 Look for data type definition in the current module.
 Look for data type definition in an imported module.
 It's just not there.
-------------------------------------------------------------------------------------------------
 | Lookup the definition of a data constructor.

   If we can't find it then `Nothing`.

 Look for data ctor in the current module, or as a primitive.
 Look for data ctor in imported modules.
 It's just not there.
-------------------------------------------------------------------------------------------------
 | Lookup the type of a value.

   If we can't find then `Nothing`.

 Look for value on the context stack.
 Look for value at the top level of the current module,
 or as a primitive.
 Look for value in imported modules.
 Its just not there.

      1 ) First try to lookup a name from the type checker context of
      3 ) Get the oracle to ask the interface store to see if the thing
module DDC.Core.Check.Context.Resolve
        ( TyConThing(..)
        , resolveTyConThing
        , lookupTypeSyn
        , lookupDataType
        , lookupDataCtor
        , lookupTypeOfValueName)
where
import DDC.Core.Check.State
import DDC.Core.Check.Context.Base
import DDC.Core.Check.Error
import DDC.Core.Interface.Oracle                (TyConThing(..))
import DDC.Type.Exp
import DDC.Type.DataDef
import qualified DDC.Core.Interface.Oracle      as Oracle
import qualified DDC.Core.Module                as C
import qualified DDC.Core.Env.EnvT              as EnvT
import qualified DDC.Core.Env.EnvX              as EnvX
import qualified Data.Map.Strict                as Map


resolveTyConThing
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (TyConThing n, Kind n)

resolveTyConThing ctx n
 = lookupTyConThing ctx n
 >>= \case
        Nothing -> throw  $ ErrorType $ ErrorTypeUndefinedTypeCtor (UName n)
        Just tk -> return tk


lookupTyConThing
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (TyConThing n, Kind n))

lookupTyConThing ctx n
 | Just k        <- EnvT.envtPrimFun (contextEnvT ctx) n
 = return $ Just (TyConThingPrim n k, k)

 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataType <- Map.lookup n (dataDefsTypes dataDefs)
 = return $ Just ( TyConThingData n dataType
                 , kindOfDataType dataType)

 | Just tBind    <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx
 , Just kBind    <- Map.lookup n $ EnvT.envtMap $ contextEnvT ctx
 = return $ Just  ( TyConThingSyn n kBind tBind
                  , kBind)

 | Just it      <- Map.lookup n $ EnvT.envtForeignTypes $ contextEnvT ctx
 = return $ Just  ( TyConThingForeign n it
                  , C.kindOfImportType it )

 | Just oracle  <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err           -> throw $ checkOfResolveError n err
        Right Nothing      -> return Nothing
        Right (Just thing) -> return $ Just (thing, Oracle.kindOfTyConThing thing)

 | otherwise
 = return Nothing


lookupTypeSyn
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (Type n))

lookupTypeSyn ctx n
 | Just tR  <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx
 = return $ Just tR

 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right (Just (TyConThingSyn _ _ t))
                        -> return $ Just t
        Right (Just _)  -> return Nothing
        Right Nothing   -> return Nothing

 | otherwise    = return Nothing


lookupDataType
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (DataType n))

lookupDataType ctx n
 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataType <- Map.lookup n (dataDefsTypes dataDefs)
 = return $ Just dataType

 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveTyConThing oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right Nothing   -> return Nothing
        Right (Just (TyConThingData _ dataType))
                        -> return $ Just dataType
        Right (Just _)  -> return Nothing

 | otherwise    = return Nothing


lookupDataCtor
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (DataCtor n))

lookupDataCtor ctx n

 | dataDefs      <- EnvX.envxDataDefs $ contextEnvX ctx
 , Just dataCtor <- Map.lookup n (dataDefsCtors dataDefs)
 = return $ Just dataCtor

 | Just oracle <- contextOracle ctx
 = (liftIO $ Oracle.resolveDataCtor oracle n)
 >>= \case
        Left err        -> throw $ checkOfResolveError n err
        Right mc        -> return mc

 | otherwise    = return Nothing


lookupTypeOfValueName
        :: (Ord n, Show n)
        => Context n -> n -> CheckM a n (Maybe (Type n))

lookupTypeOfValueName ctx n
 | Just t       <- lookupType (UName n) ctx
 = return $ Just t

 | Just t       <- EnvX.lookupX (UName n) $ contextEnvX ctx
 = return $ Just t

 | Just oracle  <- contextOracle ctx
 = (liftIO $ Oracle.resolveValueName oracle n)
 >>= \case
        Left err         -> throw  $ checkOfResolveError n err
        Right (Just ivs) -> return $ Just $ C.typeOfImportValue ivs
        Right Nothing    -> return Nothing

 | otherwise    = return Nothing


