feat(journal): update week 7

admin/planning.typ

@@ -1,6 +1,6 @@
 #set text(font: "Source Sans 3")
 
-= General Planning
+= Initial Planning
 
 #table(
   columns: (auto, 1fr),
@@ -16,3 +16,20 @@
   [*8*],
   [*9*],
 )
+
+= History
+
+#table(
+  columns: (auto, 1fr),
+  align: (center, left + horizon),
+  table.header[*Week*][*Objectives*],
+  [*1*], [Kickoff, setup project, start prototyping a syntax],
+  [*2*], [Syntax prototype, simple parser],
+  [*3*], [Basic type checker (assignments, functions, operations)],
+  [*4*], [Diagnostics, type check control flow, refine architecture, subtyping],
+  [*5*], [Generic types, methods and overloads, simple code generator],
+  [*6*], [For loops, generate assertions, generate stubs, constraints, variance, type unification],
+  [*7*], [],
+  [*8*], [],
+  [*9*], [],
+)

design/calculus_rules.typ

@@ -0,0 +1,262 @@
+#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,
+        )
+      )
+    )
+  }
+]

halfway-presentation/langs.typ

@@ -4,16 +4,21 @@
     title: "Midas: mieux typer Python",
     subtitle: "Présentation intermédiaire",
     short-title: "Midas",
+    supervisor: "Superviseure",
     "context": "Contexte",
     problematic: "Problématique",
     case-1: [Cas 1 -- Type != sémantique],
     case-2: [Cas 2 -- Erreur de type _at runtime_],
     goal: "Objectif",
     gradual-typing: [Typage graduel (_gradual typing_)],
-    static-type-checking: [Vérification statique],
+    optional-typing: "Typage optionnel",
+    static-type-checking: "Vérification statique",
+    dynamic-checks: "Vérificiations dynamiques",
     runtime-assertions: [Assertions _at runtime_],
+    value-constraints: "Contraintes de valeur",
     example: "Exemple",
     lat-lon-error: "Invalide, même si float+float est valide",
+    planning: "Planification",
     initial-planning: "Planification initiale",
     week: "Semaine",
     objectives: "Objectifs",
@@ -40,16 +45,21 @@
     title: "Midas: better type checking in Python",
     subtitle: "Halfway presentation",
     short-title: "Midas",
+    supervisor: "Supervisor",
     "context": "Context",
     problematic: "Problematic",
     case-1: [Case 1 -- Type != semantic],
     case-2: [Case 2 -- Runtime type error],
     goal: "Goal",
     gradual-typing: "Gradual typing",
+    optional-typing: "Optional typing",
     static-type-checking: "Static type checking",
+    dynamic-checks: "Dynamic checks",
     runtime-assertions: "Runtime assertions",
+    value-constraints: "Value constraints",
     example: "Example",
     lat-lon-error: "Invalid, even though float+float is valid",
+    planning: "Planning",
     initial-planning: "Initial planning",
     week: "Week",
     objectives: "Objectives",

halfway-presentation/main.typ

@@ -2,7 +2,9 @@
 #import "@preview/touying-unistra-pristine:1.4.3": *
 #import "@preview/codly:1.3.0": codly, codly-init
 #import "@preview/codly-languages:0.1.10": codly-languages
+#import "@preview/cetz:0.5.2": canvas, draw
 #import "langs.typ": i18n, i18n-date
+#import "utils.typ": title-slide
 
 #let langs = (
   fr: ("fr", "ch"),
@@ -74,9 +76,27 @@
 )
 
 #title-slide(
-  logo: image("logo_white.svg", height: 3em)
+  logo: image("logo_white.svg", height: 3em),
+  extra-body: place(
+    bottom + right,
+    dx: -2em,
+    dy: -2em
+  )[
+    #text(
+      fill: white,
+      weight: "bold"
+    )[#i18n("supervisor"): Dr D. Racordon]
+  ]
 )
 
+
+#focus-slide(
+  theme: "pink",
+  show-counter: false,
+)[
+  #i18n("context")
+]
+
 == #i18n("context")
 
 ==== #i18n("case-1")
@@ -84,13 +104,15 @@
 #[
 #set text(size: .8em)
 ```python
-df = pd.read_csv()
+df = pd.read_csv(...)
 value = df["distance"] / df["time"]
 ...
 value += df["age"]
 ```
 ]
 
+#pause
+
 ==== #i18n("case-2")
 
 #[
@@ -105,10 +127,12 @@ TypeError: unsupported operand type(s) for +: 'int' and 'NoneType'
 == #i18n("goal")
 
 - #i18n("gradual-typing")
-
-- #i18n("static-type-checking")
+  - #i18n("optional-typing")
+  - #i18n("static-type-checking")
+  - #i18n("dynamic-checks")
 
 - #i18n("runtime-assertions")
+  - #i18n("value-constraints")
 
 
 #let wah = place(
@@ -137,7 +161,7 @@ df: Frame[
     birth_date: date,
     height: float & (0 < _ < 250),
     name: Optional[str],
-    home: GeoLocation,
+    home: GeoCoordinate,
 ] = pd.read_csv(...)
 lat = df["home"].lat
 lon = df["home"].lon
@@ -145,6 +169,11 @@ invalid = lat + lon  # [[lat-lon-error]]
 ```
 ]
 
+#focus-slide(
+  theme: "yellow",
+  show-counter: false
+)[#i18n("planning")]
+
 == #i18n("initial-planning")
 
 #table(
@@ -181,6 +210,11 @@ invalid = lat + lon  # [[lat-lon-error]]
   [*9*],
 )
 
+#focus-slide(
+  theme: "neon",
+  show-counter: false
+)[#i18n("demo")]
+
 == #i18n("demo")
 
 === #i18n("def-custom-types")
@@ -217,3 +251,9 @@ speed += time  # [[invalid]]
 ```
 ]
 
+#focus-slide(
+  theme: "mandarine",
+  show-counter: false,
+)[
+  Questions ?
+]

halfway-presentation/utils.typ

@@ -0,0 +1,100 @@
+#import "@preview/touying:0.6.2": *
+#import "@preview/touying-unistra-pristine:1.4.3": *
+
+// Redefine to allow extra-body
+#let title-slide(
+  title: "",
+  subtitle: "",
+  logo: "",
+  logos: (),
+  hide: (),
+  extra-body: [],
+  ..args,
+) = touying-slide-wrapper(self => {
+  let info = self.info + args.named()
+
+  let nb-logos = logos.len()
+
+  if logo != "" and nb-logos > 0 {
+    panic("'logo' and 'logos' cannot be set at the same time.")
+  }
+
+  let logo-body = none
+  if nb-logos == 0 {
+    logo-body = logo
+  } else {
+    logo-body = grid(
+      columns: if nb-logos > 0 {
+        nb-logos
+      } else {
+        1
+      },
+      ..(logos).map(logo => logo),
+    )
+  }
+
+  let body = {
+    set text(fill: white)
+    set block(inset: 0mm, outset: 0mm, spacing: 0em)
+    set align(top + left)
+    _gradientize(
+      self,
+      block(
+        fill: none,
+        width: 100%,
+        height: 100%,
+        inset: (left: 2em, top: 1em),
+        grid(
+          columns: 1fr,
+          rows: (6em, 6em, 4em, 4em),
+          logo-body,
+          _cell([
+            #text(size: 2em, weight: "bold", if (title != "") {
+              title
+            } else {
+              info.title
+            })
+            #linebreak()
+            #text(size: 1.7em, weight: "regular", if (subtitle != "") {
+              subtitle
+            } else {
+              info.subtitle
+            })
+          ]),
+
+          _cell([
+            #if ((none, "").all(x => x != info.subtitle)) {
+              linebreak()
+            }
+            #set text(size: 1.5em, fill: self.colors.white)
+            #text(weight: "bold", info.author)
+            #if "email" in info {
+              linebreak()
+              text(info.email, size: 0.8em)
+            }
+          ]),
+          if "date" not in hide {
+            _cell([
+              #set text(fill: self.colors.white.transparentize(25%))
+              #utils.display-info-date(self)
+            ])
+          },
+        ),
+      ),
+      c1: self.colors.nblue.E,
+      c2: self.colors.cyan.E,
+    )
+  }
+
+  self = utils.merge-dicts(
+    self,
+    config-common(freeze-slide-counter: true),
+    config-page(margin: 0em),
+    config-common(subslide-preamble: none),
+  )
+
+  touying-slide(
+    self: self,
+    body + extra-body,
+  )
+})

journal/week4.typ

@@ -14,3 +14,26 @@
 - Read TAPL (22)
 - Rework abstract types
 - Generalize syntax (more modularity for generics, unions, constraints, etc.)
+- Weekly meeting
+
+#day(3)
+
+- Halfway presentations
+- Define formal syntax and typing rules
+
+#day(5)
+
+- Work on formal rules
+- Update syntax definition (EBNF + railroad diagrams)
+- Add usage documentation
+- Implement subtyping
+
+#day(6)
+
+- Implement subtyping
+
+#day(7)
+
+- Implement subtyping
+- Implement attribute reference and assignments
+- Improve diagnostics in CLI

journal/week5.typ

@@ -0,0 +1,44 @@
+#import "template.typ": week, day
+
+#show: week.with(num: 5)
+
+#day(1)
+
+- Implement generics
+- Refactor type checker
+- Create demo program
+
+#day(2)
+
+- Define formal calculus rules
+- Add type params to extend block
+
+#day(3)
+
+- Rework extend block for methods
+  - Goal: allow defining any method on types
+  - Issues:
+    - `GetExpr` can reference either a property on a `ComplexType` or a method.
+    - A method (or function) can be overloaded, for example ```py list[T].__getitem__(int) -> T``` and ```py list[T].__getitem__(slice) -> list[T]```
+
+#day(4)
+
+- Rework complex types: extension type, combine properties and methods as members
+
+#day(5)
+
+- Implement member lookup
+- Adapt operations
+- Handle generic members
+
+#day(6)
+
+- Redefine builtins with members
+- Tidy up
+- Add unary operations and subscripts
+
+#day(7)
+
+- Resolve overloaded functions
+- Add slices
+- Add simple code generator

journal/week6.typ

@@ -0,0 +1,40 @@
+#import "template.typ": week, day
+
+#show: week.with(num: 6)
+
+#day(1)
+
+- Simple code generator
+- Redesign CLI
+    - Split overloaded command into multiple simple commands
+    - Add some commands
+- Add for loops
+- Start implementing cast assertions
+
+#day(2)
+
+- Weekly meeting
+- Forward raw unhandled Python statements and expressions
+- Generate cast assertions (type)
+- Add generator tests
+
+#day(3)
+
+- Generate stubs from Midas definitions
+
+#day(4)
+
+- Generate predicate functions
+
+#day(5)
+
+- Type check predicate body
+
+#day(6)
+
+- Add variance to type variables (infer, use in subtype check, integrate in generated stubs)
+- Unify / match types in generic function calls
+
+#day(7)
+
+- Unify / match types in generic function calls

journal/week7.typ

@@ -0,0 +1,21 @@
+#import "template.typ": week, day
+
+#show: week.with(num: 7)
+
+#day(1)
+
+- better handle type variables
+- write simple demo script
+- various fixes
+
+#day(2)
+
+- weekly meeting
+- start implementing data-frame and column types
+
+#day(3)
+
+- statically check cast expressions on literal values
+- add unsafe cast
+- setup user manual
+- setup report