{-# 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
    [Backend]
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
    String -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"No backend called '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"(installed backends: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", "
        ([String] -> [String]
forall a. Ord a => [a] -> [a]
List.sort ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
otherBackends [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                     [ 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 | Backend Backend'_boot (TCMT IO) opts env menv mod def
b <- [Backend]
backends ]) String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
")"

-- | 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
  String
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
  TCMT IO Backend -> MaybeT (TCMT IO) Backend
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Backend -> MaybeT (TCMT IO) Backend)
-> TCMT IO Backend -> MaybeT (TCMT IO) Backend
forall a b. (a -> b) -> a -> 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
<$> String -> TCM (Maybe Backend)
lookupBackend String
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 Backend'_boot (TCMT IO) opts env menv mod def
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
  Backend'_boot (TCMT IO) opts env menv mod def -> QName -> TCM Bool
forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> QName -> tcm Bool
mayEraseType Backend'_boot (TCMT IO) opts env menv mod def
b QName
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 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot 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
  ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings Lens' TCState [TCWarning] -> [TCWarning] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` []

  Bool
noMain <- PragmaOptions -> Bool
optCompileNoMain (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM 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 Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let ws :: [TCWarning]
ws = CheckResult -> [TCWarning]
crWarnings CheckResult
checkResult
        mode :: ModuleCheckMode
mode = CheckResult -> ModuleCheckMode
crMode CheckResult
checkResult
    -- Possible warnings, but only scope checking: ok.
    -- (Compatibility with scope checking done during options validation).
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleCheckMode
mode ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked Bool -> Bool -> Bool
|| [TCWarning] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TCWarning]
ws) (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
"You can only compile modules without unsolved metavariables."

  [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])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t 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
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
P.prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [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 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
"."

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