ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.JS.Compiler

Main module for JS backend.

Synopsis

value jsBackend
value jsBackend'
data JSOptions
value defaultJSOptions
value jsCommandLineFlags
value jsPreCompile
value jsPostCompile
data JSModuleEnv
value jsPreModule
value jsPostModule
value jsCompileDef
value prefix
value jsMod
value jsFileName
value jsMember
value global'
value global
value reorder
value reorder'
value isTopLevelValue
value isEmptyObject
value insertAfter
type EnvWithOpts
value definition
value checkCompilerPragmas
value defJSDef
value definition'
value compileTerm
value compilePrim
value compileAlt
value visitorName
value flatName
value local
value qname
value literal
value litqname
value litmeta
value writeModule
value outFile
value primitives

PackageAgda-2.8.0.2
Exports40
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.8.0.2 · Agda.Compiler.JS.Compiler
NFData JSOptionsDefined in Agda-2.8.0.2 · Agda.Compiler.JS.Compiler
type Rep JSOptions = D1 ('MetaData "JSOptions" "Agda.Compiler.JS.Compiler" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.Compiler.JS.Compiler

valuedefaultJSOptions :: JSOptions

valuejsCommandLineFlags :: [OptDescr (Flag JSOptions)]

valuejsPreCompile :: JSOptions -> TCM JSOptions

valuejsPostCompile

Source#

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 :: JSModuleStyle -> 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 ()

Source#

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 (MemberId, Exp)

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 :: JSModuleStyle -> GlobalId -> TCM FilePath

valueprimitives :: Set PrimitiveId

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.

Orphan instances

1 instance

NFData JSModuleStyle