feat(design): some syntax and typing rules

2026-06-03 15:22:53 +02:00
parent 08dc9dd5e9
commit ec4d2473d3
1 changed files with 135 additions and 0 deletions
--- a/design/calculus_rules.typ
+++ b/design/calculus_rules.typ
@@ -0,0 +1,135 @@
+#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) = box(
+  inset: 1em,
+  stroke: black,
+  ..args,
+)[
+  === #title
+
+  #body
+]
+
+#let blank(r, c) = grid.cell(
+  rowspan: r,
+  colspan: c
+)[]
+
+#mk-box(width: 60%)[Syntax][
+  #grid(
+    columns: (auto, auto, 1fr, auto),
+    align: (left, left, left, right),
+    column-gutter: .4em,
+    row-gutter: 1em,
+    $"t"$, $::=$, none, [_terms_],
+    blank(13, 2),
+    $"x"$, [_variable_],
+    $"i"$, [_integer literal_],
+    $"f"$, [_float literal_],
+    $"s"$, [_string literal_],
+    $"True"$, [_constant true_],
+    $"False"$, [_constant false_],
+    $"None"$, [_constant none_],
+    $"x" = "t"$, [_assignment_],
+    $"x": "T" = "t"$, [_type assignment_],
+    $#syntax[def] f("x": "T") -> "T": "t"$, [_def_],
+    $f("t")$, [_call_],
+    $"t"_21 #syntax[if] "t"_1 #syntax[else] "t"_22$, [_ternary_],
+    $"t"_1 "op" "t"_2$, [_operation_],
+    grid.cell(colspan: 4)[],
+    $"v"$, $::=$, none, [_values_],
+    blank(10, 2),
+    $"i"$, [_integer literal_],
+    $"f"$, [_float literal_],
+    $"s"$, [_string literal_],
+    $"True"$, [_constant true_],
+    $"False"$, [_constant false_],
+    $"None"$, [_constant none_],
+  )
+]
+
+#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 "s": "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, "x": "T"_1 tack "t" -> "T"_2$,
+    $Gamma tack #syntax[def] f("x": "T"_1) -> "T"_2: "t" space : space "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$
+  )
+)
+
+#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: T```,
+  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```
+)
+
+#mk-box[Typing][
+  #v(1em)
+  #stack(dir: ltr, spacing: 1fr)[_*Rule*_][_*Python example*_]
+
+  #for (k, abs-rule) in abs-typ-rules.pairs() {
+    let py-rule = py-typ-rules.at(k)
+    align(
+      horizon,
+      grid(
+        columns: (auto, 1fr),
+        column-gutter: 1em,
+        align: (left + horizon, right + horizon),
+        prooftree(abs-rule),
+        py-rule
+      )
+    )
+  }
+]