refactor(report): move theory to separate chapter

report/bachelor_thesis.typ

@@ -100,9 +100,10 @@ You can also change the order or the names of the sections, for instance, if you
 
 #include "chapters/01_introduction.typ"
 #include "chapters/02_state_of_the_art.typ"
-#include "chapters/03_development.typ"
+#include "chapters/03_theory.typ"
-#include "chapters/04_results_discussion.typ"
+#include "chapters/04_implementation.typ"
-#include "chapters/05_conclusion.typ"
+#include "chapters/05_results_discussion.typ"
+#include "chapters/06_conclusion.typ"
 
 #pagebreak()
 

report/bibliography.bib

@@ -52,15 +52,16 @@
   year = 2021
 }
 
-@book{Householder1951,
+@Book{Householder1951,
   author    = {Householder, Alston S.},
   title     = {Monte Carlo Method},
+  year      = {1951},
   series    = {Applied Mathematics Series},
   number    = {12},
+  note      = {Proceedings of a symposium held June 29, 30, and July 1, 1949},
   publisher = {U.S. Department of Commerce, National Bureau of Standards},
-  year = {1951},
+  pages     = {36},
   address   = {Washington, D.C.},
-  note = {Proceedings of a symposium held June 29, 30, and July 1, 1949}
 }
 
 @Online{HOPL,

report/chapters/01_introduction.typ

@@ -2,7 +2,7 @@
 #import isc-hei-bthesis: todo
 #import "../utils.typ": quote-block
 
-= Introduction
+= Introduction <chap:intro>
 
 #quote-block[J. von Neumann @Householder1951][
   Any one who considers arithmetical methods of producing random digits is, of course, in a state of sin

report/chapters/02_state_of_the_art.typ

@@ -1,4 +1,21 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
 
-= State of the Art
+= State of the Art <chap:state-of-the-art>
+
+
+/*
+- Python type hints (https://peps.python.org/pep-0484/):
+  - base types
+  - type aliases
+  - structural subtyping with Protocols -> matches duck-typing (https://peps.python.org/pep-0544/)
+
+- Existing type checkers
+  - MyPy / Pyright
+
+- Existing libraries
+  - Pandera: runtime only, syntax heavy, but quite complete
+
+- Similar ideas
+  - Gator system (https://capra.cs.cornell.edu/research/gator/)
+*/

report/chapters/03_development.typ

@@ -1,8 +0,0 @@
-#import "../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-#import "../utils.typ": include-offset
-
-= Development and Methodology
-
-#include-offset(path("03_development/01_theory.typ"))
-#include-offset(path("03_development/02_implementation.typ"))

report/chapters/03_development/01_theory.typ

@@ -1,4 +0,0 @@
-#import "../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-
-= Underlying Theory and Typing Rules

report/chapters/03_development/02_implementation.typ

@@ -1,10 +0,0 @@
-#import "../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-#import "../../utils.typ": include-offset
-
-= Implementation
-
-#include-offset(path("02_implementation/01_overview.typ"))
-#include-offset(path("02_implementation/02_midas_language.typ"))
-#include-offset(path("02_implementation/03_python_checking.typ"))
-#include-offset(path("02_implementation/04_generation.typ"))

report/chapters/03_development/02_implementation/01_overview.typ

@@ -1,4 +0,0 @@
-#import "../../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-
-= Architecture Overview

report/chapters/03_development/02_implementation/02_midas_language.typ

@@ -1,4 +0,0 @@
-#import "../../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-
-= Midas Definition Processing

report/chapters/03_development/02_implementation/03_python_checking.typ

@@ -1,4 +0,0 @@
-#import "../../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-
-= Python Type Checking

report/chapters/03_development/02_implementation/04_generation.typ

@@ -1,4 +0,0 @@
-#import "../../../requirements.typ": isc-hei-bthesis
-#import isc-hei-bthesis: todo
-
-= Code Generation

report/chapters/03_theory.typ

@@ -0,0 +1,11 @@
+#import "../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+
+= Underlying Theory and Typing Rules <chap:theory>
+
+/*
+- Identify requirements
+- Introduction to TAPL
+- Grammar and typing rules for Midas, paralleled with TAPL
+- Omitted rules, simplifications, mechanisms not implemented
+*/

report/chapters/04_implementation.typ

@@ -0,0 +1,21 @@
+#import "../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+#import "../utils.typ": include-offset
+
+= Implementation <chap:impl>
+
+#include-offset(path("04_implementation/01_overview.typ"))
+#include-offset(path("04_implementation/02_midas_language.typ"))
+#include-offset(path("04_implementation/03_python_checking.typ"))
+#include-offset(path("04_implementation/04_generation.typ"))
+
+/*
+Subjects:
+- Variance inference
+- Environment
+- Resolver
+- Evaluator
+- CallDispatcher
+- Registry (`is_subtype`)
+- MethodRegistry (frames and columns)
+*/

report/chapters/04_implementation/01_overview.typ

@@ -0,0 +1,14 @@
+#import "../../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+
+= Architecture Overview <sec:impl-overview>
+
+/*
+- Main elements
+  - Definition language
+  - Supported Python syntax (cf. grammar and typing rules)
+  - Parse and type check
+  - Produce user-facing diagnostics
+  - Generate runtime assertions
+- Architecture overview
+*/

report/chapters/04_implementation/02_midas_language.typ

@@ -0,0 +1,16 @@
+#import "../../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+
+= Midas Definition Processing <sec:impl-midas>
+
+/*
+- Midas definition language
+  - Lexer + parser (Crafting Interpreters, Pebble)
+    - reference theory for grammar rules
+    - token location -> necessary later for diagnostics
+    - AST node generation, similar to CI (3 kinds, Stmt/Expr/Type)
+  - Typer
+    - reference theory for typing rules
+    - type structures
+    - types registry
+*/

report/chapters/04_implementation/03_python_checking.typ

@@ -0,0 +1,16 @@
+#import "../../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+
+= Python Type Checking <sec:impl-python>
+
+/*
+- Python type checking
+  - Parsing (short paragraph about AST nodes)
+  - Resolver
+    - Cf. CI
+    - Assignment analysis
+  - Typer
+    - Returns / if-else
+    - Environment
+    - Static constraint evaluation
+*/

report/chapters/04_implementation/04_generation.typ

@@ -0,0 +1,10 @@
+#import "../../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+
+= Code Generation <sec:impl-generation>
+
+/*
+- Code generation
+  - Stubs
+  - Assertions
+*/

report/chapters/05_results_discussion.typ

@@ -1,4 +1,4 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
 
-= Conclusion
+= Results and Discussion <chap:results>

report/chapters/06_conclusion.typ

@@ -1,4 +1,4 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
 
-= Results and Discussion
+= Conclusion <chap:conclusion>