Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Compiler.JS.Compiler

Description

Main module for JS backend.

Synopsis

jsBackend :: Backend
jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
data JSOptions = JSOptions {
- optJSCompile :: Bool
- optJSOptimize :: Bool
- optJSMinify :: Bool
- optJSVerify :: Bool
}
defaultJSOptions :: JSOptions
jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
jsPreCompile :: JSOptions -> TCM JSOptions
jsPostCompile :: JSOptions -> IsMain -> Map ModuleName Module -> TCM ()
mergeModules :: Map ModuleName Module -> [(GlobalId, Export)]
data JSModuleEnv = JSModuleEnv {
- jsCoinductionKit :: Maybe CoinductionKit
- jsCompile :: Bool
}
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 ()
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

Documentation

jsBackend :: Backend Source #

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

data JSOptions Source #

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

Instances details

Generic JSOptions Source #
Instance details 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 Source #
Instance details Defined in Agda.Compiler.JS.Compiler Methods rnf :: JSOptions -> () #
type Rep JSOptions Source #
Instance details 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 Source #

jsCommandLineFlags :: [OptDescr (Flag JSOptions)] Source #

jsPreCompile :: JSOptions -> TCM JSOptions Source #

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

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

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

data JSModuleEnv Source #

Constructors

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

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

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

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

prefix :: [Char] Source #

jsMod :: ModuleName -> GlobalId Source #

jsFileName :: GlobalId -> String Source #

jsMember :: Name -> MemberId Source #

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

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

reorder :: [Export] -> [Export] Source #

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

isTopLevelValue :: Export -> Bool Source #

isEmptyObject :: Export -> Bool Source #

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

type EnvWithOpts = (JSOptions, JSModuleEnv) Source #

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

checkCompilerPragmas :: QName -> TCM () Source #

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

defJSDef :: Definition -> Maybe String Source #

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

compileTerm :: EnvWithOpts -> TTerm -> TCM Exp Source #

compilePrim :: TPrim -> Exp Source #

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

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

visitorName :: QName -> TCM MemberId Source #

flatName :: MemberId Source #

local :: Nat -> Exp Source #

qname :: QName -> TCM Exp Source #

literal :: Literal -> Exp Source #

litqname :: QName -> Exp Source #

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

outFile :: GlobalId -> TCM FilePath Source #

outFile_ :: TCM FilePath Source #

primitives :: Set String Source #

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.