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

import Prelude hiding (null)

import Control.DeepSeq

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

import System.Console.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

-- 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 -> TCM (Maybe Backend)
lookupBackend BackendName
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 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
  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
    let backendSet = [BackendName] -> Set BackendName
forall a. Ord a => [a] -> Set a
Set.fromList ([BackendName] -> Set BackendName)
-> [BackendName] -> Set BackendName
forall a b. (a -> b) -> a -> b
$
          [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 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