{-# 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 (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`
    -- Andreas, 2025-07-31, cannot normalize functions with deepseq-1.5.2.0 (GHC 9.10.3).
    -- see https://github.com/haskell/deepseq/issues/111.
    -- rnf d `seq`
    -- rnf e `seq`
    -- rnf f `seq`
    -- rnf g `seq`
    -- rnf h `seq`
    -- rnf i `seq`
    -- rnf j `seq`
    Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
k () -> () -> ()
forall a b. a -> b -> b
`seq`
    -- rnf l `seq`
    -- rnf m `seq`
    -- rnf n `seq`
    ()