টাইপ সেফটি ও সাউন্ডনেস

# AST নোড: ('num', v) | ('str', v) | ('binop', op, left, right) | ('cast', subexpr)

def is_value(e):
    """একটি নোড কি ইতিমধ্যে একটি চূড়ান্ত ভ্যালু (আর কোনো ধাপ প্রয়োজন নেই)?"""
    return e[0] in ('num', 'str')


def type_of(e):
    kind = e[0]
    if kind == 'num':
        return 'int'
    if kind == 'str':
        return 'str'
    if kind == 'binop':
        _, op, left, right = e
        lt, rt = type_of(left), type_of(right)
        if lt == 'int' and rt == 'int' and op in ('+', '-', '*'):
            return 'int'
        raise TypeError(f"টাইপ এরর: '{op}' {lt} ও {rt}-এর মধ্যে প্রযোজ্য নয়")
    if kind == 'cast':
        # *** ইচ্ছাকৃতভাবে ভুল/আনসাউন্ড রুল -- সত্যিকারে subexpression কী হয়ে যাবে তা যাচাই না করেই দাবি করে ফলাফল সবসময় 'int' ***
        return 'int'
    raise ValueError(f"অজানা নোড: {e}")


def step(e):
    """স্মল-স্টেপ এভালুয়েটর -- একটি একক এভালুয়েশন ধাপ নিয়ে (নতুন_এক্সপ্রেশন, ধাপ_নেওয়া_হয়েছে_কিনা) ফেরত দেয়।"""
    kind = e[0]
    if kind in ('num', 'str'):
        return e, False  # ইতিমধ্যে ভ্যালু -- আর কোনো ধাপ নেই
    if kind == 'binop':
        _, op, left, right = e
        if not is_value(left):
            new_left, _ = step(left)
            return ('binop', op, new_left, right), True
        if not is_value(right):
            new_right, _ = step(right)
            return ('binop', op, left, new_right), True
        lv, rv = left[1], right[1]
        result = {'+': lv + rv, '-': lv - rv, '*': lv * rv}[op]
        return ('num', result), True
    if kind == 'cast':
        _, sub = e
        if not is_value(sub):
            new_sub, _ = step(sub)
            return ('cast', new_sub), True
        # "cast" আসলে যা করে: সংখ্যাটিকে তার স্ট্রিং রিপ্রেজেন্টেশনে রূপান্তর করে -- str ফেরত দেয়, int নয়!
        v = sub[1]
        return ('str', str(v)), True
    raise ValueError(f"অজানা নোড: {e}")


print("=== (2+3)*4 -- প্রতিটি ধাপে Progress ও Preservation যাচাই ===")
expr = ('binop', '*', ('binop', '+', ('num', 2), ('num', 3)), ('num', 4))
print(f"শুরু: {expr}   টাইপ: {type_of(expr)}\n")

step_no = 0
while not is_value(expr):
    t_before = type_of(expr)                 # ধাপের আগে টাইপ
    new_expr, stepped = step(expr)
    assert stepped, "PROGRESS লঙ্ঘিত! well-typed এক্সপ্রেশন আটকে গেছে।"   # Progress
    t_after = type_of(new_expr)               # ধাপের পরে টাইপ
    step_no += 1
    print(f"ধাপ {step_no}: {expr}  →  {new_expr}   (টাইপ: {t_before} → {t_after})")
    assert t_before == t_after, "PRESERVATION লঙ্ঘিত! টাইপ পরিবর্তিত হয়ে গেছে।"  # Preservation
    expr = new_expr

print(f"\nচূড়ান্ত ভ্যালু: {expr}  (টাইপ: {type_of(expr)})")
assert expr == ('num', 20)
print("সব ধাপে Progress ও Preservation ধরে রাখা হয়েছে -- (2+3)*4 নিরাপদে 20-এ এভালুয়েট হয়েছে।\n")


print("=== ইচ্ছাকৃত আনসাউন্ড 'cast' রুল -- Preservation লঙ্ঘন ধরা ===")
cast_expr = ('cast', ('num', 7))
t_before = type_of(cast_expr)
print(f"'cast' নিয়মের naive স্ট্যাটিক টাইপ: {t_before}   (এই দাবিটি টাইপ চেকার যাচাই ছাড়াই মেনে নিয়েছে!)")

new_expr, _ = step(cast_expr)
t_after = type_of(new_expr)
print(f"এভালুয়েশনের পর প্রকৃত এক্সপ্রেশন: {new_expr}   প্রকৃত টাইপ: {t_after}")

if t_before != t_after:
    print(f"\n>>> SOUNDNESS ভায়োলেশন ধরা পড়েছে! Preservation দাবি করে টাইপ '{t_before}' থাকা উচিত ছিল, "
          f"কিন্তু এভালুয়েশনের পর প্রকৃত টাইপ '{t_after}' -- 'cast' নিয়মটি আনসাউন্ড, ঠিক যেমনটা ইচ্ছাকৃতভাবে বানানো হয়েছিল।")
else:
    print("(এটা প্রিন্ট হওয়ার কথা না)")