Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Compiler.Alonzo.Main
Synopsis
compilerMain
::
TCM
()
->
TCM
()
fromCurrentModule
::
QName
->
TCM
Bool
flattenSubmodules
::
QName
->
TCM
QName
maybeQualName
:: (
QName
->
HsQName
) -> (
Name
->
HsName
) ->
QName
->
PM
HsQName
numOfMainS
:: [
QName
] ->
Maybe
Nat
processDefWithDebug
:: (
QName
,
Definition
) ->
TCM
[
HsDecl
]
infoDecl
::
String
->
String
->
HsDecl
processDef
:: (
QName
,
Definition
) ->
TCM
[
HsDecl
]
times
::
Nat
-> a -> [a]
consDefs
:: [
QName
] ->
TCM
[
Definition
]
processClause
::
Name
->
Nat
->
Clause
->
TCM
HsDecl
contClause
::
Name
->
Nat
->
Clause
->
TCM
HsDecl
foldClauses
::
Name
->
Nat
-> [
Clause
] ->
TCM
[
HsDecl
]
processArgPats
:: [
Arg
Pattern
] ->
PM
[
HsPat
]
processArgPat
::
Arg
Pattern
->
PM
HsPat
processPat
::
Pattern
->
PM
HsPat
processBody
::
ClauseBody
->
PM
HsExp
processTerm
::
Term
->
PM
HsExp
processLit
::
Literal
->
HsExp
processVap
::
HsExp
-> [
Arg
Term
] ->
PM
HsExp
unfoldVap
::
PState
->
HsExp
-> [
Arg
Term
] ->
TCM
HsExp
getDefinitions
::
TCM
Definitions
getConArity
::
QName
->
TCM
Nat
typeArity
::
Type
->
Nat
clauseBod
::
Clause
->
Term
vecApp
::
HsExp
-> [
HsExp
] ->
HsExp
Documentation
compilerMain
::
TCM
()
->
TCM
()
Source
The main function
fromCurrentModule
::
QName
->
TCM
Bool
Source
flattenSubmodules
::
QName
->
TCM
QName
Source
maybeQualName
:: (
QName
->
HsQName
) -> (
Name
->
HsName
) ->
QName
->
PM
HsQName
Source
numOfMainS
:: [
QName
] ->
Maybe
Nat
Source
processDefWithDebug
:: (
QName
,
Definition
) ->
TCM
[
HsDecl
]
Source
infoDecl
::
String
->
String
->
HsDecl
Source
processDef
:: (
QName
,
Definition
) ->
TCM
[
HsDecl
]
Source
times
::
Nat
-> a -> [a]
Source
consDefs
:: [
QName
] ->
TCM
[
Definition
]
Source
processClause
::
Name
->
Nat
->
Clause
->
TCM
HsDecl
Source
contClause
::
Name
->
Nat
->
Clause
->
TCM
HsDecl
Source
foldClauses
::
Name
->
Nat
-> [
Clause
] ->
TCM
[
HsDecl
]
Source
processArgPats
:: [
Arg
Pattern
] ->
PM
[
HsPat
]
Source
processArgPat
::
Arg
Pattern
->
PM
HsPat
Source
processPat
::
Pattern
->
PM
HsPat
Source
processBody
::
ClauseBody
->
PM
HsExp
Source
processTerm
::
Term
->
PM
HsExp
Source
processLit
::
Literal
->
HsExp
Source
processVap
::
HsExp
-> [
Arg
Term
] ->
PM
HsExp
Source
unfoldVap
::
PState
->
HsExp
-> [
Arg
Term
] ->
TCM
HsExp
Source
getDefinitions
::
TCM
Definitions
Source
getConArity
::
QName
->
TCM
Nat
Source
typeArity
::
Type
->
Nat
Source
clauseBod
::
Clause
->
Term
Source
vecApp
::
HsExp
-> [
HsExp
] ->
HsExp
Source
Produced by
Haddock
version 2.4.2