Agda.Compiler.JS.Compiler

Main module for JS backend.

Documentation

jsBackend :: Backend

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

data JSOptions

Constructors

JSOptions

Fields

• optJSCompile :: Bool
• optJSOptimize :: Bool
• optJSMinify :: Bool

  Remove spaces etc. See https://en.wikipedia.org/wiki/Minification_(programming).

• optJSVerify :: Bool

  Run generated code through interpreter.

Instances

Generic JSOptions

Defined in Agda.Compiler.JS.Compiler

Associated Types

type Rep JSOptions :: Type -> Type

Methods

from :: JSOptions -> Rep JSOptions x

to :: Rep JSOptions x -> JSOptions

NFData JSOptions

Defined in Agda.Compiler.JS.Compiler

Methods

rnf :: JSOptions -> ()

type Rep JSOptions

Defined in Agda.Compiler.JS.Compiler

type Rep JSOptions = D1 ('MetaData "JSOptions" "Agda.Compiler.JS.Compiler" "Agda-2.6.2.1.20220327-inplace" '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))))

defaultJSOptions :: JSOptions

jsCommandLineFlags :: [OptDescr (Flag JSOptions)]

jsPreCompile :: JSOptions -> TCM JSOptions

jsPostCompile :: JSOptions -> IsMain -> Map ModuleName Module -> TCM ()

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

mergeModules :: Map ModuleName Module -> [(GlobalId, Export)]

data JSModuleEnv

Constructors

JSModuleEnv

Fields

• jsCoinductionKit :: Maybe CoinductionKit
• jsCompile :: Bool

  Should this module be compiled?

jsPreModule :: JSOptions -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module)

jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM Module

jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)

prefix :: [Char]

jsMod :: ModuleName -> GlobalId

jsFileName :: GlobalId -> String

jsMember :: Name -> MemberId

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

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

reorder :: [Export] -> [Export]

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

isTopLevelValue :: Export -> Bool

isEmptyObject :: Export -> Bool

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

type EnvWithOpts = (JSOptions, JSModuleEnv)

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

checkCompilerPragmas :: QName -> TCM ()

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

defJSDef :: Definition -> Maybe String

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

compileTerm :: EnvWithOpts -> TTerm -> TCM Exp

compilePrim :: TPrim -> Exp

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

eraseLocalVars :: [Bool] -> TTerm -> TTerm

visitorName :: QName -> TCM MemberId

flatName :: MemberId

local :: Nat -> Exp

qname :: QName -> TCM Exp

literal :: Literal -> Exp

litqname :: QName -> Exp

writeModule :: Bool -> Module -> TCM ()

outFile :: GlobalId -> TCM FilePath

outFile_ :: TCM FilePath

primitives :: Set String

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.