phasm/phasm/type3/entry.py

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