Agda.Compiler.JS.Compiler

Documentation

compilerMain :: Interface -> TCM ()

compile :: Interface -> TCM ()

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 :: TCM Module

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

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

numPars :: [Clause] -> Nat

clause :: Clause -> TCM Case

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

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

pattern :: Pattern -> TCM Patt

tag :: QName -> TCM Tag

visitorName :: QName -> TCM MemberId

body :: ClauseBody -> TCM Exp

term :: Term -> TCM Exp

isSingleton :: Type -> TCM (Maybe Exp)

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

qname :: QName -> TCM Exp

literal :: Literal -> Exp

dummyLambda :: Int -> Exp -> Exp

writeModule :: Module -> TCM ()

compileDir :: TCM FilePath

outFile :: GlobalId -> TCM FilePath

outFile_ :: TCM FilePath