HEL/TB-Docs
1
0
Fork 0
Code Issues Pull Requests Releases Activity

feat(report): write Midas lexer and parser

Browse Source
This commit is contained in:
Louis Heredero
2026-07-16 12:33:16 +02:00
parent e6c8689ae8
commit a8c63d502e
9 changed files with 373 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
meta.typ
View File

@@ -7,6 +7,7 @@
#let thesis-expert = "Dr Sébastien Doeraene"
#let thesis-id = "ISC-ID-26-8"
#let project-repos = "https://git.kb28.ch/HEL/midas"
#let mirror-repo = "https://github.com/LordBaryhobal/midas"
#let school = "Haute École d'Ingénierie de Sion"
#let programme = "Informatique et systèmes de communication (ISC)"

1
report/acronyms.typ
View File

@@ -3,6 +3,7 @@
#let acronyms = (
"TaPL": ([Types and Progamming Languages@tapl],),
"LSP": (link("https://en.wikipedia.org/wiki/Liskov_substitution_principle")[Liskov substitution principle],),
"AST": ([Abstract Syntax Tree],)
)
#init-acronyms(acronyms)

233
report/appendices/midas_parsing.typ Normal file
View File

@@ -0,0 +1,233 @@
#import "@preview/acrostiche:0.7.0": acr
#import "@local/codly:1.3.1": codly-disable, codly-enable
#let token-types = (
"Punctuation": (
"LEFT_PAREN",
"RIGHT_PAREN",
"LEFT_BRACKET",
"RIGHT_BRACKET",
"LEFT_BRACE",
"RIGHT_BRACE",
"COLON",
"COMMA",
"UNDERSCORE",
"ARROW",
"AND",
"QMARK",
"DOT",
),
"Operators": (
"PLUS",
"MINUS",
"STAR",
"SLASH",
"GREATER",
"GREATER_EQUAL",
"LESS",
"LESS_EQUAL",
"EQUAL",
"EQUAL_EQUAL",
"BANG_EQUAL",
"BANG",
),
"Literals": (
"IDENTIFIER",
"NUMBER",
"TRUE",
"FALSE",
"NONE",
"STRING",
),
"Keywords": (
"TYPE",
"ALIAS",
"PREDICATE",
"EXTEND",
"WHERE",
"PROP",
"DEF",
"FUNC",
),
"Misc": (
"COMMENT",
"WHITESPACE",
"EOF",
"NEWLINE",
),
)
#let token-types-cells = {
let cells = ()
for (category, types) in token-types.pairs() {
cells.push([*#category*])
cells += types
}
// Transpose
let per-col = calc.ceil(cells.len() / 4)
let total = per-col * 4
cells = (cells + (none,) * (total - cells.len())).chunks(per-col)
cells = cells.first().zip(..cells.slice(1)).flatten()
cells
}
#let ast-nodes = (
("Other classes", none, ```python
class TypeParam:
location: Location
name: Token
bound: Optional[Type]
class MemberKind(Enum):
PROPERTY = auto()
METHOD = auto()
class ParamSpec:
l_paren: Token
pos: list[FunctionType.Parameter]
mixed: list[FunctionType.Parameter]
kw: list[FunctionType.Parameter]
```),
("Statements", `Stmt`, ```python
class TypeStmt:
name: Token
params: list[TypeParam]
type: Type
class AliasStmt:
name: Token
type: Type
class MemberStmt:
name: Token
type: Type
kind: MemberKind
class ExtendStmt:
name: Token
params: list[TypeParam]
members: list[MemberStmt]
class PredicateStmt:
name: Token
params: list[ParamSpec]
body: Expr
```),
("Expressions", `Expr`, ```python
class LogicalExpr:
left: Expr
operator: Token
right: Expr
class BinaryExpr:
left: Expr
operator: Token
right: Expr
class UnaryExpr:
operator: Token
right: Expr
class CallExpr:
callee: Expr
arguments: list[Expr]
keywords: dict[str, Expr]
class GetExpr:
expr: Expr
name: Token
class VariableExpr:
name: Token
class GroupingExpr:
expr: Expr
class LiteralExpr:
value: Any
class WildcardExpr:
token: Token
```),
("Types", `Type`, ```python
class NamedType:
name: Token
class GenericType:
type: Type
args: list[Type]
class ConstraintType:
type: Type
constraint: Expr
class FunctionType:
params: ParamSpec
returns: Type
class Parameter:
location: Optional[Location] = None
name: Optional[Token]
type: Type
required: bool
class FrameType:
columns: list[Column]
class Column:
location: Optional[Location] = None
name: Token
type: Type
```),
)
#let format-ast-nodes(name, base-cls, code) = {
let nodes = code.text.split(regex(`\n\nclass`.text)).map(n => if n.starts-with("class") {n} else {"class" + n})
let cells = nodes.map(n => raw(n, block: true, lang: "python"))
align(center)[*#name*]
if base-cls != none [Base class: #base-cls]
codly-disable()
grid(
columns: 3,
column-gutter: 1fr,
row-gutter: 1em,
align: left + top,
..cells
)
codly-enable()
}
#let midas-ast-nodes = stack(
dir: ttb,
spacing: 2em,
..ast-nodes.map(nodes => format-ast-nodes(..nodes))
)
#figure(
grid(
columns: 4,
column-gutter: 3em,
inset: .5em,
..token-types-cells,
),
caption: [Midas Token Types],
kind: table,
supplement: [Table],
) <tab:token-types>
#figure(
midas-ast-nodes,
caption: [Midas #acr("AST") Nodes],
kind: table,
supplement: [Table],
) <tab:midas-ast-nodes>

6
report/bachelor_thesis.typ
View File

@@ -134,6 +134,8 @@ You can also change the order or the names of the sections, for instance, if you
#set heading(numbering: "A.1", supplement: [Appendix])
#set figure(numbering: (..nums) => counter(heading).display("A.1") + "." + numbering("1", ..nums))
// Table of acronyms (optional). Defined near the acronyms above.
#acronym-table()
@@ -166,3 +168,7 @@ You can also change the order or the names of the sections, for instance, if you
= Function Subtyping Rules <app:function-subtyping>
#include-offset("appendices/function_subtyping.typ")
= Midas Language Objects
#include-offset("appendices/midas_parsing.typ")

36
report/bibliography.bib
View File

@@ -35,22 +35,22 @@
url={https://api.semanticscholar.org/CorpusID:1398902}
}
@book{Nystrom:2021:Crafting,
added-at = {2025-04-07T18:48:41.000+0200},
author = {Nystrom, Robert},
biburl = {https://www.bibsonomy.org/bibtex/277c8c518a2426a59a8e4c3a720e60d23/gron},
@Book{Nystrom2021,
author = {Nystrom, Robert},
title = {{Crafting Interpreters}},
year = {2021},
publisher = {Genever Benning},
isbn = {978-0990582946},
pagetotal = {640},
url = {https://craftinginterpreters.com/},
added-at = {2025-04-07T18:48:41.000+0200},
biburl = {https://www.bibsonomy.org/bibtex/277c8c518a2426a59a8e4c3a720e60d23/gron},
interhash = {98f889463df208a828c08042cd116e94},
intrahash = {77c8c518a2426a59a8e4c3a720e60d23},
isbn = {978-0990582939},
keywords = {AST Book Bytecode Interpreters Visitor},
month = {July},
pages = 639,
publisher = {Genever Benning},
timestamp = {2025-04-07T18:49:46.000+0200},
title = {{Crafting Interpreters}},
url = {https://craftinginterpreters.com/},
year = 2021
}
keywords = {AST Book Bytecode Interpreters Visitor},
month = {July},
timestamp = {2025-04-07T18:49:46.000+0200},
}
@Book{Householder1951,
author = {Householder, Alston S.},
@@ -99,4 +99,12 @@
url = {https://llis.nasa.gov/lesson/641},
}
@Online{Pebble,
author = {Louis Heredero},
title = {Pebble},
year = {2026},
url = {https://git.kb28.ch/HEL/pebble},
language = {en},
}
@Comment{jabref-meta: databaseType:biblatex;}

12
report/chapters/04_implementation.typ
View File

@@ -1,15 +1,25 @@
#import "../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: todo
#import "../utils.typ": include-offset
#import "@preview/acrostiche:0.7.0": acr
#import "@preview/gentle-clues:1.3.1" as gc
#import "../../meta.typ"
= 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.
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 #acr("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.
#gc.info[
This chapter contains many references to the project's source code, which is available in the repository at #link(meta.project-repos).\
Additionally, a mirror is also available on GitHub at #link(meta.mirror-repo).
]
#pagebreak()
#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"))

3
report/chapters/04_implementation/01_overview.typ
View File

@@ -1,6 +1,7 @@
#import "../../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: todo
#import "../../figs/architecture.typ"
#import "@preview/acrostiche:0.7.0": acr
= Architecture Overview <sec:impl-overview>
@@ -17,7 +18,7 @@ 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.
/ Generator: Take in a Python #acr("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.

75
report/chapters/04_implementation/02_midas_language.typ
View File

@@ -1,8 +1,83 @@
#import "../../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: todo
#import "../../utils.typ": fn-link, code-ref
#import "@preview/acrostiche:0.7.0": acr
= Midas Definition Processing <sec:impl-midas>
For maximum flexibility and control over the whole process, it has been chosen to implement a custom parser for the Midas language from scratch. Moreover, the student already had some experience in implementing a parser and interpreter. Thus, most of the lexer and parser logic implemented in this section has been adapted from the student's previous #fn-link(<pebble-fn>, "https://git.kb28.ch/HEL/pebble")[pebble] project, which is itself based on the wonderful _Crafting Interpreters_ by Robert Nystrom@Nystrom2021.
Processing a Midas definitions file is done in 3 steps:
+ lexing, i.e. turning raw text bytes into tokens
+ parsing, i.e. assembling tokens into an #acr("AST") according to syntax rules defined in @sec:theory-syntax-midas (and @app:midas-syntax)
+ typing, i.e. processing each statement, registering types and predicates in the registry
Each of these steps map to a dedicated class, respectively `MidasLexer`, `MidasParser` and `MidasTyper`.
== Lexing and parsing
The lexer and parser follow the structure presented by Nystrom@Nystrom2021 and implemented in #fn-link(<pebble-fn>, "https://git.kb28.ch/HEL/pebble")[pebble]@Pebble.
Concretely, the lexer scans the source code character by character and produces tokens. Several token types are defined to cover all needs in Midas, such as operators, identifiers, keywords and punctuation. The full list of token types is included in @tab:token-types. Whitespace and comments are also converted to tokens but are ignored by the parser. Each token, as represented by the class shown in @fig:token-class, has a token type, a lexeme (i.e. the raw characters making up that token) and a position. That position is crucial for reporting diagnostics as it allows precisely showing the user where an error is in the source file. Tokens representing literals also contain their literal value, like strings, numbers and constants.
#figure(
```python
class Token:
type: TokenType
lexeme: str
value: Any
position: Position
class Position:
file: Optional[str]
line: int
column: int
```,
caption: [`Token` and `Position` classes]
) <fig:token-class>
`MidasLexer` has a simple constructor, taking in a source code string and optional file path, and a concise `process` method returning a list of tokens, as shown in @fig:lexer-signatures.
#figure(
```python
class MidasLexer:
def __init__(self, source: str, file: Optional[str] = None) -> None: ...
def process(self) -> list[Token]: ...
```,
caption: [Constructor and main method signatures of `MidasLexer`]
) <fig:lexer-signatures>
The parser receives this list of tokens and produces a sequence of statements. All #acr("AST") nodes are defined using frozen dataclasses, which are similar to Java's records. Like Nystrom's implementation, #acr("AST") classes are generated from a template using a script. This script also generates a visitor interface including methods for each node type. The script is available in the repository in #code-ref(<gen-script>, "gen/gen.py").
The Midas language uses three kinds of nodes:
- Statements (`Stmt`): top-level constructs introduced by keywords, have side-effects in the registry
- Expressions (`Expr`): composable building blocks for constraint expressions
- Types (`Type`): type constructors and references
The full list of #acr("AST") nodes used for Midas is available in @tab:midas-ast-nodes and their concrete implementation in the repository in #code-ref(<midas-ast>, "midas/ast/midas.py").
Like tokens, each node also keeps track of its location. The location object contains a starting position and an optional ending position, given by the starting and end token covered by the node. @fig:node-location shows the simple dataclass that is used to hold this information.
#figure(
```python
class Location:
lineno: int
col_offset: int
end_lineno: Optional[int]
end_col_offset: Optional[int]
```,
caption: [#acr("AST") node location class]
) <fig:node-location>
The complete implementations of `MidasLexer` and `MidasParser` are available in the project's repository in the following files:
- `MidasLexer`: #code-ref(<midas-lexer>, "midas/lexer/midas.py")
- `Lexer` (base class): #code-ref(<lexer>, "midas/lexer/base.py")
- `MidasParser`: #code-ref(<midas-parser>, "midas/parser/midas.py")
- `Parser` (base class): #code-ref(<parser>, "midas/parser/base.py")
== Processing statements
/*
- Midas definition language
- Lexer + parser (Crafting Interpreters, Pebble)

22
report/utils.typ
View File

@@ -18,4 +18,26 @@
)
)
)
}
#let _fn-links = state("_fn-links", ())
#let fn-link(lbl, url, body) = context {
link(url, body)
let links = _fn-links.get()
let name = str(lbl)
if name in links {
footnote(lbl)
} else {
[#footnote(link(url)) #lbl]
_fn-links.update(links => links + (name,))
}
}
#let code-ref(lbl, path, body: auto) = {
if body == auto {
body = path
}
let url = "https://git.kb28.ch/HEL/midas/src/branch/main/" + path
fn-link(lbl, url, body)
}