fix(report): tweak layout

report/bachelor_thesis.typ

@@ -95,7 +95,10 @@
     show pagebreak: none
     tab(
       title: page-title(i18n(f, "figure-table-title"), mult: 1, top: 0.4em, bottom: 0.4em),
-      target: figure.where(kind: image),
+      target: selector.or(
+        figure.where(kind: image),
+        figure.where(kind: "ruleset"),
+      )
     )
     tab(
       title: page-title(i18n(f, "table-table-title"), mult: 1, top: 0.4em, bottom: 0.4em),

report/chapters/01_introduction.typ

@@ -8,9 +8,7 @@
   Any one who considers arithmetical methods of producing random digits is, of course, in a state of sin
 ]
 
-Dogs are often said to be man's best friends for their unwavering loyalty. As human beings, we thrive on patterns and predictability. On the other hand, our little animal friends can sometimes be irrational and surprise us with their unpredictable behavior. Computers however, these thought-less automatic machines made of metal, would be much better companions.
-
-By their fundamental essence, computers and other similar machines are deterministic. As developers, we simply give them series of instructions, algorithms, functions and other scripts. Their one and only job is to execute our commands, one after the other, sometimes at the same time. An addition is always an addition, a byte is always a byte, and most importantly, a dog is always a dog.
+By their fundamental essence, computers and other similar machines are deterministic. As developers, we simply give them series of instructions, algorithms. Their one and only job is to execute our commands, one after the other, sometimes at the same time. An addition is always an addition, a byte is always a byte.
 
 When programming, developers use formal languages to instruct their devices to do particular tasks. Theses languages are designed to be unambiguous and generally explicit about what they describe. To the machine interpreting that written text, only one meaning is possible. "But", you may say, "sometimes there are bugs when I run my program". Of course, bugs are an inherent part of programming, but not because the machine might not understand you, because you explained it wrongly.
 Errors and bugs are always caused by the human factor of computer science.#footnote[Notable exceptions are of course hardware failures which are a totally separate kind of issue]

report/chapters/03_theory.typ

@@ -65,7 +65,7 @@ The notations for context are as follows:
   [the context extended with the binding of $"t"$ to the type $"T"$],
 ))
 
-Finally, the rules expressed in @sec:theory-syntax are written in the form of theorems using the following mathematical syntaxes:
+Finally, the rules expressed in @sec:theory-typing are written in the form of theorems using the following mathematical syntaxes:
 
 #align(center, grid(
   columns: 2,
@@ -92,8 +92,8 @@ In this section, we define syntax rules for both Python and our type definition
 #figure(
   python-syntax,
   caption: [Python syntax rules],
-  supplement: [Table],
-  kind: table,
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:python-syntax-rules>
 
 Some syntaxes are simplified or omitted from @tab:python-syntax-rules for the sake of conciseness, readability and scope. Indeed, this work's primary focus is not on the theoretical and formal approach to type checking but rather on the concrete application of it to produce a useful tool for developers. For example, function signature in Python are rather complex and flexible, allowing positional-only, keyword-only and mixed parameters, argument sinks, and default values. Expressing this level of flexibility in a formal definition as those presented above is tricky and not necessarily pertinent to this work.
@@ -107,8 +107,8 @@ Our type system includes a dedicated language to define custom types that can be
 #figure(
   midas-syntax,
   caption: [Midas syntax rules],
-  supplement: [Table],
-  kind: table,
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:midas-syntax-rules>
 
 Parameter specifications in function types and predicates are simplified here for conciseness. In actuality, the supported syntax is similar to Python's regarding positional-only, keyword-only and mixed arguments, with the following notable differences:
@@ -137,8 +137,8 @@ First and foremost, we can define elementary typing rules for all literal values
 #figure(
   typing.literals,
   caption: [Typing rules: literals],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-literals>
 
 Other constructs, although not constants, directly map to builtin types. These include literal lists, tuples and dictionaries. Each of these has a corresponding `list[T]`, `tuple` and `dict[K, V]` type. We will not define formal rules in this section regarding these elements, but a more in depth explanation will be given in the implementation of the type checker, in @sec:python-check-literals.
@@ -152,8 +152,8 @@ Apart from literals, developers also need some building blocks to express their
 #figure(
   typing.expressions,
   caption: [Typing rules: expressions],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-expressions>
 
 #smallcaps[T-Var] simply states that a variable can be typed iff it is in the context.
@@ -175,8 +175,8 @@ Finally, expressions can be used in statements, which are special constructs tha
 #figure(
   typing.statements,
   caption: [Typing rules: statements],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-statements>
 
 #smallcaps[T-Annot] is a rule which handles Python type annotations. It states that the type checker must take note of type hints in the context.
@@ -200,8 +200,8 @@ Similarly to some calculi described in #acr("TaPL")@tapl and to allow flexibilit
 #figure(
   typing.subtyping,
   caption: [Typing rules: subtyping base],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-subtyping-base>
 
 The subtyping relationship is by definition both reflective (#smallcaps[S-Refl]) and transitive (#smallcaps[S-Trans]).\
@@ -213,8 +213,8 @@ For constraint types, we will take the simple approach of considering only the b
 #figure(
   typing.subtyping-constraint,
   caption: [Typing rules: subtyping constraint type],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-subtyping-constraint>
 
 Generics are handled using similar rules to the _Bounded quantification (kernel $F_(<:)$)_ calculus presented in #acr("TaPL") Chapter 26@tapl. Additionally, Midas supports implicit variance, which is inferred from the locations in which type parameters are referenced, and is used when checking subtypes of applied generic types. A detailed explanation of variance inference is provided in the corresponding implementation section, @sec:variance-inference.
@@ -224,8 +224,8 @@ Finally, functions in Python are complex types. The general subtyping rule is gi
 #figure(
   typing.subtyping-function,
   caption: [Typing rules: subtyping functions],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-subtyping-function>
 
 === Special Types <sec:theory-special-types>
@@ -237,8 +237,8 @@ In addition to `Any`, we will add a second top type to represent unknowns. When
 #figure(
   typing.subtyping-top,
   caption: [Typing rules: subtyping top types],
-  kind: table,
-  supplement: [Table],
+  kind: "ruleset",
+  supplement: [Ruleset]
 ) <tab:typing-subtyping-top>
 
 The special type `None`, also later referred to as `UnitType`, is used in Midas as a unit type, mapping Python functions' behavior regarding implicit returns.

report/chapters/04_implementation/02_types.typ

@@ -60,6 +60,7 @@ These types are implemented by the classes in @fig:types-generics.
       INVARIANT = "INVARIANT"
       COVARIANT = "COVARIANT"
       CONTRAVARIANT = "CONTRAVARIANT"
+
   class TypeVar:
       name: str
       bound: Optional[Type]
@@ -81,7 +82,7 @@ These types are implemented by the classes in @fig:types-generics.
 As noted in the theory chapter (@chap:theory), functions in Python are complex and highly flexible.
 A function type thus have a parameter specification and a return type. That parameter specification contains three kinds of parameters: positional-only (`pos`), keyword-only (`kw`) and mixed (`mixed`).
 @fig:types-functions shows the implemented structures to handle function types and their parameters.
-For simplicity, each parameter will store both its position and name, as well as its type and a flag indicating whether it is required or not (e.g. parameters with default values are optional). You may notice an additional `unsupported` flag in @fig:types-functions:10, which is added for some dataframe-related methods. More information shall be given in @sec:impl-python #todo[replace ref].
+For simplicity, each parameter will store both its position and name, as well as its type and a flag indicating whether it is required or not (e.g. parameters with default values are optional). You may notice an additional `unsupported` flag in @fig:types-functions:10, which is added for some dataframe-related methods.
 
 Finally, we will also define a structure to hold multiple signatures of an overloaded function because it cannot be represented as a single `Function`. You may also notice that `OverloadedFunction.overloads` does not store a list of `Function` but simply a list of `Type`, in @fig:types-functions:16. This allows the use of generic functions, which are `Function` types wrapped inside a `GenericType`.
 

report/chapters/04_implementation/04_midas_language.typ

@@ -268,10 +268,8 @@ Additionally, if parameters are given, they are processed and transformed into `
       params: list[TypeVar] = self._resolve_type_params(stmt.params)
 
       type: Type = stmt.type.accept(self)
-      if len(params) != 0:
-          type = GenericType(name=name, params=params, body=type)
-      else:
-          type = DerivedType(name=name, type=type)
+      if len(params) != 0: type = GenericType(name=name, params=params, body=type)
+      else:                type = DerivedType(name=name, type=type)
       try:
           self.types.define_type(name, type)
       except ValueError:
@@ -307,7 +305,6 @@ When processing a predicate definition, we first need to gather all parameters a
               self._predicate_params[param.name.lexeme] = param.type.accept(self)
       type: Type = self.type_of(stmt.body)
       params: list[ParamSpec] = [self._visit_param_spec(spec) for spec in stmt.params]
-
       if not self._is_valid_predicate(type):
           self.reporter.error(
               stmt.body.location,
@@ -413,7 +410,9 @@ By polarity, we mean that:
 - any _producer_ position, such as a function return type, is considered *positive*
 - any _consumer_ position, such as a function parameter, is considered *negative*
 
-Algorithmically, when inferring the variance of a variable, we start at the root generic type with a positive polarity. The inference function identifies all possible positions (type body and members) and recurses with the current polarity multiplied by the position's polarity. For example, if the current polarity is positive and a variable is used in a producer position, the resulting polarity used when recursing is $+ times + = +$. If however the variable is used in a consumer position, the polarity becomes $+ times - = -$. A consumer or negative position basically _flips_ the current polarity. When the recursion reaches the bottom usage, i.e. a simple `TypeVar`, the polarity is recorded.
+Algorithmically, when inferring the variance of a variable, we start at the root generic type with a positive polarity. The inference function identifies all possible positions (type body and members) and recurses with the current polarity multiplied by the position's polarity.
+
+For example, if the current polarity is positive and a variable is used in a producer position, the resulting polarity used when recursing is $+ times + = +$. If however the variable is used in a consumer position, the polarity becomes $+ times - = -$. A consumer or negative position basically _flips_ the current polarity. When the recursion reaches the bottom usage, i.e. a simple `TypeVar`, the polarity is recorded.
 This algorithm is implemented by the `VarianceInferrer` class in @fig:midas-variance-inferrer-walk (omitted parts of the code are listed in @fig:midas-variance-inferrer).
 
 #codly(

report/chapters/04_implementation/05_python_checking.typ

@@ -219,7 +219,6 @@ Similarly to how we handled variable assignments in `if` branches (see @fig:reso
   ```python
   def visit_if_stmt(self, stmt: p.IfStmt) -> None:
       test_type: Type = self.type_of(stmt.test)
-
       if (
           not self.is_subtype(test_type, self.types.get_type("bool"))
           and test_type != UnknownType()
@@ -381,7 +380,7 @@ The simple case where the callee is a `Function` involves matching call-site arg
   caption: [Call Dispatcher: call to `Function`]
 ) <fig:dispatcher-match-func>
 
-Some other simple cases mentioned above can be handled with recursion. Calls to `UnknownType` are also allowed by the type checker, only resulting in an `UnknownType` too. These form the three simple match-cases in @fig:dispatcher-match-simple.
+Some other simple cases mentioned above can be handled with recursion, as in @fig:dispatcher-match-simple. Calls to `UnknownType` are also allowed by the type checker, only resulting in an `UnknownType` too.
 
 #codly(
   range: (25, 34),

report/chapters/05_results_discussion.typ

@@ -18,7 +18,7 @@ This is more than enough to make Midas usable in a wide range of contexts, inclu
 
 == Weather Pipeline Example <sec:results-pipeline>
 
-As an example, we will consider a sample weather-data transformation pipeline as shown in @app:example-pipeline (specifically @fig:example-pipeline-types and @fig:example-pipeline-code), also available in the repository in #code-ref(<example-pipeline>, "examples/02_demonstration/weather/").
+As an example, we will consider a sample weather-data transformation pipeline as shown in @app:example-pipeline (@fig:example-pipeline-types and @fig:example-pipeline-code), also available in the repository in #code-ref(<example-pipeline>, "examples/02_demonstration/weather/").
 
 === Domain Specific Types <sec:pipeline-types>