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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.JS.Compiler

Documentation

compilerMain :: Interface -> TCM () Source

compile :: Interface -> TCM () 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 :: TCM Module Source

definition :: (QName, Definition) -> TCM Export Source

defn :: QName -> [MemberId] -> Type -> Maybe JSCode -> Defn -> TCM Exp Source

numPars :: [Clause] -> Nat Source

clause :: Clause -> TCM Case Source

mapping :: [Pattern] -> (Nat, Nat, [Exp]) Source

mapping' :: Pattern -> (Nat, Nat, [Exp]) -> (Nat, Nat, [Exp]) Source

pattern :: Pattern -> TCM Patt Source

tag :: QName -> TCM Tag Source

visitorName :: QName -> TCM MemberId Source

body :: ClauseBody -> TCM Exp Source

term :: Term -> TCM Exp Source

isSingleton :: Type -> TCM (Maybe Exp) Source

args :: Int -> Args -> TCM [Exp] Source

qname :: QName -> TCM Exp Source

literal :: Literal -> Exp Source

dummyLambda :: Int -> Exp -> Exp Source

writeModule :: Module -> TCM () Source

compileDir :: TCM FilePath Source

outFile :: GlobalId -> TCM FilePath Source

outFile_ :: TCM FilePath Source