nac3-spec/toy-impl/test_subst.py

from type_def import *
from inference import *

types = {
    'int32': PrimitiveType('int32'),
    'int64': PrimitiveType('int64'),
    'str': PrimitiveType('str'),
}

i32 = types['int32']
i64 = types['int64']
s = types['str']

variables = {
    'X': TypeVariable('X', []),
    'Y': TypeVariable('Y', []),
    'I': TypeVariable('I', [i32, i64]),
    'A': TypeVariable('A', [i32, i64, s]),
}

X = variables['X']
Y = variables['Y']
I = variables['I']
A = variables['A']


def stringify_subst(subst):
    if isinstance(subst, str):
        return subst
    elements = [f"{key}: {str(value)}" for key, value in subst.items()]
    return "{" + ', '.join(elements) + "}"

def try_case(a, b, ctx):
    result = find_subst(ctx, {}, a, b)
    print(f"{a} <- {b} w.r.t. {stringify_subst(ctx)}\n    {stringify_subst(result)}\n")


try_case(i32, i32, {})
try_case(i32, i64, {})
try_case(i32, X, {})
try_case(i32, X, {'X': i32})
try_case(i32, X, {'X': i64})
try_case(X, X, {'X': i64})
try_case(X, Y, {'Y': i64})
try_case(X, Y, {'X': i64})
try_case(I, X, {})
try_case(I, A, {})
try_case(A, I, {})
try_case(X, I, {})
try_case(ListType(i32), TupleType([i32]), {})
try_case(TupleType([i32]), ListType(i32), {})
try_case(ListType(i32), ListType(i32), {})
try_case(TupleType([X, X]), TupleType([X, Y]), {})
try_case(TupleType([X, X]), TupleType([Y, Y]), {})
try_case(TupleType([X, Y]), TupleType([X, X]), {})
try_case(TupleType([X, Y]), X, {})
try_case(TupleType([i32, Y]), X, {})