Skip to content

HORIZON HASKELL Docs lts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Compiler.JS.Compiler

Main module for JS backend.

3 types
39 values

PackageAgda-2.7.0.1
Exports42
LanguageHaskell2010
LicenceMIT
SourceCompiler.hs

valuejsBackend :: Backend

valuejsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)

datadata JSOptions

Constructors

JSOptions
- optJSCompile :: Bool
- optJSOptimize :: Bool
- optJSMinify :: Bool
  Remove spaces etc. See https://en.wikipedia.org/wiki/Minification_(programming).
- optJSVerify :: Bool
  Run generated code through interpreter.
- optJSModuleStyle :: JSModuleStyle

Instances3Generic, NFData, Rep

Generic JSOptionsDefined in Agda-2.7.0.1 · Agda.Compiler.JS.Compiler
NFData JSOptionsDefined in Agda-2.7.0.1 · Agda.Compiler.JS.Compiler
type Rep JSOptions = D1 ('MetaData "JSOptions" "Agda.Compiler.JS.Compiler" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "JSOptions" 'PrefixI 'True) ((S1 ('MetaSel ('Just "optJSCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optJSOptimize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optJSMinify") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optJSVerify") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optJSModuleStyle") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 JSModuleStyle)))))Defined in Agda-2.7.0.1 · Agda.Compiler.JS.Compiler

valuedefaultJSOptions :: JSOptions

valuejsCommandLineFlags :: [OptDescr (Flag JSOptions)]

valuejsPreCompile :: JSOptions -> TCM JSOptions

valuejsPostCompile

After all modules have been compiled, copy RTE modules and verify compiled modules.

datadata JSModuleEnv

Constructors

JSModuleEnv
- jsCoinductionKit :: Maybe CoinductionKit
- jsCompile :: Bool
  Should this module be compiled?

valuejsPreModule

valuejsPostModule

valuejsCompileDef

valueprefix :: [Char]

valuejsMod :: TopLevelModuleName -> GlobalId

valuejsFileName :: GlobalId -> String

valuejsMember :: Name -> MemberId

valueglobal' :: QName -> TCM (Exp, JSQName)

valueglobal :: QName -> TCM (Exp, JSQName)

valuereorder :: [Export] -> [Export]

valuereorder' :: Set JSQName -> [Export] -> [Export]

valueisTopLevelValue :: Export -> Bool

valueisEmptyObject :: Export -> Bool

valueinsertAfter :: Set JSQName -> Export -> [Export] -> [Export]

typetype EnvWithOpts = (JSOptions, JSModuleEnv)

valuedefinition :: EnvWithOpts -> (QName, Definition) -> TCM (Maybe Export)

valuecheckCompilerPragmas :: QName -> TCM ()

Ensure that there is at most one pragma for a name.

valuedefJSDef :: Definition -> Maybe String

valuedefinition'

:: EnvWithOpts
-> QName
-> Definition
-> Type
-> JSQName
-> TCM (Maybe Export)

valuecompileTerm :: EnvWithOpts -> TTerm -> TCM Exp

valuecompilePrim :: TPrim -> Exp

valuecompileAlt :: EnvWithOpts -> TAlt -> TCM ((QName, MemberId), Exp)

valueeraseLocalVars :: [Bool] -> TTerm -> TTerm

valuevisitorName :: QName -> TCM MemberId

valueflatName :: MemberId

valuelocal :: Nat -> Exp

valueqname :: QName -> TCM Exp

valueliteral :: Literal -> Exp

valuelitqname :: QName -> Exp

valuelitmeta :: MetaId -> Exp

valuewriteModule :: Bool -> JSModuleStyle -> Module -> TCM ()

valueoutFile :: GlobalId -> TCM FilePath

valueoutFile_ :: TCM FilePath

valueprimitives :: Set PrimitiveId

Primitives implemented in the JS Agda RTS.

TODO: Primitives that are not part of this set, and for which defJSDef does not return anything, are silently compiled to Undefined. A better approach might be to list exactly those primitives which should be compiled to Undefined.

Orphan instances

1 instance

NFData JSModuleStyle