@@ -9,7 +9,7 @@ title: "Macros Spec"
99
1010Compared to the [ Dotty reference grammar] ( ../../internals/syntax.md )
1111there are the following syntax changes:
12- ``` none
12+ ```
1313SimpleExpr ::= ...
1414 | ‘'’ ‘{’ Block ‘}’
1515 | ‘'’ ‘[’ Type ‘]’
@@ -56,7 +56,7 @@ extends simply-typed lambda calculus with quotes and splices.
5656### Syntax
5757
5858The syntax of terms, values, and types is given as follows:
59- ``` none
59+ ```
6060Terms t ::= x variable
6161 (x: T) => t lambda
6262 t t application
@@ -76,7 +76,7 @@ Typing rules are formulated using a stack of environments
7676` Es ` . Individual environments ` E ` consist as usual of variable
7777bindings ` x: T ` . Environments can be combined using the two
7878combinators ` ' ` and ` $ ` .
79- ``` none
79+ ```
8080Environment E ::= () empty
8181 E, x: T
8282
@@ -93,7 +93,7 @@ right identity `()`.
9393### Operational semantics:
9494
9595We define a small step reduction relation ` --> ` with the following rules:
96- ``` none
96+ ```
9797 ((x: T) => t) v --> [x := v]t
9898
9999 ${'u} --> u
@@ -107,7 +107,7 @@ rule says that splice and quotes cancel each other out. The third rule
107107is a context rule; it says that reduction is allowed in the hole ` [ ] `
108108position of an evaluation context. Evaluation contexts ` e ` and
109109splice evaluation context ` e_s ` are defined syntactically as follows:
110- ``` none
110+ ```
111111Eval context e ::= [ ] | e t | v e | 'e_s[${e}]
112112Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | u e_s
113113```
@@ -116,7 +116,7 @@ Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | u e_s
116116Typing judgments are of the form ` Es |- t: T ` . There are two
117117substructural rules which express the fact that quotes and splices
118118cancel each other out:
119- ``` none
119+ ```
120120 Es1 * Es2 |- t: T
121121 ---------------------------
122122 Es1 $ E1 ' E2 * Es2 |- t: T
@@ -129,7 +129,7 @@ cancel each other out:
129129The lambda calculus fragment of the rules is standard, except that we
130130use a stack of environments. The rules only interact with the topmost
131131environment of the stack.
132- ``` none
132+ ```
133133 x: T in E
134134 --------------
135135 Es * E |- x: T
@@ -146,7 +146,7 @@ environment of the stack.
146146```
147147The rules for quotes and splices map between ` expr T ` and ` T ` by trading ` ' ` and ` $ ` between
148148environments and terms.
149- ``` none
149+ ```
150150 Es $ () |- t: expr T
151151 --------------------
152152 Es |- $t: T
0 commit comments