টাইপ ইনফারেন্স

# টাইপ রিপ্রেজেন্টেশন: ('con', name) কংক্রিট টাইপ, অথবা ('var', name) টাইপ ভেরিয়েবল

def resolve(t, subst):
    """t যদি একটি ভেরিয়েবল হয় যা subst-এ ইতিমধ্যে সমাধান করা আছে, তাহলে সেই সমাধানে অনুসরণ করে চূড়ান্ত রূপ ফেরত দেয়।"""
    while t[0] == 'var' and t[1] in subst:
        t = subst[t[1]]
    return t


def occurs_in(var_name, t, subst):
    """occurs check -- t (resolve করার পর) কি ঠিক সেই var_name ভেরিয়েবলটিই?"""
    t = resolve(t, subst)
    return t[0] == 'var' and t[1] == var_name


def unify_one(t1, t2, subst):
    """একজোড়া টাইপকে ইউনিফাই করে, একটি নতুন (সম্প্রসারিত) সাবস্টিটিউশন ফেরত দেয় -- ব্যর্থ হলে TypeError।"""
    t1 = resolve(t1, subst)
    t2 = resolve(t2, subst)

    if t1 == t2:
        return subst  # ইতিমধ্যেই একই -- কিছু করার নেই

    if t1[0] == 'var':
        if occurs_in(t1[1], t2, subst):
            raise TypeError(f"occurs check ব্যর্থ: {t1} নিজেই {t2}-এর ভেতরে আছে")
        new_subst = dict(subst)
        new_subst[t1[1]] = t2
        return new_subst

    if t2[0] == 'var':
        return unify_one(t2, t1, subst)  # সিমেট্রিক -- ঘুরিয়ে আবার চেষ্টা করো

    # দুটোই কংক্রিট টাইপ, কিন্তু ভিন্ন -- সত্যিকারের সংঘর্ষ
    raise TypeError(f"ইউনিফিকেশন ব্যর্থ: {t1} এর সাথে {t2} মেলানো যায় না")


def unify(constraints):
    """কনস্ট্রেইন্টের একটি তালিকা (t1, t2) জোড়া করে ধারাবাহিকভাবে ইউনিফাই করে -- চূড়ান্ত সাবস্টিটিউশন ফেরত দেয়।"""
    subst = {}
    for (a, b) in constraints:
        subst = unify_one(a, b, subst)
    return subst


CON_INT = ('con', 'int')
T = ('var', 'T')  # x-এর টাইপ, শুরুতে অজানা

print("=== worked example: let x = 5 in x + 1 ===")
print("ধাপ ১ (ফ্রেশ ভেরিয়েবল): x -> T\n")

# ধাপ ২ (কনস্ট্রেইন্ট জেনারেশন):
#   'let x = 5' -- 5 : int, তাই x-এর টাইপ int-এর সাথে ইউনিফাই হতেই হবে
#   'x + 1'     -- 1 : int, আর + উভয় পাশে int দাবি করে, তাই আবার T int-এর সাথে ইউনিফাই হতে হবে
constraints = [
    (T, CON_INT),   # from: let x = 5
    (T, CON_INT),   # from: x + 1  (x এর ব্যবহার int-এর সাথে সামঞ্জস্যপূর্ণ হতে হবে)
]
print("ধাপ ২ (কনস্ট্রেইন্ট):", constraints)

# ধাপ ৩ (ইউনিফিকেশন):
subst = unify(constraints)
final_type = resolve(T, subst)
print("ধাপ ৩ (unify() চালানোর পর সাবস্টিটিউশন):", subst)
print(f"চূড়ান্ত ইনফার্ড টাইপ: T = {final_type}  (এক্সপ্রেশনের সামগ্রিক টাইপও int, কারণ + এর ফলাফল int)")

assert final_type == CON_INT, "প্রত্যাশিত ছিল int, কিন্তু ভিন্ন কিছু পাওয়া গেল!"
print("assertion পাস -- ইনফার্ড টাইপ সত্যিই int।\n")

print("=== ইচ্ছাকৃত ব্যর্থতা: একই ভেরিয়েবলকে int ও string উভয়ের সাথে ইউনিফাই করার চেষ্টা ===")
bad_constraints = [
    (T, CON_INT),               # T = int
    (T, ('con', 'string')),     # কিন্তু এখানে T = string -ও দাবি করা হচ্ছে -- সংঘর্ষ!
]
print("কনস্ট্রেইন্ট:", bad_constraints)
try:
    unify(bad_constraints)
    print("(এটা প্রিন্ট হওয়ার কথা না -- ইউনিফিকেশন ব্যর্থ হওয়া উচিত ছিল!)")
except TypeError as e:
    print(f"সঠিকভাবে ধরা পড়েছে -> টাইপ এরর: {e}")