{-# 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
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> opts
options :: opts
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags :: [OptDescr (Flag opts)]
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> opts -> Bool
isEnabled :: opts -> Bool
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> opts -> tcm env
preCompile :: opts -> tcm env
, 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 ()
, 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)
, 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
, 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
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> Bool
scopeCheckingSuffices :: Bool
, forall (tcm :: * -> *) opts env menv mod def.
Backend'_boot tcm opts env menv mod def -> QName -> tcm Bool
mayEraseType :: QName -> tcm Bool
}
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