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

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

import Control.Monad.State
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 System.Console.GetOpt

import Agda.Syntax.Treeless
-- 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 (getAllWarnings)
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 :: Backend' opts env menv mod def -> Backend

data Backend' opts env menv mod def = Backend'
  { Backend' opts env menv mod def -> String
backendName      :: String
  , Backend' opts env menv mod def -> Maybe String
backendVersion   :: Maybe String
      -- ^ Optional version information to be printed with @--version@.
  , Backend' opts env menv mod def -> opts
options          :: opts
      -- ^ Default options
  , 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.
  , 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.
  , Backend' opts env menv mod def -> opts -> TCM env
preCompile       :: opts -> TCM env
      -- ^ Called after type checking completes, but before compilation starts.
  , Backend' opts env menv mod def
-> env -> IsMain -> Map ModuleName mod -> TCM ()
postCompile      :: env -> IsMain -> Map ModuleName mod -> TCM ()
      -- ^ Called after module compilation has completed. The @IsMain@ argument
      --   is @NotMain@ if the @--no-main@ flag is present.
  , Backend' opts env menv mod def
-> env
-> IsMain
-> ModuleName
-> String
-> TCM (Recompile menv mod)
preModule        :: env -> IsMain -> ModuleName -> 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.
  , Backend' opts env menv mod def
-> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
postModule       :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
      -- ^ Called after all definitions of a module have been compiled.
  , Backend' opts env menv mod def
-> env -> menv -> IsMain -> Definition -> TCM def
compileDef       :: env -> menv -> IsMain -> Definition -> TCM def
      -- ^ Compile a single definition.
  , Backend' opts env menv mod def -> Bool
scopeCheckingSuffices :: Bool
      -- ^ True if the backend works if @--only-scope-checking@ is used.
  , 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.
  }

data Recompile menv mod = Recompile menv | Skip mod

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

callBackend :: String -> IsMain -> Interface -> TCM ()
callBackend :: String -> IsMain -> Interface -> TCM ()
callBackend String
name IsMain
iMain Interface
i = String -> TCM (Maybe Backend)
lookupBackend String
name TCM (Maybe Backend) -> (Maybe Backend -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Backend Backend' opts env menv mod def
b) -> Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
forall opts env menv mod def.
Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
compilerMain Backend' opts env menv mod def
b IsMain
iMain Interface
i
  Maybe Backend
Nothing -> do
    [Backend]
backends <- Lens' [Backend] TCState -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [Backend] TCState
stBackends
    String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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' opts env menv mod def -> String
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 ]) 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
"LaTeX", String
"QuickLaTeX"]

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

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

-- Internals --------------------------------------------------------------

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

forgetOpts :: BackendWithOpts opts -> Backend
forgetOpts :: BackendWithOpts opts -> Backend
forgetOpts (BackendWithOpts Backend' opts env menv mod def
backend) = Backend' opts env menv mod def -> Backend
forall opts env menv mod def.
Backend' opts env menv mod def -> Backend
Backend Backend' opts env menv mod def
backend

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

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

embedOpt :: Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt :: Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt Lens' a b
l = (Flag a -> Flag b) -> OptDescr (Flag a) -> OptDescr (Flag b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Lens' a b -> Flag a -> Flag b
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 (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' CommandLineOptions (a, CommandLineOptions)
-> OptDescr (Flag CommandLineOptions)
-> OptDescr (Flag (a, CommandLineOptions))
forall a b. Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt forall b a. Lens' b (a, b)
Lens' CommandLineOptions (a, 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 forall x1. Index i x1 -> Some (Index i)
forall k (f :: k -> *) (i :: k). f i -> Some f
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 opts env menv mod def.
Backend' 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 (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' i (All BackendWithOpts i, CommandLineOptions)
-> OptDescr (Flag i)
-> OptDescr (Flag (All BackendWithOpts i, CommandLineOptions))
forall a b. Lens' a b -> 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. Lens' a (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' (BackendWithOpts i) (All BackendWithOpts i)
forall x1 (xs :: [x1]) (x2 :: x1) (p :: x1 -> *).
Index xs x2 -> Lens' (p x2) (All p xs)
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. Lens' opts (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'
  CommandLineOptions (All BackendWithOpts i, CommandLineOptions)
-> Flag CommandLineOptions
-> Flag (All BackendWithOpts i, CommandLineOptions)
forall a b. Lens' a b -> Flag a -> Flag b
embedFlag forall b a. Lens' b (a, b)
Lens'
  CommandLineOptions (All BackendWithOpts i, 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
checkOpts CommandLineOptions
opts
      ([Backend], CommandLineOptions)
-> OptM ([Backend], CommandLineOptions)
forall (m :: * -> *) a. Monad m => a -> m a
return ((forall x1. BackendWithOpts x1 -> Backend)
-> All BackendWithOpts i -> [Backend]
forall x (b :: x -> *) a (xs :: [x]).
(forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
forgetAll forall x1. BackendWithOpts x1 -> Backend
forgetOpts All BackendWithOpts i
backends, CommandLineOptions
opts)

backendInteraction :: [Backend] -> (TCM (Maybe Interface) -> TCM ()) -> TCM (Maybe Interface) -> TCM ()
backendInteraction :: [Backend]
-> (TCM (Maybe Interface) -> TCM ())
-> TCM (Maybe Interface)
-> TCM ()
backendInteraction [] TCM (Maybe Interface) -> TCM ()
fallback TCM (Maybe Interface)
check = TCM (Maybe Interface) -> TCM ()
fallback TCM (Maybe Interface)
check
backendInteraction [Backend]
backends TCM (Maybe Interface) -> TCM ()
_ TCM (Maybe Interface)
check = do
  CommandLineOptions
opts   <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let backendNames :: [String]
backendNames = [ Backend' opts env menv mod def -> String
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 ]
      err :: String -> TCM ()
err String
flag = String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"Cannot mix --" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
flag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and backends (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [String]
backendNames String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optInteractive     CommandLineOptions
opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM ()
err String
"interactive"
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM ()
err String
"interaction"
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optJSONInteraction CommandLineOptions
opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM ()
err String
"interaction-json"
  Maybe Interface
mi     <- TCM (Maybe Interface)
check

  -- reset warnings
  Lens' [TCWarning] TCState
stTCWarnings Lens' [TCWarning] TCState -> [TCWarning] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> 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
  case Maybe Interface
mi of
    Maybe Interface
Nothing -> String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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."
    Just Interface
i  -> [TCM ()] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
forall opts env menv mod def.
Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
compilerMain Backend' opts env menv mod def
backend IsMain
isMain Interface
i | 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]
getAllWarnings WhichWarnings
AllWarnings
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> 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 -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"warning" VerboseLevel
1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
P.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws


compilerMain :: Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
compilerMain :: Backend' opts env menv mod def -> IsMain -> Interface -> TCM ()
compilerMain Backend' opts env menv mod def
backend IsMain
isMain0 Interface
i = Interface -> TCM () -> TCM ()
forall a. Interface -> TCM a -> TCM a
inCompilerEnv Interface
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  Lens' (Maybe String) TCEnv
-> (Maybe String -> Maybe String) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Maybe String) TCEnv
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 opts env menv mod def.
Backend' 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
    Bool
onlyScoping <- CommandLineOptions -> Bool
optOnlyScopeChecking (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Backend' opts env menv mod def -> Bool
forall opts env menv mod def.
Backend' opts env menv mod def -> Bool
scopeCheckingSuffices Backend' opts env menv mod def
backend) Bool -> Bool -> Bool
&& Bool
onlyScoping) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
backend String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

    -- 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 (m :: * -> *) a. Monad m => a -> m a
return IsMain
NotMain)
      {-else-} (IsMain -> TCMT IO IsMain
forall (m :: * -> *) a. Monad m => a -> m a
return IsMain
isMain0)

    env
env  <- Backend' opts env menv mod def -> opts -> TCM env
forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> TCM env
preCompile Backend' opts env menv mod def
backend (Backend' opts env menv mod def -> opts
forall opts env menv mod def.
Backend' opts env menv mod def -> opts
options Backend' opts env menv mod def
backend)
    Map ModuleName mod
mods <- IsMain
-> Interface
-> (IsMain -> Interface -> TCM (Map ModuleName mod))
-> TCM (Map ModuleName mod)
forall r.
Monoid r =>
IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r
doCompile IsMain
isMain Interface
i ((IsMain -> Interface -> TCM (Map ModuleName mod))
 -> TCM (Map ModuleName mod))
-> (IsMain -> Interface -> TCM (Map ModuleName mod))
-> TCM (Map ModuleName mod)
forall a b. (a -> b) -> a -> b
$ \ IsMain
isMain Interface
i -> ModuleName -> mod -> Map ModuleName mod
forall k a. k -> a -> Map k a
Map.singleton (Interface -> ModuleName
iModuleName Interface
i) (mod -> Map ModuleName mod)
-> TCMT IO mod -> TCM (Map ModuleName 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
isMain Interface
i
    Interface -> TCM ()
setInterface Interface
i
    Backend' opts env menv mod def
-> env -> IsMain -> Map ModuleName mod -> TCM ()
forall opts env menv mod def.
Backend' opts env menv mod def
-> env -> IsMain -> Map ModuleName mod -> TCM ()
postCompile Backend' opts env menv mod def
backend env
env IsMain
isMain Map ModuleName mod
mods

compileModule :: Backend' opts env menv mod def -> env -> IsMain -> Interface -> TCM mod
compileModule :: 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 <- ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> TCMT IO ModuleName -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
curMName
  String
ifile <- String
-> (InterfaceFile -> String) -> Maybe InterfaceFile -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
forall a. HasCallStack => a
__IMPOSSIBLE__ (AbsolutePath -> String
filePath (AbsolutePath -> String)
-> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterfaceFile -> AbsolutePath
intFilePath) (Maybe InterfaceFile -> String)
-> TCMT IO (Maybe InterfaceFile) -> TCMT IO 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
-> ModuleName
-> String
-> TCM (Recompile menv mod)
forall opts env menv mod def.
Backend' opts env menv mod def
-> env
-> IsMain
-> ModuleName
-> String
-> TCM (Recompile menv mod)
preModule Backend' opts env menv mod def
backend env
env IsMain
isMain (Interface -> ModuleName
iModuleName Interface
i) String
ifile
  case Recompile menv mod
r of
    Skip mod
m         -> mod -> TCM mod
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
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)
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 -> TCMT IO def)
-> (Definition -> TCMT IO Definition) -> Definition -> TCMT IO def
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Definition -> TCMT IO Definition
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull) [Definition]
defs
      Backend' opts env menv mod def
-> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
forall opts env menv mod def.
Backend' opts env menv mod def
-> env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
postModule Backend' opts env menv mod def
backend env
env menv
menv IsMain
isMain (Interface -> ModuleName
iModuleName Interface
i) [def]
res

compileDef' :: Backend' opts env menv mod def -> env -> menv -> IsMain -> Definition -> TCM def
compileDef' :: 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 -> TCM def -> TCM def
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange (Definition -> QName
defName Definition
def) (TCM def -> TCM def) -> TCM def -> TCM def
forall a b. (a -> b) -> a -> b
$
    Backend' opts env menv mod def
-> env -> menv -> IsMain -> Definition -> TCM 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
def