Compare commits
4
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
9f3c8b96e9
|
||
|
|
a195893c0e
|
||
|
|
6575ae525e
|
||
|
|
24b5f796af
|
@@ -1,5 +1,7 @@
|
|||||||
<h1>Midas</h1>
|
<h1>Midas</h1>
|
||||||
|
|
||||||
|
<img src="https://git.kb28.ch/HEL/midas/actions/workflows/tests.yaml/badge.svg">
|
||||||
|
|
||||||
*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.
|
*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.
|
||||||
|
|
||||||
*Midas* aims at providing Python developers with a simple annotation system to enable compile-time integrity and data type checks, as well as generating runtime assertions.
|
*Midas* aims at providing Python developers with a simple annotation system to enable compile-time integrity and data type checks, as well as generating runtime assertions.
|
||||||
|
|||||||
@@ -1,150 +0,0 @@
|
|||||||
#import "@preview/cetz:0.5.2": canvas, draw
|
|
||||||
|
|
||||||
#let diagram-only = false
|
|
||||||
|
|
||||||
#set document(
|
|
||||||
title: [Midas Architecture],
|
|
||||||
//author: "Louis Heredero",
|
|
||||||
)
|
|
||||||
|
|
||||||
#set text(
|
|
||||||
font: "Source Sans 3",
|
|
||||||
)
|
|
||||||
|
|
||||||
#let diagram = canvas({
|
|
||||||
let framed = draw.content.with(
|
|
||||||
padding: (x: .8em, y: 1em),
|
|
||||||
frame: "rect",
|
|
||||||
stroke: black,
|
|
||||||
)
|
|
||||||
let arrow = draw.line.with(mark: (end: ">", fill: black))
|
|
||||||
framed(
|
|
||||||
(0, 0),
|
|
||||||
name: "python-parser",
|
|
||||||
)[Python parser]
|
|
||||||
|
|
||||||
draw.content(
|
|
||||||
(rel: (0, 1), to: "python-parser.north"),
|
|
||||||
padding: 5pt,
|
|
||||||
anchor: "south",
|
|
||||||
name: "source-py",
|
|
||||||
)[_`source.py`_]
|
|
||||||
arrow("source-py", "python-parser")
|
|
||||||
|
|
||||||
framed(
|
|
||||||
(rel: (3, 0), to: "python-parser.east"),
|
|
||||||
anchor: "west",
|
|
||||||
name: "custom-parser",
|
|
||||||
align(center)[Custom python\ parser],
|
|
||||||
)
|
|
||||||
|
|
||||||
arrow("python-parser", "custom-parser", name: "arrow-python-ast")
|
|
||||||
draw.content(
|
|
||||||
"arrow-python-ast",
|
|
||||||
anchor: "south",
|
|
||||||
padding: 5pt,
|
|
||||||
)[`ast.Module`]
|
|
||||||
|
|
||||||
framed(
|
|
||||||
(rel: (-3, -2), to: "custom-parser.south"),
|
|
||||||
anchor: "east",
|
|
||||||
name: "python-resolver",
|
|
||||||
)[Python Resolver]
|
|
||||||
arrow(
|
|
||||||
"custom-parser",
|
|
||||||
((), "|-", "python-resolver.east"),
|
|
||||||
"python-resolver",
|
|
||||||
name: "arrow-python-custom-ast",
|
|
||||||
)
|
|
||||||
draw.content(
|
|
||||||
(rel: (1.5, 0), to: "arrow-python-custom-ast.end"),
|
|
||||||
padding: 5pt,
|
|
||||||
anchor: "south",
|
|
||||||
)[P-AST#footnote[#strong[P]ython *AST*]<fn-past>]
|
|
||||||
draw.content(
|
|
||||||
"python-resolver.west",
|
|
||||||
padding: 5pt,
|
|
||||||
anchor: "south-east",
|
|
||||||
)[Resolved P-AST@fn-past]
|
|
||||||
|
|
||||||
draw.circle(
|
|
||||||
(rel: (1, -2), to: "custom-parser.south-east"),
|
|
||||||
radius: .4,
|
|
||||||
name: "midas-loader",
|
|
||||||
)
|
|
||||||
arrow(
|
|
||||||
"custom-parser",
|
|
||||||
"midas-loader",
|
|
||||||
name: "arrow-load-midas",
|
|
||||||
mark: (end: (symbol: ">", fill: black), start: "o"),
|
|
||||||
)
|
|
||||||
draw.content(
|
|
||||||
"arrow-load-midas",
|
|
||||||
anchor: "west",
|
|
||||||
padding: 5pt,
|
|
||||||
)[```python midas.using("types.midas")```]
|
|
||||||
|
|
||||||
framed(
|
|
||||||
(rel: (0, -2), to: "midas-loader.south"),
|
|
||||||
name: "midas-parser",
|
|
||||||
)[Midas lexer/parser]
|
|
||||||
arrow("midas-loader", "midas-parser", name: "arrow-midas-source")
|
|
||||||
draw.content(
|
|
||||||
"arrow-midas-source",
|
|
||||||
anchor: "west",
|
|
||||||
padding: 5pt,
|
|
||||||
)[_`types.midas`_]
|
|
||||||
|
|
||||||
|
|
||||||
framed(
|
|
||||||
(rel: (-2, 0), to: "midas-parser.west"),
|
|
||||||
anchor: "east",
|
|
||||||
name: "midas-resolver",
|
|
||||||
)[Midas Resolver]
|
|
||||||
arrow("midas-parser", "midas-resolver", name: "arrow-midas-ast")
|
|
||||||
draw.content(
|
|
||||||
"arrow-midas-ast",
|
|
||||||
anchor: "south",
|
|
||||||
padding: 5pt,
|
|
||||||
)[M-AST#footnote[#strong[M]idas *AST*]<fn-mast>]
|
|
||||||
|
|
||||||
framed(
|
|
||||||
(rel: (-3, 0), to: "midas-resolver.west"),
|
|
||||||
anchor: "east",
|
|
||||||
name: "checker",
|
|
||||||
)[Checker]
|
|
||||||
arrow("midas-resolver", "checker", name: "arrow-type-ctx")
|
|
||||||
arrow(
|
|
||||||
"python-resolver",
|
|
||||||
((), "-|", "checker.north"),
|
|
||||||
"checker",
|
|
||||||
)
|
|
||||||
draw.content(
|
|
||||||
"arrow-type-ctx",
|
|
||||||
anchor: "south",
|
|
||||||
padding: 5pt,
|
|
||||||
)[Types context]
|
|
||||||
})
|
|
||||||
|
|
||||||
#show: doc => if diagram-only {
|
|
||||||
set page(width: auto, height: auto, margin: .5cm)
|
|
||||||
diagram
|
|
||||||
} else { doc }
|
|
||||||
|
|
||||||
#align(center, title())
|
|
||||||
|
|
||||||
#v(1cm)
|
|
||||||
|
|
||||||
#figure(
|
|
||||||
diagram,
|
|
||||||
caption: [Midas type-checker architecture],
|
|
||||||
)
|
|
||||||
|
|
||||||
== Components
|
|
||||||
|
|
||||||
- *Python parser*: builtin Python AST parser, extracts abstract syntax from the raw Python source (```python ast.parse(...)```)
|
|
||||||
- *Custom python parser*: converts the raw Python AST into custom, more suitable constructs, especially for type annotations
|
|
||||||
- *Python resolver*: resolves bindings and references, tracks binding scopes
|
|
||||||
- *Midas lexer/parser*: parses a Midas type definition file and extracts its AST
|
|
||||||
- *Midas resolver*: walks the AST and fills the environment with the defined types and operations
|
|
||||||
- *Checker*: evaluates expressions and checks type coherence
|
|
||||||
@@ -0,0 +1,14 @@
|
|||||||
|
# Local Variables:
|
||||||
|
# mode: makefile
|
||||||
|
# End:
|
||||||
|
set shell := ["bash", "-uc"]
|
||||||
|
|
||||||
|
build-docs:
|
||||||
|
typst c --root . docs/manual.typ
|
||||||
|
typst c --root . docs/function_subtyping.typ
|
||||||
|
|
||||||
|
tests:
|
||||||
|
uv run -m tests
|
||||||
|
|
||||||
|
check-docstrings:
|
||||||
|
uv run scripts/docstring_checker.py
|
||||||
@@ -1,33 +0,0 @@
|
|||||||
import json
|
|
||||||
from pathlib import Path
|
|
||||||
|
|
||||||
from midas.ast.printer import MidasAstPrinter
|
|
||||||
from midas.lexer.midas import MidasLexer
|
|
||||||
from midas.lexer.token import Token
|
|
||||||
from midas.parser.midas import MidasParser
|
|
||||||
|
|
||||||
|
|
||||||
def test_midas():
|
|
||||||
# Midas type definitions
|
|
||||||
path: Path = Path("examples") / "00_syntax_prototype" / "03_custom_types_v2.midas"
|
|
||||||
definitions: str = path.read_text()
|
|
||||||
midas_lexer: MidasLexer = MidasLexer(definitions, path.name)
|
|
||||||
tokens: list[Token] = midas_lexer.process()
|
|
||||||
# print([f"{t.type.name}('{t.lexeme}')" for t in tokens])
|
|
||||||
with open("tokens.json", "w") as f:
|
|
||||||
json.dump([f"{t.type.name}('{t.lexeme}')" for t in tokens], f, indent=4)
|
|
||||||
|
|
||||||
parser = MidasParser(tokens)
|
|
||||||
parsed = parser.parse()
|
|
||||||
print(parsed)
|
|
||||||
for err in parser.errors:
|
|
||||||
print(err.get_report())
|
|
||||||
printer = MidasAstPrinter()
|
|
||||||
for stmt in parsed:
|
|
||||||
if stmt is None:
|
|
||||||
print("None")
|
|
||||||
continue
|
|
||||||
print(printer.print(stmt))
|
|
||||||
|
|
||||||
|
|
||||||
test_midas()
|
|
||||||
Reference in New Issue
Block a user