{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.Backend.Base where

import Agda.Interaction.Options (ArgDescr(..), OptDescr(..), Flag)
import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Common (IsMain)
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (Definition)


import Control.DeepSeq (NFData, rnf)
import Data.Map (Map)

import GHC.Generics (Generic)

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

data Backend'_boot tcm opts env menv mod def = Backend'
  { forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> String
backendName      :: String
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> Maybe String
backendVersion   :: Maybe String
      -- ^ Optional version information to be printed with @--version@.
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> opts
options          :: opts
      -- ^ Default options
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> opts -> tcm env
preCompile       :: opts -> tcm env
      -- ^ Called after type checking completes, but before compilation starts.
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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 (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def
-> env -> menv -> IsMain -> Definition -> tcm def
compileDef       :: env -> menv -> IsMain -> Definition -> tcm def
      -- ^ Compile a single definition.
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> Bool
scopeCheckingSuffices :: Bool
      -- ^ True if the backend works if @--only-scope-checking@ is used.
  , forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm 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'_boot tcm opts env menv mod def
 -> Rep (Backend'_boot tcm opts env menv mod def) x)
-> (forall x.
    Rep (Backend'_boot tcm opts env menv mod def) x
    -> Backend'_boot tcm opts env menv mod def)
-> Generic (Backend'_boot tcm opts env menv mod def)
forall x.
Rep (Backend'_boot tcm opts env menv mod def) x
-> Backend'_boot tcm opts env menv mod def
forall x.
Backend'_boot tcm opts env menv mod def
-> Rep (Backend'_boot tcm opts env menv mod def) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (tcm :: * -> *) opts env menv mod def x.
Rep (Backend'_boot tcm opts env menv mod def) x
-> Backend'_boot tcm opts env menv mod def
forall (tcm :: * -> *) opts env menv mod def x.
Backend'_boot tcm opts env menv mod def
-> Rep (Backend'_boot tcm opts env menv mod def) x
$cfrom :: forall (tcm :: * -> *) opts env menv mod def x.
Backend'_boot tcm opts env menv mod def
-> Rep (Backend'_boot tcm opts env menv mod def) x
from :: forall x.
Backend'_boot tcm opts env menv mod def
-> Rep (Backend'_boot tcm opts env menv mod def) x
$cto :: forall (tcm :: * -> *) opts env menv mod def x.
Rep (Backend'_boot tcm opts env menv mod def) x
-> Backend'_boot tcm opts env menv mod def
to :: forall x.
Rep (Backend'_boot tcm opts env menv mod def) x
-> Backend'_boot tcm opts env menv mod def
Generic

data Recompile menv mod = Recompile menv | Skip mod


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

instance NFData opts => NFData (Backend'_boot tcm opts env menv mod def) where
  rnf :: Backend'_boot tcm 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