feat(report): write implementation intro and overview
This commit is contained in:
@@ -4,6 +4,12 @@
|
||||
|
||||
= Implementation <chap:impl>
|
||||
|
||||
Now that we have chosen a subset of Python to support and some type checking rules, we may start implementing the type checker itself. We will split the implementation into three relatively independent parts: the Midas language (parsing and registering types), type checking Python and the generator (to output runnable code with runtime assertions).
|
||||
|
||||
The Python language has been chosen for implementing the type checker for several reasons. First, the student was already greatly familiar with that language and its environment. Secondly, as stated in the introduction, Python is a highly versatile tool which is particularly good at manipulating data, and is easy to iterate with. Then, the student had already implemented a simple interpreter which could be reused and adapted for Midas, as explained in @sec:impl-midas. Finally, Python already provides an `ast` module in its standard library to parse and unparse Python source code, and manipulate its AST nodes.
|
||||
|
||||
In @sec:impl-overview, we will first look at the whole system from a top-down perspective to locate its components and get a feel of how they connect to each other.
|
||||
|
||||
#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"))
|
||||
|
||||
@@ -1,8 +1,26 @@
|
||||
#import "../../requirements.typ": isc-hei-bthesis
|
||||
#import isc-hei-bthesis: todo
|
||||
#import "../../figs/architecture.typ"
|
||||
|
||||
= Architecture Overview <sec:impl-overview>
|
||||
|
||||
Our type checker is composed of several interdependent elements shown in @fig:architecture. At its core, there is a type registry which holds a list of all registered types. This registry is initialized with builtin types, like `float` and `str`, and can be further populated by user definitions written in the Midas language. Finally, it is used when type checking the Python source code based on the type checking rules we defined in @sec:theory-typing.
|
||||
|
||||
#figure(
|
||||
architecture.overview,
|
||||
caption: [Implementation Architecture Overview],
|
||||
kind: image,
|
||||
supplement: [Figure],
|
||||
) <fig:architecture>
|
||||
|
||||
The different components have the following responsibilities:
|
||||
/ Midas Typer: Take in a Midas definition file or some source code, parse it, process each statement and register new types in the registry. It must also check references between types and provide users with diagnostics in case of errors.
|
||||
/ Python Typer: Take in a Python file or some source code, parse it, walk through each statement and expression, take note of type hints and otherwise infer types if possible, detect any incompatibilities, i.e. type errors and report them to the user.
|
||||
/ Types Registry: Hold a registry of existing types (builtin or user-defined) and predicates, provide a method to check subtyping according to our rules (i.e. `is_subtype(type1, type2)`) and provide some methods to register, lookup and manipulate types.
|
||||
/ Generator: Take in a Python AST, type judgments (i.e. conclusions of the type checker) and the registry to produce new Python code with assertions that check types at runtime where necessary as well as constraint predicates.
|
||||
|
||||
Apart from the types registry, another component will be used across the whole system which is not shown in @fig:architecture: the reporter. The reporter is a simple object that will collect all diagnostics produced at different steps of the process. That includes syntax errors in Midas files, unknown references, type errors and more.
|
||||
|
||||
/*
|
||||
- Main elements
|
||||
- Definition language
|
||||
|
||||
16
report/figs/architecture.typ
Normal file
16
report/figs/architecture.typ
Normal file
@@ -0,0 +1,16 @@
|
||||
#import "@preview/cetz:0.5.2": canvas, draw
|
||||
#import "@preview/fletcher:0.5.8" as fletcher: diagram, node, edge
|
||||
|
||||
#let overview = diagram(
|
||||
node-stroke: .6pt,
|
||||
node-fill: white,
|
||||
node((0, 0), [Midas Typer], name: <midas>),
|
||||
node((1, 0), [Python Typer], name: <python>),
|
||||
node((0.5, 1), [Types Registry], name: <reg>),
|
||||
node((1, 2), [Generator], name: <gen>),
|
||||
edge(<midas>, "d", <reg>, "<|-|>"),
|
||||
edge(<python>, "d", <reg>, "<|-"),
|
||||
edge((<python.south>, 50%, <python.south-east>), "d", <gen>, "-|>"),
|
||||
edge(<reg>, "d", <gen>, "-|>"),
|
||||
node(align(bottom + left)[*Type Checker*], enclose: (<midas>, <python>, <reg>, <gen>), fill: teal.lighten(80%))
|
||||
)
|
||||
Reference in New Issue
Block a user