Agda-2.6.2.0.20211129: 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 #

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.0.20211129-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))))

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

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

data JSModuleEnv Source #

Constructors

JSModuleEnv 

Fields

checkCompilerPragmas :: QName -> TCM () Source #

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

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.