159 lines
5.4 KiB
Python
159 lines
5.4 KiB
Python
"""
|
|
Entry point to the type3 system
|
|
"""
|
|
from typing import Dict, List
|
|
|
|
from .. import codestyle, ourlang
|
|
from .constraints import (
|
|
ConstraintBase,
|
|
Error,
|
|
RequireTypeSubstitutes,
|
|
SameTypeConstraint,
|
|
SubstitutionMap,
|
|
)
|
|
from .constraintsgenerator import phasm_type3_generate_constraints
|
|
from .placeholders import (
|
|
PlaceholderForType,
|
|
Type3OrPlaceholder,
|
|
)
|
|
from .types import Type3
|
|
|
|
MAX_RESTACK_COUNT = 100
|
|
|
|
class Type3Exception(BaseException):
|
|
"""
|
|
Thrown when the Type3 system detects constraints that do not hold
|
|
"""
|
|
|
|
def phasm_type3(inp: ourlang.Module, verbose: bool = False) -> None:
|
|
constraint_list = phasm_type3_generate_constraints(inp)
|
|
assert constraint_list
|
|
|
|
placeholder_substitutes: Dict[PlaceholderForType, Type3] = {}
|
|
placeholder_id_map: Dict[int, str] = {}
|
|
|
|
error_list: List[Error] = []
|
|
for _ in range(MAX_RESTACK_COUNT):
|
|
if verbose:
|
|
print()
|
|
print_constraint_list(placeholder_id_map, constraint_list, placeholder_substitutes)
|
|
|
|
old_constraint_ids = {id(x) for x in constraint_list}
|
|
old_placeholder_substitutes_len = len(placeholder_substitutes)
|
|
|
|
back_on_todo_list_count = 0
|
|
|
|
new_constraint_list = []
|
|
for constraint in constraint_list:
|
|
check_result = constraint.check()
|
|
if check_result is None:
|
|
if verbose:
|
|
print_constraint(placeholder_id_map, constraint)
|
|
print('-> Constraint checks out')
|
|
continue
|
|
|
|
if isinstance(check_result, dict):
|
|
placeholder_substitutes.update(check_result)
|
|
|
|
if verbose:
|
|
print_constraint(placeholder_id_map, constraint)
|
|
print('-> Constraint checks out, and gave us new information')
|
|
continue
|
|
|
|
if isinstance(check_result, Error):
|
|
error_list.append(check_result)
|
|
if verbose:
|
|
print_constraint(placeholder_id_map, constraint)
|
|
print('-> Got an error')
|
|
continue
|
|
|
|
if isinstance(check_result, RequireTypeSubstitutes):
|
|
new_constraint_list.append(constraint)
|
|
|
|
back_on_todo_list_count += 1
|
|
continue
|
|
|
|
if isinstance(check_result, list):
|
|
new_constraint_list.extend(check_result)
|
|
|
|
if verbose:
|
|
print_constraint(placeholder_id_map, constraint)
|
|
print(f'-> Resulted in {len(check_result)} new constraints')
|
|
continue
|
|
|
|
raise NotImplementedError(constraint, check_result)
|
|
|
|
if verbose and 0 < back_on_todo_list_count:
|
|
print(f'{back_on_todo_list_count} constraints skipped for now')
|
|
|
|
if not new_constraint_list:
|
|
constraint_list = new_constraint_list
|
|
break
|
|
|
|
# Infinite loop detection
|
|
new_constraint_ids = {id(x) for x in new_constraint_list}
|
|
new_placeholder_substitutes_len = len(placeholder_substitutes)
|
|
|
|
if old_constraint_ids == new_constraint_ids and old_placeholder_substitutes_len == new_placeholder_substitutes_len:
|
|
if error_list:
|
|
raise Type3Exception(error_list)
|
|
|
|
raise Exception('Cannot type this program - not enough information')
|
|
|
|
constraint_list = new_constraint_list
|
|
|
|
if verbose:
|
|
print()
|
|
print_constraint_list(placeholder_id_map, constraint_list, placeholder_substitutes)
|
|
|
|
if constraint_list:
|
|
raise Exception(f'Cannot type this program - tried {MAX_RESTACK_COUNT} iterations')
|
|
|
|
if error_list:
|
|
raise Type3Exception(error_list)
|
|
|
|
for plh, typ in placeholder_substitutes.items():
|
|
for expr in plh.update_on_substitution:
|
|
expr.type3 = typ
|
|
|
|
def print_constraint(placeholder_id_map: Dict[int, str], constraint: ConstraintBase) -> None:
|
|
txt, fmt = constraint.human_readable()
|
|
act_fmt: Dict[str, str] = {}
|
|
for fmt_key, fmt_val in fmt.items():
|
|
if isinstance(fmt_val, ourlang.Expression):
|
|
fmt_val = codestyle.expression(fmt_val)
|
|
|
|
if isinstance(fmt_val, Type3) or isinstance(fmt_val, PlaceholderForType):
|
|
fmt_val = get_printable_type_name(fmt_val, placeholder_id_map)
|
|
|
|
if not isinstance(fmt_val, str):
|
|
fmt_val = repr(fmt_val)
|
|
|
|
act_fmt[fmt_key] = fmt_val
|
|
|
|
if constraint.comment is not None:
|
|
print('- ' + txt.format(**act_fmt).ljust(40) + '; ' + constraint.comment)
|
|
else:
|
|
print('- ' + txt.format(**act_fmt))
|
|
|
|
def get_printable_type_name(inp: Type3OrPlaceholder, placeholder_id_map: Dict[int, str]) -> str:
|
|
if isinstance(inp, Type3):
|
|
return inp.name
|
|
|
|
if isinstance(inp, PlaceholderForType):
|
|
placeholder_id = id(inp)
|
|
if placeholder_id not in placeholder_id_map:
|
|
placeholder_id_map[placeholder_id] = 'T' + str(len(placeholder_id_map) + 1)
|
|
return placeholder_id_map[placeholder_id]
|
|
|
|
raise NotImplementedError(inp)
|
|
|
|
def print_constraint_list(placeholder_id_map: Dict[int, str], constraint_list: List[ConstraintBase], placeholder_substitutes: SubstitutionMap) -> None:
|
|
print('=== v type3 constraint_list v === ')
|
|
for psk, psv in placeholder_substitutes.items():
|
|
print_constraint(placeholder_id_map, SameTypeConstraint(psk, psv, comment='Deduced type'))
|
|
|
|
for constraint in constraint_list:
|
|
print_constraint(placeholder_id_map, constraint)
|
|
print('=== ^ type3 constraint_list ^ === ')
|