Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.JS.Compiler

Description

Main module for JS backend.

Synopsis

Documentation

data JSOptions Source #

Constructors

JSOptions 

Fields

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.4-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) :*: S1 ('MetaSel ('Just "optJSModuleStyle") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 JSModuleStyle)))))

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

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

data JSModuleEnv Source #

Constructors

JSModuleEnv 

Fields

prefix :: [Char] Source #

checkCompilerPragmas :: QName -> TCM () Source #

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

defJSDef :: Definition -> Maybe String Source #

outFile :: GlobalId -> TCM FilePath Source #

outFile_ :: TCM FilePath Source #

primitives :: 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

NFData JSModuleStyle Source # 
Instance details

Methods

rnf :: JSModuleStyle -> ()