Agda.Compiler.JS.Compiler

Documentation

jsBackend :: Backend

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

data JSOptions

Constructors

JSOptions

Fields

• optJSCompile :: Bool

defaultJSOptions :: JSOptions

jsCommandLineFlags :: [OptDescr (Flag JSOptions)]

jsPreCompile :: JSOptions -> TCM JSOptions

jsPostCompile :: JSOptions -> IsMain -> a -> TCM ()

type JSModuleEnv = Maybe CoinductionKit

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

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

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

prefix :: [Char]

jsMod :: ModuleName -> GlobalId

jsFileName :: GlobalId -> String

jsMember :: Name -> MemberId

global' :: QName -> TCM (Exp, [MemberId])

global :: QName -> TCM (Exp, [MemberId])

reorder :: [Export] -> [Export]

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

isTopLevelValue :: Export -> Bool

isEmptyObject :: Export -> Bool

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

curModule :: IsMain -> TCM Module

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

checkCompilerPragmas :: QName -> TCM ()

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

defJSDef :: Definition -> Maybe String

definition' :: Maybe CoinductionKit -> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)

compileTerm :: TTerm -> TCM Exp

compileTerm' :: Maybe CoinductionKit -> TTerm -> TCM Exp

compilePrim :: TPrim -> Exp

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

visitorName :: QName -> TCM MemberId

flatName :: MemberId

local :: Nat -> Exp

qname :: QName -> TCM Exp

literal :: Literal -> Exp

litqname :: QName -> Exp

writeModule :: Module -> TCM ()

outFile :: GlobalId -> TCM FilePath

outFile_ :: TCM FilePath

copyRTEModules :: TCM ()

primitives :: Set String

Primitives implemented in the JS Agda RTS.