HEL/midas
1
0
Fork 0
Code Issues Pull Requests Releases Activity

feat(cli): add option to show type judgements

Browse Source
This commit is contained in:
Louis Heredero
2026-06-12 14:44:02 +02:00
parent 80e611e49c
commit 01d6e41893
1 changed files with 15 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
midas/cli/main.py
View File

@@ -88,11 +88,13 @@ def print_diagnostic(lines: list[str], diagnostic: Diagnostic, indent: int = 4):
@click.option("-l", "--highlight", type=click.File("w")) @click.option("-l", "--highlight", type=click.File("w"))
@click.option("-t", "--types", type=click.File("r"), multiple=True) @click.option("-t", "--types", type=click.File("r"), multiple=True)
@click.option("-v", "--verbose", is_flag=True) @click.option("-v", "--verbose", is_flag=True)
@click.option("-j", "--show-judgements", is_flag=True)
@click.argument("file", type=click.File("r")) @click.argument("file", type=click.File("r"))
def compile( def compile(
highlight: Optional[TextIO], highlight: Optional[TextIO],
types: tuple[TextIO], types: tuple[TextIO],
verbose: bool, verbose: bool,
show_judgements: bool,
file: TextIO, file: TextIO,
): ):
logging.basicConfig(level=logging.DEBUG if verbose else logging.WARN) logging.basicConfig(level=logging.DEBUG if verbose else logging.WARN)
@@ -104,10 +106,22 @@ def compile(
checker.import_midas(Path(types_file.name).resolve()) checker.import_midas(Path(types_file.name).resolve())
checker.type_check_source(source, str(source_path)) checker.type_check_source(source, str(source_path))
diagnostics: list[Diagnostic] = checker.diagnostics diagnostics: list[Diagnostic] = checker.diagnostics.copy()
lines: list[str] = source.split("\n") lines: list[str] = source.split("\n")
files: dict[Optional[str], list[str]] = {None: []} 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: for diagnostic in diagnostics:
filename: Optional[str] = diagnostic.file_path filename: Optional[str] = diagnostic.file_path
if filename is not None and filename not in files: if filename is not None and filename not in files: