SIC evaluator (so symmetrical) {untested}

sic.py

import itertools

from dataclasses import dataclass


type Name = int

name = itertools.count()


type Term = Pos | Neg

type Pos = Var | Nil | Lam | Sup

type Neg = Sub | Era | App | Dup


@dataclass(frozen=True)
class Var:
    nam: Name


@dataclass(frozen=True)
class Sub:
    nam: Name


@dataclass(frozen=True)
class Nil:
    pass


@dataclass(frozen=True)
class Era:
    pass


@dataclass(frozen=True)
class Lam:
    bnd: Neg
    bod: Pos


@dataclass(frozen=True)
class App:
    arg: Pos
    ret: Neg


@dataclass(frozen=True)
class Dup:
    dp0: Neg
    dp1: Neg


@dataclass(frozen=True)
class Sup:
    sp0: Pos
    sp1: Pos


def show(term: Term, vars: dict[Name, Pos] = {}, subs: dict[Name, Neg] = {}) -> str:
    match term:
        case Var(nam):
            if nam in vars:
                return f"{show(vars[nam], vars, subs)}"
            else:
                return f"+{nam}"
        case Sub(nam):
            if nam in subs:
                return f"{show(subs[nam], vars, subs)}"
            else:
                return f"-{nam}"
        case Nil():
            return f"+_"
        case Era():
            return f"-_"
        case Lam(bnd, bod):
            return f"+({show(bnd, vars, subs)} {show(bod, vars, subs)})"
        case App(arg, ret):
            return f"-({show(arg, vars, subs)} {show(ret, vars, subs)})"
        case Dup(dp0, dp1):
            return f"-{{{show(dp0, vars, subs)} {show(dp1, vars, subs)}}}"
        case Sup(sp0, sp1):
            return f"+{{{show(sp0, vars, subs)} {show(sp1, vars, subs)}}}"


def wire() -> tuple[Pos, Neg]:
    x = next(name)
    return Var(x), Sub(x)


type Rdx = tuple[Neg, Pos]


def reduce(book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> None:
    while book:
        match book.pop():
            case lhs, Var(nam):
                if nam in vars:
                    book.add((lhs, vars.pop(nam)))
                else:
                    subs[nam] = lhs
            case Sub(nam), rhs:
                if nam in subs:
                    book.add((subs.pop(nam), rhs))
                else:
                    vars[nam] = rhs

            case Era(), Nil():
                pass
            case Era(), Lam(bnd, bod):
                book.add((bnd, Nil()))
                book.add((Era(), bod))
            case Era(), Sup(sp0, sp1):
                book.add((Era(), sp0))
                book.add((Era(), sp1))

            case App(arg, ret), Nil():
                book.add((Era(), arg))
                book.add((ret, Nil()))
            case App(arg, ret), Lam(bnd, bod):
                book.add((bnd, arg))
                book.add((ret, bod))
            case App(arg, ret), Sup(sp0, sp1):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((Dup(an, bn), arg))
                book.add((ret, Sup(cp, dp)))
                book.add((App(ap, cn), sp0))
                book.add((App(bp, dn), sp1))

            case Dup(dp0, dp1), Nil():
                book.add((dp0, Nil()))
                book.add((dp1, Nil()))
            case Dup(dp0, dp1), Lam(bnd, bod):
                ap, an = wire()
                bp, bn = wire()
                cp, cn = wire()
                dp, dn = wire()
                book.add((dp0, Lam(an, bp)))
                book.add((dp1, Lam(cn, dp)))
                book.add((bnd, Sup(ap, cp)))
                book.add((Dup(bn, dn), bod))
            case Dup(dp0, dp1), Sup(sp0, sp1):
                book.add((dp0, sp0))
                book.add((dp1, sp1))


def print_state(root: Term, book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> None:
    print("ROOT:")
    print(f"{show(root, vars, subs)}")
    print()
    print("BOOK:")
    for lhs, rhs in book:
        print(f"{show(lhs, vars, subs)} ⋈ {show(rhs, vars, subs)}")


def print_reduction(root: Term, book: set[Rdx], vars: dict[Name, Pos], subs: dict[Name, Neg]) -> None:
    print("=" * 30)
    print("=", "ORIG".center(26), "=")
    print("=" * 30)
    print()

    print_state(root, book, vars, subs)

    print("\n" * 2)

    print("=" * 30)
    print("=", "REDUCED".center(26), "=")
    print("=" * 30)
    print()

    reduce(book, vars, subs)

    print_state(root, book, vars, subs)


def main() -> None:
    # (λa.(&b.a b) λc.c)   ->   λd.d

    ap, an = wire()
    bp, bn = wire()
    cp, cn = wire()
    rp, rn = wire()

    root: Term = rp

    book: set[Rdx] = {
        (App(Lam(cn, cp), rn), Lam(Dup(an, App(ap, bn)), bp)),
    }

    vars: dict[Name, Pos] = {}
    subs: dict[Name, Neg] = {}

    print_reduction(root, book, vars, subs)


main()