{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}


-- | Interface for compiler backend writers.
module Agda.Compiler.Backend
  ( 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 Control.DeepSeq
import Control.Monad              ( (<=<) )
import Control.Monad.Trans        ( lift )
import Control.Monad.Trans.Maybe

import qualified Data.List as List
import Data.Maybe

import Data.Map (Map)
import qualified Data.Map as Map

import GHC.Generics (Generic)

import System.Console.GetOpt

import Agda.Syntax.TopLevelModuleName
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 -------------------------------------------------------

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

data Backend' opts env menv mod def = Backend'
  { forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName      :: String
  , forall opts env menv mod def.
Backend' opts env menv mod def -> Maybe String
backendVersion   :: Maybe String
      -- ^ Optional version information to be printed with @--version@.
  , forall opts env menv mod def.
Backend' opts env menv mod def -> opts
options          :: opts
      -- ^ Default options
  , forall opts env menv mod def.
Backend' opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags :: [OptDescr (Flag opts)]
      -- ^ Backend-specific command-line flags. Should at minimum contain a
      --   flag to enable the backend.
  , forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> Bool
isEnabled        :: opts -> Bool
      -- ^ Unless the backend has been enabled, @runAgda@ will fall back to
      --   vanilla Agda behaviour.
  , forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> TCM env
preCompile       :: opts -> TCM env
      -- ^ Called after type checking completes, but before compilation starts.
  , forall opts env menv mod def.
Backend' opts env menv mod def
-> env -> IsMain -> Map TopLevelModuleName mod -> TCM ()
postCompile      :: env -> IsMain -> Map TopLevelModuleName mod ->
                        TCM ()
      -- ^ Called after module compilation has completed. The @IsMain@ argument
      --   is @NotMain@ if the @--no-main@ flag is present.
  , forall opts env menv mod def.
Backend' opts env menv mod def
-> env
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile menv mod)
preModule        :: env -> IsMain -> TopLevelModuleName ->
                        Maybe FilePath -> TCM (Recompile menv mod)
      -- ^ Called before compilation of each module. Gets the path to the
      --   @.agdai@ file to allow up-to-date checking of previously written
      --   compilation results. Should return @Skip m@ if compilation is not
      --   required. Will be @Nothing@ if only scope checking.
  , forall opts env menv mod def.
Backend' opts env menv mod def
-> env -> menv -> IsMain -> TopLevelModuleName -> [def] -> TCM mod
postModule       :: env -> menv -> IsMain -> TopLevelModuleName ->
                        [def] -> TCM mod
      -- ^ Called after all definitions of a module have been compiled.
  , forall opts env menv mod def.
Backend' opts env menv mod def
-> env -> menv -> IsMain -> Definition -> TCM def
compileDef       :: env -> menv -> IsMain -> Definition -> TCM def
      -- ^ Compile a single definition.
  , forall opts env menv mod def.
Backend' opts env menv mod def -> Bool
scopeCheckingSuffices :: Bool
      -- ^ True if the backend works if @--only-scope-checking@ is used.
  , forall opts env menv mod def.
Backend' opts env menv mod def -> QName -> TCM Bool
mayEraseType     :: QName -> TCM Bool
      -- ^ The treeless compiler may ask the Backend if elements
      --   of the given type maybe possibly erased.
      --   The answer should be 'False' if the compilation of the type
      --   is used by a third party, e.g. in a FFI binding.
  }
  deriving forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall opts env menv mod def x.
Rep (Backend' opts env menv mod def) x
-> Backend' opts env menv mod def
forall opts env menv mod def x.
Backend' opts env menv mod def
-> Rep (Backend' opts env menv mod def) x
$cto :: forall opts env menv mod def x.
Rep (Backend' opts env menv mod def) x
-> Backend' opts env menv mod def
$cfrom :: forall opts env menv mod def x.
Backend' opts env menv mod def
-> Rep (Backend' opts env menv mod def) x
Generic

data Recompile menv mod = Recompile menv | Skip mod

-- | 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Backend Backend' opts env menv mod def
b) -> forall opts env menv mod def.
Backend' opts env menv mod def -> IsMain -> CheckResult -> TCM ()
compilerMain Backend' opts env menv mod def
b IsMain
iMain CheckResult
checkResult
  Maybe Backend
Nothing -> do
    [Backend]
backends <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [Backend] TCState
stBackends
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError forall a b. (a -> b) -> a -> b
$
      String
"No backend called '" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
"' " forall a. [a] -> [a] -> [a]
++
      String
"(installed backends: " forall a. [a] -> [a] -> [a]
++
      forall a. [a] -> [[a]] -> [a]
List.intercalate String
", "
        (forall a. Ord a => [a] -> [a]
List.sort forall a b. (a -> b) -> a -> b
$ [String]
otherBackends forall a. [a] -> [a] -> [a]
++
                     [ forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b | Backend Backend' opts env menv mod def
b <- [Backend]
backends ]) 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 = forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [Backend] TCState
stBackends forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ [Backend]
backends ->
  forall a. [a] -> Maybe a
listToMaybe [ Backend
b | b :: Backend
b@(Backend Backend' opts env menv mod def
b') <- [Backend]
backends, forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b' 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 = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
  String
bname <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe String
envActiveBackendName
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ 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' opts env menv mod def
b <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe Backend)
activeBackend
  forall opts env menv mod def.
Backend' opts env menv mod def -> QName -> TCM Bool
mayEraseType Backend' opts env menv mod def
b QName
q

instance NFData Backend where
  rnf :: Backend -> ()
rnf (Backend Backend' opts env menv mod def
b) = forall a. NFData a => a -> ()
rnf Backend' opts env menv mod def
b

instance NFData opts => NFData (Backend' opts env menv mod def) where
  rnf :: Backend' opts env menv mod def -> ()
rnf (Backend' String
a Maybe String
b opts
c [OptDescr (Flag opts)]
d opts -> Bool
e opts -> TCM env
f env -> IsMain -> Map TopLevelModuleName mod -> TCM ()
g env
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile menv mod)
h env -> menv -> IsMain -> TopLevelModuleName -> [def] -> TCM mod
i env -> menv -> IsMain -> Definition -> TCM def
j Bool
k QName -> TCM Bool
l) =
    forall a. NFData a => a -> ()
rnf String
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe String
b seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf opts
c seq :: forall a b. a -> b -> b
`seq` forall {a}. NFData a => [OptDescr a] -> ()
rnf' [OptDescr (Flag opts)]
d seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf opts -> Bool
e seq :: forall a b. a -> b -> b
`seq`
    forall a. NFData a => a -> ()
rnf opts -> TCM env
f seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf env -> IsMain -> Map TopLevelModuleName mod -> TCM ()
g seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf env
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile menv mod)
h seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf env -> menv -> IsMain -> TopLevelModuleName -> [def] -> TCM mod
i seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf env -> menv -> IsMain -> Definition -> TCM def
j seq :: forall a b. a -> b -> b
`seq`
    forall a. NFData a => a -> ()
rnf Bool
k seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf QName -> TCM Bool
l
    where
    rnf' :: [OptDescr a] -> ()
rnf' []                   = ()
    rnf' (Option String
a [String]
b ArgDescr a
c String
d : [OptDescr a]
e) =
      forall a. NFData a => a -> ()
rnf String
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf [String]
b seq :: forall a b. a -> b -> b
`seq` forall {a}. NFData a => ArgDescr a -> ()
rnf'' ArgDescr a
c seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf String
d seq :: forall a b. a -> b -> b
`seq` [OptDescr a] -> ()
rnf' [OptDescr a]
e

    rnf'' :: ArgDescr a -> ()
rnf'' (NoArg a
a)    = forall a. NFData a => a -> ()
rnf a
a
    rnf'' (ReqArg String -> a
a String
b) = forall a. NFData a => a -> ()
rnf String -> a
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf String
b
    rnf'' (OptArg Maybe String -> a
a String
b) = forall a. NFData a => a -> ()
rnf Maybe String -> a
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf String
b

-- 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' opts env menv mod def
backend) = forall {k} (f :: k -> *) (opts :: k). f opts -> Some f
Some (forall opts opts env menv mod.
NFData opts =>
Backend' opts opts env menv mod -> BackendWithOpts opts
BackendWithOpts Backend' 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) = forall opts env menv mod def.
NFData opts =>
Backend' opts env menv mod def -> Backend
Backend Backend' opts env menv mod def
backend

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

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

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

parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
parseBackendOptions :: [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [String]
argv CommandLineOptions
opts0 =
  case 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    = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt forall b a. Lens' b (a, b)
lSnd) ([OptDescr (Flag CommandLineOptions)]
deadStandardOptions forall a. [a] -> [a] -> [a]
++ [OptDescr (Flag CommandLineOptions)]
standardOptions)
          backendFlags :: [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
backendFlags = do
            Some Index i i
i            <- forall {x} (b :: x -> *) a (xs :: [x]).
(forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
forgetAll forall {k} (f :: k -> *) (opts :: k). f opts -> Some f
Some forall a b. (a -> b) -> a -> b
$ 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 <- [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               <- forall opts env menv mod def.
Backend' opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags Backend' i env menv mod def
b
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt (forall a b. Lens' a (a, b)
lFst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> *).
Index xs x2 -> Lens' (p x2) (All p xs)
lIndex Index i i
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall opts. Lens' opts (BackendWithOpts opts)
bOptions) OptDescr (Flag i)
opt
      (All BackendWithOpts i
backends, CommandLineOptions
opts) <- forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple ([String] -> [String]
stripRTS [String]
argv)
                                       (forall {a}. [OptDescr (Flag (a, CommandLineOptions))]
agdaFlags forall a. [a] -> [a] -> [a]
++ [OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))]
backendFlags) (forall a b. Lens' a b -> Flag a -> Flag b
embedFlag forall b a. Lens' b (a, b)
lSnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Flag CommandLineOptions
inputFlag)
                                       (All BackendWithOpts i
bs, CommandLineOptions
opts0)
      CommandLineOptions
opts <- Flag CommandLineOptions
checkOpts CommandLineOptions
opts
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall {x} (b :: x -> *) a (xs :: [x]).
(forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
forgetAll 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
  Lens' [TCWarning] TCState
stTCWarnings forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` []

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

  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optAllowUnsolved forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) 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).
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleCheckMode
mode forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TCWarning]
ws) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError forall a b. (a -> b) -> a -> b
$ String
"You can only compile modules without unsolved metavariables."

  forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ 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 <- forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TCWarning]
ws) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc String
"warning" VerboseLevel
1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM 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 = forall a. CheckResult -> TCM a -> TCM a
inCompilerEnv CheckResult
checkResult forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Maybe String) TCEnv
eActiveBackendName (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
backend) 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.
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall opts env menv mod def.
Backend' opts env menv mod def -> Bool
scopeCheckingSuffices Backend' opts env menv mod def
backend) Bool -> Bool -> Bool
&& CheckResult -> ModuleCheckMode
crMode CheckResult
checkResult forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError forall a b. (a -> b) -> a -> b
$
        String
"The --only-scope-checking flag cannot be combined with " forall a. [a] -> [a] -> [a]
++
        forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
backend forall a. [a] -> [a] -> [a]
++ String
"."

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

    env
env  <- forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> TCM env
preCompile Backend' opts env menv mod def
backend (forall opts env menv mod def.
Backend' opts env menv mod def -> opts
options Backend' opts env menv mod def
backend)
    Map TopLevelModuleName mod
mods <- 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 ->
          forall k a. k -> a -> Map k a
Map.singleton (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
iface) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          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
    forall opts env menv mod def.
Backend' 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 <- 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 <- (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterfaceFile -> AbsolutePath
intFilePath forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile TopLevelModuleName
mName
  Recompile menv mod
r      <- forall opts env menv mod def.
Backend' 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         -> forall (m :: * -> *) a. Monad m => a -> m a
return mod
m
    Recompile menv
menv -> do
      [Definition]
defs <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definitions -> [(QName, Definition)]
sortDefs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Definitions
curDefs
      [def]
res  <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull) [Definition]
defs
      forall opts env menv mod def.
Backend' 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 =
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Definition -> QName
defName Definition
def) forall a b. (a -> b) -> a -> b
$
    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