{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.Backend.Base where

import Control.DeepSeq (NFData, rnf)
import Data.Map (Map)
import Data.Text (Text)
import GHC.Generics (Generic)

import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Common (BackendName, IsMain, InteractionId)
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
import Agda.Syntax.Position (Range)

import Agda.Interaction.Base (CommandM')
import Agda.Interaction.Options (ArgDescr(..), OptDescr(..), Flag)

type BackendVersion = Text

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

data Backend'_boot definition tcm opts env menv mod def = Backend'
  { forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> BackendName
backendName      :: BackendName
      -- ^ the name of the backend
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> Maybe BackendName
backendVersion   :: Maybe BackendVersion
      -- ^ Optional version information to be printed with @--version@.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> opts
options          :: opts
      -- ^ Default options
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition 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 definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition 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 definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> opts -> tcm env
preCompile       :: opts -> tcm env
      -- ^ Called after type checking completes, but before compilation starts.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition 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 definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> env
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> 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 definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition 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 definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> env -> menv -> IsMain -> definition -> tcm def
compileDef       :: env -> menv -> IsMain -> definition -> tcm def
      -- ^ Compile a single definition.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> Bool
scopeCheckingSuffices :: Bool
      -- ^ True if the backend works if @--only-scope-checking@ is used.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition 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.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> Maybe (BackendCommandTop tcm)
backendInteractTop  :: Maybe (BackendCommandTop tcm)
      -- ^ Backend-specific top-level interactive command.
  , forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def
-> Maybe (BackendCommandHole tcm)
backendInteractHole :: Maybe (BackendCommandHole tcm)
      -- ^ Backend-specific hole-level interactive command.
  }
  deriving (forall x.
 Backend'_boot definition tcm opts env menv mod def
 -> Rep (Backend'_boot definition tcm opts env menv mod def) x)
-> (forall x.
    Rep (Backend'_boot definition tcm opts env menv mod def) x
    -> Backend'_boot definition tcm opts env menv mod def)
-> Generic (Backend'_boot definition tcm opts env menv mod def)
forall x.
Rep (Backend'_boot definition tcm opts env menv mod def) x
-> Backend'_boot definition tcm opts env menv mod def
forall x.
Backend'_boot definition tcm opts env menv mod def
-> Rep (Backend'_boot definition tcm opts env menv mod def) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall definition (tcm :: * -> *) opts env menv mod def x.
Rep (Backend'_boot definition tcm opts env menv mod def) x
-> Backend'_boot definition tcm opts env menv mod def
forall definition (tcm :: * -> *) opts env menv mod def x.
Backend'_boot definition tcm opts env menv mod def
-> Rep (Backend'_boot definition tcm opts env menv mod def) x
$cfrom :: forall definition (tcm :: * -> *) opts env menv mod def x.
Backend'_boot definition tcm opts env menv mod def
-> Rep (Backend'_boot definition tcm opts env menv mod def) x
from :: forall x.
Backend'_boot definition tcm opts env menv mod def
-> Rep (Backend'_boot definition tcm opts env menv mod def) x
$cto :: forall definition (tcm :: * -> *) opts env menv mod def x.
Rep (Backend'_boot definition tcm opts env menv mod def) x
-> Backend'_boot definition tcm opts env menv mod def
to :: forall x.
Rep (Backend'_boot definition tcm opts env menv mod def) x
-> Backend'_boot definition tcm opts env menv mod def
Generic

data Recompile menv mod = Recompile menv | Skip mod

-- | For the sake of flexibility, we parametrize interactive commands with an
-- arbitrary string payload, e.g. to allow extra user input, or have backends
-- provide multiple commands with a single record field.
type CommandPayload = String

-- | The type of top-level backend interactive commmands.
type BackendCommandTop tcm
   = CommandPayload -- ^ arbitrary user payload
  -> CommandM' tcm ()

-- | The type of top-level backend interactive commmands.
type BackendCommandHole tcm
   = CommandPayload -- ^ arbitrary user payload
  -> InteractionId  -- ^ the hole's ID
  -> Range          -- ^ the hole's range
  -> String         -- ^ the hole's contents
  -> CommandM' tcm ()

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

instance NFData opts => NFData (Backend'_boot definition tcm opts env menv mod def) where
  rnf :: Backend'_boot definition tcm opts env menv mod def -> ()
rnf (Backend' BackendName
a Maybe BackendName
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 FilePath
-> 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 Maybe (BackendCommandTop tcm)
m Maybe (BackendCommandHole tcm)
n) =
    BackendName -> ()
forall a. NFData a => a -> ()
rnf BackendName
a () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe BackendName -> ()
forall a. NFData a => a -> ()
rnf Maybe BackendName
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 FilePath
 -> tcm (Recompile menv mod))
-> ()
forall a. NFData a => a -> ()
rnf env
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> 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 () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe (BackendCommandTop tcm) -> ()
forall a. NFData a => a -> ()
rnf Maybe (BackendCommandTop tcm)
m () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe (BackendCommandHole tcm) -> ()
forall a. NFData a => a -> ()
rnf Maybe (BackendCommandHole tcm)
n
    where
    rnf' :: [OptDescr a] -> ()
rnf' []                   = ()
    rnf' (Option FilePath
a [FilePath]
b ArgDescr a
c FilePath
d : [OptDescr a]
e) =
      FilePath -> ()
forall a. NFData a => a -> ()
rnf FilePath
a () -> () -> ()
forall a b. a -> b -> b
`seq` [FilePath] -> ()
forall a. NFData a => a -> ()
rnf [FilePath]
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` FilePath -> ()
forall a. NFData a => a -> ()
rnf FilePath
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 FilePath -> a
a FilePath
b) = (FilePath -> a) -> ()
forall a. NFData a => a -> ()
rnf FilePath -> a
a () -> () -> ()
forall a b. a -> b -> b
`seq` FilePath -> ()
forall a. NFData a => a -> ()
rnf FilePath
b
    rnf'' (OptArg Maybe FilePath -> a
a FilePath
b) = (Maybe FilePath -> a) -> ()
forall a. NFData a => a -> ()
rnf Maybe FilePath -> a
a () -> () -> ()
forall a b. a -> b -> b
`seq` FilePath -> ()
forall a. NFData a => a -> ()
rnf FilePath
b