semantics-1: typst pt. 2
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -28,13 +28,10 @@
|
||||
// premises (content), conclusion (content)
|
||||
#let bsrule(name, premises, conclusion) = {
|
||||
grid(
|
||||
columns: (auto, 1fr),
|
||||
columns: (auto, auto),
|
||||
column-gutter: 1em,
|
||||
align: (right + horizon, left + horizon),
|
||||
rel(name),
|
||||
math.equation(block: true, numbering: none,
|
||||
math.frac(premises, conclusion)
|
||||
),
|
||||
rel(name), math.equation(block: true, numbering: none, math.frac(premises, conclusion)),
|
||||
)
|
||||
v(0.4em)
|
||||
}
|
||||
@@ -42,16 +39,17 @@
|
||||
// Definition head: "e ::= ..." with label
|
||||
#let mydefhead(lhs, label) = {
|
||||
grid(
|
||||
columns: (1fr, auto),
|
||||
[#lhs],
|
||||
emph(label),
|
||||
columns: (auto, auto),
|
||||
column-gutter: 1fr,
|
||||
[#lhs], emph(label),
|
||||
)
|
||||
}
|
||||
|
||||
// Definition case: indented alternative with description
|
||||
#let mydefcase(alt, desc) = {
|
||||
grid(
|
||||
columns: (2em, 1fr, auto),
|
||||
columns: (2em, auto, auto),
|
||||
column-gutter: 1fr,
|
||||
[], [#alt], [#desc],
|
||||
)
|
||||
}
|
||||
@@ -96,7 +94,7 @@ expressions always will.)
|
||||
// ----- Figure 1: language definition ------------------------
|
||||
|
||||
#figure(
|
||||
block(inset: (left: 2em))[
|
||||
box(width: 80%, inset: (left: 2em))[
|
||||
#set align(left)
|
||||
#mydefhead[$e ::=$ #h(6em)][Expressions]
|
||||
#mydefcase(tr, [true value])
|
||||
@@ -138,36 +136,21 @@ The above line should be read as "the expression $e$ evaluates to the value $v$"
|
||||
// ----- Figure 2: big-step semantics -------------------------
|
||||
|
||||
#figure(
|
||||
block(inset: (left: 1em))[
|
||||
box(width: 80%, inset: (left: 1em))[
|
||||
#set align(left)
|
||||
#text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$v$]$)
|
||||
|
||||
#v(0.6em)
|
||||
|
||||
#bsrule("B-Value",
|
||||
$emptyset$,
|
||||
$#bstep[$v$][$v$]$,
|
||||
)
|
||||
#bsrule("B-Value", $emptyset$, $#bstep[$v$][$v$]$)
|
||||
|
||||
#bsrule("B-IfTrue",
|
||||
$#bstep[$e_1$][$#tr$] #h(2em) #bstep[$e_2$][$v$]$,
|
||||
$#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$,
|
||||
)
|
||||
#bsrule("B-IfTrue", $#bstep[$e_1$][$#tr$] #h(2em) #bstep[$e_2$][$v$]$, $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$)
|
||||
|
||||
#bsrule("B-IfFalse",
|
||||
$#bstep[$e_1$][$#fl$] #h(2em) #bstep[$e_3$][$v$]$,
|
||||
$#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$,
|
||||
)
|
||||
#bsrule("B-IfFalse", $#bstep[$e_1$][$#fl$] #h(2em) #bstep[$e_3$][$v$]$, $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$)
|
||||
|
||||
#bsrule("B-Succ",
|
||||
$#bstep[$e$][$i$]$,
|
||||
$#bstep[#suc[$e$]][$i + 1$]$,
|
||||
)
|
||||
#bsrule("B-Succ", $#bstep[$e$][$i$]$, $#bstep[#suc[$e$]][$i + 1$]$)
|
||||
|
||||
#bsrule("B-Pred",
|
||||
$#bstep[$e$][$i$]$,
|
||||
$#bstep[#prd[$e$]][$i - 1$]$,
|
||||
)
|
||||
#bsrule("B-Pred", $#bstep[$e$][$i$]$, $#bstep[#prd[$e$]][$i - 1$]$)
|
||||
],
|
||||
caption: [Big-step semantics for BoolInt\*],
|
||||
) <fig:bigstep>
|
||||
|
||||
Reference in New Issue
Block a user