feat(cli): refactor CLI and add some commands

This commit is contained in:
2026-06-15 14:17:54 +02:00
parent 74f51f361a
commit 59c1a0c7b6
12 changed files with 450 additions and 261 deletions

View File

@@ -0,0 +1,8 @@
from .check import check as check
from .compile import compile as compile
from .format import format as format
from .highlight import highlight as highlight
from .parse import parse as parse
from .registry import dump_registry as dump_registry
from .types import types as types
from .validate import validate as validate

View File

@@ -0,0 +1,41 @@
# **Run type checker and report diagnostics**
# ```shell
# midas check <file.py> [--types <file.midas>]
# ```
from pathlib import Path
from typing import Optional, TextIO
import click
from midas.checker.checker import TypeChecker
from midas.checker.diagnostic import Diagnostic
from midas.cli.highlighter import DiagnosticsHighlighter
from midas.cli.utils import DiagnosticPrinter
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-t", "--types", type=click.File("r"), multiple=True)
@click.option("-l", "--highlight", type=click.File("w"))
def check(
file: TextIO,
types: tuple[TextIO],
highlight: Optional[TextIO],
):
source_path: Path = Path(file.name).resolve()
checker = TypeChecker()
for types_file in types:
checker.import_midas(Path(types_file.name).resolve())
checker.type_check(source_path)
diagnostics: list[Diagnostic] = checker.diagnostics.copy()
printer = DiagnosticPrinter()
printer.print_all(diagnostics)
if highlight is not None:
source: str = file.read()
highlighter = DiagnosticsHighlighter(source)
highlighter.highlight(diagnostics)
highlighter.dump(highlight)

View File

@@ -0,0 +1,38 @@
# **Compile source**
# ```shell
# midas compile <file.py> [--types <file.midas>] [-o <output>] [--assertions|--strict|--no-checks]
# ```
from pathlib import Path
from typing import TextIO
import click
from midas.checker.checker import TypeChecker
from midas.checker.diagnostic import Diagnostic
from midas.cli.utils import DiagnosticPrinter
from midas.generator.generator import Generator
from midas.utils import TypedAST
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-t", "--types", type=click.File("r"), multiple=True)
def compile(
file: TextIO,
types: tuple[TextIO],
):
source: str = file.read()
source_path: Path = Path(file.name).resolve()
checker = TypeChecker()
for types_file in types:
checker.import_midas(Path(types_file.name).resolve())
typed_ast: TypedAST = checker.type_check_source(source, str(source_path))
diagnostics: list[Diagnostic] = checker.diagnostics.copy()
printer = DiagnosticPrinter()
printer.print_all(diagnostics)
generator = Generator(workdir=source_path.parent)
generator.generate(typed_ast, source_path)

View File

@@ -0,0 +1,25 @@
from typing import TextIO
import click
import midas.ast.midas as m
from midas.ast.printer import MidasPrinter
from midas.lexer.midas import MidasLexer
from midas.lexer.token import Token
from midas.parser.midas import MidasParser
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-o", "--output", type=click.File("w"), default="-")
def format(file: TextIO, output: TextIO):
source: str = file.read()
printer = MidasPrinter()
lexer = MidasLexer(source, file=file.name)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
for err in parser.errors:
print(err.get_report())
for stmt in stmts:
output.write(printer.print(stmt) + "\n")

View File

@@ -0,0 +1,63 @@
import ast
from typing import TextIO
import click
import midas.ast.midas as m
import midas.ast.python as p
from midas.cli.highlighter import (
Highlighter,
LocatableToken,
MidasHighlighter,
PythonHighlighter,
)
from midas.lexer.midas import MidasLexer
from midas.lexer.token import Token, TokenType
from midas.parser.midas import MidasParser
from midas.parser.python import PythonParser
def highlight_python(source: str, path: str) -> Highlighter:
tree: ast.Module = ast.parse(source, filename=path)
parser = PythonParser()
stmts: list[p.Stmt] = parser.parse_module(tree)
highlighter = PythonHighlighter(source)
for stmt in stmts:
highlighter.highlight(stmt)
return highlighter
def highlight_midas(source: str, path: str) -> Highlighter:
lexer = MidasLexer(source, file=path)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
highlighter = MidasHighlighter(source)
for err in parser.errors:
print(err.get_report())
for stmt in stmts:
highlighter.highlight(stmt)
for token in tokens:
if token.type == TokenType.COMMENT:
highlighter.wrap(LocatableToken(token), "comment")
elif token.is_keyword:
highlighter.wrap(LocatableToken(token), "keyword")
return highlighter
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-o", "--output", type=click.File("w"), default="-")
def highlight(output: TextIO, file: TextIO):
source: str = file.read()
highlighter: Highlighter
if file.name.endswith(".py"):
highlighter = highlight_python(source, file.name)
elif file.name.endswith(".midas"):
highlighter = highlight_midas(source, file.name)
else:
raise ValueError("Unsupported file type")
highlighter.dump(output)

View File

@@ -0,0 +1,66 @@
# **Parse and pretty-print AST**
# ```shell
# midas parse <file.midas / file.py>
# ```
import ast
from typing import TextIO
import click
import midas.ast.midas as m
import midas.ast.python as p
from midas.ast.printer import MidasAstPrinter, PythonAstPrinter
from midas.lexer.midas import MidasLexer
from midas.lexer.token import Token
from midas.parser.midas import MidasParser
from midas.parser.python import PythonParser
def dump_python_ast(tree: ast.Module) -> str:
parser = PythonParser()
stmts: list[p.Stmt] = parser.parse_module(tree)
printer = PythonAstPrinter()
dump: str = ""
for stmt in stmts:
dump += printer.print(stmt)
dump += "\n"
return dump
def dump_midas_ast(source: str, filename: str) -> str:
lexer = MidasLexer(source, file=filename)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
if len(parser.errors) != 0:
for err in parser.errors:
print(err.get_report())
raise RuntimeError("A parsing error occurred")
printer = MidasAstPrinter()
dump: str = ""
for stmt in stmts:
dump += printer.print(stmt)
dump += "\n"
return dump
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("--raw", is_flag=True)
def parse(file: TextIO, raw: bool):
source: str = file.read()
dump: str
if file.name.endswith(".py"):
tree: ast.Module = ast.parse(source, filename=file.name)
if raw:
dump = ast.dump(tree, indent=4)
else:
dump = dump_python_ast(tree)
elif file.name.endswith(".midas"):
dump = dump_midas_ast(source, file.name)
else:
raise ValueError("Unsupported file type")
click.echo(dump)

View File

@@ -0,0 +1,30 @@
# **Dump types registry**
# ```shell
# midas dump-registry [--types <file.midas>]
# ```
from pathlib import Path
from typing import TextIO
import click
from midas.checker.checker import TypeChecker
from midas.checker.types import Type
@click.command()
@click.option("-t", "--types", type=click.File("r"), multiple=True)
def dump_registry(
types: tuple[TextIO],
):
checker = TypeChecker()
for types_file in types:
checker.import_midas(Path(types_file.name).resolve())
for name, type in checker.types._types.items():
members: dict[str, Type] = checker.types._members.get(name, {})
print(f"{name} = {type}")
if len(members) != 0:
print(" " * 4 + "Members:")
for member_name, member_type in members.items():
print(" " * 8 + f"{member_name}: {member_type}")

View File

@@ -0,0 +1,51 @@
# **Print judgements**
# ```shell
# midas types <file.py> [--types <file.midas>]
# ```
from pathlib import Path
from typing import Optional, TextIO
import click
from midas.checker.checker import TypeChecker
from midas.checker.diagnostic import Diagnostic, DiagnosticType
from midas.cli.highlighter import DiagnosticsHighlighter
from midas.cli.utils import DiagnosticPrinter
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-t", "--types", type=click.File("r"), multiple=True)
@click.option("-l", "--highlight", type=click.File("w"))
def types(
file: TextIO,
types: tuple[TextIO],
highlight: Optional[TextIO],
):
source_path: Path = Path(file.name).resolve()
checker = TypeChecker()
for types_file in types:
checker.import_midas(Path(types_file.name).resolve())
checker.type_check(source_path)
diagnostics: list[Diagnostic] = []
for expr, type in checker.python_typer.judgements:
diagnostics.append(
Diagnostic(
file_path=str(source_path),
location=expr.location,
type=DiagnosticType.INFO,
message=f"Type: {type}",
)
)
printer = DiagnosticPrinter()
printer.print_all(diagnostics)
if highlight is not None:
source: str = file.read()
highlighter = DiagnosticsHighlighter(source)
highlighter.highlight(diagnostics)
highlighter.dump(highlight)

View File

@@ -0,0 +1,37 @@
# **Validate midas definitions**
# ```shell
# midas validate <file.midas>
# ```
from pathlib import Path
from typing import Optional, TextIO
import click
from midas.checker.checker import TypeChecker
from midas.checker.diagnostic import Diagnostic
from midas.cli.highlighter import DiagnosticsHighlighter
from midas.cli.utils import DiagnosticPrinter
@click.command()
@click.argument("file", type=click.File("r"))
@click.option("-l", "--highlight", type=click.File("w"))
def validate(
file: TextIO,
highlight: Optional[TextIO],
):
source_path: Path = Path(file.name).resolve()
checker = TypeChecker()
checker.import_midas(source_path)
diagnostics: list[Diagnostic] = checker.diagnostics.copy()
printer = DiagnosticPrinter()
printer.print_all(diagnostics)
if highlight is not None:
source: str = file.read()
highlighter = DiagnosticsHighlighter(source)
highlighter.highlight(diagnostics)
highlighter.dump(highlight)

View File

@@ -1,273 +1,24 @@
import ast
import json
import logging
from pathlib import Path
from typing import Optional, TextIO, get_args
import click
import midas.ast.midas as m
import midas.ast.python as p
from midas.ast.location import Location
from midas.ast.printer import MidasAstPrinter, MidasPrinter, PythonAstPrinter
from midas.checker.checker import TypeChecker
from midas.checker.diagnostic import Diagnostic, DiagnosticType
from midas.checker.types import Type
from midas.cli.ansi import Ansi
from midas.cli.highlighter import (
DiagnosticsHighlighter,
Highlighter,
LocatableToken,
MidasHighlighter,
PythonHighlighter,
)
from midas.lexer.midas import MidasLexer
from midas.lexer.token import Token, TokenType
from midas.parser.midas import MidasParser
from midas.parser.python import PythonParser
from midas.utils import UniversalJSONDumper
from midas.cli import commands
@click.group()
def midas():
pass
def print_diagnostic(lines: list[str], diagnostic: Diagnostic, indent: int = 4):
"""Pretty-print a diagnostic, showing some context if possible
If the diagnostic concerns a specific part of one line, the line is shown
with the affected part highlighted. The message is clearly printed under the
line with an underline further indicating the target expression.
If multiple lines are concerned, no context is shown, only the
diagnostic type, location and message
Args:
lines (list[str]): source code lines
diagnostic (Diagnostic): the diagnostic to print
indent (int, optional): the number of spaces added before the target line to indent if from the location header. Defaults to 4.
"""
loc: Location = diagnostic.location
if loc.lineno != loc.end_lineno:
print(diagnostic)
return
start_offset: int = loc.col_offset
end_offset: int = loc.end_col_offset or (start_offset + 1)
line: str = lines[loc.lineno - 1]
before: str = line[:start_offset]
after: str = line[end_offset:]
color: int = {
DiagnosticType.ERROR: Ansi.RED,
DiagnosticType.WARNING: Ansi.YELLOW,
DiagnosticType.INFO: Ansi.CYAN,
}.get(diagnostic.type, Ansi.WHITE)
subject: str = Ansi.FG(color) + line[start_offset:end_offset] + Ansi.RESET
cursor: str = (
" " * start_offset
+ Ansi.FG(color)
+ "~" * (end_offset - start_offset)
+ "> "
+ diagnostic.message
+ Ansi.RESET
)
indent_str: str = " " * indent
print(diagnostic.location_str + ":")
print(indent_str + before + subject + after)
print(indent_str + cursor)
print()
@midas.command()
@click.option("-l", "--highlight", type=click.File("w"))
@click.option("-t", "--types", type=click.File("r"), multiple=True)
@click.option("-v", "--verbose", is_flag=True)
@click.option("-j", "--show-judgements", is_flag=True)
@click.argument("file", type=click.File("r"))
def compile(
highlight: Optional[TextIO],
types: tuple[TextIO],
verbose: bool,
show_judgements: bool,
file: TextIO,
):
def midas(verbose: bool):
logging.basicConfig(level=logging.DEBUG if verbose else logging.WARN)
source: str = file.read()
source_path: Path = Path(file.name).resolve()
checker = TypeChecker()
for types_file in types:
checker.import_midas(Path(types_file.name).resolve())
checker.type_check_source(source, str(source_path))
diagnostics: list[Diagnostic] = checker.diagnostics.copy()
lines: list[str] = source.split("\n")
files: dict[Optional[str], list[str]] = {None: []}
if show_judgements:
for expr, type in checker.python_typer.judgements:
print(f"Judged that {expr} at {expr.location} is of type {type}")
diagnostics.append(
Diagnostic(
file_path=str(source_path),
location=expr.location,
type=DiagnosticType.INFO,
message=f"Type: {type}",
)
)
for diagnostic in diagnostics:
filename: Optional[str] = diagnostic.file_path
if filename is not None and filename not in files:
path: Path = Path(filename)
if path.exists() and path.is_file():
files[filename] = path.read_text().split("\n")
else:
files[filename] = []
lines: list[str] = files[filename]
print_diagnostic(lines, diagnostic)
if verbose:
print(
json.dumps(
UniversalJSONDumper.dump(
checker.python_typer.global_env,
[("Environment", "_children")],
lambda obj: isinstance(obj, get_args(Type)),
),
indent=4,
)
)
if highlight is not None:
highlighter = DiagnosticsHighlighter(source)
highlighter.highlight(diagnostics)
highlighter.dump(highlight)
@midas.group()
def utils():
pass
def dump_python_ast(tree: ast.Module) -> str:
parser = PythonParser()
stmts: list[p.Stmt] = parser.parse_module(tree)
printer = PythonAstPrinter()
dump: str = ""
for stmt in stmts:
dump += printer.print(stmt)
dump += "\n"
return dump
def dump_midas_ast(source: str, filename: str) -> str:
lexer = MidasLexer(source, file=filename)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
if len(parser.errors) != 0:
for err in parser.errors:
print(err.get_report())
raise RuntimeError("A parsing error occurred")
printer = MidasAstPrinter()
dump: str = ""
for stmt in stmts:
dump += printer.print(stmt)
dump += "\n"
return dump
@utils.command()
@click.option("-o", "--output", type=click.File("w"))
@click.option("-p", "--parse", is_flag=True)
@click.argument("file", type=click.File("r"))
def dump_ast(output: Optional[TextIO], parse: bool, file: TextIO):
source: str = file.read()
dump: str
if file.name.endswith(".py"):
tree: ast.Module = ast.parse(source, filename=file.name)
if parse:
dump = dump_python_ast(tree)
else:
dump = ast.dump(tree, indent=4)
elif file.name.endswith(".midas"):
dump = dump_midas_ast(source, file.name)
else:
raise ValueError("Unsupported file type")
if output is None:
click.echo(dump)
else:
output.write(dump)
def highlight_python(source: str, path: str) -> Highlighter:
tree: ast.Module = ast.parse(source, filename=path)
parser = PythonParser()
stmts: list[p.Stmt] = parser.parse_module(tree)
highlighter = PythonHighlighter(source)
for stmt in stmts:
highlighter.highlight(stmt)
return highlighter
def highlight_midas(source: str, path: str) -> Highlighter:
lexer = MidasLexer(source, file=path)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
highlighter = MidasHighlighter(source)
for err in parser.errors:
print(err.get_report())
for stmt in stmts:
highlighter.highlight(stmt)
for token in tokens:
if token.type == TokenType.COMMENT:
highlighter.wrap(LocatableToken(token), "comment")
elif token.is_keyword:
highlighter.wrap(LocatableToken(token), "keyword")
return highlighter
@utils.command()
@click.option("-o", "--output", type=click.File("w"), default="-")
@click.argument("file", type=click.File("r"))
def highlight(output: TextIO, file: TextIO):
source: str = file.read()
highlighter: Highlighter
if file.name.endswith(".py"):
highlighter = highlight_python(source, file.name)
elif file.name.endswith(".midas"):
highlighter = highlight_midas(source, file.name)
else:
raise ValueError("Unsupported file type")
highlighter.dump(output)
@midas.command()
@click.option("-o", "--output", type=click.File("w"), default="-")
@click.argument("file", type=click.File("r"))
def format(output: TextIO, file: TextIO):
source: str = file.read()
printer = MidasPrinter()
lexer = MidasLexer(source, file=file.name)
tokens: list[Token] = lexer.process()
parser = MidasParser(tokens)
stmts: list[m.Stmt] = parser.parse()
for err in parser.errors:
print(err.get_report())
for stmt in stmts:
output.write(printer.print(stmt) + "\n")
midas.add_command(commands.check)
midas.add_command(commands.compile)
midas.add_command(commands.format)
midas.add_command(commands.highlight)
midas.add_command(commands.parse)
midas.add_command(commands.dump_registry)
midas.add_command(commands.types)
midas.add_command(commands.validate)
if __name__ == "__main__":

78
midas/cli/utils.py Normal file
View File

@@ -0,0 +1,78 @@
from pathlib import Path
from typing import Optional
from midas.ast.location import Location
from midas.checker.diagnostic import Diagnostic, DiagnosticType
from midas.cli.ansi import Ansi
class DiagnosticPrinter:
def __init__(self) -> None:
self.files: dict[Optional[str], list[str]] = {}
def get_lines(self, filename: Optional[str]) -> list[str]:
if filename is None:
return []
if filename not in self.files:
path: Path = Path(filename)
if path.exists() and path.is_file():
self.files[filename] = path.read_text().split("\n")
else:
self.files[filename] = []
return self.files[filename]
def print_all(self, diagnostics: list[Diagnostic], indent: int = 4):
for diagnostic in diagnostics:
filename: Optional[str] = diagnostic.file_path
lines = self.get_lines(filename)
self.print(lines, diagnostic, indent=indent)
def print(self, lines: list[str], diagnostic: Diagnostic, indent: int = 4):
"""Pretty-print a diagnostic, showing some context if possible
If the diagnostic concerns a specific part of one line, the line is shown
with the affected part highlighted. The message is clearly printed under the
line with an underline further indicating the target expression.
If multiple lines are concerned, no context is shown, only the
diagnostic type, location and message
Args:
lines (list[str]): source code lines
diagnostic (Diagnostic): the diagnostic to print
indent (int, optional): the number of spaces added before the target line to indent if from the location header. Defaults to 4.
"""
loc: Location = diagnostic.location
if loc.lineno != loc.end_lineno:
print(diagnostic)
return
start_offset: int = loc.col_offset
end_offset: int = loc.end_col_offset or (start_offset + 1)
line: str = lines[loc.lineno - 1]
before: str = line[:start_offset]
after: str = line[end_offset:]
color: int = {
DiagnosticType.ERROR: Ansi.RED,
DiagnosticType.WARNING: Ansi.YELLOW,
DiagnosticType.INFO: Ansi.CYAN,
}.get(diagnostic.type, Ansi.WHITE)
subject: str = Ansi.FG(color) + line[start_offset:end_offset] + Ansi.RESET
cursor: str = (
" " * start_offset
+ Ansi.FG(color)
+ "~" * (end_offset - start_offset)
+ "> "
+ diagnostic.message
+ Ansi.RESET
)
indent_str: str = " " * indent
print(diagnostic.location_str + ":")
print(indent_str + before + subject + after)
print(indent_str + cursor)
print()

View File

@@ -1,14 +1,15 @@
import ast
import midas.ast.python as p
from midas.utils import TypedAST
class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]):
def __init__(self) -> None:
pass
def generate(self, stmts: list[p.Stmt]) -> str:
body: list[ast.stmt] = self._visit_body(stmts)
def generate(self, typed_ast: TypedAST, src_path: Path) -> str:
body: list[ast.stmt] = self._visit_body(typed_ast.stmts)
module = ast.Module(body=body, type_ignores=[])
module = ast.fix_missing_locations(module)
return ast.unparse(module)