Compare commits

..

26 Commits

Author SHA1 Message Date
776a3fb86c fix(checker): change back warning to errors 2026-06-19 22:12:47 +02:00
fcbbff0177 tests: add predicates and constraints test 2026-06-19 22:09:16 +02:00
e2efbf693e fix(checker) minor tweaks 2026-06-19 21:54:13 +02:00
68f83ab6cf feat(parser): parse strings in Midas files 2026-06-19 21:53:35 +02:00
4118f95753 fix(parser): correctly parse keyword arguments 2026-06-19 21:10:59 +02:00
d5972df3f6 fix(checker): handle all operations and calls in predicates 2026-06-19 21:10:33 +02:00
3411aa9953 fix(checker): lookup predicate variables in preamble 2026-06-19 21:09:02 +02:00
7a2ee5a4cc feat(cli): print predicate with dump-registry 2026-06-19 15:06:55 +02:00
359ed21bb8 fix(checker): typo in docstring 2026-06-19 15:05:49 +02:00
d0f1178c17 fix(checker): change some diagnostics to warnings
temporarily change type errors in predicates to warnings until operations are fully type checked
2026-06-19 14:41:43 +02:00
0eca23b894 feat(gen): generate type hints for functions 2026-06-19 14:11:38 +02:00
f664fb4a4f feat(gen): handle predicate aliases
handle cases where a predicate is defined as an alias, i.e. without any parameters
2026-06-19 14:05:34 +02:00
32330243c6 fix(parser): fix call expr location span 2026-06-19 13:57:49 +02:00
96e76065cf feat(types): detect constraint base subtyping 2026-06-19 13:57:21 +02:00
7b7d87e59a feat(checker): type check predicate body 2026-06-19 13:55:32 +02:00
1eb90164e6 fix(gen): remove id from named predicate function 2026-06-19 10:15:09 +02:00
35ec0d0db8 fix(tests): update generator tester 2026-06-18 22:49:08 +02:00
48fcb499a1 feat(gen): generate predicate functions 2026-06-18 22:48:10 +02:00
bdc1b265a6 feat(gen): generate basic constraint assertion 2026-06-18 13:19:17 +02:00
1fb4b6f8c6 feat(types): add ConstraintType 2026-06-18 12:52:39 +02:00
48c1ecc1c8 refactor: ensure exhaustiveness in some match/case 2026-06-18 12:51:28 +02:00
04853eac70 tests: update with new predicate AST representation 2026-06-18 12:43:24 +02:00
020824d1f8 fix(tests): correctly serialize param name 2026-06-18 12:43:02 +02:00
ad86446a2d feat(midas): generalize param spec of predicate and parse 2026-06-18 12:38:24 +02:00
94d84ab170 feat(midas): add CallExpr 2026-06-18 12:34:29 +02:00
8381f4f31d refactor: add param spec for FunctionType 2026-06-18 11:06:02 +02:00

View File

@@ -1,4 +1,4 @@
<h1>Midas</h1>
# Midas
*Midas* is a type system to _Maintain Integrity of Data with Annotated Structures_. In Greek mythology, [Midas](https://en.wikipedia.org/wiki/Midas) was a Phrygian king who was blessed with the gift of turning everything he touched into gold.
@@ -6,24 +6,6 @@
This framework is being developed as part of a Bachelor's Thesis by Louis Heredero at HEI Sion.
<details>
<summary><strong>Table of Contents</strong></summary>
- [Requirements](#requirements)
- [Installation](#installation)
- [Commands](#commands)
- [Type Checking](#type-checking)
- [Compiling](#compiling)
- [Formatting](#formatting)
- [Highlighting](#highlighting)
- [Dumping the AST](#dumping-the-ast)
- [Dumping the Registry](#dumping-the-registry)
- [Showing Type Judgements](#showing-type-judgements)
- [Validating Definitions](#validating-definitions)
- [Tests](#tests)
</details>
## Requirements
- Python 3.11+
@@ -50,49 +32,25 @@ This framework is being developed as part of a Bachelor's Thesis by Louis Herede
## Commands
<!--
check
compile
format
highlight
parse
dump_registry
types
validate
-->
### Type Checking
```shell
midas check -t types.midas source.py
```
This command parses the given files and run the type checkers against the Midas definitions and Python program. Diagnostics are then printed showing warnings and errors.
### Compiling
> [!NOTE]
> In the current state of the project, the `compile` command doesn't generate any runnable code, it only runs the parsers and type checker on the provided files
```shell
midas compile -t types.midas source.py
```
With the `compile` command, you can process a source Python file, with any number of custom type definition files (`-t FILE` option), and the type checker will verify the coherence of your program and generate the runnable code with valid syntax and runtime assertions.
### Formatting
```shell
midas format types.midas
midas format types.midas -o formatted.midas
```
This command parses the given Midas file and outputs a pretty printed file from the AST.
The optional `-l FILE` option lets you produce a highlighted version of the source code showing diagnostics from the type checker (see [Highlighting](#highlighting))
### Highlighting
```shell
midas highlight source.py
midas highlight source.py -o highlighted.html
midas highlight types.midas
midas highlight types.midas -o highlighted.html
midas utils highlight source.py
# or
midas utils highlight types.midas
```
The `highlight` command takes in a source file (Python or Midas), runs the appropriate parser and outputs an HTML file containing the source code with added highlighting. This highlighting takes the form of hoverable annotations showing some of the parsed structures (e.g. a function definition, an assignment, a generic type, etc.)
@@ -102,35 +60,14 @@ The optional `-o FILE` option can be used to specify an output path. By default,
### Dumping the AST
```shell
midas parse source.py
midas parse types.midas
midas utils dump-ast source.py
# or
midas utils dump-ast types.midas
```
For debugging purposes, you can output the AST parsed from a Python or Midas file. For Python files, the `--raw` flags lets you toggle the custom AST parsing. With `--raw`, the raw AST is returned, as produced by the builtin `ast` module. This flag has no effect on Midas files.
For debugging purposes, you can output the AST parsed from a Python or Midas file. For Python files, the `-p` flags lets you toggle the custom AST parsing. Without `-p`, the raw AST is returned, as produced by the builtin `ast` module. This flag has no effect on Midas files.
### Dumping the Registry
```shell
midas dump-registry -t types.midas
```
This command processes the given Midas definitions and dumps the contents of the types registry.
### Showing Type Judgements
```shell
midas types -t types.midas source.py
```
This command type checks the given Python source file and logs all typing judgements made by the type checker.
### Validating Definitions
```shell
midas validate types.midas
```
This command lets you validate a Midas definition file by running the parser and type checker, verifying syntax and references.
The optional `-o FILE` option can be used to specify an output path. By default, the file is printed in stdout (equivalent to `-o -`).
## Tests
@@ -140,7 +77,6 @@ Several snapshot tests are available to assert the good behaviour of the parsers
uv run -m tests.midas run -a
uv run -m tests.python run -a
uv run -m tests.checker run -a
uv run -m tests.generator run -a
```
**Available subcommands:**