Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

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 Source # Methods from :: JSOptions -> Rep JSOptions x Source # to :: Rep JSOptions x -> JSOptions Source #
NFData JSOptions Source # |
Instance details Defined in Agda.Compiler.JS.Compiler Methods rnf :: JSOptions -> () Source #
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.2-7KnEKyKhaJHFPwDzdI3vIK" '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`.