type5 is much more first principles based, so we get a lot of weird quirks removed: - FromLiteral no longer needs to understand AST - Type unifications works more like Haskell - Function types are just ordinary types, saving a lot of manual busywork and more.
132 lines
4.8 KiB
Python
132 lines
4.8 KiB
Python
from typing import Any
|
|
|
|
from ..ourlang import Module
|
|
from .constraints import ConstraintBase, Context
|
|
from .fromast import phasm_type5_generate_constraints
|
|
from .typeexpr import TypeExpr, TypeVariable, replace_variable
|
|
from .unify import ReplaceVariable
|
|
|
|
MAX_RESTACK_COUNT = 10 # 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]] = []
|
|
|
|
if verbose:
|
|
print('Constraints')
|
|
|
|
for _ in range(MAX_RESTACK_COUNT):
|
|
if verbose:
|
|
for constraint in constraint_list:
|
|
print(f"{constraint.sourceref!s} {constraint!s}")
|
|
print("Validating")
|
|
|
|
new_constraint_list: list[ConstraintBase] = []
|
|
while constraint_list:
|
|
constraint = constraint_list.pop(0)
|
|
result = constraint.check()
|
|
|
|
if verbose:
|
|
print(f"{constraint.sourceref!s} {constraint!s}")
|
|
print(f"{constraint.sourceref!s} => {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)
|
|
|
|
if isinstance(action, ReplaceVariable):
|
|
action_var: TypeExpr = action.var
|
|
while isinstance(action_var, TypeVariable) and action_var in placeholder_types:
|
|
# TODO: Does this still happen?
|
|
action_var = placeholder_types[action_var]
|
|
|
|
action_typ: TypeExpr = action.typ
|
|
while isinstance(action_typ, TypeVariable) and action_typ in placeholder_types:
|
|
# TODO: Does this still happen?
|
|
action_typ = placeholder_types[action_typ]
|
|
|
|
# print(inp.build.type5_name(action_var), ':=', inp.build.type5_name(action_typ))
|
|
|
|
if action_var == action_typ:
|
|
continue
|
|
|
|
if not isinstance(action_var, TypeVariable) and isinstance(action_typ, TypeVariable):
|
|
action_typ, action_var = action_var, action_typ
|
|
|
|
if isinstance(action_var, TypeVariable):
|
|
# Ensure all existing found types are updated
|
|
placeholder_types = {
|
|
k: replace_variable(v, action_var, action_typ)
|
|
for k, v in placeholder_types.items()
|
|
}
|
|
placeholder_types[action_var] = action_typ
|
|
|
|
for oth_const in new_constraint_list + constraint_list:
|
|
if oth_const is constraint and result.done:
|
|
continue
|
|
|
|
old_str = str(oth_const)
|
|
oth_const.replace_variable(action_var, action_typ)
|
|
new_str = str(oth_const)
|
|
|
|
if verbose and old_str != new_str:
|
|
print(f"{oth_const.sourceref!s} => - {old_str!s}")
|
|
print(f"{oth_const.sourceref!s} => + {new_str!s}")
|
|
continue
|
|
|
|
error_list.append((str(constraint.sourceref), str(constraint), "Not the same type", ))
|
|
if verbose:
|
|
print(f"{constraint.sourceref!s} => ERR: Conflict in applying {action.to_str(inp.build.type5_name)}")
|
|
continue
|
|
|
|
# Action of unsupported type
|
|
raise NotImplementedError(action)
|
|
|
|
for failure in result.failures:
|
|
error_list.append((str(constraint.sourceref), str(constraint), failure.msg, ))
|
|
|
|
new_constraint_list.extend(result.new_constraints)
|
|
|
|
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():
|
|
if expression is None:
|
|
continue
|
|
|
|
new_type5 = placeholder_types[placeholder]
|
|
while isinstance(new_type5, TypeVariable):
|
|
new_type5 = placeholder_types[new_type5]
|
|
|
|
expression.type5 = new_type5
|