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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.JS.Compiler

Synopsis

- jsBackend :: Backend
- jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv () (Maybe Export)
- data JSOptions = JSOptions {
  - optJSCompile :: Bool
  }
- defaultJSOptions :: JSOptions
- jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
- jsPreCompile :: JSOptions -> TCM JSOptions
- jsPostCompile :: JSOptions -> IsMain -> a -> TCM ()
- type JSModuleEnv = Maybe CoinductionKit
- jsPreModule :: JSOptions -> ModuleName -> FilePath -> TCM (Recompile JSModuleEnv ())
- jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM ()
- jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
- prefix :: [Char]
- jsMod :: ModuleName -> GlobalId
- jsFileName :: GlobalId -> String
- jsMember :: Name -> MemberId
- global' :: QName -> TCM (Exp, [MemberId])
- global :: QName -> TCM (Exp, [MemberId])
- reorder :: [Export] -> [Export]
- reorder' :: Set [MemberId] -> [Export] -> [Export]
- isTopLevelValue :: Export -> Bool
- isEmptyObject :: Export -> Bool
- insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export]
- curModule :: IsMain -> TCM Module
- definition :: Maybe CoinductionKit -> (QName, Definition) -> TCM (Maybe Export)
- checkCompilerPragmas :: QName -> TCM ()
- defJSDef :: Definition -> Maybe String
- definition' :: Maybe CoinductionKit -> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)
- compileTerm :: TTerm -> TCM Exp
- compileTerm' :: Maybe CoinductionKit -> TTerm -> TCM Exp
- compilePrim :: TPrim -> Exp
- compileAlt :: TAlt -> TCM (MemberId, Exp)
- visitorName :: QName -> TCM MemberId
- flatName :: MemberId
- local :: Nat -> Exp
- qname :: QName -> TCM Exp
- literal :: Literal -> Exp
- litqname :: QName -> Exp
- writeModule :: Module -> TCM ()
- outFile :: GlobalId -> TCM FilePath
- outFile_ :: TCM FilePath
- copyRTEModules :: TCM ()
- primitives :: Set String

# Documentation

jsBackend :: Backend Source #

jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv () (Maybe Export) Source #

data JSOptions Source #

Constructors

JSOptions |

Fields

- optJSCompile :: Bool

defaultJSOptions :: JSOptions Source #

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

jsPreCompile :: JSOptions -> TCM JSOptions Source #

jsPostCompile :: JSOptions -> IsMain -> a -> TCM () Source #

type JSModuleEnv = Maybe CoinductionKit Source #

jsPreModule :: JSOptions -> ModuleName -> FilePath -> TCM (Recompile JSModuleEnv ()) Source #

jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM () 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, [MemberId]) Source #

global :: QName -> TCM (Exp, [MemberId]) Source #

reorder :: [Export] -> [Export] Source #

reorder' :: Set [MemberId] -> [Export] -> [Export] Source #

isTopLevelValue :: Export -> Bool Source #

isEmptyObject :: Export -> Bool Source #

insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export] Source #

curModule :: IsMain -> TCM Module Source #

definition :: Maybe CoinductionKit -> (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' :: Maybe CoinductionKit -> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export) Source #

compileTerm :: TTerm -> TCM Exp Source #

compileTerm' :: Maybe CoinductionKit -> TTerm -> TCM Exp Source #

compilePrim :: TPrim -> Exp Source #

compileAlt :: 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 #

writeModule :: Module -> TCM () Source #

outFile :: GlobalId -> TCM FilePath Source #

outFile_ :: TCM FilePath Source #

copyRTEModules :: TCM () Source #

primitives :: Set String Source #

Primitives implemented in the JS Agda RTS.