{-# 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.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 GHC.Generics (Generic)

import System.Console.GetOpt

import Agda.Syntax.Treeless
import Agda.TypeChecking.Errors (getAllWarnings)
-- Agda.TypeChecking.Monad.Base imports us, relying on the .hs-boot file to
-- resolve the circular dependency. Fine. However, ghci loads the module after
-- compilation, so it brings in all of the symbols. That causes .Base to see
-- getBenchmark (defined in Agda.TypeChecking.Monad.State) *and* the one
-- defined in Agda.Utils.Benchmark, which causes an error. So we explicitly
-- hide it here to prevent it from being seen there and causing an error.
import Agda.TypeChecking.Monad hiding (getBenchmark)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty as P

import Agda.Interaction.Options
import Agda.Interaction.FindFile
import Agda.Interaction.Imports as CheckResult (CheckResult(CheckResult), crInterface, crWarnings, crMode)
import Agda.TypeChecking.Warnings

import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.IndexedList
import Agda.Utils.Lens
import Agda.Utils.Monad

import Agda.Compiler.ToTreeless
import Agda.Compiler.Common

import Agda.Utils.Impossible

-- Public interface -------------------------------------------------------

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 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.
  , forall opts env menv mod def.
Backend' opts env menv mod def
-> env
-> IsMain
-> ModuleName
-> Maybe String
-> TCM (Recompile menv mod)
preModule        :: env -> IsMain -> ModuleName -> 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 -> ModuleName -> [def] -> TCM mod
postModule       :: env -> menv -> IsMain -> ModuleName -> [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
$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 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 -> 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 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 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

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 ModuleName mod -> TCM ()
g env
-> IsMain -> ModuleName -> Maybe String -> TCM (Recompile menv mod)
h env -> menv -> IsMain -> ModuleName -> [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 () -> () -> ()
`seq` Maybe String -> ()
forall a. NFData a => a -> ()
rnf Maybe String
b () -> () -> ()
`seq` opts -> ()
forall a. NFData a => a -> ()
rnf opts
c () -> () -> ()
`seq` [OptDescr (Flag opts)] -> ()
forall {a}. NFData a => [OptDescr a] -> ()
rnf' [OptDescr (Flag opts)]
d () -> () -> ()
`seq` (opts -> Bool) -> ()
forall a. NFData a => a -> ()
rnf opts -> Bool
e () -> () -> ()
`seq`
    (opts -> TCM env) -> ()
forall a. NFData a => a -> ()
rnf opts -> TCM env
f () -> () -> ()
`seq` (env -> IsMain -> Map ModuleName mod -> TCM ()) -> ()
forall a. NFData a => a -> ()
rnf env -> IsMain -> Map ModuleName mod -> TCM ()
g () -> () -> ()
`seq` (env
 -> IsMain
 -> ModuleName
 -> Maybe String
 -> TCM (Recompile menv mod))
-> ()
forall a. NFData a => a -> ()
rnf env
-> IsMain -> ModuleName -> Maybe String -> TCM (Recompile menv mod)
h () -> () -> ()
`seq` (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod) -> ()
forall a. NFData a => a -> ()
rnf env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
i () -> () -> ()
`seq` (env -> menv -> IsMain -> Definition -> TCM def) -> ()
forall a. NFData a => a -> ()
rnf env -> menv -> IsMain -> Definition -> TCM def
j () -> () -> ()
`seq`
    Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
k () -> () -> ()
`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 () -> () -> ()
`seq` [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
b () -> () -> ()
`seq` ArgDescr a -> ()
forall {a}. NFData a => ArgDescr a -> ()
rnf'' ArgDescr a
c () -> () -> ()
`seq` String -> ()
forall a. NFData a => a -> ()
rnf String
d () -> () -> ()
`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 () -> () -> ()
`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 () -> () -> ()
`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} (f :: k -> *) (opts :: k). f opts -> Some f
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. Lens' opts (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 -> ExceptT String Identity 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 (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 -> *) (opts :: k). f opts -> 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 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 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 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 (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 (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
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 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 (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 -> TCM (Map ModuleName mod))
-> IsMain -> Interface -> TCM (Map ModuleName 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 -> ModuleName -> mod -> Map ModuleName mod
forall k a. k -> a -> Map k a
Map.singleton (Interface -> ModuleName
iModuleName Interface
iface) (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
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 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 :: 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 <- 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
forall (m :: * -> *). ReadTCState m => m ModuleName
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
-> ModuleName
-> Maybe String
-> TCM (Recompile menv mod)
forall opts env menv mod def.
Backend' opts env menv mod def
-> env
-> IsMain
-> ModuleName
-> Maybe String
-> TCM (Recompile menv mod)
preModule Backend' opts env menv mod def
backend env
env IsMain
isMain (Interface -> ModuleName
iModuleName Interface
i) Maybe String
mifile
  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
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)
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' :: 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