from __future__ import barry_as_FLUFL
from collections.abc import Callable
from dataclasses import dataclass, field
import functools
import typing, types

@dataclass
class UpperIdent:
    name: str
    def __repr__(self) -> str:
        return self.name

@dataclass
class LowerIdent:
    name: str
    def __repr__(self) -> str:
        return self.name

type Token = UpperIdent | LowerIdent  | typing.Literal["-", ">", "<>", "<"]
type TokenTree = list[Token | TokenTree]

def bracketize(p: Proxy, constraints: types.UnionType | type) -> TokenTree:
    return unpython(p) if isinstance(p, constraints) else [unpython(p)]

def unpython(tree: Proxy) -> TokenTree:
    match tree:
        case Ident(name):
            if name.istitle():
                return [UpperIdent(name)]
            else:
                return [LowerIdent(name)]
        case Neg(inner):
            return ["-", *bracketize(inner, Ident | Neg)]
        case xenia(left, right):
            return [*bracketize(left, Ident | Neg | xenia), "-", *bracketize(right, Ident | Neg)]
        case Compare(prefix, last):
            return [
                tok for p, op in prefix for tok in [*bracketize(p, Ident | Neg | xenia), op]
            ] + bracketize(last, Ident | Neg | xenia)
        case other:
            raise RuntimeError("Unreachable")

@dataclass
class UnboundTypeNode:
    name: str
    def __repr__(self) -> str:
        return self.name

@dataclass
class ConcreteTypeNode:
    name: str
    params: list[TypeNode]
    def __repr__(self) -> str:
        # technically too conservative with parenthesization
        return " <> ".join([self.name] + [parenthesize(t, UnboundTypeNode, hack=True) for t in self.params])

@dataclass
class FunctionTypeNode:
    left: TypeNode
    right: TypeNode
    def __repr__(self) -> str:
        left = parenthesize(self.left, UnboundTypeNode | ConcreteTypeNode)
        right = parenthesize(self.right, UnboundTypeNode | ConcreteTypeNode | FunctionTypeNode)
        return f"{left} > {right}"

type TypeNode = UnboundTypeNode | ConcreteTypeNode | FunctionTypeNode

def parse_type(tree: TokenTree, lazy: bool = False, variant: bool = False) -> tuple[TypeNode, int]:
    consumed = 0
    match tree[consumed]:
        case [*wrapped]:
            consumed += 1
            t, n = parse_type(wrapped)
            head = t
        case LowerIdent(name):
            consumed += 1
            head = UnboundTypeNode(name)
        case UpperIdent(name):
            consumed += 1
            head = ConcreteTypeNode(name, [])
        case other:
            raise SyntaxError(f"Unexpected token {other} in type")
    while tree[consumed:] and not lazy:
        match tree[consumed]:
            case "<>":
                consumed += 1
                t, n = parse_type(tree[consumed:], lazy=True)
                consumed += n
                match head:
                    case UnboundTypeNode(name):
                        raise SyntaxError("Higher-kinded types are unsupported.")
                    case FunctionTypeNode(left, right):
                        raise SyntaxError("Function type received unexpected parameter")
                    case ConcreteTypeNode(name, params):
                        params.append(t)
            case ">":
                consumed += 1
                t, n = parse_type(tree[consumed:])
                consumed += n
                return FunctionTypeNode(head, t), consumed
            case "-" if variant:
                return head, consumed
            case other:
                raise SyntaxError(f"Unsupported operation {other} in type context")
    return head, consumed

@dataclass
class DataNode:
    params: list[UnboundTypeNode]
    variants: list[ConcreteTypeNode]
    def __repr__(self) -> str:
        ps = "".join(f"{p} > " for p in self.params)
        vs = " ".join(f"-{v}" for v in self.variants)
        return ps + vs

@dataclass
class TypeAliasNode:
    params: list[UnboundTypeNode]
    type: TypeNode
    def __repr__(self) -> str:
        return "".join(f"{p} > " for p in self.params) + str(self.type)

type TypeImplNode = DataNode | TypeAliasNode

def parse_type_impl(tree: TokenTree) -> tuple[TypeImplNode, int]:
    consumed = 0
    match tree[consumed]:
        case [*wrapped]:
            consumed += 1
            t, n = parse_type_impl(wrapped)
            return t, consumed
        case LowerIdent(name):
            # type parameters for type alias or data type
            raise SyntaxError("Generic types are currently unsupported.")
        case UpperIdent(name):
            # parameterless type alias
            t, n = parse_type(tree[consumed:])
            consumed += n
            return TypeAliasNode([], t), consumed
        case "-":
            # parameterless data type
            variants = []
            while len(tree[consumed:]) > 0 and tree[consumed] == "-":
                consumed += 1
                t, n = parse_type(tree[consumed:], variant=True)
                consumed += n
                if not isinstance(t, ConcreteTypeNode):
                    raise SyntaxError("Unexpected type in data type variant")
                variants.append(t)
            return DataNode([], variants), consumed
        case other:
            raise SyntaxError(f"Unexpected token {other} in data type definition")

@dataclass(unsafe_hash=True)
class VarNode:
    name: str
    def __repr__(self) -> str:
        return f"[{self.name}]"

@dataclass(unsafe_hash=True)
class ConstructorNode:
    name: str
    def __repr__(self) -> str:
        return f"[{self.name}]"

@dataclass(unsafe_hash=True)
class ApplyNode:
    left: ExprNode
    right: ExprNode
    def __repr__(self) -> str:
        left = parenthesize(self.left, VarNode | ConstructorNode | ApplyNode)
        right = parenthesize(self.right, VarNode | ConstructorNode)
        return f"[{left} <> {right}]"

@dataclass(unsafe_hash=True)
class ApplyRightNode:
    left: ExprNode
    right: ExprNode
    def __repr__(self) -> str:
        left = parenthesize(self.left, VarNode | ConstructorNode)
        return f"[{left} < {self.right}]"

@dataclass(unsafe_hash=True)
class LambdaNode:
    param: VarNode
    body: ExprNode
    def __repr__(self) -> str:
        left = parenthesize(self.param, VarNode | ConstructorNode)
        return f"[{left} > {self.body}]"

@dataclass(unsafe_hash=True)
class ArmNode:
    pattern: PatternNode
    body: ExprNode
    def __repr__(self) -> str:
        return f"{self.pattern} > {self.body}"

@dataclass(unsafe_hash=True)
class DestructureNode:
    name: str
    def __repr__(self) -> str:
        return self.name

@dataclass(unsafe_hash=True)
class CatchAllNode:
    name: str
    def __repr__(self) -> str:
        return self.name

@dataclass(unsafe_hash=True)
class CompositePatternNode:
    left: PatternNode
    right: PatternNode
    def __repr__(self) -> str:
        left = parenthesize(self.left, DestructureNode | CatchAllNode | CompositePatternNode)
        right = parenthesize(self.right, DestructureNode | CatchAllNode)
        return f"{left} <> {right}"

type PatternNode = DestructureNode | CatchAllNode | CompositePatternNode

@dataclass(unsafe_hash=True)
class LambdaCaseNode:
    depth: int
    arms: tuple[ArmNode, ...]
    def __repr__(self) -> str:
        return "[" + " ".join(f"{'-' * self.depth}{arm}" for arm in self.arms) + "]"

type ExprNode = VarNode | ConstructorNode | ApplyNode | ApplyRightNode | LambdaNode | LambdaCaseNode

def parse_pattern(tree: TokenTree) -> tuple[PatternNode, int]:
    consumed = 0
    applications = []
    sequence = []
    def apply(p: PatternNode):
        if applications:
            sequence.append(CompositePatternNode(sequence.pop(), p))
            applications.pop()
        else:
            sequence.append(p)
    while tree[consumed:]:
        match tree[consumed]:
            case [*wrapped]:
                t, n = parse_pattern(wrapped)
                consumed += 1
                apply(t)
            case UpperIdent(name):
                consumed += 1
                apply(DestructureNode(name))
            case LowerIdent(name):
                consumed += 1
                apply(CatchAllNode(name))
            case other:
                raise SyntaxError(f"Unexpected token {other} in pattern")
        match tree[consumed]:
            case "<>":
                consumed += 1
                applications.append("<>")
            case ">":
                consumed += 1
                return sequence[0], consumed
            case other:
                raise SyntaxError(f"Unexpected token {other} in pattern")
    raise SyntaxError("Unexpected end of tokens while parsing pattern")

def parse_expr(tree: TokenTree) -> tuple[ExprNode, int]:
    ops = []
    vars = []
    consumed = 0
    def apply(t: ExprNode):
        if ops and ops[-1] == "<>":
            vars.append(ApplyNode(vars.pop(), t))
            ops.pop()
        else:
            vars.append(t)
    operator = False
    while tree[consumed:]:
        if not operator:
            match tree[consumed]:
                case [*wrapped]:
                    t, n = parse_expr(wrapped)
                    consumed += 1
                    apply(t)
                    operator = True
                case UpperIdent(name):
                    consumed += 1
                    apply(ConstructorNode(name))
                    operator = True
                case LowerIdent(name):
                    consumed += 1
                    apply(VarNode(name))
                    operator = True
                case "-":
                    consumed += 1
                    depth = 1
                    while tree[consumed:] and tree[consumed] == "-":
                        depth += 1
                        consumed += 1
                    # in introducing position
                    ops.append([depth, []])
                    p, n = parse_pattern(tree[consumed:])
                    consumed += n
                    ops[-1][1].append(p)
                case other:
                    raise SyntaxError(f"Unexpected token {other} in expression")
        else:
            match tree[consumed]:
                case "<>" | "<" | ">" as op:
                    consumed += 1
                    ops.append(op)
                    operator = False
                case "-":
                    consumed += 1
                    depth = 1
                    while tree[consumed:] and tree[consumed] == "-":
                        depth += 1
                        consumed += 1
                    # pop until a matching case
                    while ops and not (isinstance(ops[-1], list) and ops[-1][0] == depth):
                        op = ops.pop()
                        match op:
                            case ">":
                                arg = vars.pop()
                                param = vars.pop()
                                if not isinstance(param, VarNode):
                                    raise SyntaxError("Lambdas can only take simple parameters")
                                vars.append(LambdaNode(param, arg))
                            case "<":
                                fn = vars.pop()
                                arg = vars.pop()
                                vars.append(ApplyRightNode(arg, fn))
                            case "<>":
                                raise SyntaxError("Unexpected <> while collapsing expression stack, this should be unreachable?")
                            case [d, list(arms)]:
                                bodies: list[ExprNode] = []
                                for _ in range(len(arms)):
                                    bodies.insert(0, vars.pop())
                                comp = []
                                for arm, body in zip(arms, bodies):
                                    comp.append(ArmNode(arm, body))
                                vars.append(LambdaCaseNode(d, tuple(comp)))
                    if ops and isinstance(ops[-1], list) and ops[-1][0] == depth:
                        p, n = parse_pattern(tree[consumed:])
                        consumed += n
                        ops[-1][1].append(p)
                        operator = False
                    else:
                        raise SyntaxError(f"Unknown variant with depth {depth} ({depth * '-'})")
                case other:
                    raise SyntaxError(f"Unexpected token {other} in expression")
    # final pops
    while ops:
        op = ops.pop()
        match op:
            case ">":
                arg = vars.pop()
                param = vars.pop()
                if not isinstance(param, VarNode):
                    raise SyntaxError("Lambdas can only take simple parameters")
                vars.append(LambdaNode(param, arg))
            case "<":
                fn = vars.pop()
                arg = vars.pop()
                vars.append(ApplyRightNode(arg, fn))
            case "<>":
                raise SyntaxError("Unexpected <> while collapsing expression stack, this should be unreachable?")
            case [d, list(arms)]:
                bodies2: list[ExprNode] = []
                for _ in range(len(arms)):
                    bodies2.insert(0, vars.pop())
                comp = []
                for arm, body in zip(arms, bodies2):
                    comp.append(ArmNode(arm, body))
                vars.append(LambdaCaseNode(d, tuple(comp)))
    return vars[0], consumed

@dataclass
class DataDeclarationNode:
    name: str
    decl: DataNode
    def __repr__(self) -> str:
        return f"** {self.name} = {self.decl},"

@dataclass
class TypeAliasDeclarationNode:
    name: str
    alias: TypeAliasNode
    def __repr__(self) -> str:
        return f"** {self.name} = {self.alias},"

@dataclass
class ValueDeclarationNode:
    name: str
    type: TypeNode | None
    value: ExprNode
    def __repr__(self) -> str:
        if self.type is None:
            return f"{self.name}: <inferred> = {self.value},"
        else:
            return f"{self.name}: {self.type} = {self.value},"

type DeclarationNode = DataDeclarationNode | TypeAliasDeclarationNode | ValueDeclarationNode

@dataclass
class Data:
    constructor: str
    values: list[Value]
    closure: dict[str, Value]
    def __repr__(self) -> str:
        return f"{self.constructor}{''.join(f" <> ({value})" for value in self.values)}"

@dataclass
class Construct:
    name: str
    remaining: int
    values: list[Value]
    closure: dict[str, Value]
    def __repr__(self) -> str:
        return f"{self.name}{''.join(f" <> ({value})" for value in self.values)}{''.join(" <> _" for _ in range(self.remaining))}"

@dataclass
class Function:
    param: str
    body: ExprNode
    closure: dict[str, Value]
    def __repr__(self) -> str:
        return f"{self.param} > {self.body}"

@dataclass
class Thunk:
    body: ExprNode
    closure: dict[str, Value]
    evaluated: Value | None = None
    def __repr__(self) -> str:
        return f"{self.evaluated}" if self.evaluated is not None else f"{self.body}"

@dataclass
class Cases:
    arms: list[ArmNode]
    closure: dict[str, Value]
    def __repr__(self) -> str:
        return f"{self.arms}"

type Value = Thunk | Data | Function | Cases | Construct

@dataclass(unsafe_hash=True)
class DataT:
    name: str

@dataclass
class FuncT:
    left: T
    right: T

type T = DataT | FuncT

class Program:
    def __init__(self, declarations: list[DeclarationNode]) -> None:
        self.dots = 0
        self.type_env: dict[str, T] = {}
        self.datas: set[DataT] = set()
        self.constructors: dict[str, ConcreteTypeNode] = {}
        self.aliases: dict[str, TypeAliasNode] = {}
        self.globals: dict[str, Value] = {}
        for decl in declarations:
            match decl:
                case DataDeclarationNode(name, data):
                    dt = DataT(name)
                    if dt in self.datas:
                        raise TypeError("Type names must be unique")
                    self.datas.add(dt)
                    for c in data.variants:
                        if c.name in self.constructors:
                            raise TypeError("Constructors must currently be unique")
                        self.constructors[c.name] = c
                        if len(c.params) == 0:
                            self.globals[c.name] = Data(c.name, [], {})
                        else:
                            self.globals[c.name] = Construct(c.name, len(c.params), [], {})
                case TypeAliasDeclarationNode(name, alias):
                    self.aliases[name] = alias
                case ValueDeclarationNode(name, type, value):
                    self.globals[name] = Thunk(value, {})

    def construct_type_names(self):
        # form dependency tree
        tree = []
        resolved: dict[str, T] = {}
        for aname, alias in self.aliases.items():
            params = alias.params
            match alias.type:
                case UnboundTypeNode(name):
                    if name not in params:
                        raise TypeError("Undefined generic type in type alias")
                    # todo handle generic types
                case ConcreteTypeNode(name, params):
                    # todo handle generic types
                    if name in self.aliases:
                        # raise RuntimeError("Aliases to other aliases are still unimplemented")
                        pass
                    else:
                        t = DataT(name)
                        resolved[aname] = t
                case FunctionTypeNode(left, right):
                    raise RuntimeError("Aliases to function types are still unimplemented")
        self.type_env = resolved | {d.name: d for d in self.datas}

    '''



 []
(x -> (y -> x)) <> z
       [x]  [x,y]
 [x,y]

apply ., .
eval left (x->.), .
bind (x=.->.)



    '''

    def possible_binds(self, pattern: PatternNode) -> set[str]:
        match pattern:
            case CatchAllNode(name):
                return {name}
            case DestructureNode(name):
                return set()
            case CompositePatternNode(left, right):
                return self.possible_binds(left) | self.possible_binds(right)

    @functools.lru_cache
    def needed_vars(self, expr: ExprNode) -> set[str]:
        match expr:
            case VarNode(name):
                if name in self.globals:
                    return set()
                else:
                    return {name}
            case ConstructorNode():
                return set()
            case ApplyNode(left, right) | ApplyRightNode(left, right):
                return self.needed_vars(left) | self.needed_vars(right)
            case LambdaNode(param, body):
                return self.needed_vars(body) - {param.name}
            case LambdaCaseNode(depth, arms):
                total = set()
                for arm in arms:
                    binds = self.possible_binds(arm.pattern)
                    total |= self.needed_vars(arm.body) - binds
                return total
            case other:
                raise TypeError(f"unexpected {other}")

    def resolved(self, scope: dict[str, Value], thunk: Thunk) -> Value:
        if thunk.evaluated is not None:
            return thunk.evaluated
        else:
            eval = self.evaluate(scope | thunk.closure, thunk.body)
            if isinstance(eval, Thunk):
                final = self.resolved(scope | thunk.closure | eval.closure, eval)
                self.dots += 1
                if self.dots % 10000 == 0:
                    print(".", end="", flush=True)
                thunk.evaluated = final
                thunk.closure = {}
            else:
                self.dots += 1
                if self.dots % 10000 == 0:
                    print(".", end="", flush=True)
                thunk.evaluated = eval
                thunk.closure = {}
            return thunk.evaluated

    def evaluate(self, scope: dict[str, Value], expr: ExprNode) -> Value:
        match expr:
            case VarNode(name):
                if name in scope:
                    return scope[name]
                elif name in self.globals:
                    return self.globals[name]
                else:
                    raise TypeError(f"Undefined variable {name}")
            case ConstructorNode(name):
                if name in self.globals:
                    return self.globals[name]
                else:
                    raise TypeError(f"Undefined type constructor {name}")
            case ApplyNode(left, right) | ApplyRightNode(left, right):
                left = self.evaluate(scope, left)
                if isinstance(left, Thunk):
                    left = self.resolved(scope, left)
                match left:
                    case Data(constructor, values):
                        raise TypeError("Data is not callable")
                    case Function(param, body, closure):
                        right = Thunk(right, {k: v for k, v in (scope | closure).items() if k in self.needed_vars(right)})
                        fcall = self.evaluate(scope | closure | {param: right}, body)
                        return fcall
                    case Cases(arms, closure):
                        right = Thunk(right, {k: v for k, v in (scope | closure).items() if k in self.needed_vars(right)})
                        for arm in arms:
                            res = self.bind(scope | closure, arm.pattern, right)
                            if res is not None:
                                right, binds = res
                                evaluated = self.evaluate(scope | closure | binds, arm.body)
                                return evaluated
                        raise TypeError("Match not exhaustive")
                    case Construct(name, remaining, values, closure):
                        if remaining == 1:
                            needed = {k: v for k, v in (scope | closure).items() if k in self.needed_vars(right)}
                            return Data(name, [*values, Thunk(right, needed)], needed)
                        else:
                            needed = {k: v for k, v in (scope | closure).items() if k in self.needed_vars(right)}
                            return Construct(name, remaining - 1, [*values, Thunk(right, needed)], needed)
                    case other:
                        raise RuntimeError(f"Unexpected value {other}")
            case LambdaNode(param, body):
                return Function(param.name, body, {k: v for k, v in scope.items() if k in self.needed_vars(body)})
            case LambdaCaseNode(depth, arms) as lc:
                return Cases(arms, {k: v for k, v in scope.items() if k in self.needed_vars(lc)})
            case other:
                raise RuntimeError(f"Unexpected expression {other}")

    def bind(self, scope: dict[str, Value], pattern: PatternNode, value: Value) -> tuple[Value, dict[str, Value]] | None:
        match pattern:
            case CatchAllNode(name):
                return value, {name: value}
            case DestructureNode(name):
                if isinstance(value, Thunk):
                    value = self.resolved(scope, value)
                if not isinstance(value, Data):
                    raise TypeError("Matched value must be a data type")
                if value.constructor == name:
                    if len(value.values) == 0:
                        return value, {}
                    else:
                        raise TypeError("Some data fields were ignored")
                else:
                    return None
            case CompositePatternNode(left, right):
                if isinstance(value, Thunk):
                    value = self.resolved(scope, value)
                if not isinstance(value, Data):
                    raise TypeError("Matched value must be a data type")
                # ((A b) c) d
                res = self.bind(scope, left, Data(value.constructor, value.values[:-1], value.closure))
                if res is None:
                    return None
                _, bl = res
                val = value.values[-1]
                res = self.bind(scope, right, val)
                if res is None:
                    return None
                _, br = res
                return value, bl | br

    def reify(self, scope: dict[str, Value], value: Value):
        match value:
            case Function() | Cases() | Construct():
                return value
            case Data(constructor, values, closure):
                vals = [self.reify(scope, val) for val in values]
                return Data(constructor, vals, closure)
            case Thunk(body, closure, evaluated) as thunk:
                eval = self.evaluate(scope | closure, body)
                thunk.evaluated = self.reify(scope | closure, eval)
                return thunk.evaluated

    def run(self):
        self.construct_type_names()
        # self.type_check() not yet implemented
        eval = self.reify({}, self.globals["main"])
        print("=", eval)
'''

defs: dict[str, Value]

Value = Data | Thunk

Match =
Function = param * thunk
Data = constructor * fields
Thunk = (env -> result) | result



'''

show_generations = False
debug = False
class Meta(type):
    def __new__(mcls, name, bases, ns):
        if ns.get('__doc__') <> "I love you":
            return super().__new__(mcls, name, bases, ns)
        defs = ns['__type_params__']
        parsed: list[DeclarationNode] = []
        for defn in defs:
            fns = [defn.evaluate_default]
            resolved: list[Proxy] = []
            if isinstance(defn, typing.TypeVar) and defn.evaluate_bound is not None:
                fns.append(defn.evaluate_bound)
            for fn in fns:
                for closure in fn.__closure__ or []:
                    if not isinstance(closure.cell_contents, Ident):
                        closure.cell_contents = Ident(closure.cell_contents.__name__)
                for key in ["set", "any", "all", "map", "list", "min", "max"]: # todo: be more rigorous
                    fn.__globals__[key] = Ident(key)
                sweep_count = 0
                original_snapshots = []
                global false_index
                false_index = -1
                while True:
                    try:
                        snapshots.clear()
                        built_value = fn()
                        original_snapshots = snapshots.copy()
                        sweep_count = len(snapshots)
                        if debug:
                            print("1" * sweep_count or "-", defn.__name__, "::", snapshots, "::", built_value)
                        break
                    except NameError as e:
                        fn.__globals__[e.name] = Ident(e.name or "")

                output_locations = {}
                dependencies = []
                for sweep_index in range(sweep_count):
                    false_index = sweep_index
                    snapshots.clear()
                    value = fn()
                    if debug:
                        print(
                            "1" * sweep_index + "0" + "1" * (len(snapshots) - sweep_index - 1) + "-" * (sweep_count - len(snapshots)),
                            defn.__name__, "::", snapshots, "::", value
                        )
                    location = value.index(snapshots[sweep_index])
                    if location is not None:
                        output_locations.setdefault(location, []).append(sweep_index)
                    else:
                        for i, snap in enumerate(snapshots[sweep_index + 1:], start=sweep_index + 1):
                            # account for calls that were skipped in between
                            i += len(original_snapshots) - len(snapshots)
                            location = snap.index(snapshots[sweep_index])
                            if location is not None:
                                dependencies.append((sweep_index, i, location))
                                break

                for source, target, location in dependencies: # todo: evaluate in correct topological order?
                    val = original_snapshots[target].get(location)
                    prefix = [piece for piece in original_snapshots[source].prefix]
                    prefix.extend(val.prefix)
                    last = val.last
                    val.reconstruct(prefix, last)

                for location, indices in sorted(output_locations.items(), reverse=True):
                    val = built_value.get(location)
                    prefix = [piece for index in indices for piece in original_snapshots[index].prefix]
                    prefix.extend(val.prefix)
                    last = val.last
                    val.reconstruct(prefix, last)
                resolved.append(built_value)
            if isinstance(defn, typing.ParamSpec):
                impl, consumed = parse_type_impl(unpython(resolved[0]))
                if isinstance(impl, TypeAliasNode):
                    parsed.append(TypeAliasDeclarationNode(defn.__name__, impl))
                else:
                    parsed.append(DataDeclarationNode(defn.__name__, impl))
            else:
                if len(resolved) == 2:
                    type, consumed = parse_type(unpython(resolved[1]))
                    expr, consumed2 = parse_expr(unpython(resolved[0]))
                    parsed.append(ValueDeclarationNode(defn.__name__, type, expr))
                else:
                    expr, consumed = parse_expr(unpython(resolved[0]))
                    parsed.append(ValueDeclarationNode(defn.__name__, None, expr))
        #print(*parsed, sep="\n")
        prog = Program(parsed)
        prog.run()

@dataclass()
class Proxy:
    generation: int = field(init=False, default_factory = lambda: len(snapshots))

    def __neg__(self):
        return Neg(self)

    def __sub__(self, other):
        return xenia(self, other)

    def __gt__(self, other):
        return Compare([(self, ">")], other)

    def __lt__(self, other):
        return Compare([(self, "<")], other)

    def __ne__(self, value): # type: ignore
        return Compare([(self, "<>")], value)

    def __bool__(self):
        result = not (len(snapshots) == false_index)
        snapshots.append(self)
        return result

    @property
    def children(self) -> list[Proxy]:
        return []

    def get(self, index: tuple[int, ...]) -> Proxy | None:
        if index == ():
            return self
        if 0 <= index[0] < len(self.children):
            return self.children[index[0]].get(index[1:])

    def index_where(self, fn: Callable[[Proxy], bool]) -> tuple[int, ...] | None:
        if fn(self):
            return ()
        for i, child in enumerate(self.children):
            result = child.index_where(fn)
            if result is not None:
                return (i, *result)

    def index(self, node: Proxy) -> tuple[int, ...] | None:
        return self.index_where(lambda p: p is node)

    @property
    def gen(self):
        return f"[{self.generation}]" * show_generations

def parenthesize(x: object, constraints: types.UnionType | type, hack = False) -> str:
    return (
        f"{x}" if isinstance(x, constraints)
        or (hack and isinstance(x, ConcreteTypeNode) and len(x.params) == 0)
        else f"({x})"
    )

@dataclass
class Ident(Proxy):
    value: str
    def __repr__(self) -> str:
        return f"{self.value}{self.gen}"

@dataclass
class Neg(Proxy):
    inner: Proxy
    @property
    def children(self) -> list[Proxy]:
        return [self.inner]
    def __repr__(self) -> str:
        inner = parenthesize(self.inner, Ident | Neg)
        return f"-{self.gen}{inner}"

@dataclass
class xenia(Proxy):
    left: Proxy
    right: Proxy
    @property
    def children(self) -> list[Proxy]:
        return [self.left, self.right]
    def __repr__(self) -> str:
        left = parenthesize(self.left, Ident | Neg | xenia)
        right = parenthesize(self.right, Ident | Neg )
        return f"{left} -{self.gen} {right}"

type Op = typing.Literal["<>", ">", "<"]

@dataclass
class Compare(Proxy):
    prefix: list[tuple[Proxy, Op]]
    last: Proxy
    @property
    def children(self) -> list[Proxy]:
        return [*[p for p, _ in self.prefix], self.last]
    def __repr__(self) -> str:
        rest = "".join([f"{
            parenthesize(x, Ident | Neg | xenia)
        } {op}{self.gen} " for x, op in self.prefix])
        return f"{rest}{parenthesize(self.last, Ident | Neg | xenia)}"

    def reconstruct(self, prefix: list[tuple[Proxy, Op]], last: Proxy):
        self.prefix = prefix
        self.last = last

snapshots: list[Proxy] = []
false_index = -1

class Base(metaclass=Meta):
    pass

import sys
sys.setrecursionlimit((1 << 31) - 1)
sys.modules[__name__] = Base