{-# 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 x.
 Backend' opts env menv mod def
 -> Rep (Backend' opts env menv mod def) x)
-> (forall x.
    Rep (Backend' opts env menv mod def) x
    -> Backend' opts env menv mod def)
-> Generic (Backend' opts env menv mod def)
forall x.
Rep (Backend' opts env menv mod def) x
-> Backend' opts env menv mod def
forall x.
Backend' opts env menv mod def
-> Rep (Backend' opts env menv mod def) x
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
$cfrom :: forall opts env menv mod def x.
Backend' opts env menv mod def
-> Rep (Backend' opts env menv mod def) x
from :: forall 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
to :: forall x.
Rep (Backend' opts env menv mod def) x
-> Backend' opts env menv mod def
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 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' opts env menv mod def
b) -> 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
b IsMain
iMain CheckResult
checkResult
  Maybe Backend
Nothing -> do
    [Backend]
backends <- Lens' [Backend] TCState -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
Lens' [Backend] TCState
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' 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
"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 ([Backend] -> f [Backend]) -> TCState -> f TCState
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 (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' 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

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

    rnf'' :: ArgDescr a -> ()
rnf'' (NoArg a
a)    = a -> ()
forall a. NFData a => a -> ()
rnf a
a
    rnf'' (ReqArg String -> a
a String
b) = (String -> a) -> ()
forall a. NFData a => a -> ()
rnf String -> a
a () -> () -> ()
forall a b. a -> b -> b
`seq` String -> ()
forall a. NFData a => a -> ()
rnf String
b
    rnf'' (OptArg Maybe String -> a
a String
b) = (Maybe String -> a) -> ()
forall a. NFData a => a -> ()
rnf Maybe String -> a
a () -> () -> ()
forall a b. a -> b -> b
`seq` String -> ()
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) = BackendWithOpts opts -> Some BackendWithOpts
forall {k} (a :: k -> *) (i :: k). a i -> Some a
Some (Backend' opts env menv mod def -> BackendWithOpts opts
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) = 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 (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 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 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 = Flag a -> b -> OptM b
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 = (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' a b -> Flag a -> Flag b
forall a b. Lens' a b -> Flag a -> Flag b
embedFlag (a -> f a) -> b -> f b
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 (CommandLineOptions -> f CommandLineOptions)
-> (a, CommandLineOptions) -> f (a, CommandLineOptions)
forall b a (f :: * -> *).
Functor f =>
(b -> f b) -> (a, b) -> f (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 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 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 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' 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 (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' (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 (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'
  CommandLineOptions (All BackendWithOpts i, CommandLineOptions)
-> Flag CommandLineOptions
-> Flag (All BackendWithOpts i, CommandLineOptions)
forall a b. Lens' a b -> Flag a -> Flag b
embedFlag (CommandLineOptions -> f CommandLineOptions)
-> (All BackendWithOpts i, CommandLineOptions)
-> f (All BackendWithOpts i, CommandLineOptions)
forall b a (f :: * -> *).
Functor f =>
(b -> f b) -> (a, b) -> f (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 -> OptM ()
forall (m :: * -> *).
MonadError String m =>
CommandLineOptions -> m ()
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' [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

  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) =>
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 ()
reportSDoc 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' (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 (Maybe String -> f (Maybe String)) -> TCEnv -> f TCEnv
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
    -- 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 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 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 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
"."

    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 <- 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 -> 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 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 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 <- 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
-> TCM (Recompile menv mod)
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         -> 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 -> 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 -> TopLevelModuleName -> [def] -> TCM mod
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 =
  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 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