    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Interface for compiler backend writers.
    module Agda.Compiler.Backend
      ( module Agda.Compiler.Backend.Base
      , Recompile(..), IsMain(..)
      , Flag
      , toTreeless
      , module Agda.Syntax.Treeless
      , module Agda.TypeChecking.Monad
      , module CheckResult
        -- For Agda.Main
      , backendInteraction
      , parseBackendOptions
        -- For InteractionTop
      , callBackend
      , callBackendInteractTop
      , callBackendInteractHole
      ) where

    import Prelude hiding (null)

    import Control.DeepSeq

    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import Agda.Utils.GetOpt

    import Agda.Compiler.Backend.Base
    import Agda.Compiler.Common
    import Agda.Compiler.ToTreeless

    import Agda.Interaction.Options
    import Agda.Interaction.FindFile
    import Agda.Interaction.Imports as CheckResult (CheckResult(CheckResult), crInterface, crWarnings, crMode)

    import Agda.Syntax.Common (BackendName)
    import Agda.Syntax.Treeless

    import Agda.TypeChecking.Errors (getAllWarnings)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Warnings

    import Agda.Utils.CallStack (HasCallStack)
    import Agda.Utils.FileName
    import Agda.Utils.Functor
    import Agda.Utils.IndexedList
    import Agda.Utils.Lens
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Maybe
    import Agda.Syntax.Common (InteractionId)
    import Agda.Syntax.Position (Range)

    import Agda.Interaction.Command (CommandM)

    -- Public interface -------------------------------------------------------

    -- | Call the 'compilerMain' function of the given backend.
    callBackend :: BackendName -> IsMain -> CheckResult -> TCM ()
    callBackend :: BackendName -> IsMain -> CheckResult -> TCM ()
    callBackend BackendName
    name IsMain
    iMain CheckResult
    checkResult =
      BackendName -> (Backend -> TCM ()) -> TCM ()
    forall (m :: * -> *).
    (MonadTCError m, ReadTCState m) =>
    BackendName -> (Backend -> m ()) -> m ()
    withKnownBackend BackendName
    name ((Backend -> TCM ()) -> TCM ()) -> (Backend -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \(Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) ->
        Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> IsMain -> CheckResult -> TCM ()
    forall opts env menv mod def.
    Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain Backend'_boot Definition (TCMT IO) opts env menv mod def
    b IsMain
    iMain CheckResult
    checkResult

    -- | Call the 'backendInteractTop' function of the given backend.
    callBackendInteractTop :: BackendName -> String -> CommandM ()
    callBackendInteractTop :: BackendName -> String -> CommandM ()
    callBackendInteractTop BackendName
    name String
    cmd =
      BackendName -> (Backend -> CommandM ()) -> CommandM ()
    forall (m :: * -> *).
    (MonadTCError m, ReadTCState m) =>
    BackendName -> (Backend -> m ()) -> m ()
    withKnownBackend BackendName
    name ((Backend -> CommandM ()) -> CommandM ())
    -> (Backend -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \(Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) ->
        Maybe (String -> CommandM ())
    -> ((String -> CommandM ()) -> CommandM ()) -> CommandM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> Maybe (String -> CommandM ())
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def
    -> Maybe (BackendCommandTop tcm)
    backendInteractTop Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) \String -> CommandM ()
    bi ->
          String -> CommandM ()
    bi String
    cmd

    -- | Call the 'backendInteractHole' function of the given backend.
    callBackendInteractHole ::
      BackendName -> String -> InteractionId -> Range -> String -> CommandM ()
    callBackendInteractHole :: BackendName
    -> String -> InteractionId -> Range -> String -> CommandM ()
    callBackendInteractHole BackendName
    name String
    cmd InteractionId
    ii Range
    rng String
    s =
      BackendName -> (Backend -> CommandM ()) -> CommandM ()
    forall (m :: * -> *).
    (MonadTCError m, ReadTCState m) =>
    BackendName -> (Backend -> m ()) -> m ()
    withKnownBackend BackendName
    name ((Backend -> CommandM ()) -> CommandM ())
    -> (Backend -> CommandM ()) -> CommandM ()
    forall a b. (a -> b) -> a -> b
    $ \(Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) ->
        Maybe (String -> InteractionId -> Range -> String -> CommandM ())
    -> ((String -> InteractionId -> Range -> String -> CommandM ())
        -> CommandM ())
    -> CommandM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> Maybe
         (String -> InteractionId -> Range -> String -> CommandM ())
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def
    -> Maybe (BackendCommandHole tcm)
    backendInteractHole Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) \String -> InteractionId -> Range -> String -> CommandM ()
    bi ->
          String -> InteractionId -> Range -> String -> CommandM ()
    bi String
    cmd InteractionId
    ii Range
    rng String
    s

    -- | Run a monadic action given an existing backend.
    -- Throws an error if the user requested an unknown backend.
    withKnownBackend ::
      (MonadTCError m, ReadTCState m) => BackendName -> (Backend -> m ()) -> m ()
    withKnownBackend :: forall (m :: * -> *).
    (MonadTCError m, ReadTCState m) =>
    BackendName -> (Backend -> m ()) -> m ()
    withKnownBackend BackendName
    name Backend -> m ()
    k = m (Maybe Backend) -> (Backend -> m ()) -> m () -> m ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> (a -> m b) -> m b -> m b
    ifJustM (BackendName -> m (Maybe Backend)
    forall (m :: * -> *).
    ReadTCState m =>
    BackendName -> m (Maybe Backend)
    lookupBackend BackendName
    name) Backend -> m ()
    k (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      backends <- Lens' TCState [Backend] -> m [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
    Lens' TCState [Backend]
    stBackends
      let backendSet = [BackendName]
    otherBackends [BackendName] -> [BackendName] -> [BackendName]
    forall a. [a] -> [a] -> [a]
    ++ [ Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> BackendName
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> BackendName
    backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
    b | Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b <- [Backend]
    backends ]
      typeError $ UnknownBackend name (Set.fromList backendSet)

    -- | Backends that are not included in the state, but still available
    --   to the user.
    otherBackends :: [BackendName]
    otherBackends :: [BackendName]
    otherBackends = [BackendName
    "GHCNoMain", BackendName
    "QuickLaTeX"]

    -- Internals --------------------------------------------------------------

    data BackendWithOpts opts where
      BackendWithOpts ::
        NFData opts =>
        Backend' opts env menv mod def ->
        BackendWithOpts opts

    backendWithOpts :: Backend -> Some BackendWithOpts
    backendWithOpts :: Backend -> Some BackendWithOpts
    backendWithOpts (Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    backend) = BackendWithOpts opts -> Some BackendWithOpts
    forall {k} (a :: k -> *) (i :: k). a i -> Some a
    Some (Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> BackendWithOpts opts
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> BackendWithOpts opts
    BackendWithOpts Backend'_boot Definition (TCMT IO) opts env menv mod def
    backend)

    forgetOpts :: BackendWithOpts opts -> Backend
    forgetOpts :: forall opts. BackendWithOpts opts -> Backend
    forgetOpts (BackendWithOpts Backend' opts env menv mod def
    backend) = Backend' opts env menv mod def -> Backend
    forall opts definition (tcm :: * -> *) env menv mod def.
    NFData opts =>
    Backend'_boot definition tcm opts env menv mod def
    -> Backend_boot definition tcm
    Backend Backend' opts env menv mod def
    backend

    bOptions :: Lens' (BackendWithOpts opts) opts
    bOptions :: forall opts (f :: * -> *).
    Functor f =>
    (opts -> f opts)
    -> BackendWithOpts opts -> f (BackendWithOpts opts)
    bOptions opts -> f opts
    f (BackendWithOpts Backend' opts env menv mod def
    b) = opts -> f opts
    f (Backend' opts env menv mod def -> opts
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> opts
    options Backend' opts env menv mod def
    b) f opts
    -> (opts -> BackendWithOpts opts) -> f (BackendWithOpts opts)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ opts
    opts -> Backend' opts env menv mod def -> BackendWithOpts opts
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> BackendWithOpts opts
    BackendWithOpts Backend' opts env menv mod def
    b{ options = opts }

    embedFlag :: Lens' b a -> Flag a -> Flag b
    embedFlag :: forall b a. Lens' b a -> Flag a -> Flag b
    embedFlag Lens' b a
    l Flag a
    flag = Flag a -> b -> OptM b
    Lens' b a
    l Flag a
    flag

    embedOpt :: Lens' b a -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt :: forall b a. Lens' b a -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt Lens' b a
    l = (Flag a -> Flag b) -> OptDescr (Flag a) -> OptDescr (Flag b)
    forall a b. (a -> b) -> OptDescr a -> OptDescr b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Lens' b a -> Flag a -> Flag b
    forall b a. Lens' b a -> Flag a -> Flag b
    embedFlag (a -> f a) -> b -> f b
    Lens' b a
    l)

    parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions :: [Backend]
    -> [String]
    -> CommandLineOptions
    -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions [Backend]
    backends [String]
    argv CommandLineOptions
    opts0 =
      case (Backend -> Some BackendWithOpts)
    -> [Backend] -> Some (All BackendWithOpts)
    forall {x} a (b :: x -> *). (a -> Some b) -> [a] -> Some (All b)
    makeAll Backend -> Some BackendWithOpts
    backendWithOpts [Backend]
    backends of
        Some All BackendWithOpts i
    bs -> do
          let agdaFlags :: [OptDescr (Flag (a, CommandLineOptions))]
    agdaFlags    = (OptDescr (Flag CommandLineOptions)
     -> OptDescr (Flag (a, CommandLineOptions)))
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag (a, CommandLineOptions))]
    forall a b. (a -> b) -> [a] -> [b]
    map (Lens' (a, CommandLineOptions) CommandLineOptions
    -> OptDescr (Flag CommandLineOptions)
    -> OptDescr (Flag (a, CommandLineOptions))
    forall b a. Lens' b a -> OptDescr (Flag a) -> OptDescr (Flag b)
    embedOpt (CommandLineOptions -> f CommandLineOptions)
    -> (a, CommandLineOptions) -> f (a, CommandLineOptions)
    forall a b (f :: * -> *).
    Functor f =>
    (b -> f b) -> (a, b) -> f (a, b)
    Lens' (a, CommandLineOptions) CommandLineOptions
    lSnd) ([OptDescr (Flag CommandLineOptions)]
    deadStandardOptions [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag CommandLineOptions)]
    standardOptions)
              backendFlags :: [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    backendFlags = do
                Some i            <- (forall x1. Index i x1 -> Some (Index i))
    -> All (Index i) i -> [Some (Index i)]
    forall {x} (b :: x -> *) a (xs :: [x]).
    (forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
    forgetAll Index i x1 -> Some (Index i)
    forall x1. Index i x1 -> Some (Index i)
    forall {k} (a :: k -> *) (i :: k). a i -> Some a
    Some (All (Index i) i -> [Some (Index i)])
    -> All (Index i) i -> [Some (Index i)]
    forall a b. (a -> b) -> a -> b
    $ All BackendWithOpts i -> All (Index i) i
    forall {x} (p :: x -> *) (xs :: [x]). All p xs -> All (Index xs) xs
    allIndices All BackendWithOpts i
    bs
                BackendWithOpts b <- [lookupIndex bs i]
                opt               <- commandLineFlags b
                return $ embedOpt (lFst . lIndex i . bOptions) opt
          (backends, opts) <- [String]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> (String -> Flag (All BackendWithOpts i, CommandLineOptions))
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple ([String] -> [String]
    stripRTS [String]
    argv)
                                           ([OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall {a}. [OptDescr (Flag (a, CommandLineOptions))]
    agdaFlags [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
    backendFlags) (Lens'
      (All BackendWithOpts i, CommandLineOptions) CommandLineOptions
    -> Flag CommandLineOptions
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall b a. Lens' b a -> Flag a -> Flag b
    embedFlag (CommandLineOptions -> f CommandLineOptions)
    -> (All BackendWithOpts i, CommandLineOptions)
    -> f (All BackendWithOpts i, CommandLineOptions)
    forall a b (f :: * -> *).
    Functor f =>
    (b -> f b) -> (a, b) -> f (a, b)
    Lens'
      (All BackendWithOpts i, CommandLineOptions) CommandLineOptions
    lSnd (Flag CommandLineOptions
     -> Flag (All BackendWithOpts i, CommandLineOptions))
    -> (String -> Flag CommandLineOptions)
    -> String
    -> Flag (All BackendWithOpts i, CommandLineOptions)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Flag CommandLineOptions
    inputFlag)
                                           (All BackendWithOpts i
    bs, CommandLineOptions
    opts0)
          opts <- checkOpts opts
          return (forgetAll forgetOpts backends, opts)

    backendInteraction :: AbsolutePath -> [Backend] -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
    backendInteraction :: AbsolutePath
    -> [Backend]
    -> TCM ()
    -> (AbsolutePath -> TCM CheckResult)
    -> TCM ()
    backendInteraction AbsolutePath
    mainFile [Backend]
    backends TCM ()
    setup AbsolutePath -> TCM CheckResult
    check = do
      TCM ()
    setup
      checkResult <- AbsolutePath -> TCM CheckResult
    check AbsolutePath
    mainFile

      -- reset warnings
      stTCWarnings `setTCLens` empty

      noMain <- optCompileNoMain <$> pragmaOptions
      let isMain | Bool
    noMain    = IsMain
    NotMain
                 | Bool
    otherwise = IsMain
    IsMain

      sequence_ [ compilerMain backend isMain checkResult | Backend backend <- backends ]

      -- print warnings that might have accumulated during compilation
      ws <- filter (not . isUnsolvedWarning . tcWarning) . Set.toAscList <$> getAllWarnings AllWarnings
      unless (null ws) $ alwaysReportSDoc "warning" 1 $
        -- Andreas, 2024-09-06 start warning list by a newline
        -- since type checker warnings are also newline separated.
        -- See e.g. test/Succeed/CompileBuiltinListWarning.warn.
        -- Also separate warnings by newlines (issue #6919).
        vcat $ concatMap (\ TCWarning
    w -> [ TCMT IO Doc
    "", TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
    prettyTCM TCWarning
    w ]) ws

    compilerMain :: Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain :: forall opts env menv mod def.
    Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
    compilerMain Backend' opts env menv mod def
    backend IsMain
    isMain0 CheckResult
    checkResult = CheckResult -> TCM () -> TCM ()
    forall a. CheckResult -> TCM a -> TCM a
    inCompilerEnv CheckResult
    checkResult (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      Lens' TCEnv (Maybe BackendName)
    -> (Maybe BackendName -> Maybe BackendName) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Maybe BackendName -> f (Maybe BackendName)) -> TCEnv -> f TCEnv
    Lens' TCEnv (Maybe BackendName)
    eActiveBackendName (Maybe BackendName -> Maybe BackendName -> Maybe BackendName
    forall a b. a -> b -> a
    const (Maybe BackendName -> Maybe BackendName -> Maybe BackendName)
    -> Maybe BackendName -> Maybe BackendName -> Maybe BackendName
    forall a b. (a -> b) -> a -> b
    $ BackendName -> Maybe BackendName
    forall a. a -> Maybe a
    Just (BackendName -> Maybe BackendName)
    -> BackendName -> Maybe BackendName
    forall a b. (a -> b) -> a -> b
    $ Backend' opts env menv mod def -> BackendName
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> BackendName
    backendName Backend' opts env menv mod def
    backend) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        -- BEWARE: Do not use @optOnlyScopeChecking@ here; it does not authoritatively describe the type-checking mode!
        -- InteractionTop currently may invoke type-checking with scope checking regardless of that flag.
        Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Bool -> Bool
    not (Backend' opts env menv mod def -> Bool
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> Bool
    scopeCheckingSuffices Backend' opts env menv mod def
    backend) Bool -> Bool -> Bool
    && CheckResult -> ModuleCheckMode
    crMode CheckResult
    checkResult ModuleCheckMode -> ModuleCheckMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleCheckMode
    ModuleScopeChecked) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ BackendName -> TypeError
    BackendDoesNotSupportOnlyScopeChecking (BackendName -> TypeError) -> BackendName -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Backend' opts env menv mod def -> BackendName
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> BackendName
    backendName Backend' opts env menv mod def
    backend

        !i <- Interface -> TCMT IO Interface
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Interface -> TCMT IO Interface) -> Interface -> TCMT IO Interface
    forall a b. (a -> b) -> a -> b
    $ CheckResult -> Interface
    crInterface CheckResult
    checkResult
        -- Andreas, 2017-08-23, issue #2714
        -- If the backend is invoked from Emacs, we can only get the --no-main
        -- pragma option now, coming from the interface file.
        !isMain <- ifM (optCompileNoMain <$> pragmaOptions)
          {-then-} (return NotMain)
          {-else-} (return isMain0)

        env  <- preCompile backend (options backend)
        mods <- doCompile
            -- This inner function is called for both `Agda.Primitive` and the module in question,
            -- and all (distinct) imported modules. So avoid shadowing "isMain" or "i".
            (\IsMain
    ifaceIsMain Interface
    iface ->
              TopLevelModuleName -> mod -> Map TopLevelModuleName mod
    forall k a. k -> a -> Map k a
    Map.singleton (Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    iface) (mod -> Map TopLevelModuleName mod)
    -> TCMT IO mod -> TCM (Map TopLevelModuleName mod)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCMT IO mod
    forall opts env menv mod def.
    HasCallStack =>
    Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCM mod
    compileModule Backend' opts env menv mod def
    backend env
    env IsMain
    ifaceIsMain Interface
    iface)
            isMain i
        -- Note that `doCompile` calls `setInterface` for each distinct module in the graph prior to calling into
        -- `compileModule`. This last one is just to ensure it's reset to _this_ module.
        setInterface i
        postCompile backend env isMain mods

    compileModule :: HasCallStack => Backend' opts env menv mod def -> env -> IsMain -> Interface -> TCM mod
    compileModule :: forall opts env menv mod def.
    HasCallStack =>
    Backend' opts env menv mod def
    -> env -> IsMain -> Interface -> TCM mod
    compileModule Backend' opts env menv mod def
    backend env
    env IsMain
    isMain Interface
    i = do
      mName <- TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
      -- The interface file will only exist if performing af full type-check, vs scoping.
      -- FIXME: Expecting backends to read the timestamp of the output path of the interface
      --        file for dirtiness checking is very roundabout and heavily couples backend
      --        implementations to the filesystem as the source of cache state.
      mifile <- (Just . filePath . intFilePath =<<) <$> findInterfaceFile mName
      r      <- preModule backend env isMain (iTopLevelModuleName i) mifile
      case r of
        Skip mod
    m         -> mod -> TCMT IO mod
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return mod
    m
        Recompile menv
    menv -> do
          defs <- ((QName, Definition) -> Definition)
    -> [(QName, Definition)] -> [Definition]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName, Definition) -> Definition
    forall a b. (a, b) -> b
    snd ([(QName, Definition)] -> [Definition])
    -> (Definitions -> [(QName, Definition)])
    -> Definitions
    -> [Definition]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definitions -> [(QName, Definition)]
    sortDefs (Definitions -> [Definition])
    -> TCMT IO Definitions -> TCMT IO [Definition]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Definitions
    forall (m :: * -> *). ReadTCState m => m Definitions
    curDefs
          res  <- mapM (compileDef' backend env menv isMain) defs
          postModule backend env menv isMain (iTopLevelModuleName i) res

    compileDef' :: Backend' opts env menv mod def -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef' :: forall opts env menv mod def.
    Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCM def
    compileDef' Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain Definition
    def =
      QName -> TCMT IO def -> TCMT IO def
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Definition -> QName
    defName Definition
    def) (TCMT IO def -> TCMT IO def) -> TCMT IO def -> TCMT IO def
    forall a b. (a -> b) -> a -> b
    $
        Backend' opts env menv mod def
    -> env -> menv -> IsMain -> Definition -> TCMT IO def
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def
    -> env -> menv -> IsMain -> definition -> tcm def
    compileDef Backend' opts env menv mod def
    backend env
    env menv
    menv IsMain
    isMain Definition
    def