content: -- Copyright 2020 Google LLC
  --
  -- Use of this source code is governed by a BSD-style
  -- license that can be found in the LICENSE file or at
  -- https://developers.google.com/open-source/licenses/bsd
  
  {-# LANGUAGE UndecidableInstances #-}
  
  module TopLevel (
    EvalConfig (..), Topper, TopperM, runTopperM,
    evalSourceBlockRepl, OptLevel (..), TopStateEx (..), LibPath (..),
    evalSourceBlockIO, initTopState, loadCache, storeCache, clearCache,
    ensureModuleLoaded, importModule, printCodegen,
    loadObject, toCFunction, packageLLVMCallable,
    simpOptimizations, loweredOptimizations, compileTopLevelFun,
    ExitStatus (..), parseSourceBlocks, captureLogs) where
  
  import Data.Functor
  import Data.Maybe (catMaybes)
  import Control.Exception (throwIO, catch)
  import Control.Monad.Writer.Strict  hiding (pass)
  import Control.Monad.State.Strict
  import Control.Monad.Reader
  import qualified Data.ByteString as BS
  import qualified Data.Text as T
  import Data.IORef
  import Data.Text.Prettyprint.Doc
  import Data.Store (encode, decode)
  import Data.String (fromString)
  import qualified Data.Map.Strict as M
  import qualified Data.Set        as S
  import Foreign.Ptr
  import Foreign.C.String
  import GHC.Generics (Generic (..))
  import System.FilePath
  import System.Directory
  import System.IO (stderr, hPutStrLn)
  import System.IO.Error (isDoesNotExistError)
  
  import LLVM.Link
  import LLVM.Compile
  import qualified LLVM.AST
  
  import AbstractSyntax
  import Builder
  import CheckType ( CheckableE (..), checkTypeIs)
  #ifdef DEX_DEBUG
  import CheckType (checkTypes)
  #endif
  import Core
  import ConcreteSyntax
  import CheapReduction
  import Err
  import IRVariants
  import Imp
  import ImpToLLVM
  import Inference
  import Inline
  import Lower
  import MonadUtil
  import MTL1
  import Subst
  import Name
  import OccAnalysis
  import Optimize
  import Paths_dex  (getDataFileName)
  import QueryType
  import Runtime
  import Serialize (takePtrSnapshot, restorePtrSnapshot)
  import Simplify
  import SourceRename
  import SourceIdTraversal
  import PPrint
  import Types.Core
  import Types.Imp
  import Types.Primitives
  import Types.Source
  import Types.Top
  import Util ( Tree (..), File (..), readFileWithHash)
  import Vectorize
  
  -- === top-level monad ===
  
  data LibPath = LibDirectory FilePath | LibBuiltinPath
  
  data EvalConfig = EvalConfig
    { backendName   :: Backend
    , libPaths      :: [LibPath]
    , preludeFile   :: Maybe FilePath
    , optLevel      :: OptLevel
    , printBackend  :: PrintBackend
    , cfgLogLevel   :: LogLevel }
  
  type LogAction = Outputs -> IO ()
  class Monad m => ConfigReader m where
    getConfig :: m EvalConfig
  
  class Monad m => RuntimeEnvReader m where
    getRuntimeEnv :: m RuntimeEnv
  
  type TopLogger m = (MonadIO m, Logger Outputs m)
  
  class ( forall n. Fallible (m n)
        , forall n. Logger Outputs (m n)
        , forall n. HasIOLogger Outputs (m n)
        , forall n. CanSetIOLogger Outputs (m n)
        , forall n. Catchable (m n)
        , forall n. ConfigReader (m n)
        , forall n. RuntimeEnvReader (m n)
        , forall n. MonadIO (m n)  -- TODO: something more restricted here
        , TopBuilder m )
        => Topper m
  
  data TopperReaderData = TopperReaderData
    { topperEvalConfig :: EvalConfig
    , topperLogAction  :: LogAction
    , topperRuntimeEnv :: RuntimeEnv }
  
  newtype TopperM (n::S) a = TopperM
    { runTopperM'
      :: TopBuilderT (ReaderT TopperReaderData IO) n a }
      deriving ( Functor, Applicative, Monad, MonadIO, MonadFail
               , Fallible, EnvReader, ScopeReader, Catchable)
  
  -- Hides the `n` parameter as an existential
  data TopStateEx where
    TopStateEx :: Distinct n => Env n -> RuntimeEnv -> TopStateEx
  instance Show TopStateEx where show _ = "TopStateEx"
  
  -- Hides the `n` parameter as an existential
  data TopSerializedStateEx where
    TopSerializedStateEx :: Distinct n => SerializedEnv n -> TopSerializedStateEx
  
  runTopperM
    :: EvalConfig -> LogAction -> TopStateEx
    -> (forall n. Mut n => TopperM n a)
    -> IO (a, TopStateEx)
  runTopperM opts logger (TopStateEx env rtEnv) cont = do
    Abs frag (LiftE result) <-
      flip runReaderT (TopperReaderData opts logger rtEnv) $
        runTopBuilderT env $ runTopperM' do
          localTopBuilder $ LiftE <$> cont
    return (result, extendTopEnv env rtEnv frag)
  
  extendTopEnv :: Distinct n => Env n -> RuntimeEnv -> TopEnvFrag n l -> TopStateEx
  extendTopEnv env rtEnv frag = do
    refreshAbsPure (toScope env) (Abs frag UnitE) \_ frag' UnitE ->
      TopStateEx (extendOutMap env frag') rtEnv
  
  initTopState :: IO TopStateEx
  initTopState = do
    dyvarStores <- allocateDynamicVarKeyPtrs
    return $ TopStateEx emptyOutMap dyvarStores
  
  allocateDynamicVarKeyPtrs :: IO DynamicVarKeyPtrs
  allocateDynamicVarKeyPtrs = do
    ptr <- createTLSKey
    return [(OutStreamDyvar, castPtr ptr)]
  
  captureLogs :: (LogAction -> IO a) -> IO (a, Outputs)
  captureLogs cont = do
    ref <- newIORef mempty
    ans <- cont \outs -> modifyIORef ref (<>outs)
    finalOuts <- readIORef ref
    return (ans, finalOuts)
  
  -- ======
  
  parseSourceBlocks :: T.Text -> [SourceBlock]
  parseSourceBlocks source = uModuleSourceBlocks $ parseUModule Main source
  
  evalSourceBlockIO
    :: EvalConfig -> LogAction -> TopStateEx -> SourceBlock -> IO (ExitStatus, TopStateEx)
  evalSourceBlockIO opts logger env block =
    runTopperM opts logger env $ evalSourceBlockRepl block
  
  data ExitStatus = ExitSuccess | ExitFailure  deriving (Show)
  
  -- Module imports have to be handled differently in the repl because we don't
  -- know ahead of time which modules will be needed.
  evalSourceBlockRepl :: (Topper m, Mut n) => SourceBlock -> m n ExitStatus
  evalSourceBlockRepl block = do
    case sbContents block of
      Misc (ImportModule name) -> do
        -- TODO: clear source map and synth candidates before calling this
        ensureModuleLoaded name
      _ -> return ()
    maybeErr <- evalSourceBlock Main block
    case maybeErr of
      Success () -> return ExitSuccess
      Failure e -> do
        logTop $ Error e
        return $ ExitFailure
  
  -- XXX: This ensures that a module and its transitive dependencies are loaded,
  -- (which will require evaluating them if they're not in the cache) but it
  -- doesn't bring the names and instances into scope. The modules are "loaded"
  -- but not yet "imported".
  ensureModuleLoaded :: (Topper m, Mut n) => ModuleSourceName -> m n ()
  ensureModuleLoaded moduleSourceName = do
    -- TODO: think about where import errors should be handled
    depsRequired <- findDepsTransitively moduleSourceName
    forM_ depsRequired \md -> do
      evaluated <- evalPartiallyParsedUModuleCached md
      updateTopEnv $ UpdateLoadedModules (umppName md) evaluated
  {-# SCC ensureModuleLoaded #-}
  
  evalSourceBlock
    :: (Topper m, Mut n) => ModuleSourceName -> SourceBlock -> m n (Except ())
  evalSourceBlock mname block = do
    maybeErr <- catchErrExcept do
      logTop $ SourceInfo $ SIGroupingInfo $ getGroupingInfo $ sbContents block
      evalSourceBlock' mname block
    case (maybeErr, sbContents block) of
      (Failure _, TopDecl decl) -> do
        case parseDecl decl of
          Success decl' -> emitSourceMap $ uDeclErrSourceMap (makeTopNameDescription mname block) decl'
          Failure _ -> return ()
      _ -> return ()
    return maybeErr
  
  evalSourceBlock'
    :: (Topper m, Mut n) => ModuleSourceName -> SourceBlock -> m n ()
  evalSourceBlock' mname block = case sbContents block of
    TopDecl decl -> parseDecl decl >>= execUDecl (makeTopNameDescription mname block)
    Command cmd expr' -> do
     expr <- parseExpr expr'
     case cmd of
      -- TODO: we should filter the top-level emissions we produce in this path
      -- we want cache entries but we don't want dead names.
      EvalExpr fmt -> when (mname == Main) case fmt of
        Printed maybeExplicitBackend -> do
          printMode <- case maybeExplicitBackend of
            Just backend -> return backend
            Nothing -> printBackend <$> getConfig
          case printMode of
            PrintHaskell -> do
              val <- evalUExpr expr
              logTop $ TextOut $ pprint val
            PrintCodegen -> do
              stringVal <- evalUExpr $ addShowAny expr
              s <- getDexString stringVal
              logTop $ TextOut s
        RenderHtml -> do
          stringVal <- evalUExpr $ addTypeAnn expr (referTo $ WithSrc (srcPos expr) "String")
          s <- getDexString stringVal
          logTop $ HtmlOut s
      ExportFun _ -> error "not implemented"
      --   f <- evalUModuleVal v m
      --   void $ traverseLiterals f \val -> case val of
      --     PtrLit _ _ -> throw CompilerErr $
      --       "Can't export functions with captured pointers (not implemented)."
      --     _ -> return $ Con $ Lit val
      --   logTop $ ExportedFun name f
      GetType -> do  -- TODO: don't actually evaluate it
        val <- evalUExpr expr
        logTop $ TextOut $ pprintCanonicalized $ getType val
    DeclareForeign fname (WithSrc _ dexName) cTy -> do
      ty <- evalUType =<< parseExpr cTy
      asFFIFunType ty >>= \case
        Nothing -> throwErr $ MiscErr $ MiscMiscErr
          "FFI functions must be n-ary first order functions with the IO effect"
        Just (impFunTy, naryPiTy) -> do
          -- TODO: query linking stuff and check the function is actually available
          let hint = fromString $ pprint dexName
          fTop  <- emitBinding hint $ TopFunBinding $ FFITopFun (pprint $ withoutSrc fname) impFunTy
          vCore <- emitBinding hint $ AtomNameBinding $ FFIFunBound naryPiTy fTop
          let desc = makeTopNameDescription mname block
          emitSourceMap $ SourceMap $
            M.singleton dexName [ModuleVar desc (Just $ UAtomVar vCore)]
    DeclareCustomLinearization fname zeros g -> do
      expr <- parseExpr g
      lookupSourceMap (withoutSrc fname) >>= \case
        Nothing -> throw rootSrcId $ UnboundVarErr $ pprint fname
        Just (UAtomVar fname') -> do
          lookupCustomRules fname' >>= \case
            Nothing -> return ()
            Just _  -> throwErr $ MiscErr $ MiscMiscErr
              $ pprint fname ++ " already has a custom linearization"
          lookupAtomName fname' >>= \case
            NoinlineFun _ _ -> return ()
            _ -> throwErr $ MiscErr $ MiscMiscErr "Custom linearizations only apply to @noinline functions"
          -- We do some special casing to avoid instantiating polymorphic functions.
          impl <- case expr of
            WithSrcE _ (UVar _) ->
              renameSourceNamesUExpr expr >>= \case
                WithSrcE _ (UVar (InternalName _ _ (UAtomVar v))) -> toAtom <$> toAtomVar v
                _ -> error "Expected a variable"
            _ -> evalUExpr expr
          fType <- getType <$> toAtomVar fname'
          (nimplicit, nexplicit, linFunTy) <- liftExceptEnvReaderM $ getLinearizationType zeros fType
          liftEnvReaderT (impl `checkTypeIs` linFunTy) >>= \case
            Failure _ -> do
              let implTy = getType impl
              throwErr $ MiscErr $ MiscMiscErr $ unlines
                [ "Expected the custom linearization to have type:" , "" , pprint linFunTy , ""
                , "but it has type:" , "" , pprint implTy]
            Success () -> return ()
          updateTopEnv $ AddCustomRule fname' $ CustomLinearize nimplicit nexplicit zeros impl
        Just _ -> throwErr $ MiscErr $ MiscMiscErr $ "Custom linearization can only be defined for functions"
    UnParseable _ s -> throwErr $ ParseErr $ MiscParseErr s
    Misc m -> case m of
      GetNameType v -> do
        lookupSourceMap (withoutSrc v) >>= \case
          Nothing -> throw rootSrcId $ UnboundVarErr $ pprint v
          Just uvar -> do
            ty <- getUVarType uvar
            logTop $ TextOut $ pprintCanonicalized ty
      ImportModule moduleName -> importModule moduleName
      QueryEnv query -> void $ runEnvQuery query $> UnitE
      ProseBlock _ -> return ()
      CommentLine  -> return ()
      EmptyLines   -> return ()
    where
      addTypeAnn :: UExpr n -> UExpr n -> UExpr n
      addTypeAnn e = WithSrcE (srcPos e) . UTypeAnn e
      addShowAny :: UExpr n -> UExpr n
      addShowAny e = WithSrcE (srcPos e) $ UApp (referTo $ WithSrc (srcPos e) "show_any") [e] []
      referTo :: SourceNameW -> UExpr n
      referTo (WithSrc sid name) =  WithSrcE sid $ UVar $ SourceName sid name
  
  runEnvQuery :: Topper m => EnvQuery -> m n ()
  runEnvQuery query = do
    env <- unsafeGetEnv
    case query of
      DumpSubst -> logTop $ TextOut $ pprint $ env
      InternalNameInfo name ->
        case lookupSubstFragRaw (fromRecSubst $ envDefs $ topEnv env) name of
          Nothing      -> throw rootSrcId $ UnboundVarErr $ pprint name
          Just binding -> logTop $ TextOut $ pprint binding
      SourceNameInfo name -> do
        lookupSourceMap name >>= \case
          Nothing -> throw rootSrcId $ UnboundVarErr $ pprint name
          Just uvar -> do
            logTop $ TextOut $ pprint uvar
            info <- case uvar of
              UAtomVar     v' -> pprint <$> lookupEnv v'
              UTyConVar    v' -> pprint <$> lookupEnv v'
              UDataConVar  v' -> pprint <$> lookupEnv v'
              UClassVar    v' -> pprint <$> lookupEnv v'
              UMethodVar   v' -> pprint <$> lookupEnv v'
              UPunVar v' -> do
                val <- lookupEnv v'
                return $ pprint val ++ "\n(type constructor and data constructor share the same name)"
            logTop $ TextOut $ "Binding:\n" ++ info
  
  -- returns a toposorted list of the module's transitive dependencies (including
  -- the module itself) excluding those provided in the set of already known
  -- modules.
  findDepsTransitively
    :: forall m n. (Topper m, Mut n)
    => ModuleSourceName -> m n [UModulePartialParse]
  findDepsTransitively initialModuleName = do
    alreadyLoaded <- M.keysSet . fromLoadedModules
      <$> withEnv (envLoadedModules . topEnv)
    flip evalStateT alreadyLoaded $ execWriterT $ go initialModuleName
    where
      go :: ModuleSourceName -> WriterT [UModulePartialParse]
                                  (StateT (S.Set ModuleSourceName) (m n)) ()
      go name = do
        alreadyVisited <- S.member name <$> get
        unless alreadyVisited do
          modify $ S.insert name
          config <- lift $ lift $ getConfig
          source <- loadModuleSource config name
          deps <- lift $ lift $ parseUModuleDepsCached name source
          mapM_ go deps
          tell [UModulePartialParse name deps source]
  
  -- What would it look like to abstract away pattern used here and in
  -- `evalPartiallyParsedUModuleCached`? We still want case-by-case control over
  -- keys, eviction policy, etc. Maybe some a type class for caches that implement
  -- query/extend, with `extend` being where the eviction happens?
  parseUModuleDepsCached
    :: (Mut n, TopBuilder m) => ModuleSourceName -> File -> m n [ModuleSourceName]
  parseUModuleDepsCached Main file = return $ parseUModuleDeps Main file
  parseUModuleDepsCached name file = do
    cache <- parsedDeps <$> getCache
    let req = fHash file
    case M.lookup name cache of
      Just (cachedReq, result) | cachedReq == req -> return result
      _ -> do
        let result = parseUModuleDeps name file
        updateTopEnv $ ExtendCache $ mempty { parsedDeps = M.singleton name (req, result) }
        return result
  
  evalPartiallyParsedUModuleCached
    :: (Topper m, Mut n)
    => UModulePartialParse -> m n (ModuleName n)
  evalPartiallyParsedUModuleCached md@(UModulePartialParse name deps source) = do
    case name of
      Main -> evalPartiallyParsedUModule md  -- Don't cache main
      _ -> do
        LiftE cache <- withEnv $ LiftE . moduleEvaluations . envCache . topEnv
        -- TODO: we know that these are sufficient to determine the result of
        -- module evaluation, but maybe we should actually restrict the
        -- environment we pass to `evalUModule` so that it can't possibly depend
        -- on anything else.
        directDeps <- forM deps \dep -> do
          lookupLoadedModule dep >>= \case
            Just depVal -> return depVal
            Nothing -> throwInternal $ pprint dep ++ " isn't loaded"
        let req = (fHash source, directDeps)
        case M.lookup name cache of
          Just (cachedReq, result) | cachedReq == req -> return result
          _ -> do
            liftIO $ hPutStrLn stderr $ "Compiling " ++ pprint name
            result <- evalPartiallyParsedUModule md
            updateTopEnv $ ExtendCache $ mempty {
              moduleEvaluations = M.singleton name (req, result) }
            return result
  
  -- Assumes all module dependencies have been loaded already
  evalPartiallyParsedUModule
    :: (Topper m, Mut n)
    => UModulePartialParse -> m n (ModuleName n)
  evalPartiallyParsedUModule partiallyParsed = do
    let name = umppName partiallyParsed
    let uModule = finishUModuleParse partiallyParsed
    evaluated <- evalUModule uModule
    emitBinding (getNameHint name) $ ModuleBinding evaluated
  
  -- Assumes all module dependencies have been loaded already
  evalUModule :: (Topper m, Mut n) => UModule -> m n (Module n)
  evalUModule (UModule name _ blocks) = dropSourceInfoLogging do
    Abs topFrag UnitE <- localTopBuilder $ mapM_ (evalSourceBlock' name) blocks >> return UnitE
    TopEnvFrag envFrag moduleEnvFrag otherUpdates <- return topFrag
    ModuleEnv (ImportStatus directDeps transDeps) sm scs <- return moduleEnvFrag
    let fragToReEmit = TopEnvFrag envFrag mempty otherUpdates
    let evaluatedModule = Module name directDeps transDeps sm scs
    emitEnv $ Abs fragToReEmit evaluatedModule
  
  dropSourceInfoLogging :: Topper m => m n a -> m n a
  dropSourceInfoLogging cont = do
    (ans, Outputs logs) <- captureIOLogs cont
    let logs' = filter isNotSourceInfo logs
    emitLog $ Outputs logs'
    return ans
    where
      isNotSourceInfo = \case
        SourceInfo _ -> False
        _ -> True
  
  importModule :: (Mut n, TopBuilder m, Fallible1 m) => ModuleSourceName -> m n ()
  importModule name = do
    lookupLoadedModule name >>= \case
      Nothing -> throwErr $ MiscErr $ ModuleImportErr $ pprint name
      Just name' -> do
        Module _ _ transImports' _ _ <- lookupModule name'
        let importStatus = ImportStatus (S.singleton name')
              (S.singleton name' <> transImports')
        emitLocalModuleEnv $ mempty { envImportStatus = importStatus }
  {-# SCC importModule #-}
  
  evalUType :: (Topper m, Mut n) => UType VoidS -> m n (CType n)
  evalUType ty = do
    logPass Parse ty
    renamed <- renameSourceNamesUExpr ty
    logPass RenamePass renamed
    checkPass TypePass $ checkTopUType renamed
  
  evalUExpr :: (Topper m, Mut n) => UExpr VoidS -> m n (CAtom n)
  evalUExpr expr = do
    logPass Parse expr
    renamed <- renameSourceNamesUExpr expr
    logPass RenamePass renamed
    typed <- checkPass TypePass $ inferTopUExpr renamed
    evalBlock typed
  
  whenOpt :: Topper m => a -> (a -> m n a) -> m n a
  whenOpt x act = getConfig <&> optLevel >>= \case
    NoOptimize -> return x
    Optimize   -> act x
  
  evalBlock :: (Topper m, Mut n) => TopBlock CoreIR n -> m n (CAtom n)
  evalBlock typed = do
    SimplifiedTopLam simp recon <- checkPass SimpPass $ simplifyTopBlock typed
    opt <- simpOptimizations simp
    simpResult <- case opt of
      TopLam _ _ (LamExpr Empty (Atom result)) -> return result
      _ -> do
        lowered <- checkPass LowerPass $ lowerFullySequential True opt
        lOpt <- checkPass OptPass $ loweredOptimizations lowered
        cc <- getEntryFunCC
        impOpt <- checkPass ImpPass $ toImpFunction cc lOpt
        llvmOpt <- packageLLVMCallable impOpt
        resultVals <- liftIO $ callEntryFun llvmOpt []
        TopLam _ destTy _ <- return lOpt
        EffTy _ resultTy <- return $ assumeConst $ piTypeWithoutDest destTy
        repValAtom =<< repValFromFlatList resultTy resultVals
    applyReconTop recon simpResult
  {-# SCC evalBlock #-}
  
  simpOptimizations :: Topper m => STopLam n -> m n (STopLam n)
  simpOptimizations simp = do
    analyzed <- whenOpt simp $ checkPass OccAnalysisPass . analyzeOccurrences
    inlined <- whenOpt analyzed $ checkPass InlinePass . inlineBindings
    analyzed2 <- whenOpt inlined $ checkPass OccAnalysisPass . analyzeOccurrences
    inlined2 <- whenOpt analyzed2 $ checkPass InlinePass . inlineBindings
    whenOpt inlined2 $ checkPass OptPass . optimize
  
  loweredOptimizations :: Topper m => STopLam n -> m n (STopLam n)
  loweredOptimizations lowered = do
    lopt <- whenOpt lowered $ checkPass LowerOptPass .
      (dceTop >=> hoistLoopInvariant)
    whenOpt lopt \lo -> do
      (vo, errs) <- vectorizeLoops 64 lo
      logTop $ TextOut $ pprint errs
      checkPass VectPass $ return vo
  
  loweredOptimizationsNoDest :: Topper m => STopLam n -> m n (STopLam n)
  loweredOptimizationsNoDest lowered = do
    lopt <- whenOpt lowered $ checkPass LowerOptPass .
      (dceTop >=> hoistLoopInvariant)
    -- TODO Add a NoDest entry point for vectorization and add it here
    return lopt
  
  evalSpecializations :: (Topper m, Mut n) => [TopFunName n] -> m n ()
  evalSpecializations fs = do
    fSimps <- toposortAnnVars <$> catMaybes <$> forM fs \f -> lookupTopFun f >>= \case
      DexTopFun _ simp Waiting -> return $ Just (f, simp)
      _ -> return Nothing
    forM_ fSimps \(f, simp) -> do
      -- Prevents infinite loop in case compiling `v` ends up requiring `v`
      -- (even without recursion in Dex itself this is possible via the
      -- specialization cache)
      updateTopEnv $ UpdateTopFunEvalStatus f Running
      imp <- compileTopLevelFun StandardCC simp
      objName <- toCFunction (getNameHint f) imp >>= emitObjFile
      void $ loadObject objName
      updateTopEnv $ UpdateTopFunEvalStatus f (Finished $ TopFunLowerings objName)
  
  evalDictSpecializations :: (Topper m, Mut n) => [SpecDictName n] -> m n ()
  evalDictSpecializations ds = do
    -- TODO Do we have to do these in order, like evalSpecializations, or are they
    -- independent enough not to need it?
    -- TODO Do we need to gate the status of these, too?
    forM_ ds \dName -> do
      SpecializedDict _ (Just fs) <- lookupSpecDict dName
      fs' <- forM fs \lam -> do
        opt <- simpOptimizations lam
        lowered <- checkPass LowerPass $ lowerFullySequential False opt
        loweredOptimizationsNoDest lowered
      updateTopEnv $ LowerDictSpecialization dName fs'
    return ()
  
  execUDecl
    :: (Topper m, Mut n) => TopNameDescription -> UTopDecl VoidS VoidS -> m n ()
  execUDecl desc decl = do
    logPass Parse decl
    renamed@(Abs renamedDecl sourceMap) <- renameSourceNamesTopUDecl desc decl
    logPass RenamePass renamed
    inferenceResult <- checkPass TypePass $ inferTopUDecl renamedDecl sourceMap
    case inferenceResult of
      UDeclResultBindName ann block (Abs b sm) -> do
        result <- evalBlock block
        case ann of
          NoInlineLet -> do
            let fTy = getType result
            f <- emitBinding (getNameHint b) $ AtomNameBinding $ NoinlineFun fTy result
            applyRename (b@>f) sm >>= emitSourceMap
          _ -> do
            v <- emitTopLet (getNameHint b) ann (Atom result)
            applyRename (b@>atomVarName v) sm >>= emitSourceMap
      UDeclResultBindPattern hint block (Abs bs sm) -> do
        result <- evalBlock block
        xs <- unpackTelescope bs result
        vs <- forM xs \x -> emitTopLet hint PlainLet (Atom x)
        applyRename (bs@@>(atomVarName <$> vs)) sm >>= emitSourceMap
      UDeclResultDone sourceMap' -> emitSourceMap sourceMap'
  
  compileTopLevelFun :: (Topper m, Mut n)
    => CallingConvention -> STopLam n -> m n (ImpFunction n)
  compileTopLevelFun cc fSimp = do
    fOpt <- simpOptimizations fSimp
    fLower <- checkPass LowerPass $ lowerFullySequential True fOpt
    flOpt <- loweredOptimizations fLower
    checkPass ImpPass $ toImpFunction cc flOpt
  
  printCodegen :: (Topper m, Mut n) => CAtom n -> m n String
  printCodegen x = do
    block <- liftBuilder $ buildBlock $ emit $ ShowAny $ sink x
    (topBlock, _) <- asTopBlock block
    getDexString =<< evalBlock topBlock
  
  loadObject :: (Topper m, Mut n) => FunObjCodeName n -> m n NativeFunction
  loadObject fname =
    lookupLoadedObject fname >>= \case
      Just p -> return p
      Nothing -> do
        f <- lookupFunObjCode fname >>= loadObjectContent
        updateTopEnv $ UpdateLoadedObjects fname f
        return f
  
  loadObjectContent :: (Topper m, Mut n) => CFunction n -> m n NativeFunction
  loadObjectContent CFunction{objectCode, linkerNames} = do
    (LinktimeNames funNames ptrNames) <- return linkerNames
    funVals <- forM funNames \name -> nativeFunPtr <$> loadObject name
    ptrVals <- forM ptrNames \name -> snd <$> lookupPtrName name
    dyvarStores <- getRuntimeEnv
    liftIO $ linkFunObjCode objectCode dyvarStores $ LinktimeVals funVals ptrVals
  
  linkFunObjCode
    :: FunObjCode -> DynamicVarKeyPtrs -> LinktimeVals -> IO NativeFunction
  linkFunObjCode objCode dyvarStores (LinktimeVals funVals ptrVals) = do
    let (WithCNameInterface code mainFunName reqFuns reqPtrs dtors) = objCode
    let linkMap =   zip reqFuns (map castFunPtrToPtr funVals)
                 <> zip reqPtrs ptrVals
                 <> dynamicVarLinkMap dyvarStores
    l <- createLinker
    addExplicitLinkMap l linkMap
    addObjectFile l code
    ptr <- getFunctionPointer l mainFunName
    dtorPtrs <- mapM (getFunctionPointer l) dtors
    let destructor :: IO () = do
          mapM_ callDtor dtorPtrs
          destroyLinker l
    return $ NativeFunction ptr destructor
  
  toCFunction :: (Topper m, Mut n) => NameHint -> ImpFunction n -> m n (CFunction n)
  toCFunction nameHint impFun = do
    logger <- getIOLogger
    (closedImpFun, reqFuns, reqPtrNames) <- abstractLinktimeObjects impFun
    obj <- impToLLVM logger nameHint closedImpFun >>= compileToObjCode
    reqObjNames <- mapM funNameToObj reqFuns
    return $ CFunction nameHint obj (LinktimeNames reqObjNames reqPtrNames)
  
  getLLVMOptLevel :: EvalConfig -> LLVMOptLevel
  getLLVMOptLevel cfg = case optLevel cfg of
    NoOptimize -> OptALittle
    Optimize   -> OptAggressively
  
  getEntryFunCC :: Topper m => m n CallingConvention
  getEntryFunCC = getConfig <&> backendName <&> \case
      LLVMCUDA -> EntryFunCC CUDARequired
      _        -> EntryFunCC CUDANotRequired
  
  packageLLVMCallable :: forall n m. (Topper m, Mut n)
    => ImpFunction n -> m n LLVMCallable
  packageLLVMCallable impFun = do
    nativeFun <- toCFunction "main" impFun >>= loadObjectContent
    logger <- getIOLogger
    let IFunType _ _ resultTypes = impFunType impFun
    return LLVMCallable{..}
  
  compileToObjCode :: Topper m => WithCNameInterface LLVM.AST.Module -> m n FunObjCode
  compileToObjCode astWithNames = forM astWithNames \ast -> do
    logger <- getIOLogger
    opt <- getLLVMOptLevel <$> getConfig
    liftIO $ compileLLVM logger opt ast (cniMainFunName astWithNames)
  
  funNameToObj
    :: (EnvReader m, Fallible1 m) => ImpFunName n -> m n (FunObjCodeName n)
  funNameToObj v = do
    lookupEnv v >>= \case
      TopFunBinding (DexTopFun _ _ (Finished impl)) -> return $ topFunObjCode impl
      b -> error $ "couldn't find object cache entry for " ++ pprint v ++ "\ngot:\n" ++ pprint b
  
  checkPass :: (Topper m, Pretty (e n), CheckableE r e)
            => PassName -> m n (e n) -> m n (e n)
  checkPass name cont = do
    result <- cont
    logPass name result
  #ifdef DEX_DEBUG
    logDebug $ return $ MiscLog $ "Running checks"
    checkTypes result
    logDebug $ return $ MiscLog $ "Checks passed"
  #else
    logDebug $ return $ MiscLog $ "Checks skipped (not a debug build)"
  #endif
    return result
  
  logTop :: TopLogger m => Output -> m ()
  logTop x = emitLog $ Outputs [x]
  
  logDebug :: TopLogger m => m Output -> m ()
  logDebug m = getLogLevel >>= \case
    NormalLogLevel -> return ()
    DebugLogLevel -> do
      x <- m
      emitLog $ Outputs [x]
  
  logPass :: Topper m => Pretty a => PassName -> a -> m n ()
  logPass passName result = do
    getLogLevel >>= \case
      NormalLogLevel -> logTop $ PassResult passName Nothing
      DebugLogLevel  -> logTop $ PassResult passName  $ Just s
        where s = "=== " <> pprint passName <> " ===\n" <> pprint result
  
  loadModuleSource
    :: (MonadIO m, Fallible m) => EvalConfig -> ModuleSourceName -> m File
  loadModuleSource config moduleName = do
    fullPath <- case moduleName of
      OrdinaryModule moduleName' -> findFullPath $ pprint moduleName' ++ ".dx"
      Prelude -> case preludeFile config of
        Nothing -> findFullPath "prelude.dx"
        Just path -> return path
      Main -> error "shouldn't be trying to load the source for main"
    readFileWithHash fullPath
    where
      findFullPath :: (MonadIO m, Fallible m) => String -> m FilePath
      findFullPath fname = do
        fsPaths <- liftIO $ traverse resolveBuiltinPath $ libPaths config
        liftIO (findFile fsPaths fname) >>= \case
          Just fpath -> return fpath
          Nothing    -> throwErr $ MiscErr $ CantFindModuleSource $ pprint moduleName
      resolveBuiltinPath = \case
        LibBuiltinPath   -> liftIO $ getDataFileName "lib"
        LibDirectory dir -> return dir
  {-# SCC loadModuleSource #-}
  
  getDexString :: (MonadIO1 m, EnvReader m, Fallible1 m) => Val CoreIR n -> m n String
  getDexString val = do
    -- TODO: use a `ByteString` instead of `String`
    Stuck _ (LiftSimp _ (RepValAtom (RepVal _ tree))) <- return val
    Branch [Leaf (IIdxRepVal n), Leaf (IPtrVar ptrName _)] <- return tree
    PtrBinding (CPU, Scalar Word8Type) (PtrLitVal ptr) <- lookupEnv ptrName
    liftIO $ peekCStringLen (castPtr ptr, fromIntegral n)
  
  -- === saving cache to disk ===
  
  -- None of this is safe in the presence of multiple processes trying to interact
  -- with the cache. But we plan to fix that by using an actual database.
  
  loadCache :: MonadIO m => m TopStateEx
  loadCache = liftIO do
    cachePath <- getCachePath
    cacheExists <- doesFileExist cachePath
    if cacheExists
      then do
        decoded <- decode <$> BS.readFile cachePath
        case decoded of
          Right result -> fromSerializedEnv result
          _            -> removeFile cachePath >> initTopState
      else initTopState
  {-# SCC loadCache #-}
  
  storeCache :: MonadIO m => TopStateEx -> m ()
  storeCache env = liftIO do
    cachePath <- getCachePath
    createDirectoryIfMissing True =<< getCacheDir
    TopSerializedStateEx sEnv <- toSerializedEnv env
    BS.writeFile cachePath $ encode sEnv
  
  snapshotPtrs :: MonadIO m => RecSubst Binding n -> m (RecSubst Binding n)
  snapshotPtrs bindings = RecSubst <$> traverseSubstFrag
    (\case
        PtrBinding ty p -> liftIO $ PtrBinding ty <$> takePtrSnapshot ty p
        b -> return b)
    (fromRecSubst bindings)
  
  traverseBindingsTopStateEx
    :: Monad m => TopStateEx
    -> (forall c n. Binding c n -> m (Binding c n)) -> m TopStateEx
  traverseBindingsTopStateEx (TopStateEx (Env tenv menv) dyvars) f = do
    defs <- traverseSubstFrag f $ fromRecSubst $ envDefs tenv
    return $ TopStateEx (Env (tenv {envDefs = RecSubst defs}) menv) dyvars
  
  fromSerializedEnv :: forall n m. MonadIO m => SerializedEnv n -> m TopStateEx
  fromSerializedEnv (SerializedEnv defs rules cache) = do
    Distinct <- return (fabricateDistinctEvidence :: DistinctEvidence n)
    dyvarStores <- liftIO allocateDynamicVarKeyPtrs
    let topEnv = Env (TopEnv defs rules cache mempty mempty) mempty
    restorePtrSnapshots $ TopStateEx topEnv dyvarStores
  
  toSerializedEnv :: MonadIO m => TopStateEx -> m TopSerializedStateEx
  toSerializedEnv (TopStateEx (Env (TopEnv (RecSubst defs) (CustomRules rules) cache _ _) _) _) = do
    collectGarbage (RecSubstFrag defs) (PairE (CustomRules rules) cache)
      \defsFrag'@(RecSubstFrag defs') (PairE (CustomRules rules') cache') -> do
        let liveNames = toNameSet $ toScopeFrag defsFrag'
        let rules'' = CustomRules
             $ M.filterWithKey (\k _ -> k `isInNameSet` liveNames) rules'
        defs'' <- snapshotPtrs (RecSubst defs')
        return $ TopSerializedStateEx $ SerializedEnv defs'' rules'' cache'
  
  getCacheDir :: MonadIO m => m FilePath
  getCacheDir = liftIO $ getXdgDirectory XdgCache "dex"
  
  getCachePath :: MonadIO m => m FilePath
  getCachePath = liftIO do
    cacheDir <- getCacheDir
    return $ cacheDir </> "dex.cache"
  
  clearCache :: MonadIO m => m ()
  clearCache = liftIO do
    cachePath <- getCachePath
    removeFile cachePath `catch` \e -> unless (isDoesNotExistError e) (throwIO e)
  
  restorePtrSnapshots :: MonadIO m => TopStateEx -> m TopStateEx
  restorePtrSnapshots s = traverseBindingsTopStateEx s \case
    PtrBinding ty p  -> liftIO $ PtrBinding ty <$> restorePtrSnapshot p
    b -> return b
  
  -- === instances ===
  
  instance RuntimeEnvReader (TopperM n) where
    getRuntimeEnv = TopperM $ asks topperRuntimeEnv
  
  instance ConfigReader (TopperM n) where
    getConfig = TopperM $ asks topperEvalConfig
  
  instance (Monad1 m, ConfigReader (m n)) => ConfigReader (StateT1 s m n) where
    getConfig = lift11 getConfig
  
  instance Topper TopperM
  
  instance TopBuilder TopperM where
    emitBinding = emitBindingDefault
    emitEnv (Abs frag result) = do
      result' `PairE` ListE fNames `PairE` ListE dictNames <- TopperM $ emitEnv $
        Abs frag $ result `PairE` ListE (boundNamesList frag) `PairE` ListE (boundNamesList frag)
      evalSpecializations fNames
      evalDictSpecializations dictNames
      return result'
    emitNamelessEnv env = TopperM $ emitNamelessEnv env
    localTopBuilder cont = TopperM $ localTopBuilder $ runTopperM' cont
  
  instance Logger Outputs (TopperM n) where
    emitLog x = do
      logger <- getIOLogAction
      liftIO $ logger x
    getLogLevel = cfgLogLevel <$> getConfig
  
  instance HasIOLogger Outputs (TopperM n) where
    getIOLogAction = TopperM $ asks topperLogAction
  
  instance CanSetIOLogger Outputs (TopperM n) where
    withIOLogAction logger (TopperM m) = TopperM do
      local (\r -> r { topperLogAction = logger }) m
  
  instance Generic TopStateEx where
    type Rep TopStateEx = Rep (Env UnsafeS, RuntimeEnv)
    from (TopStateEx env rtEnv) = from ((unsafeCoerceE env :: Env UnsafeS), rtEnv)
    to rep = do
      case fabricateDistinctEvidence :: DistinctEvidence UnsafeS of
        Distinct -> uncurry TopStateEx (to rep :: (Env UnsafeS, RuntimeEnv))
  
  getLinearizationType :: SymbolicZeros -> CType n -> EnvReaderT Except n (Int, Int, CType n)
  getLinearizationType zeros = \case
    TyCon (Pi (CorePiType ExplicitApp expls bs (EffTy Pure resultTy))) -> do
      (numIs, numEs) <- getNumImplicits expls
      refreshAbs (Abs bs resultTy) \bs' resultTy' -> do
        PairB _ bsE <- return $ splitNestAt numIs bs'
        let explicitArgTys = nestToList (\b -> sink $ binderType b) bsE
        argTanTys <- forM explicitArgTys \t -> maybeTangentType t >>= \case
          Just tty -> case zeros of
            InstantiateZeros -> return tty
            SymbolicZeros    -> symbolicTangentTy tty
          Nothing  -> throwErr $ MiscErr $ MiscMiscErr $ "No tangent type for: " ++ pprint t
        resultTanTy <- maybeTangentType resultTy' >>= \case
          Just rtt -> return rtt
          Nothing  -> throwErr $ MiscErr $ MiscMiscErr $ "No tangent type for: " ++ pprint resultTy'
        let tanFunTy = toType $ Pi $ nonDepPiType argTanTys Pure resultTanTy
        let fullTy = CorePiType ExplicitApp expls bs' $ EffTy Pure (PairTy resultTy' tanFunTy)
        return (numIs, numEs, toType $ Pi fullTy)
    _ -> throwErr $ MiscErr $ MiscMiscErr $ "Can't define a custom linearization for implicit or impure functions"
    where
      getNumImplicits :: Fallible m => [Explicitness] -> m (Int, Int)
      getNumImplicits = \case
        [] -> return (0, 0)
        expl:expls -> do
          (ni, ne) <- getNumImplicits expls
          case expl of
            Inferred _ _ -> return (ni + 1, ne)
            Explicit -> case ni of
              0 -> return (0, ne + 1)
              _ -> throwErr $ MiscErr $ MiscMiscErr "All implicit args must precede implicit args"
  