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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.JS.Compiler

Contents

- Orphan instances

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
  - optJSModuleStyle :: JSModuleStyle
  }
- defaultJSOptions :: JSOptions
- jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
- jsPreCompile :: JSOptions -> TCM JSOptions
- jsPostCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCM ()
- data JSModuleEnv = JSModuleEnv {
  - jsCoinductionKit :: Maybe CoinductionKit
  - jsCompile :: Bool
  }
- jsPreModule :: JSOptions -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module)
- jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> TopLevelModuleName -> [Maybe Export] -> TCM Module
- jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
- prefix :: [Char]
- jsMod :: TopLevelModuleName -> GlobalId
- jsFileName :: JSModuleStyle -> 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 (MemberId, Exp)
- visitorName :: QName -> TCM MemberId
- flatName :: MemberId
- local :: Nat -> Exp
- qname :: QName -> TCM Exp
- literal :: Literal -> Exp
- litqname :: QName -> Exp
- litmeta :: MetaId -> Exp
- writeModule :: Bool -> JSModuleStyle -> Module -> TCM ()
- outFile :: JSModuleStyle -> GlobalId -> TCM FilePath
- primitives :: Set PrimitiveId

# 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.

- optJSModuleStyle :: JSModuleStyle

#### Instances

Instances details

NFData JSOptions Source # |
Instance details Defined in Agda.Compiler.JS.Compiler Methods rnf :: JSOptions -> () Source #
Generic JSOptions Source # |

Instance details

Defined in Agda.Compiler.JS.Compiler

Associated Types

type Rep JSOptions |

Instance details

Defined in Agda.Compiler.JS.Compiler

type Rep JSOptions = D1 ('MetaData "JSOptions" "Agda.Compiler.JS.Compiler" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: JSOptions -> Rep JSOptions x Source #

to :: Rep JSOptions x -> 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.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

defaultJSOptions :: JSOptions Source #

jsCommandLineFlags :: [OptDescr (Flag JSOptions)] Source #

jsPreCompile :: JSOptions -> TCM JSOptions Source #

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

- jsCoinductionKit :: Maybe CoinductionKit
- jsCompile :: Bool

  Should this module be compiled?

jsPreModule :: JSOptions -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module) Source #

jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> TopLevelModuleName -> [Maybe Export] -> TCM Module Source #

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

prefix :: [Char] Source #

jsMod :: TopLevelModuleName -> GlobalId Source #

jsFileName :: JSModuleStyle -> 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 (MemberId, Exp) 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 #

litmeta :: MetaId -> Exp Source #

writeModule :: Bool -> JSModuleStyle -> Module -> TCM () Source #

outFile :: JSModuleStyle -> GlobalId -> 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 -> () Source #