fix(report): use Ruleset supplement instead of Table

This commit is contained in:
HEL
2026-07-23 20:39:52 +02:00
parent 49ae884b09
commit e73156638b
3 changed files with 23 additions and 20 deletions
+4 -1
View File
@@ -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),
+18 -18
View File
@@ -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.
+1 -1
View File
@@ -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>