{-# 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
  [Backend]
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]
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 -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ BackendName -> Set BackendName -> TypeError
UnknownBackend BackendName
name ([BackendName] -> Set BackendName
forall a. Ord a => [a] -> Set a
Set.fromList [BackendName]
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 Index i i
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 Backend' i env menv mod def
b <- [All BackendWithOpts i -> Index i i -> BackendWithOpts i
forall {x1} (p :: x1 -> *) (xs :: [x1]) (x2 :: x1).
All p xs -> Index xs x2 -> p x2
lookupIndex All BackendWithOpts i
bs Index i i
i]
            OptDescr (Flag i)
opt               <- Backend' i env menv mod def -> [OptDescr (Flag i)]
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> [OptDescr (Flag opts)]
commandLineFlags Backend' i env menv mod def
b
            OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
-> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
 -> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))])
-> OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
-> [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
forall a b. (a -> b) -> a -> b
$ Lens' (All BackendWithOpts i, CommandLineOptions) i
-> OptDescr (Flag i)
-> OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
forall b a. Lens' b a -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt ((All BackendWithOpts i -> f (All BackendWithOpts i))
-> (All BackendWithOpts i, CommandLineOptions)
-> f (All BackendWithOpts i, CommandLineOptions)
forall a b (f :: * -> *).
Functor f =>
(a -> f a) -> (a, b) -> f (a, b)
lFst ((All BackendWithOpts i -> f (All BackendWithOpts i))
 -> (All BackendWithOpts i, CommandLineOptions)
 -> f (All BackendWithOpts i, CommandLineOptions))
-> ((i -> f i)
    -> All BackendWithOpts i -> f (All BackendWithOpts i))
-> (i -> f i)
-> (All BackendWithOpts i, CommandLineOptions)
-> f (All BackendWithOpts i, CommandLineOptions)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index i i -> Lens' (All BackendWithOpts i) (BackendWithOpts i)
forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> *).
Index xs x2 -> Lens' (All p xs) (p x2)
lIndex Index i i
i ((BackendWithOpts i -> f (BackendWithOpts i))
 -> All BackendWithOpts i -> f (All BackendWithOpts i))
-> ((i -> f i) -> BackendWithOpts i -> f (BackendWithOpts i))
-> (i -> f i)
-> All BackendWithOpts i
-> f (All BackendWithOpts i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i -> f i) -> BackendWithOpts i -> f (BackendWithOpts i)
forall opts (f :: * -> *).
Functor f =>
(opts -> f opts)
-> BackendWithOpts opts -> f (BackendWithOpts opts)
bOptions) OptDescr (Flag i)
opt
      (All BackendWithOpts i
backends, CommandLineOptions
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)
      CommandLineOptions
opts <- Flag CommandLineOptions
forall (m :: * -> *).
MonadError String m =>
CommandLineOptions -> m CommandLineOptions
checkOpts CommandLineOptions
opts
      ([Backend], CommandLineOptions)
-> OptM ([Backend], CommandLineOptions)
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((forall opts. BackendWithOpts opts -> Backend)
-> All BackendWithOpts i -> [Backend]
forall {x} (b :: x -> *) a (xs :: [x]).
(forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
forgetAll BackendWithOpts x1 -> Backend
forall opts. BackendWithOpts opts -> Backend
forgetOpts All BackendWithOpts i
backends, CommandLineOptions
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
checkResult <- AbsolutePath -> TCM CheckResult
check AbsolutePath
mainFile

  -- reset warnings
  (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
Lens' TCState (Set TCWarning)
stTCWarnings Lens' TCState (Set TCWarning) -> Set TCWarning -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` Set TCWarning
forall a. Null a => a
empty

  Bool
noMain <- PragmaOptions -> Bool
optCompileNoMain (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let isMain :: IsMain
isMain | Bool
noMain    = IsMain
NotMain
             | Bool
otherwise = IsMain
IsMain

  [TCM ()] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Backend' 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' opts env menv mod def
backend IsMain
isMain CheckResult
checkResult | Backend Backend' opts env menv mod def
backend <- [Backend]
backends ]

  -- print warnings that might have accumulated during compilation
  [TCWarning]
ws <- (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) ([TCWarning] -> [TCWarning])
-> (Set TCWarning -> [TCWarning]) -> Set TCWarning -> [TCWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList (Set TCWarning -> [TCWarning])
-> TCMT IO (Set TCWarning) -> TCMT IO [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
  Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
alwaysReportSDoc String
"warning" VerboseLevel
1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    -- 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).
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> [TCMT IO Doc]) -> [TCWarning] -> [TCMT IO Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
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 ]) [TCWarning]
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

    !Interface
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
isMain <- TCMT IO Bool -> TCMT IO IsMain -> TCMT IO IsMain -> TCMT IO IsMain
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCompileNoMain (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      {-then-} (IsMain -> TCMT IO IsMain
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return IsMain
NotMain)
      {-else-} (IsMain -> TCMT IO IsMain
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return IsMain
isMain0)

    env
env  <- Backend' opts env menv mod def -> opts -> TCMT IO env
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> opts -> tcm env
preCompile Backend' opts env menv mod def
backend (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
backend)
    Map TopLevelModuleName mod
mods <- (IsMain -> Interface -> TCM (Map TopLevelModuleName mod))
-> IsMain -> Interface -> TCM (Map TopLevelModuleName mod)
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
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
isMain Interface
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.
    Interface -> TCM ()
setInterface Interface
i
    Backend' opts env menv mod def
-> env -> IsMain -> Map TopLevelModuleName mod -> TCM ()
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> env -> IsMain -> Map TopLevelModuleName mod -> tcm ()
postCompile Backend' opts env menv mod def
backend env
env IsMain
isMain Map TopLevelModuleName mod
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
  TopLevelModuleName
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.
  Maybe String
mifile <- (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (InterfaceFile -> String) -> InterfaceFile -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath (AbsolutePath -> String)
-> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterfaceFile -> AbsolutePath
intFilePath (InterfaceFile -> Maybe String)
-> Maybe InterfaceFile -> Maybe String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Maybe InterfaceFile -> Maybe String)
-> TCMT IO (Maybe InterfaceFile) -> TCMT IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => TopLevelModuleName -> TCMT IO (Maybe InterfaceFile)
TopLevelModuleName -> TCMT IO (Maybe InterfaceFile)
findInterfaceFile TopLevelModuleName
mName
  Recompile menv mod
r      <- Backend' opts env menv mod def
-> env
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCMT IO (Recompile menv mod)
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> env
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> tcm (Recompile menv mod)
preModule Backend' opts env menv mod def
backend env
env IsMain
isMain (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i) Maybe String
mifile
  case Recompile menv mod
r of
    Skip mod
m         -> mod -> TCM mod
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return mod
m
    Recompile menv
menv -> do
      [Definition]
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
      [def]
res  <- (Definition -> TCMT IO def) -> [Definition] -> TCMT IO [def]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Backend' opts env menv mod def
-> env -> menv -> IsMain -> Definition -> TCMT IO def
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]
defs
      Backend' opts env menv mod def
-> env -> menv -> IsMain -> TopLevelModuleName -> [def] -> TCM mod
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod
postModule Backend' opts env menv mod def
backend env
env menv
menv IsMain
isMain (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i) [def]
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