1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
%%
%% CoreSyn.ott
%%
%% defines formal version of core syntax
%%
%% See accompanying README file
embed {{ tex-preamble
\newcommand{\coderef}[2]{\ghcfile{#1}:\texttt{#2}%
}
\newcommand{\keyword}[1]{\textbf{#1} }
\newcommand{\labeledjudge}[1]{\vdash_{\!\!\mathsf{#1} } }
}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Metavariables %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
metavar f, x, y, z ::= {{ com Variable names }}
metavar K ::= {{ com Data constructor names }}
indexvar i, j, k, n ::= {{ com Indices to be used in lists }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
grammar
lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
{{ com Literals, \coderef{GHC/Types/Literal.hs}{Literal} }}
op {{ tex \textsf{op} }} :: 'StgOp_' ::=
{{ com Primitive operation or foreign call, \coderef{GHC/Stg/Syntax.hs}{StgOp} }}
cc {{ tex \textsf{cc} }} :: 'CostCentre_' ::=
{{ com Cost-centre, \coderef{GHC/Types/CostCentre.hs}{CostCentre} }}
ccs {{ tex \textsf{ccs} }} :: 'CostCentreStack_' ::=
| CCCS :: :: CurrentCCS {{ com Current cost-centre stack }}
{{ tex \bullet }}
| _ :: :: DontCareCCS {{ com Don't care cost-centre stack }}
| ccs ^ ccs' :: :: EnterFunCCS {{ com Function entry, \coderef{rts/Profiling.c}{enterFunCCS} }}
| ccs # cc :: :: PushCC {{ com Push a cost-centre, \coderef{rts/Profiling.c}{pushCostCentre} }}
{{ com Cost-centre stack, \coderef{GHC/Types/CostCentre.hs}{CostCentreStack} }}
a, b, c :: 'StgArg_' ::= {{ com Arguments, \coderef{GHC/Stg/Syntax.hs}{StgArg} }}
| x :: :: StgVarArg {{ com Variable }}
| lit :: :: StgLitArg {{ com Literal }}
args :: 'StgArgs_' ::= {{ com List of arguments }}
| </ ai // , // i /> :: :: List
| args args' :: :: Append
| xs :: :: CastVariables
| nil :: :: EmptyList
xs :: 'Ids_' ::= {{ com List of variables }}
| </ xi // , // i /> :: :: List
| nil :: :: EmptyList
| xs xs' :: :: Append
e :: 'StgExpr_' ::= {{ com Expressions, \coderef{GHC/Stg/Syntax.hs}{StgExpr} }}
| lit :: :: StgLit {{ com Literal }}
| x args :: :: StgApp {{ com Function application (or variable) }}
| K args :: :: StgConApp {{ com Saturated constructor application }}
| op args :: :: StgOpApp {{ com Saturated primitive application }}
| case e as x of </ alti // | // i /> :: :: StgCase {{ com Pattern match }}
| let binding in e :: :: StgLet {{ com Let binding }}
| lne binding in e :: :: StgLetNoEscape {{ com Let-no-escape binding }}
| scc cc e :: :: StgSCC {{ com Set cost-centre }}
| ( e ) :: M :: Parens {{ com Parenthesized expression }}
| e' subst :: M :: Tsub
subst :: 'Subst_' ::= {{ com List of substitutions }}
| [ a / x ] :: :: Mapping
| </ substi // i /> :: :: List
binding :: 'StgBind_' ::= {{ com Let-bindings, \coderef{GHC/Stg/Syntax.hs}{StgBind} }}
| x = rhs :: :: StgNonRec {{ com Non-recursive binding }}
| rec </ xi = rhsi // and // i /> :: :: StgRec {{ com Recursive binding }}
upd :: 'UpdateFlag_' ::= {{ com Update flag, \coderef{GHC/Stg/Syntax.hs}{UpdateFlag} }}
| r :: :: ReEntrant {{ com Function (re-entrant closure) }}
| u :: :: Updatable {{ com Thunk (updatable closure) }}
cl :: 'StgRhsClosure_' ::= {{ com StgRhsClosure }}
| \ upd ccs xs . e :: :: StgRhsClosure
rhs :: 'StgRhs_' ::= {{ com Right-hand sides, \coderef{GHC/Stg/Syntax.hs}{StgRhs} }}
| cl :: :: StgRhsClosure {{ com Closure }}
| K ccs args :: :: StgRhsCon {{ com Constructor }}
| x :: :: StgRhsIndirection {{ com Indirection (runtime only) }}
alt :: 'StgAlt_' ::= {{ com Case alternative, \coderef{GHC/Stg/Syntax.hs}{StgAlt} }}
| K </ xi // i /> -> e :: :: StgAlt {{ com Constructor applied to fresh names }}
terminals :: 'terminals_' ::=
| \ :: :: lambda {{ tex \lambda }}
| -> :: :: arrow {{ tex \rightarrow }}
| |-> :: :: mapsto {{ tex \mapsto }}
| <> :: :: union {{ tex \mathbin{\mathaccent\cdot\cup} }}
| nil :: :: empty {{ tex \cdot }}
| /= :: :: neq {{ tex \neq }}
| ^ :: :: enterFun {{ tex \bowtie }}
| # :: :: push {{ tex \triangleright }}
|