phasm/phasm/type3/entry.py

"""
Entry point to the type3 system
"""
from typing import Any, Dict, List, Set

from .. import codestyle
from .. import ourlang

from .constraints import ConstraintBase, Error, RequireTypeSubstitutes, SameTypeConstraint, SubstitutionMap
from .constraintsgenerator import phasm_type3_generate_constraints
from .types import AppliedType3, IntType3, PlaceholderForType, PrimitiveType3, StructType3, Type3, Type3OrPlaceholder

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)

    # FIXME: This doesn't work with e.g. `:: [a] -> a`, as the placeholder is inside a type
    for plh, typ in placeholder_substitutes.items():
        for expr in plh.update_on_substitution:
            assert expr.type3 is plh

            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, (PrimitiveType3, StructType3, IntType3, )):
        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]

    if isinstance(inp, AppliedType3):
        return (
            get_printable_type_name(inp.base, placeholder_id_map)
            + ' ('
            + ') ('.join(get_printable_type_name(x, placeholder_id_map) for x in inp.args)
            + ')'
        )

    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 ^ === ')