263 lines
6.6 KiB
Typst
263 lines
6.6 KiB
Typst
#import "@preview/curryst:0.6.0": rule, prooftree, rule-set
|
|
#import "@preview/codly:1.3.0": codly-init
|
|
|
|
#show: codly-init
|
|
|
|
#let syntax(body) = {
|
|
set text(weight: "bold", fill: rgb(100, 50, 0))
|
|
body
|
|
}
|
|
|
|
#let mk-box(title, body, ..args) = block(
|
|
inset: 1em,
|
|
stroke: black,
|
|
..args,
|
|
)[
|
|
=== #title
|
|
|
|
#body
|
|
]
|
|
|
|
#let blank(r, c) = grid.cell(
|
|
rowspan: r,
|
|
colspan: c
|
|
)[]
|
|
|
|
#let tab = sym.arrow.r.stop
|
|
#let nl = move(dx: -2pt, dy: 2pt, sym.arrow.curve.l)
|
|
#let syntax-preamble = doc => {
|
|
show tab: set text(fill: gray.darken(20%))
|
|
show sym.arrow.curve.l: set text(fill: gray.darken(20%))
|
|
set math.cases(gap: 4pt)
|
|
|
|
show math.equation: set align(left)
|
|
|
|
doc
|
|
}
|
|
|
|
#let python-syntax = mk-box(width: 100%)[Python Syntax][
|
|
#show: syntax-preamble
|
|
#grid(
|
|
columns: (auto, auto, 1fr, auto),
|
|
align: (left, left, left, right).map(a => a + horizon),
|
|
column-gutter: .4em,
|
|
row-gutter: 1.2em,
|
|
$"t"$, $::=$, none, [_terms_],
|
|
blank(11, 2),
|
|
$"x"$, [_variable_],
|
|
$"i"$, [_integer literal_],
|
|
$"f"$, [_float literal_],
|
|
$"z"$, [_string literal_],
|
|
$"True"$, [_constant true_],
|
|
$"False"$, [_constant false_],
|
|
$"None"$, [_constant none_],
|
|
$f("t")$, [_call_],
|
|
$"t"_21 #syntax[if] "t"_1 #syntax[else] "t"_22$, [_ternary_],
|
|
$"t"_1 "op" "t"_2$, [_operation_],
|
|
$"s"; "t"$, [_sequence_],
|
|
grid.cell(colspan: 4)[],
|
|
|
|
$"v"$, $::=$, none, [_values_],
|
|
blank(6, 2),
|
|
$"i"$, [_integer literal_],
|
|
$"f"$, [_float literal_],
|
|
$"z"$, [_string literal_],
|
|
$"True"$, [_constant true_],
|
|
$"False"$, [_constant false_],
|
|
$"None"$, [_constant none_],
|
|
grid.cell(colspan: 4)[],
|
|
|
|
$"s"$, $::=$, none, [_statements_],
|
|
blank(4, 2),
|
|
$"x" = "t"$, [_assignment_],
|
|
$"x": "T"$, [_variable declaration_],
|
|
$ cases(
|
|
#syntax[def] f("x": "T") -> "T": #nl,
|
|
#tab "t" #nl,
|
|
delim: "["
|
|
) $, [_def_],
|
|
$ cases(
|
|
#syntax[if] "t": #nl,
|
|
tab "s" #nl,
|
|
#syntax[else]: #nl,
|
|
tab "s" #nl,
|
|
delim: "["
|
|
) $, [_if / else_],
|
|
)
|
|
]
|
|
|
|
#let midas-syntax = mk-box(width: 100%)[Midas Syntax][
|
|
#show: syntax-preamble
|
|
#grid(
|
|
columns: (auto, auto, 1fr, auto),
|
|
align: (left, left, left, right).map(a => a + horizon),
|
|
column-gutter: .4em,
|
|
row-gutter: 1.2em,
|
|
$"T"$, $::=$, none, [_types_],
|
|
blank(5, 2),
|
|
$"X"$, [_named type_],
|
|
$"T" ["T"]$, [_type application_],
|
|
$"T" #syntax[where] "c"$, [_constraint type_],
|
|
${attach("p"_i: "T"_i, tr: i in 1..n)}$, [_complex type_],
|
|
$(attach("a"_i: "T"_i, tr: i in 1..n)) -> "T"$, [_function type_],
|
|
grid.cell(colspan: 4)[],
|
|
|
|
$"s"$, $::=$, none, [_statements_],
|
|
blank(2, 2),
|
|
$#syntax[type] "X" = "T"$, [_type definition_],
|
|
$#syntax[type] "X"["Y"] = "T"$, [_generic definition_],
|
|
)
|
|
]
|
|
|
|
#grid(
|
|
columns: (1fr, 1fr),
|
|
column-gutter: 1em,
|
|
python-syntax,
|
|
midas-syntax
|
|
)
|
|
|
|
#pagebreak()
|
|
|
|
#let abs-typ-rules = (
|
|
int: rule($Gamma tack "i": "Int"$, name: [(T-Int)]),
|
|
float: rule($Gamma tack "f": "Float"$, name: [(T-Float)]),
|
|
str: rule($Gamma tack "z": "Str"$, name: [(T-Str)]),
|
|
"true": rule($Gamma tack "True": "Bool"$, name: [(T-True)]),
|
|
"false": rule($Gamma tack "False": "Bool"$, name: [(T-False)]),
|
|
"none": rule($Gamma tack "None": "None"$, name: [(T-None)]),
|
|
var: rule(
|
|
$"x": "T" in Gamma$,
|
|
$Gamma tack "x": "T"$,
|
|
name: [(T-Var)]
|
|
),
|
|
def: rule(
|
|
$Gamma, f: "T"_1 -> "T"_2, "x": "T"_1 tack "t": "T"_2$,
|
|
$Gamma tack #syntax[def] f("x": "T"_1) -> "T"_2: "t" space tack.l space Gamma, f: "T"_1 -> "T"_2 $,
|
|
name: [(T-Def)]
|
|
),
|
|
call: rule(
|
|
$Gamma tack f: "T"_1 -> "T"_2$,
|
|
$Gamma tack "t": "T"_1$,
|
|
$Gamma tack f("t"): "T"_2$,
|
|
name: [(T-Call)]
|
|
),
|
|
ternary: rule(
|
|
$Gamma tack "t"_1: "Bool"$,
|
|
$Gamma tack "t"_21: "T"$,
|
|
$Gamma tack "t"_22: "T"$,
|
|
$Gamma tack "t"_21 #syntax[if] "t"_1 #syntax[else] "t"_22: "T"$,
|
|
name: [(T-Tern)]
|
|
),
|
|
op: rule(
|
|
$Gamma tack "t"_1: "T"_1$,
|
|
$Gamma tack "t"_2: "T"_2$,
|
|
$"op": "T"_1 -> "T"_2 -> "T"_3 in Gamma$,
|
|
$Gamma tack "t"_1 "op" "t"_2: "T"_3$,
|
|
name: [(T-Op)]
|
|
),
|
|
seq: rule(
|
|
$Gamma tack "s" tack.l Gamma'$,
|
|
$Gamma' tack "t": "T"$,
|
|
$Gamma tack "s"; "t": "T"$,
|
|
name: [(T-Seq)]
|
|
),
|
|
annot: rule(
|
|
$Gamma tack "x": "T" tack.l Gamma, "x": "T"$,
|
|
name: [(T-Annot)]
|
|
),
|
|
if-else: rule(
|
|
$Gamma tack "t": "Bool"$,
|
|
$Gamma tack "s"_1 tack.l Gamma'$,
|
|
$Gamma tack "s"_2 tack.l Gamma''$,
|
|
$Gamma tack #syntax[if] "t": "s"_1 #syntax[else]: "s"_2 tack.l Gamma$,
|
|
name: [(T-IfElse)]
|
|
)
|
|
)
|
|
|
|
#let py-typ-rules = (
|
|
int: ```py 12: int```,
|
|
float: ```py 12.34: float```,
|
|
str: ```py "foo": str```,
|
|
"true": ```py True: bool```,
|
|
"false": ```py False: bool```,
|
|
"none": ```py None: None```,
|
|
var: ```py x```,
|
|
def: ```py
|
|
def func(a: S) -> T:
|
|
return ...: T
|
|
```,
|
|
call: ```py
|
|
def func(a: S) -> T: ...
|
|
...
|
|
func(a: S): T
|
|
```,
|
|
ternary: ```py (true if cond else false): T ```,
|
|
op: ```py (a + b): T```,
|
|
annot: ```py x: T```,
|
|
if-else: ```py
|
|
if cond:
|
|
...
|
|
else:
|
|
...
|
|
```,
|
|
)
|
|
|
|
#let reading-keys = (
|
|
def: [
|
|
_Gamma_ judges that $#syntax[def] f("x": "T"_1) -> "T"_2: "t"$ adds $f: "T"_1 -> "T"_2$ to the context, iff by adding $f: "T"_1 -> "T"_2$ and $"x": "T"_1$ to _Gamma_, it can judge that $"t": "T"_2$
|
|
],
|
|
annot: [
|
|
_Gamma_ judges that $"x": "T"$ adds $"x": "T"$ to the context
|
|
],
|
|
if-else: [
|
|
_Gamma_ judges that $#syntax[if] "t": "s"_1 #syntax[else]: "s"_2$ produces an the unchanged context $Gamma'$, iff _Gamma_ judges that $"t": "Bool"$, that $"s"_1$ produces the context $Gamma'$, and $"s"_2$ produces the context $Gamma''$. This means that statements in
|
|
]
|
|
)
|
|
|
|
#mk-box[Python Typing][
|
|
#v(1em)
|
|
#stack(dir: ltr, spacing: 1fr)[_*Rule*_][_*Python example*_]
|
|
|
|
#for (i, (k, abs-rule)) in abs-typ-rules.pairs().enumerate() {
|
|
let py-rule = py-typ-rules.at(k, default: none)
|
|
let reading-key = reading-keys.at(k, default: none)
|
|
let cells = (
|
|
prooftree(abs-rule),
|
|
py-rule
|
|
)
|
|
if reading-key != none {
|
|
cells.push(
|
|
grid.cell(
|
|
colspan: 2,
|
|
inset: (x: .8em, y: .4em),
|
|
stroke: (left: gray.lighten(50%) + 2pt),
|
|
)[
|
|
#set text(size: .8em)
|
|
#show math.equation: box.with(
|
|
fill: red.lighten(90%),
|
|
outset: (y: .3em, x: 1pt),
|
|
)
|
|
*Reading key*:\
|
|
#reading-key
|
|
]
|
|
)
|
|
}
|
|
|
|
box(
|
|
fill: if calc.even(i) {gray.lighten(95%)} else {},
|
|
outset: (x: .5em),
|
|
inset: (y: .5em),
|
|
align(
|
|
horizon,
|
|
grid(
|
|
columns: (auto, 1fr),
|
|
column-gutter: 1em,
|
|
row-gutter: .5em,
|
|
align: (left + horizon, right + horizon),
|
|
..cells,
|
|
)
|
|
)
|
|
)
|
|
}
|
|
]
|