phasm/phasm/type5/solver.py
Johan B.W. de Vries 388f6754d3 Notes
2025-07-30 19:08:07 +02:00

102 lines
3.5 KiB
Python

from typing import Any
from ..ourlang import Module, SourceRef
from .constraints import Context
from .fromast import phasm_type5_generate_constraints
from .typeexpr import TypeExpr, TypeVariable
from .unify import ReplaceVariable
MAX_RESTACK_COUNT = 3 # 100
class Type5SolverException(Exception):
pass
def phasm_type5(inp: Module[Any], verbose: bool = False) -> None:
ctx = Context(inp.build)
constraint_list = phasm_type5_generate_constraints(ctx, inp)
assert constraint_list
placeholder_types: dict[TypeVariable, TypeExpr] = {}
error_list: list[tuple[str, str, str]] = []
for _ in range(MAX_RESTACK_COUNT):
if verbose:
for constraint in constraint_list:
sourceref = constraint.sourceref or SourceRef("?", 0, 0)
print(f"{sourceref!s} {constraint!s:<70}")
print()
new_constraint_list = []
for constraint in constraint_list:
result = constraint.check()
sourceref = constraint.sourceref or SourceRef("?", 0, 0)
if verbose:
print(f"{sourceref!s} {constraint!s:<70} {result.to_str(inp.build.type5_name)}")
if not result:
# None or empty list
# Means it checks out and we don't need do anything
continue
while result.actions:
action = result.actions.pop(0)
for constraint in constraint_list:
constraint.apply(action)
if isinstance(action, ReplaceVariable):
exist_typ = placeholder_types.get(action.var)
if exist_typ is None:
placeholder_types[action.var] = action.typ
continue
if exist_typ == action.typ:
continue
if isinstance(action.typ, TypeVariable):
# Callable[a, a, a] ~ Callable[i32, p_2, i32] {a := i32, a := p_2, a := i32}
# Dealing with a := p_2 - but a is already being replaced with i32
# Since p_2 is a variable as well, we can just replace p_2 with i32
result.actions.append(ReplaceVariable(action.typ, exist_typ))
continue
if isinstance(exist_typ, TypeVariable):
# Callable[p_1, p_1, p_1] ~ Callable[p_1, p_3, i32] {p_1 := p_3, p_1 := i32}
# Dealing with p_1 := i32 - but p_1 is already being replaced with p_3
# We should replace p_3 with i32 instead
result.actions.append(ReplaceVariable(exist_typ, action.typ))
continue
# This is probably a type error
raise NotImplementedError(action, exist_typ)
for failure in result.failures:
error_list.append((str(sourceref), str(constraint), failure.msg, ))
if result.done:
continue
new_constraint_list.append(constraint)
if error_list:
raise Type5SolverException(error_list)
if not new_constraint_list:
break
if verbose:
print()
print('New round')
constraint_list = new_constraint_list
if new_constraint_list:
raise Type5SolverException('Was unable to complete typing this program')
for placeholder, expression in ctx.placeholder_update.items():
expression.type5 = placeholder_types[placeholder]