{-# OPTIONS_GHC -Wunused-imports #-}

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

import Agda.Compiler.Backend.Base

import Control.DeepSeq
import Control.Monad.Trans        ( lift )
import Control.Monad.Trans.Maybe

import qualified Data.List as List
import Data.Maybe

import qualified Data.Map as Map

import System.Console.GetOpt

import Agda.Syntax.Treeless
import Agda.TypeChecking.Errors (getAllWarnings)
-- Agda.TypeChecking.Monad.Base imports us, relying on the .hs-boot file to
-- resolve the circular dependency. Fine. However, ghci loads the module after
-- compilation, so it brings in all of the symbols. That causes .Base to see
-- getBenchmark (defined in Agda.TypeChecking.Monad.State) *and* the one
-- defined in Agda.Utils.Benchmark, which causes an error. So we explicitly
-- hide it here to prevent it from being seen there and causing an error.
import Agda.TypeChecking.Monad hiding (getBenchmark)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty as P

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

import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.IndexedList
import Agda.Utils.Lens
import Agda.Utils.Monad

import Agda.Compiler.ToTreeless
import Agda.Compiler.Common

import Agda.Utils.Impossible

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

type Backend = Backend_boot TCM

type Backend' opts env menv mod def = Backend'_boot TCM opts env menv mod def

-- | Call the 'compilerMain' function of the given backend.

callBackend :: String -> IsMain -> CheckResult -> TCM ()
callBackend :: String -> IsMain -> CheckResult -> TCM ()
callBackend String
name IsMain
iMain CheckResult
checkResult = String -> TCM (Maybe Backend)
lookupBackend String
name TCM (Maybe Backend) -> (Maybe Backend -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Backend Backend'_boot (TCMT IO) opts env menv mod def
b) -> Backend'_boot (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 (TCMT IO) opts env menv mod def
b IsMain
iMain CheckResult
checkResult
  Maybe Backend
Nothing -> do
    backends <- Lens' TCState [Backend] -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
Lens' TCState [Backend]
stBackends
    genericError $
      "No backend called '" ++ name ++ "' " ++
      "(installed backends: " ++
      List.intercalate ", "
        (List.sort $ otherBackends ++
                     [ backendName b | Backend b <- backends ]) ++
      ")"

-- | Backends that are not included in the state, but still available
--   to the user.

otherBackends :: [String]
otherBackends :: [String]
otherBackends = [String
"GHCNoMain", String
"QuickLaTeX"]

-- | Look for a backend of the given name.

lookupBackend :: BackendName -> TCM (Maybe Backend)
lookupBackend :: String -> TCM (Maybe Backend)
lookupBackend String
name = Lens' TCState [Backend] -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
Lens' TCState [Backend]
stBackends TCMT IO [Backend]
-> ([Backend] -> Maybe Backend) -> TCM (Maybe Backend)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [Backend]
backends ->
  [Backend] -> Maybe Backend
forall a. [a] -> Maybe a
listToMaybe [ Backend
b | b :: Backend
b@(Backend Backend'_boot (TCMT IO) opts env menv mod def
b') <- [Backend]
backends, Backend'_boot (TCMT IO) opts env menv mod def -> String
forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> String
backendName Backend'_boot (TCMT IO) opts env menv mod def
b' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name ]

-- | Get the currently active backend (if any).

activeBackend :: TCM (Maybe Backend)
activeBackend :: TCM (Maybe Backend)
activeBackend = MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) Backend -> TCM (Maybe Backend))
-> MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
forall a b. (a -> b) -> a -> b
$ do
  bname <- TCMT IO (Maybe String) -> MaybeT (TCMT IO) String
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe String) -> MaybeT (TCMT IO) String)
-> TCMT IO (Maybe String) -> MaybeT (TCMT IO) String
forall a b. (a -> b) -> a -> b
$ (TCEnv -> Maybe String) -> TCMT IO (Maybe String)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe String
envActiveBackendName
  lift $ fromMaybe __IMPOSSIBLE__ <$> lookupBackend bname

-- | Ask the active backend whether a type may be erased.
--   See issue #3732.

activeBackendMayEraseType :: QName -> TCM Bool
activeBackendMayEraseType :: QName -> TCM Bool
activeBackendMayEraseType QName
q = do
  Backend b <- Backend -> Maybe Backend -> Backend
forall a. a -> Maybe a -> a
fromMaybe Backend
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Backend -> Backend)
-> TCM (Maybe Backend) -> TCMT IO Backend
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe Backend)
activeBackend
  mayEraseType b q

-- 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 (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 (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 (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 (tcm :: * -> *) env menv mod def.
NFData opts =>
Backend'_boot tcm opts env menv mod def -> Backend_boot 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot 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` []

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

  unlessM (optAllowUnsolved <$> pragmaOptions) $ do
    let ws = CheckResult -> [TCWarning]
crWarnings CheckResult
checkResult
        mode = CheckResult -> ModuleCheckMode
crMode CheckResult
checkResult
    -- Possible warnings, but only scope checking: ok.
    -- (Compatibility with scope checking done during options validation).
    unless (mode == ModuleScopeChecked || null ws) $
      genericError $ "You can only compile modules without unsolved metavariables."

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

  -- print warnings that might have accumulated during compilation
  ws <- filter (not . isUnsolvedWarning . tcWarning) <$> getAllWarnings AllWarnings
  unless (null ws) $ alwaysReportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> 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 String)
-> (Maybe String -> Maybe String) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Maybe String -> f (Maybe String)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe String)
eActiveBackendName (Maybe String -> Maybe String -> Maybe String
forall a b. a -> b -> a
const (Maybe String -> Maybe String -> Maybe String)
-> Maybe String -> Maybe String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Backend' opts env menv mod def -> String
forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> String
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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Backend' opts env menv mod def -> Bool
forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot 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
$
      String -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
        String
"The --only-scope-checking flag cannot be combined with " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        Backend' opts env menv mod def -> String
forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> String
backendName Backend' opts env menv mod def
backend String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

    !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.
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 :: Backend' opts env menv mod def -> env -> IsMain -> Interface -> TCM mod
compileModule :: forall opts env menv mod def.
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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot 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