feat(design): add statement typing rules

design/calculus_rules.typ

@@ -30,36 +30,42 @@
     column-gutter: .4em,
     row-gutter: 1em,
     $"t"$, $::=$, none, [_terms_],
-    blank(13, 2),
+    blank(11, 2),
     $"x"$, [_variable_],
     $"i"$, [_integer literal_],
     $"f"$, [_float literal_],
-    $"s"$, [_string literal_],
+    $"z"$, [_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_],
+    $"s"; "t"$, [_sequence_],
     grid.cell(colspan: 4)[],
+
     $"v"$, $::=$, none, [_values_],
-    blank(10, 2),
+    blank(6, 2),
     $"i"$, [_integer literal_],
     $"f"$, [_float literal_],
-    $"s"$, [_string literal_],
+    $"z"$, [_string literal_],
     $"True"$, [_constant true_],
     $"False"$, [_constant false_],
     $"None"$, [_constant none_],
+    grid.cell(colspan: 4)[],
+
+    $"s"$, $::=$, none, [_statements_],
+    blank(3, 2),
+    $"x" = "t"$, [_assignment_],
+    $"x": "T"$, [_variable declaration_],
+    $#syntax[def] f("x": "T") -> "T": "t"$, [_def_],
   )
 ]
 
 #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)]),
+  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)]),
@@ -69,8 +75,8 @@
     name: [(T-Var)]
   ),
   def: rule(
-    $Gamma, "x": "T"_1 tack "t" -> "T"_2$,
+    $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 : space "T"_1 -> "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(
@@ -89,9 +95,20 @@
   op: rule(
     $Gamma tack "t"_1: "T"_1$,
     $Gamma tack "t"_2: "T"_2$,
-    $"op": T_1 -> T_2 -> T_3 in Gamma$,
+    $"op": "T"_1 -> "T"_2 -> "T"_3 in Gamma$,
-    $Gamma tack "t"_1 "op" "t"_2: "T"_3$
+    $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)]
+  ),
 )
 
 #let py-typ-rules = (
@@ -101,7 +118,7 @@
   "true": ```py True: bool```,
   "false": ```py False: bool```,
   "none": ```py None: None```,
-  var: ```py x: T```,
+  var: ```py x```,
   def: ```py
     def func(a: S) -> T:
       return ...: T
@@ -112,23 +129,61 @@
     func(a: S): T
   ```,
   ternary: ```py (true if cond else false): T ```,
-  op: ```py (a + b): T```
+  op: ```py (a + b): T```,
+  annot: ```py x: T```,
+)
+
+#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
+  ]
 )
 
 #mk-box[Typing][
   #v(1em)
   #stack(dir: ltr, spacing: 1fr)[_*Rule*_][_*Python example*_]
 
-  #for (k, abs-rule) in abs-typ-rules.pairs() {
+  #for (i, (k, abs-rule)) in abs-typ-rules.pairs().enumerate() {
-    let py-rule = py-typ-rules.at(k)
+    let py-rule = py-typ-rules.at(k, default: none)
-    align(
+    let reading-key = reading-keys.at(k, default: none)
-      horizon,
+    let cells = (
-      grid(
+      prooftree(abs-rule),
-        columns: (auto, 1fr),
+      py-rule
-        column-gutter: 1em,
+    )
-        align: (left + horizon, right + horizon),
+    if reading-key != none {
-        prooftree(abs-rule),
+      cells.push(
-        py-rule
+        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,
+        )
       )
     )
   }