@@ -9,7 +9,7 @@ title: "Macros Spec"
9
9
10
10
Compared to the [ Dotty reference grammar] ( ../../internals/syntax.md )
11
11
there are the following syntax changes:
12
- ``` none
12
+ ```
13
13
SimpleExpr ::= ...
14
14
| ‘'’ ‘{’ Block ‘}’
15
15
| ‘'’ ‘[’ Type ‘]’
@@ -56,7 +56,7 @@ extends simply-typed lambda calculus with quotes and splices.
56
56
### Syntax
57
57
58
58
The syntax of terms, values, and types is given as follows:
59
- ``` none
59
+ ```
60
60
Terms t ::= x variable
61
61
(x: T) => t lambda
62
62
t t application
@@ -76,7 +76,7 @@ Typing rules are formulated using a stack of environments
76
76
` Es ` . Individual environments ` E ` consist as usual of variable
77
77
bindings ` x: T ` . Environments can be combined using the two
78
78
combinators ` ' ` and ` $ ` .
79
- ``` none
79
+ ```
80
80
Environment E ::= () empty
81
81
E, x: T
82
82
@@ -93,7 +93,7 @@ right identity `()`.
93
93
### Operational semantics:
94
94
95
95
We define a small step reduction relation ` --> ` with the following rules:
96
- ``` none
96
+ ```
97
97
((x: T) => t) v --> [x := v]t
98
98
99
99
${'u} --> u
@@ -107,7 +107,7 @@ rule says that splice and quotes cancel each other out. The third rule
107
107
is a context rule; it says that reduction is allowed in the hole ` [ ] `
108
108
position of an evaluation context. Evaluation contexts ` e ` and
109
109
splice evaluation context ` e_s ` are defined syntactically as follows:
110
- ``` none
110
+ ```
111
111
Eval context e ::= [ ] | e t | v e | 'e_s[${e}]
112
112
Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | u e_s
113
113
```
@@ -116,7 +116,7 @@ Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | u e_s
116
116
Typing judgments are of the form ` Es |- t: T ` . There are two
117
117
substructural rules which express the fact that quotes and splices
118
118
cancel each other out:
119
- ``` none
119
+ ```
120
120
Es1 * Es2 |- t: T
121
121
---------------------------
122
122
Es1 $ E1 ' E2 * Es2 |- t: T
@@ -129,7 +129,7 @@ cancel each other out:
129
129
The lambda calculus fragment of the rules is standard, except that we
130
130
use a stack of environments. The rules only interact with the topmost
131
131
environment of the stack.
132
- ``` none
132
+ ```
133
133
x: T in E
134
134
--------------
135
135
Es * E |- x: T
@@ -146,7 +146,7 @@ environment of the stack.
146
146
```
147
147
The rules for quotes and splices map between ` expr T ` and ` T ` by trading ` ' ` and ` $ ` between
148
148
environments and terms.
149
- ``` none
149
+ ```
150
150
Es $ () |- t: expr T
151
151
--------------------
152
152
Es |- $t: T
0 commit comments