doc = """
# Ternary Decision Diagram (TDD) for Set-Theoretic Types in Elixir

## 1. Introduction

This document outlines the design and implementation of a Ternary Decision Diagram (TDD) based system for representing and manipulating set-theoretic types, inspired by systems like CDuce. The goal is to create a robust way to perform type checking, type inference, and other type-level computations for a rich set of datatypes, similar to those found in Elixir.

A TDD is a directed acyclic graph (DAG) used to represent a function `f(v1, v2, ..., vn) -> {true, false, dont_care}`. In our context, it represents a characteristic function for a type: given a value, the TDD determines if the value belongs to the type (`true`), does not belong (`false`), or if the specific predicates tested so far are insufficient or irrelevant for this particular type operation (`dont_care`).

The TDDs are kept **ordered** and **reduced** to ensure a canonical representation for each type, making type equivalence checks (and other operations) efficient.
-   **Ordered**: Variables (predicates) appear in the same fixed global order on all paths from the root to a terminal.
-   **Reduced**: Isomorphic subgraphs are merged (shared), and nodes whose children would make the test redundant under certain TDD algebra rules are eliminated or simplified.

## 2. Core TDD Structure and Operations

### 2.1. Nodes

There are two kinds of nodes:

1.  **Terminal Nodes**:
  *   `TRUE_TERMINAL` (ID: `1`): Represents the universal set (type `any`). A path ending here means the value (or part of it) satisfies the type constraints along that path.
  *   `FALSE_TERMINAL` (ID: `0`): Represents the empty set (type `none`). A path ending here means the value fails the type constraints.

2.  **Variable Nodes**:
  *   Represented as a tuple: `{variable_identifier, yes_child_id, no_child_id, dc_child_id}`.
  *   `variable_identifier`: A unique, globally ordered term identifying the predicate being tested at this node (e.g., "is the value an atom?", "is the integer value < 10?").
  *   `yes_child_id`: The ID of the next TDD node if the predicate is true.
  *   `no_child_id`: The ID of the next TDD node if the predicate is false.
  *   `dc_child_id` (Don't Care): The ID of the next TDD node if the predicate is irrelevant for the current type or operation. The semantic interpretation of `dc` is crucial and aligns with common TDD usage (e.g., for a union operation, `dc(A | B) = dc(A) | dc(B)`).

### 2.2. Node Management (`Tdd` module state)

The `Tdd` module maintains global state (currently via `Process.put/get` for simplicity, ideally a `GenServer`):

*   `@nodes`: A map from `node_tuple ({variable, yes_id, no_id, dc_id})` to `node_id`. This ensures that structurally identical nodes are shared (part of the "reduced" property).
*   `@node_by_id`: A map from `node_id` to its `node_tuple` or a terminal symbol (`:true_terminal`, `:false_terminal`).
*   `@next_id`: The next available integer ID for a new node.
*   `@op_cache`: A map for memoizing results of operations like `apply` (binary ops), `negate`, and `simplify_with_constraints`. Keys are typically `{{op_name, id1, id2}, result_id}` or `{{op_name, id1}, result_id}`.

### 2.3. Variable Ordering

A strict global total order of all possible `variable_identifier`s is essential. This is achieved by defining variable identifiers as Elixir tuples, which have a natural sort order.
The proposed structure for variable identifiers is:
`{category_integer, predicate_type_atom, specific_value_or_nested_id}`

Example categories:
*   `0`: Primary type discriminators (e.g., `is_atom`, `is_integer`, `is_list`).
*   `1`: Atom-specific predicates (e.g., `value == :foo`).
*   `2`: Integer-specific predicates (e.g., `value < 10`).
*   `4`: Tuple-specific predicates (e.g., `size == 2`, `element 0 has_type X`).
*   And so on for other types.

### 2.4. Core Operations

1.  **`make_node_raw(variable, yes_id, no_id, dc_id)`**:
  *   The fundamental private function for creating or retrieving unique structural nodes.
  *   Implements structural sharing via the `@nodes` table.
  *   Implements a basic reduction rule: if `yes_id == no_id == dc_id`, the node is redundant, and that common child ID is returned.

2.  **`check_assumptions_consistency(assumptions_map)`**:
  *   A private helper function crucial for semantic reduction.
  *   Takes a map `%{variable_id => value (true/false/:dc)}` representing current path assumptions.
  *   Returns `:consistent` or `:contradiction` based on predefined semantic rules of the type system (e.g., `is_atom=true` AND `is_tuple=true` is a contradiction).
  *   This function will be expanded as more types and predicates are added.

3.  **`simplify_with_constraints(tdd_id, assumptions_map)`**:
  *   A private, memoized, recursive function that takes a `tdd_id` and an `assumptions_map`.
  *   It produces a new `tdd_id` that is semantically equivalent to the input `tdd_id` under the given assumptions, but potentially simpler.
  *   **Crucial Behavior**: If `check_assumptions_consistency(assumptions_map)` returns `:contradiction` at any point, `simplify_with_constraints` immediately returns `@false_node_id`.
  *   If the TDD's variable is already in `assumptions_map`, it follows the constrained path.
  *   Otherwise, it recursively simplifies children, adding the current node's variable assignment to the assumptions for those deeper calls, and rebuilds the node using `make_node_raw`.

4.  **`apply_raw(op_name, op_lambda, u1_id, u2_id)`**:
  *   The private, memoized, recursive Shannon expansion algorithm for binary set operations (union, intersection).
  *   `op_lambda` defines the operation on terminal nodes.
  *   It selects the `top_var` based on the global variable order.
  *   Recursively calls `apply_raw` on the children.
  *   Uses `make_node_raw` to construct result nodes.
  *   This function computes the *structural* result of the operation.

5.  **Public API Operations (`sum/2`, `intersect/2`, `negate/1`)**:
  *   These functions orchestrate the operation:
      1.  Call the respective `_raw` version (e.g., `apply_raw` for `sum`/`intersect`, `negate_raw` for `negate`).
      2.  Take the `raw_result_id` from step 1.
      3.  Return `simplify_with_constraints(raw_result_id, %{})`. This final step ensures that all TDDs exposed through the public API are not only structurally canonical (via `make_node_raw` and `apply_raw`) but also *semantically canonical* (i.e., known impossible paths or contradictions are resolved to `@false_node_id`).

6.  **Type Constructors (e.g., `type_atom()`, `type_atom_literal(:foo)`)**:
  *   These public functions build the TDD for a specific type.
  *   They use `make_node_raw` to define the basic structure.
  *   They then return `simplify_with_constraints(raw_id, %{})` to ensure the constructed type is in its simplest semantic form.

7.  **`is_subtype(sub_id, super_id)`**:
  *   Defined as `simplify_with_constraints(intersect(sub_id, negate(super_id)), %{}) == @false_node_id`.
  *   Since `intersect` and `negate` now return semantically simplified TDDs, if `A ∩ ¬B` represents an empty set, the result of the intersection will be `@false_node_id`.

## 3. Datatype Representation Details

This section outlines how various Elixir-like datatypes are (or will be) represented using TDD variables and constructors. All constructors ensure the final TDD is passed through `simplify_with_constraints(raw_id, %{})`.

### 3.1. Atoms

*   **Variables**:
  *   `@v_is_atom = {0, :is_atom}`: Primary type check.
  *   `v_atom_eq_A = {1, :value, A}`: Checks if the atom's value is `A`. Order by `A`.
*   **Constructors**:
  *   `type_atom()`: Represents any atom. TDD: `make_node_raw(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)`.
  *   `type_atom_literal(val)`: Represents a specific atom. TDD: `make_node_raw(@v_is_atom, node_for_val_eq, @false_node_id, @false_node_id)` where `node_for_val_eq = make_node_raw(v_atom_eq_A, @true_node_id, @false_node_id, @false_node_id)`.
*   **Semantic Constraints for `check_assumptions_consistency`**:
  *   If `assumptions_map` contains `{{0, :is_atom}, true}` and `{{0, other_primary_type}, true}` -> contradiction.
  *   If `assumptions_map` contains `{{1, :value, A}, true}` and `{{1, :value, B}, true}` where `A != B` -> contradiction.

### 3.2. Tuples

*   **Variables**:
  *   `@v_is_tuple = {0, :is_tuple}`: Primary type check.
  *   `v_tuple_size_eq_N = {4, :size, N}`: Checks if tuple size is `N`. Order by `N`.
  *   `v_tuple_elem_I_PRED = {4, :element, Index_I, NESTED_PREDICATE_ID}`: Predicate for element at `Index_I`. `NESTED_PREDICATE_ID` is a variable from the global order, applied to the element. (e.g., `{4, :element, 0, {0, :is_atom}}` checks if element 0 is an atom). Order by `Index_I`, then by `NESTED_PREDICATE_ID`.
*   **Constructors**:
  *   `type_tuple()`: Any tuple.
  *   `type_empty_tuple()`: The tuple `{}`.
  *   `type_tuple_sized_any(size)`: Any tuple of a given size.
  *   `type_tuple_specific(element_type_ids_list)`: e.g., for `{atom(), integer()}`. This will involve creating nodes for size, then for each element, applying the TDD for that element's type.
*   **Semantic Constraints**:
  *   `is_tuple=true` vs. other primary types.
  *   If `{{4, :size, N}, true}` and `{{4, :size, M}, true}` where `N != M` -> contradiction.
  *   If `{{4, :size, N}, true}` and a predicate `{{4, :element, I, _}, _}` exists where `I >= N` -> potential contradiction or path simplification (element doesn't exist).

### 3.3. Integers (Next to Implement)

*   **Variables**:
  *   `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties).
  * INT_CAT variables (names of variables prefixed with `a b c` to force ordering 
    *   `v_int_lt_N = {INT_CAT, :alt, N}` (value < N).
    *   `v_int_eq_N = {INT_CAT, :beq, N}`.
    *   `v_int_gt_N = {INT_CAT, :cgt, N}` (value > N).
    *   *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).*
*   **Constructors**:
  *   `type_integer()`: Any integer.
  *   `type_int_eq(n)`: A specific integer value.
  *   `type_int_lt(n)`, `type_int_gt(n)`.
  *   `type_int_range(min, max, min_inclusive, max_inclusive)`: Integers within a specific range.
*   **Semantic Constraints**:
  *   `is_integer=true` vs. other primary types.
  *   `eq(N)` and `eq(M)` with `N != M` -> contradiction.
  *   `eq(N)` and `lt(M)` if `N >= M` -> contradiction.
  *   `eq(N)` and `gt(M)` if `N <= M` -> contradiction.
  *   `lt(N)` and `gt(M)` if `N <= M+1` (or `N <= M` if `gt` means `>=`) -> contradiction. (e.g., `x < 5` and `x > 4` has no integer solution).
  *   *Strategy for complex integer constraints*: Maintain a "current allowed interval" `[min_assumed, max_assumed]` based on `assumptions_map`. If this interval becomes empty or invalid, it's a contradiction. Each new integer assumption (`lt, gt, eq`) refines this interval.

### 3.4. Lists (Implemented)

*   **Variables**:
  *   `@v_is_list = {0, :is_list}`.
  *   `v_list_is_empty = {5, :is_empty}`.
  *   *If not empty*:
      *   `v_list_head_pred = {5, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head.
      *   `v_list_tail_pred = {5, :tail, NESTED_PREDICATE_ID_FOR_TAIL}`: Applies a global predicate (usually list predicates) to the tail.
*   **Constructors**:
  *   `type_list()`: Represents any list.
  *   `type_empty_list()`: Represents the empty list `[]`.
  *   `type_cons(head_type_id, tail_type_id)`: Represents a non-empty list `[H|T]` where `H` is of type `head_type_id` and `T` is of type `tail_type_id`.
*   **Semantic Constraints**:
  *   `is_list=true` vs. other primary types.
  *   If `is_empty=true`, any predicate on the `head` or `tail` is a contradiction.
  *   Recursive consistency checks on `head` and `tail` sub-types.

### 3.5. Strings & Binaries (Planned)

*   **Variables**:
  *   `@v_is_binary = {0, :is_binary}`.
  *   `@v_is_string = {0, :is_string}` (can be a check after `is_binary` or a distinct primary type if model demands).
  *   Size/length predicates: `v_binary_size_eq_N`, `v_string_length_eq_N`.
  *   Content predicates: `v_string_eq_S`, `v_string_prefix_P`, `v_string_suffix_S`, `v_string_matches_regex_R`.
*   **Semantic Constraints**: Size vs content (e.g., `size=1` and `prefix="foo"` is a contradiction). `eq(S1)` and `eq(S2)` if `S1 != S2`.

### 3.6. Maps (Planned - Complex)

*   **Variables**:
  *   `@v_is_map = {0, :is_map}`.
  *   `v_map_size_eq_N`.
  *   `v_map_has_key_K`: (K is a canonical representation of an Elixir term).
  *   *If `has_key_K` is true*:
      *   `v_map_key_K_value_VAR = {MAP_CAT, :key_value, K, NESTED_PREDICATE_ID}`: Applies a global predicate to the value associated with key K.
  *   For `%{pattern_key => pattern_value}` types:
      *   This requires careful thought. Might involve predicates like `v_map_all_keys_matching_TYPE_X_have_values_matching_TYPE_Y`.
*   **Semantic Constraints**: `is_map` vs. others. Size vs. `has_key` interactions. Contradictory type requirements for the same key's value.

### 3.7. Functions (Planned - Very Complex)

*   Representation of function types (`fun((Arg1Type, Arg2Type, ...) -> ReturnType)`) is a significant challenge for TDDs.
*   **Variables (Tentative)**:
  *   `@v_is_function = {0, :is_function}`.
  *   `v_fun_arity_eq_A`.
  *   Predicates for argument types at specific positions (e.g., `v_fun_arg_I_type_VAR`).
  *   Predicates for return type (e.g., `v_fun_return_type_VAR`).
*   Intersection and union of function types involve concepts like contravariance of arguments and covariance of return types. This may require specialized logic beyond simple TDD operations or a very elaborate variable scheme. Often, function types are handled with auxiliary structures in type systems.

## 4. Current Status & Next Steps

*   **Implemented**: Atoms, basic Tuples (any, empty, sized_any). Core TDD operations (`sum`, `intersect`, `negate`, `is_subtype`) with semantic simplification framework (`simplify_with_constraints` and `check_assumptions_consistency`).
*   **Passing Tests**: A suite of tests for atom/tuple interactions, unions, intersections, negations, and subtyping, including resolution of contradictions like `atom & tuple == none`.
*   **Next Immediate Step**: Implement **Integer types** as outlined in section 3.3. This will involve:
  1.  Defining integer-specific predicates and their global order.
  2.  Creating integer type constructors.
  3.  Significantly expanding `check_assumptions_consistency` to handle integer comparisons (`eq`, `lt`, `gt`) and their interactions.
  4.  Adding comprehensive tests for integers.

## 5. Future Considerations

*   **Performance**: For very large TDDs or complex types, the number of nodes and cache sizes can grow. Investigate optimizations if needed.
*   **Generality of `check_assumptions_consistency`**: Designing this to be easily extensible and correct for many interacting predicates is challenging. A rule-based system or a more abstract way to define predicate interactions might be beneficial.
*   **"Don't Care" (`dc`) branch semantics**: Ensure the `dc` branch is consistently and correctly handled in all operations, especially `simplify_with_constraints` if assumptions can make a variable "don't care". Currently, `simplify_with_constraints` assumes `true/false/:dc` values in the `assumptions_map` if a variable is already constrained.
*   **Type Inference**: Using the TDD operations to infer types or solve type constraints.
*   **Polymorphism**: Representing and operating on types with free type variables. Typically, free variables are treated as `any` or involve substitution before TDD construction.

This document provides a snapshot of the current TDD system and a roadmap for its extension. The core principle is the combination of structurally canonical ROBDDs (via `make_node_raw` and `apply_raw`) with a semantic simplification layer (`simplify_with_constraints`) that embeds knowledge of the type system's rules.
"""

defmodule Tdd.Core do
  @moduledoc """
  The core, semantically-unaware TDD graph engine.

  This module is responsible for:
  - Storing and managing a unique table of TDD nodes.
  - Providing a function `make_node/4` that creates nodes while ensuring
    structural sharing and basic reduction (redundant nodes).
  - Implementing a generic, structural `apply/4` algorithm for binary
    operations on TDDs.

  It knows nothing about what the variables (`{0, :is_atom}`, etc.) mean.
  """

  # --- Terminal Node IDs ---
  @false_node_id 0
  @true_node_id 1

  def true_id, do: @true_node_id
  def false_id, do: @false_node_id
  defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id

  def terminal_id?(id) when is_terminal_id(id), do: true
  def terminal_id?(_), do: false

  # --- State Management ---

  def init do
    Process.put(:tdd_nodes, %{})
    Process.put(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true})
    Process.put(:tdd_next_id, 2)
    Process.put(:tdd_op_cache, %{})
    :ok
  end

  defp get_state do
    %{
      nodes: Process.get(:tdd_nodes, %{}),
      node_by_id: Process.get(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true}),
      next_id: Process.get(:tdd_next_id, 2),
      op_cache: Process.get(:tdd_op_cache, %{})
    }
  end

  defp update_state(changes) do
    current_state = get_state()
    new_state = Map.merge(current_state, changes)
    Process.put(:tdd_nodes, new_state.nodes)
    Process.put(:tdd_node_by_id, new_state.node_by_id)
    Process.put(:tdd_next_id, new_state.next_id)
    Process.put(:tdd_op_cache, new_state.op_cache)
  end

  def clear_op_cache, do: Process.put(:tdd_op_cache, %{})

  # --- Public API for the Core Engine ---

  def get_node(id) when is_terminal_id(id), do: if(id == @true_node_id, do: true, else: false)
  def get_node(id), do: get_state().node_by_id[id]

  def get_op_cache(key), do: get_state().op_cache[key]

  def put_op_cache(key, value),
    do: update_state(%{op_cache: Map.put(get_state().op_cache, key, value)})

  @doc """
  Creates or retrieves a unique TDD node.
  This is the heart of structural canonicalization (the 'R' in ROBDD).
  """

  def make_node(variable, yes_id, no_id, dc_id) do
    # NEW, MORE POWERFUL REDUCTION RULE:
    # If the 'yes' and 'no' paths lead to the same result, the test on this
    # variable is redundant. The entire node can be replaced by that result.
    cond do
      yes_id == no_id ->
        yes_id

      yes_id == dc_id && no_id == dc_id ->
        yes_id

      true ->
        state = get_state()
        node_tuple = {variable, yes_id, no_id, dc_id}

        if Map.has_key?(state.nodes, node_tuple) do
          state.nodes[node_tuple]
        else
          new_id = state.next_id

          update_state(%{
            nodes: Map.put(state.nodes, node_tuple, new_id),
            node_by_id: Map.put(state.node_by_id, new_id, node_tuple),
            next_id: new_id + 1
          })

          new_id
        end
    end
  end

  @doc """
  The generic Shannon expansion algorithm for any binary operation.
  This is purely structural and relies on the caller (the semantic layer)
  to ensure the inputs and results are meaningful.
  """
  def apply(op_name, op_lambda, u1_id, u2_id) do
    state = get_state()
    cache_key = {op_name, Enum.sort([u1_id, u2_id])}

    cond do
      Map.has_key?(state.op_cache, cache_key) ->
        state.op_cache[cache_key]

      is_terminal_id(u1_id) && is_terminal_id(u2_id) ->
        res_terminal = op_lambda.(get_node(u1_id), get_node(u2_id))
        if res_terminal == true, do: @true_node_id, else: @false_node_id

      true ->
        u1_details = get_node(u1_id)
        u2_details = get_node(u2_id)

        result_id =
          cond do
            u1_details == true or u1_details == false ->
              {var2, y2, n2, d2} = u2_details
              res_y = apply(op_name, op_lambda, u1_id, y2)
              res_n = apply(op_name, op_lambda, u1_id, n2)
              res_d = apply(op_name, op_lambda, u1_id, d2)
              make_node(var2, res_y, res_n, res_d)

            u2_details == true or u2_details == false ->
              {var1, y1, n1, d1} = u1_details
              res_y = apply(op_name, op_lambda, y1, u2_id)
              res_n = apply(op_name, op_lambda, n1, u2_id)
              res_d = apply(op_name, op_lambda, d1, u2_id)
              make_node(var1, res_y, res_n, d1)

            true ->
              {var1, y1, n1, d1} = u1_details
              {var2, y2, n2, d2} = u2_details
              top_var = Enum.min([var1, var2])

              res_y =
                apply(
                  op_name,
                  op_lambda,
                  if(var1 == top_var, do: y1, else: u1_id),
                  if(var2 == top_var, do: y2, else: u2_id)
                )

              res_n =
                apply(
                  op_name,
                  op_lambda,
                  if(var1 == top_var, do: n1, else: u1_id),
                  if(var2 == top_var, do: n2, else: u2_id)
                )

              res_d =
                apply(
                  op_name,
                  op_lambda,
                  if(var1 == top_var, do: d1, else: u1_id),
                  if(var2 == top_var, do: d2, else: u2_id)
                )

              make_node(top_var, res_y, res_n, res_d)
          end

        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
        result_id
    end
  end
end

defmodule Tdd.PredicateLogic do
  @moduledoc "..."
  alias Tdd.Variables, as: V

  @primary_types [:is_atom, :is_tuple, :is_integer, :is_list]
  @primary_type_exclusivity_rules (for type <- @primary_types, into: %{} do
                                     antecedent = {{0, type}, true}

                                     consequents =
                                       for other_type <- @primary_types,
                                           other_type != type,
                                           do: {{{0, other_type}, false}}

                                     {antecedent, consequents}
                                   end)
  @rules @primary_type_exclusivity_rules

  def saturate(assumptions) do
    case apply_static_rules(assumptions) do
      {:ok, saturated_facts} -> final_check(saturated_facts)
      :contradiction -> :contradiction
      {:contradiction, _} -> :contradiction
    end
  end

  defp apply_static_rules(facts) do
    Enum.reduce(facts, {:ok, facts}, fn {var, val}, {status, acc_facts} ->
      if status == :contradiction do
        {:contradiction, %{}}
      else
        rules_for_fact = Map.get(@rules, {var, val}, [])

        # --- THE CORRECTED PATTERN MATCH IS HERE ---
        # The data is `{{{Var, Val}}}`. We need to match this shape.
        Enum.reduce_while(rules_for_fact, {:ok, acc_facts}, fn {{consequent_var, consequent_val}},
                                                               {_st, inner_facts} ->
          case Map.get(inner_facts, consequent_var) do
            nil -> {:cont, {:ok, Map.put(inner_facts, consequent_var, consequent_val)}}
            ^consequent_val -> {:cont, {:ok, inner_facts}}
            _ -> {:halt, {:contradiction, %{}}}
          end
        end)
      end
    end)
  end

  defp final_check(facts) do
    cond do
      check_atom_values(facts) == :contradiction -> :contradiction
      check_tuple_values(facts) == :contradiction -> :contradiction
      check_integer_ranges(facts) == :contradiction -> :contradiction
      check_list_structure(facts) == :contradiction -> :contradiction
      true -> {:ok, facts}
    end
  end

  defp check_atom_values(facts) do
    trues =
      Enum.reduce(facts, MapSet.new(), fn
        {{1, :value, atom_val}, true}, acc -> MapSet.put(acc, atom_val)
        _, acc -> acc
      end)

    if MapSet.size(trues) > 1, do: :contradiction, else: :ok
  end

  defp check_tuple_values(facts) do
    trues =
      Enum.reduce(facts, MapSet.new(), fn
        {{4, :size, size_val}, true}, acc -> MapSet.put(acc, size_val)
        _, acc -> acc
      end)

    if MapSet.size(trues) > 1, do: :contradiction, else: :ok
  end

  defp check_list_structure(facts) do
    is_assumed_empty = Map.get(facts, V.v_list_is_empty()) == true

    if is_assumed_empty do
      has_head_or_tail_pred =
        Enum.any?(facts, fn {var, _} ->
          case var do
            {5, :head, _} -> true
            {5, :tail, _} -> true
            _ -> false
          end
        end)

      if has_head_or_tail_pred, do: :contradiction, else: :ok
    else
      :ok
    end
  end

  # --- Integer Logic ---

  # THIS IS THE SINGLE, CORRECT DEFINITION TO USE
  defp check_integer_ranges(facts) do
    if facts[V.v_is_integer()] != true do
      :ok
    else
      if calculate_integer_interval(facts) == :contradiction, do: :contradiction, else: :ok
    end
  end

  @doc """
  A general-purpose reasoner that uses the main `saturate` function.
  It determines if a predicate is implied true or false by a set of constraints
  by checking if adding its opposite leads to a contradiction.
  """
  defp _reason_by_contradiction(predicate, constraints) do
    # Is `predicate` implied TRUE? (i.e., is `constraints AND NOT predicate` a contradiction?)
    cond do
      saturate(Map.put(constraints, predicate, false)) == :contradiction ->
        true

      # Is `predicate` implied FALSE? (i.e., is `constraints AND predicate` a contradiction?)
      saturate(Map.put(constraints, predicate, true)) == :contradiction ->
        false

      true ->
        :unknown
    end
  end

  @doc """
  Checks if a `predicate` is logically implied (or contradicted) by a
  set of `constraints`.
  """
  def check_implication(predicate, constraints) do
    case predicate do
      # --- NEW HANDLER for primary type predicates ---
      {0, _} ->
        _reason_by_contradiction(predicate, constraints)

      # --- EXISTING BASE CASES ---
      {1, :value, _} ->
        _atom_implication(predicate, constraints)

      {2, _, _} ->
        _integer_implication(predicate, constraints)

      {4, :size, _} ->
        _tuple_size_implication(predicate, constraints)

      # --- EXISTING RECURSIVE CASES ---
      {4, :element, index, inner_predicate} ->
        element_constraints =
          gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1))

        check_implication(inner_predicate, element_constraints)

      {5, :head, inner_predicate} ->
        head_constraints =
          gather_local_constraints(constraints, &match?({5, :head, _}, &1))

        check_implication(inner_predicate, head_constraints)

      {5, :tail, inner_predicate} ->
        tail_constraints =
          gather_local_constraints(constraints, &match?({5, :tail, _}, &1))

        check_implication(inner_predicate, tail_constraints)

      # --- DEFAULT CASE ---
      _ ->
        # We don't have specific reasoning logic for this predicate type.
        :unknown
    end
  end

  # ===================================================================
  # == PRIVATE HELPERS
  # ===================================================================

  # --- Constraint Isolation Helper ---

  @doc """
  Gathers, unwraps, and isolates constraints for a specific component.
  """
  defp gather_local_constraints(all_constraints, filter_fun) do
    for {var, bool_val} <- all_constraints,
        filter_fun.(var),
        into: %{} do
      # Unwrap the predicate for the local check.
      # e.g., from `{4, :element, 0, {2, :beq, 5}}` we want `{2, :beq, 5}`
      inner_predicate = elem(var, tuple_size(var) - 1)
      {inner_predicate, bool_val}
    end
  end

  # --- Base Case Reasoners ---

  # Reasoner for integer predicates.
  # Renamed from `check_integer_implication` to `_integer_implication` to denote it's a private helper.
  defp _integer_implication(predicate, constraints) do
    case calculate_integer_interval(constraints) do
      :contradiction ->
        # A contradiction implies anything.
        true

      {min_val, max_val} ->
        {_p_cat, p_type, p_val} = predicate

        cond do
          # The current interval [min, max] is a SUBSET of the predicate's interval
          (p_type == :alt and is_integer(max_val) and max_val < p_val) or
            (p_type == :cgt and is_integer(min_val) and min_val > p_val) or
              (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
            true

          # The current interval [min, max] is DISJOINT from the predicate's interval
          (p_type == :alt and is_integer(min_val) and min_val >= p_val) or
            (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
              (p_type == :beq and
                 ((is_integer(min_val) and min_val > p_val) or
                    (is_integer(max_val) and max_val < p_val))) ->
            false

          true ->
            :unknown
        end
    end
  end

  # Reasoner for atom predicates using Enum.reduce
  defp _atom_implication(predicate, constraints) do
    # The predicate we are testing, e.g., {{1, :value, :foo}, true}
    {{1, :value, p_val}, _} = {predicate, true}

    # Use Enum.reduce to find all atom values constrained to be true or false.
    {true_atoms, false_atoms} =
      Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
        # Match a constraint that an atom value MUST be true
        {{1, :value, val}, true}, {true_set, false_set} ->
          {MapSet.put(true_set, val), false_set}

        # Match a constraint that an atom value MUST be false
        {{1, :value, val}, false}, {true_set, false_set} ->
          {true_set, MapSet.put(false_set, val)}

        # Ignore any other kind of constraint
        _, acc ->
          acc
      end)

    cond do
      # If the predicate's value is explicitly known to be false.
      p_val in false_atoms ->
        false

      # If the predicate's value is explicitly known to be true.
      p_val in true_atoms ->
        true

      # If we know the value MUST be something else (and it's not our predicate's value).
      # e.g., constraints say the value is :bar, and we're checking for :foo.
      not Enum.empty?(true_atoms) and p_val not in true_atoms ->
        false

      # Otherwise, we don't have enough information.
      true ->
        :unknown
    end
  end

  # Reasoner for tuple size predicates using Enum.reduce
  defp _tuple_size_implication(predicate, constraints) do
    # The predicate we are testing, e.g., {{4, :size, 2}, true}
    {{4, :size, p_val}, _} = {predicate, true}

    {true_sizes, false_sizes} =
      Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
        {{4, :size, val}, true}, {true_set, false_set} ->
          {MapSet.put(true_set, val), false_set}

        {{4, :size, val}, false}, {true_set, false_set} ->
          {true_set, MapSet.put(false_set, val)}

        _, acc ->
          acc
      end)

    cond do
      # If the predicate's size is explicitly known to be false.
      p_val in false_sizes ->
        false

      # If the predicate's size is explicitly known to be true.
      p_val in true_sizes ->
        true

      # If we know the size MUST be something else.
      not Enum.empty?(true_sizes) and p_val not in true_sizes ->
        false

      # Otherwise, we don't know.
      true ->
        :unknown
    end
  end

  defp check_integer_implication(predicate, constraints) do
    if constraints[V.v_is_integer()] != true do
      :unknown
    else
      case calculate_integer_interval(constraints) do
        :contradiction ->
          true

        {min_val, max_val} ->
          {_p_cat, p_type, p_val} = predicate

          cond do
            (p_type == :alt and is_integer(max_val) and max_val < p_val) or
              (p_type == :cgt and is_integer(min_val) and min_val > p_val) or
                (p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
              true

            (p_type == :alt and is_integer(min_val) and min_val >= p_val) or
              (p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
                (p_type == :beq and
                   ((is_integer(min_val) and min_val > p_val) or
                      (is_integer(max_val) and max_val < p_val))) ->
              false

            true ->
              :unknown
          end
      end
    end
  end

  defp calculate_integer_interval(facts) do
    bounds =
      Enum.reduce(facts, %{eq: nil, min: nil, max: nil}, fn
        {var, true}, acc ->
          case var do
            {2, :beq, n} ->
              if(is_nil(acc.eq) or acc.eq == n, do: %{acc | eq: n}, else: %{acc | eq: :conflict})

            {2, :alt, n} ->
              %{acc | max: min_opt(acc.max, n - 1)}

            {2, :cgt, n} ->
              %{acc | min: max_opt(acc.min, n + 1)}

            _ ->
              acc
          end

        {var, false}, acc ->
          case var do
            {2, :alt, n} -> %{acc | min: max_opt(acc.min, n)}
            {2, :cgt, n} -> %{acc | max: min_opt(acc.max, n)}
            _ -> acc
          end

        _, acc ->
          acc
      end)

    cond do
      bounds.eq == :conflict ->
        :contradiction

      is_integer(bounds.eq) ->
        if (is_nil(bounds.min) or bounds.eq >= bounds.min) and
             (is_nil(bounds.max) or bounds.eq <= bounds.max) do
          {bounds.eq, bounds.eq}
        else
          :contradiction
        end

      is_integer(bounds.min) and is_integer(bounds.max) and bounds.min > bounds.max ->
        :contradiction

      true ->
        {bounds.min, bounds.max}
    end
  end

  defp min_opt(nil, x), do: x
  defp min_opt(x, nil), do: x
  defp min_opt(x, y), do: min(x, y)

  defp max_opt(nil, x), do: x
  defp max_opt(x, nil), do: x
  defp max_opt(x, y), do: max(x, y)
end

defmodule Tdd do
  @moduledoc """
  The main public API and semantic layer for the TDD system.
  It uses Tdd.Core for graph manipulation and Tdd.PredicateLogic
  for reasoning about type system rules.

  This layer implements the high-level, type-aware algorithms for
  intersection, union, negation, and subtyping.
  """
  alias Tdd.Core
  alias Tdd.PredicateLogic
  alias Tdd.Variables, as: V

  # --- System Init ---
  def init_tdd_system do
    Core.init()
    IO.puts("TDD system initialized with new architecture.")
  end

  # --- Variable Definitions (could be in their own module) ---
  defmodule Variables do
    def v_is_atom, do: {0, :is_atom}
    def v_is_tuple, do: {0, :is_tuple}
    def v_is_integer, do: {0, :is_integer}
    def v_is_list, do: {0, :is_list}
    def v_atom_eq(v), do: {1, :value, v}
    def v_int_eq(n), do: {2, :beq, n}
    def v_int_lt(n), do: {2, :alt, n}
    def v_int_gt(n), do: {2, :cgt, n}
    def v_tuple_size_eq(n), do: {4, :size, n}
    def v_tuple_elem_pred(i, v), do: {4, :element, i, v}
    def v_list_is_empty, do: {5, :is_empty}
    def v_list_head_pred(v), do: {5, :head, v}
    def v_list_tail_pred(v), do: {5, :tail, v}
    def v_list_all_elements_are(id), do: {5, :all_elements, id}
  end

  # --- Type Constructors (Completed) ---

  def type_any, do: Core.true_id()
  def type_none, do: Core.false_id()

  # Base type constructors
  def type_atom, do: Core.make_node(V.v_is_atom(), type_any(), type_none(), type_none())
  def type_tuple, do: Core.make_node(V.v_is_tuple(), type_any(), type_none(), type_none())
  def type_integer, do: Core.make_node(V.v_is_integer(), type_any(), type_none(), type_none())
  def type_list, do: Core.make_node(V.v_is_list(), type_any(), type_none(), type_none())

  # --- Atom Constructors ---

  def type_atom_literal(val) do
    # A specific atom is the intersection of `atom()` and `value == val`.
    constraint_node = Core.make_node(V.v_atom_eq(val), type_any(), type_none(), type_none())
    intersect(type_atom(), constraint_node)
  end

  # --- Integer Constructors ---

  def type_int_eq(n) do
    # A specific integer is the intersection of `integer()` and `value == n`.
    constraint_node = Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none())
    intersect(type_integer(), constraint_node)
  end

  def type_int_lt(n) do
    # An integer `< n` is the intersection of `integer()` and `value < n`.
    constraint_node = Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none())
    intersect(type_integer(), constraint_node)
  end

  def type_int_gt(n) do
    # An integer `> n` is the intersection of `integer()` and `value > n`.
    constraint_node = Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none())
    intersect(type_integer(), constraint_node)
  end

  # --- Tuple Constructors ---

  def type_empty_tuple do
    # `{}` is the intersection of `tuple()` and `size == 0`.
    constraint_node = Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none())
    intersect(type_tuple(), constraint_node)
  end

  def type_tuple_sized_any(size) do
    # A tuple of a fixed size is the intersection of `tuple()` and `size == N`.
    constraint_node =
      Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none())

    intersect(type_tuple(), constraint_node)
  end

  def type_tuple(element_type_ids) when is_list(element_type_ids) do
    # This is the most complex tuple constructor. It represents a tuple with
    # a specific size and specific types for each element.
    # e.g., type_tuple([type_atom(), type_integer()]) for `{atom(), integer()}`

    num_elements = length(element_type_ids)

    # 1. Start with the base constraint: a tuple of the correct size.
    base_type = type_tuple_sized_any(num_elements)

    # 2. Iteratively intersect with constraints for each element's type.
    Enum.reduce(Enum.with_index(element_type_ids), base_type, fn {elem_type_id, index}, acc_tdd ->
      # For each element, we create a TDD that represents the constraint on that element.
      # `map_tdd_to_component` wraps all predicates of `elem_type_id` inside
      # `v_tuple_elem_pred(index, ...)`, effectively focusing the type check
      # on just that element of the tuple.
      elem_constraint_tdd =
        map_tdd_to_component(elem_type_id, &V.v_tuple_elem_pred(index, &1), type_any())

      # Intersect the accumulated TDD with the new element constraint.
      intersect(acc_tdd, elem_constraint_tdd)
    end)
  end

  # --- List Constructors ---

  def type_empty_list do
    # `[]` is the intersection of `list()` and `is_empty == true`.
    constraint_node = Core.make_node(V.v_list_is_empty(), type_any(), type_none(), type_none())
    intersect(type_list(), constraint_node)
  end

  def type_cons(head_type_id, tail_type_id) do
    # A cons cell `[H|T]` is a list that is NOT empty, where the head
    # has type H and the tail has type T.

    # 1. Base type: a non-empty list.
    non_empty_list = intersect(type_list(), negate(type_empty_list()))

    # 2. Create the constraint for the head's type.
    head_constraint =
      map_tdd_to_component(head_type_id, &V.v_list_head_pred/1, type_any())

    # 3. Create the constraint for the tail's type.
    tail_constraint =
      map_tdd_to_component(tail_type_id, &V.v_list_tail_pred/1, type_any())

    # 4. Intersect them all together.
    non_empty_list
    |> intersect(head_constraint)
    |> intersect(tail_constraint)
  end

  def type_list_of(element_type_id) do
    # The type `list(T)` is a list where `all_elements` have type T.
    # This predicate `{5, :all_elements, T}` is a "macro" predicate that implies
    # a recursive check. The logic for handling its interaction with other
    # list predicates must be encoded in the `intersect` algorithm itself
    # (or more precisely, in `PredicateLogic` if it implies other simple facts).
    # For now, we represent it with a single node.
    # If T is `any`, then `list(any)` is just `list()`.
    if element_type_id == type_any() do
      type_list()
    else
      constraint_node =
        Core.make_node(
          V.v_list_all_elements_are(element_type_id),
          type_any(),
          type_none(),
          type_none()
        )

      intersect(type_list(), constraint_node)
    end
  end

  # --- High-Level Operations ---

  def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{}) |> simplify(%{})
  def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) |> simplify(%{})

  def negate(u_id) do
    negate_recursive(u_id, %{})
    |> simplify(%{})
  end

  def is_subtype(sub_id, super_id) do
    # A <: B  <=>  A & ~B == none
    IO.inspect("sub_id in is_subtype")
    Tdd.print_tdd(sub_id)
    IO.inspect("negate(super_id) in is_subtype")
    Tdd.print_tdd(negate(super_id))
    IO.inspect("intersect(sub_id, negate(super_id)) in is_subtype")
    Tdd.print_tdd(intersect(sub_id, negate(super_id)))
    intersect(sub_id, negate(super_id)) == type_none()
  end

  # NEW DEDICATED NEGATE FUNCTION
  defp negate_recursive(id, constraints) do
    # Memoization
    cache_key = {:negate, id, Map.to_list(constraints) |> Enum.sort()}

    res =
      if cached = Core.get_op_cache(cache_key) do
        cached
      else
        compute_negate(id, constraints)
      end

    Core.put_op_cache(cache_key, res)
    res
  end

  defp compute_negate(id, constraints) do
    case PredicateLogic.saturate(constraints) do
      :contradiction ->
        # not(contradiction) is not(false) which is true
        type_any()

      {:ok, saturated_constraints} ->
        # First, simplify the node we are about to negate
        s_id = simplify(id, saturated_constraints)

        case Core.get_node(s_id) do
          true ->
            type_none()

          false ->
            type_any()

          {var, y, n, d} ->
            # Recurse, adding the constraint for each branch
            res_y = negate_recursive(y, Map.put(saturated_constraints, var, true))
            res_n = negate_recursive(n, Map.put(saturated_constraints, var, false))
            res_d = negate_recursive(d, Map.put(saturated_constraints, var, :dc))
            Core.make_node(var, res_y, res_n, res_d)
        end
    end
  end

  # --- Core Recursive Operation Logic ---

  defp do_op(op_name, u1_id, u2_id, constraints) do
    # Memoization using the Core cache
    cache_key = {op_name, Enum.sort([u1_id, u2_id]), Map.to_list(constraints) |> Enum.sort()}

    if cached = Core.get_op_cache(cache_key) do
      cached
    else
      res = compute_op(op_name, u1_id, u2_id, constraints)
      Core.put_op_cache(cache_key, res)
      res
    end
  end

  defp compute_op(op_name, u1_id, u2_id, constraints) do
    case PredicateLogic.saturate(constraints) do
      :contradiction ->
        # This path is impossible. For an intersection, the result is the empty set.
        handle_contradiction(op_name)

      {:ok, saturated_constraints} ->
        # REMOVED: No more pre-simplifying inputs here.
        # We pass the original IDs and the full context to dispatch_op.
        n1 = Core.get_node(u1_id)
        n2 = Core.get_node(u2_id)
        dispatch_op(op_name, u1_id, n1, u2_id, n2, saturated_constraints)
    end
  end

  # If a path is contradictory, what does it mean for the operation?
  # For intersection, it's `none`. For union, it depends on the other branch.
  # This function is a placeholder for more complex logic if needed.
  # For now, `none` for intersect and negate is safe. For `sum`, it's more complex.
  defp handle_contradiction(:intersect), do: type_none()
  # ¬(false) = true
  defp handle_contradiction(:negate), do: type_any()
  # a+b, if a is impossible, result is b. Needs other branch info.
  defp handle_contradiction(:sum), do: type_none()

  # This is the replacement for the "implied value" check in the old `simplify_with_constraints`.
  def simplify(id, constraints) do
    # Memoization is critical for performance
    cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()}

    if cached = Core.get_op_cache(cache_key) do
      cached
    else
      # We will call saturate at the beginning of the operation (in compute_op),
      # so we can assume constraints are consistent here.
      res = compute_simplify(id, constraints)
      Core.put_op_cache(cache_key, res)
      res
    end
  end

  defp compute_simplify(id, constraints) do
    case Core.get_node(id) do
      true ->
        type_any()

      false ->
        type_none()

      {var, y, n, d} ->
        contradiction =
          case var do
            {5, :head, head_predicate} ->
              all_elements_type_id =
                Enum.find_value(constraints, fn
                  {{5, :all_elements, type_id}, true} -> type_id
                  _ -> nil
                end)

              if all_elements_type_id do
                head_type = predicate_to_tdd(head_predicate)
                # Is the required head type compatible with the element type?
                intersect(head_type, all_elements_type_id) == type_none()
              else
                false
              end

            {5, :tail, tail_predicate} ->
              all_elements_type_id =
                Enum.find_value(constraints, fn
                  {{5, :all_elements, type_id}, true} -> type_id
                  _ -> nil
                end)

              if all_elements_type_id do
                tail_type = predicate_to_tdd(tail_predicate)
                # The tail must be a list of the element type.
                required_tail_type = type_list_of(all_elements_type_id)
                intersect(tail_type, required_tail_type) == type_none()
              else
                false
              end

            _ ->
              false
          end

        if contradiction do
          # The 'yes' branch is impossible. The node simplifies to its 'no' branch.
          simplify(n, constraints)
        else
          case Map.get(constraints, var) do
            true ->
              simplify(y, constraints)

            false ->
              simplify(n, constraints)

            :dc ->
              simplify(d, constraints)

            nil ->
              case PredicateLogic.check_implication(var, constraints) do
                true ->
                  simplify(y, constraints)

                false ->
                  simplify(n, constraints)

                :unknown ->
                  res_y = simplify(y, Map.put(constraints, var, true))
                  res_n = simplify(n, Map.put(constraints, var, false))
                  res_d = simplify(d, Map.put(constraints, var, :dc))
                  Core.make_node(var, res_y, res_n, res_d)
              end
          end
        end
    end
  end

  defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do
    # --- Step 1: Simplify the current nodes under the given constraints. ---
    # This is the crucial change. We simplify first, before doing anything else.
    s1_id = simplify(u1_id, constraints)
    s2_id = simplify(u2_id, constraints)

    # If simplification resolved either to a terminal, we can take a shortcut.
    if Core.terminal_id?(s1_id) or Core.terminal_id?(s2_id) do
      apply_terminals(op_name, s1_id, s2_id)
    else
      # --- Step 2: Get details of the *simplified* nodes and proceed. ---
      sn1 = Core.get_node(s1_id)
      sn2 = Core.get_node(s2_id)

      {var1, y1, n1_child, d1} = sn1
      {var2, y2, n2_child, d2} = sn2
      top_var = Enum.min([var1, var2])

      # Determine children for the recursive call based on top_var.
      call_y1 = if(var1 == top_var, do: y1, else: s1_id)
      call_y2 = if(var2 == top_var, do: y2, else: s2_id)
      call_n1 = if(var1 == top_var, do: n1_child, else: s1_id)
      call_n2 = if(var2 == top_var, do: n2_child, else: s2_id)
      call_d1 = if(var1 == top_var, do: d1, else: s1_id)
      call_d2 = if(var2 == top_var, do: d2, else: s2_id)

      # --- Step 3: Recurse with the original do_op entry point ---
      res_y = do_op(op_name, call_y1, call_y2, Map.put(constraints, top_var, true))
      res_n = do_op(op_name, call_n1, call_n2, Map.put(constraints, top_var, false))
      res_d = do_op(op_name, call_d1, call_d2, Map.put(constraints, top_var, :dc))

      Core.make_node(top_var, res_y, res_n, res_d)
    end
  end

  defp apply_terminals(op_name, id1, id2) do
    lambda = op_lambda(op_name)
    n1 = Core.get_node(id1)
    n2 = Core.get_node(id2)

    # If both are terminals, just apply the op.
    if Core.terminal_id?(id1) and Core.terminal_id?(id2) do
      if lambda.(n1, n2), do: type_any(), else: type_none()
    else
      # If only one is a terminal, we must recurse on the other's children.
      # This ensures correctness for operations like `A & true -> A`.
      non_terminal_id = if(Core.terminal_id?(id1), do: id2, else: id1)
      terminal_id = if(Core.terminal_id?(id1), do: id1, else: id2)
      {var, y, n, d} = Core.get_node(non_terminal_id)

      res_y = apply_terminals(op_name, y, terminal_id)
      res_n = apply_terminals(op_name, n, terminal_id)
      res_d = apply_terminals(op_name, d, terminal_id)
      Core.make_node(var, res_y, res_n, res_d)
    end
  end

  defp op_lambda(:intersect) do
    fn
      false, _ -> false
      _, false -> false
      true, v2 -> v2
      v1, true -> v1
    end
  end

  defp op_lambda(:sum) do
    fn
      true, _ -> true
      _, true -> true
      false, v2 -> v2
      v1, false -> v1
    end
  end

  # Helper from original code, still useful for constructors
  defp map_tdd_to_component(tdd_id, wrapper_fun, success_id) do
    case Core.get_node(tdd_id) do
      true ->
        success_id

      false ->
        type_none()

      {var, y, n, d} ->
        component_var = wrapper_fun.(var)
        res_y = map_tdd_to_component(y, wrapper_fun, success_id)
        res_n = map_tdd_to_component(n, wrapper_fun, success_id)
        res_d = map_tdd_to_component(d, wrapper_fun, success_id)
        Core.make_node(component_var, res_y, res_n, res_d)
    end
  end

  @doc """
  Converts a single predicate variable into a full TDD type.
  This is the key to comparing predicates with other TDD types.
  """
  defp predicate_to_tdd(predicate) do
    # Memoize for performance, as this might be called repeatedly.
    cache_key = {:predicate_to_tdd, predicate}

    if cached = Core.get_op_cache(cache_key) do
      cached
    else
      res =
        case predicate do
          {0, :is_atom} -> type_atom()
          {0, :is_tuple} -> type_tuple()
          {0, :is_integer} -> type_integer()
          {0, :is_list} -> type_list()
          {1, :value, val} -> type_atom_literal(val)
          {2, :beq, n} -> type_int_eq(n)
          {2, :alt, n} -> type_int_lt(n)
          {2, :cgt, n} -> type_int_gt(n)
          {4, :size, n} -> type_tuple_sized_any(n)
          {5, :is_empty} -> type_empty_list()
          # A head/tail predicate implies the value is a list AND has that head/tail.
          # The inner predicate is what we care about for the type check.
          {5, :head, inner_p} -> predicate_to_tdd(inner_p)
          {5, :tail, inner_p} -> predicate_to_tdd(inner_p)
          {5, :all_elements, type_id} -> type_list_of(type_id)
          # A tuple element predicate is about the element, not the tuple itself.
          {4, :element, _, inner_p} -> predicate_to_tdd(inner_p)
          # Fallback for unknown/complex predicates: assume they can be anything.
          _ -> type_any()
        end

      Core.put_op_cache(cache_key, res)
      res
    end
  end

  @doc """
  Prints a human-readable representation of a TDD, starting from the given ID.
  It recursively prints the structure of the graph.
  """
  def print_tdd(id, indent \\ 0) do
    prefix = String.duplicate("  ", indent)
    # Use Tdd.Core to get node details
    details = Core.get_node(id)

    IO.puts("#{prefix}ID #{id}: #{inspect(details)}")

    case details do
      # A variable node
      {_var, y, n, d} ->
        IO.puts("#{prefix}  Yes ->")
        print_tdd(y, indent + 1)
        IO.puts("#{prefix}  No  ->")
        print_tdd(n, indent + 1)
        IO.puts("#{prefix}  DC  ->")
        print_tdd(d, indent + 1)

      # Terminal nodes (:true or :false)
      true ->
        :ok

      false ->
        :ok

      # Handle cases where an ID might not be found
      nil ->
        IO.puts("#{prefix} Error: Unknown ID #{id}")
    end
  end
end

# --- Example Usage ---
Tdd.init_tdd_system()

# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()

test = fn name, expected, result ->
  current_failures = Process.get(:test_failures, [])

  if expected != result do
    Process.put(:test_failures, [name | current_failures])
  end

  status = if expected == result, do: "PASSED", else: "FAILED"
  IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
end

# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_baz = Tdd.type_atom_literal(:baz)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_tuple = Tdd.type_tuple()
# Tuple of size 2, e.g. {any, any}
tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()

test_all = fn ->
  IO.puts("\n--- TDD for :foo ---")
  Tdd.print_tdd(tdd_foo)

  IO.puts("\n--- TDD for not :foo ---")
  Tdd.print_tdd(Tdd.negate(tdd_foo))

  IO.puts("\n--- TDD for atom ---")
  Tdd.print_tdd(tdd_atom)

  IO.puts("\n--- TDD for not atom ---")
  # Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
  # This represents "anything that is not an atom". The DC branch becomes true because if
  # "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
  Tdd.print_tdd(Tdd.negate(tdd_atom))

  IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
  tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
  # Expected ID 0: :false_terminal
  Tdd.print_tdd(tdd_foo_and_bar)

  IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
  tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
  # Expected to be structurally identical to tdd_foo
  Tdd.print_tdd(tdd_foo_and_atom)
  IO.puts("\n--- Basic Subtyping Tests ---")
  test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
  test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
  test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
  test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
  test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
  test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
  test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
  test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
  test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
  test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))

  IO.puts("\n--- Any/None Subtyping Tests ---")
  test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
  test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
  test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
  test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
  test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
  test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
  test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
  test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))

  IO.puts("\n--- Union related Subtyping ---")
  tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
  tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)

  test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
  test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
  test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
  test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))

  test.(
    "(:foo | :bar) <: (:foo | :bar | :baz)",
    true,
    Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
  )

  test.(
    "(:foo | :bar | :baz) <: (:foo | :bar)",
    false,
    Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
  )

  # Test against a non-member of the union
  test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))

  IO.puts("\n--- Intersection related Subtyping ---")
  # Should be equivalent to tdd_foo
  tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
  # Should be tdd_none
  tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)

  test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
  test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
  test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
  test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
  test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
  # An intersection is a subtype of its components
  test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
  # (none <: atom)
  test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
  # (none <: tuple)
  test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))

  IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
  # Reminder: ¬A <: ¬B  is equivalent to B <: A (contrapositive)

  # Test 1: ¬atom <: ¬:foo  (Equivalent to :foo <: atom, which is true)
  test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))

  # Test 2: ¬:foo <: ¬atom  (Equivalent to atom <: :foo, which is false)
  test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))

  # Double negation
  test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
  test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))

  # Disjoint types
  test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
  test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
  test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))

  IO.puts("\n--- Mixed Types & Complex Subtyping ---")
  tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
  tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)

  test.(
    "(:foo | {}) <: (atom | tuple)",
    true,
    Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
  )

  test.(
    "(atom | tuple) <: (:foo | {})",
    false,
    Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
  )

  test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
  test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))

  # De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
  # (:foo | :bar) <: ¬(¬:foo & ¬:bar)
  tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))

  test.(
    "(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
    true,
    Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
  )

  test.(
    "¬(¬:foo & ¬:bar) <: (:foo | :bar)",
    true,
    Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
  )

  # Type difference: atom - :foo  (represented as atom & ¬:foo)
  tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
  test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
  test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
  # True if :bar is in (atom - :foo)
  test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
  test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))

  # (atom - :foo) | :foo should be atom
  tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo)
  test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom))
  test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom))

  # (atom | {}) & (tuple | :foo) must be (:foo | {})
  # Represents `atom() | {}`
  tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
  # Represents `tuple() | :foo`
  tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
  intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
  # Expected result for intersected_complex is tdd_foo_or_empty_tuple

  test.(
    "(atom | {}) & (tuple | :foo) <: (:foo | {})",
    true,
    Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple)
  )

  test.(
    "(:foo | {}) <: (atom | {}) & (tuple | :foo)",
    true,
    Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex)
  )

  # {} | tuple_size_2 should be a subtype of tuple
  tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2)
  test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple))

  test.(
    "({} | tuple_size_2) <: ({} | tuple_size_2)",
    true,
    Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2)
  )

  test.(
    "({} | tuple_size_2) <: tuple_size_2",
    false,
    Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2)
  )

  # IO.puts("\n--- TDD structure for (atom - :foo) ---")
  # Tdd.print_tdd(tdd_atom_minus_foo)
  # IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
  # Tdd.print_tdd(tdd_recombined_atom)
  # IO.puts("\n--- TDD structure for 'atom' for comparison ---")
  # Tdd.print_tdd(tdd_atom)

  IO.inspect(Process.get(:test_failures, []))
end

defmodule IntegerTests do
  def run(test_fn) do
    Process.put(:test_failures, [])
    # Reset for each test group if needed, or once globally
    Tdd.init_tdd_system()

    # Integer types
    tdd_int = Tdd.type_integer()
    tdd_int_5 = Tdd.type_int_eq(5)
    tdd_int_7 = Tdd.type_int_eq(7)
    # x < 10
    tdd_int_lt_10 = Tdd.type_int_lt(10)
    # x > 3
    tdd_int_gt_3 = Tdd.type_int_gt(3)
    # x < 3
    tdd_int_lt_3 = Tdd.type_int_lt(3)
    # x > 10
    tdd_int_gt_10 = Tdd.type_int_gt(10)
    tdd_atom_foo = Tdd.type_atom_literal(:foo)
    #
    # IO.puts("\n--- Integer Type Structures ---")
    # IO.puts("Integer:")
    # Tdd.print_tdd(tdd_int)
    # IO.puts("Int == 5:")
    # Tdd.print_tdd(tdd_int_5)
    # IO.puts("Int < 10:")
    # Tdd.print_tdd(tdd_int_lt_10)

    IO.puts("\n--- Integer Subtyping Tests ---")
    test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
    test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5))
    test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7))
    test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5))
    test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo))

    test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int))
    test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10))
    # 5 < 10
    test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10))
    test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5))

    test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int))
    # 5 > 3
    test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3))
    test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5))

    # x < 3 implies x < 10
    test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10))
    # x > 10 implies x > 3
    test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
    test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3))
    test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10))

    IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
    intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7)
    test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none())
    # IO.puts("Structure of int_5 & int_7 (should be ID 0):")
    # Tdd.print_tdd(intersect_5_7)

    # x < 3 AND x > 10
    intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10)
    test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none())
    # IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
    # Tdd.print_tdd(intersect_lt3_gt10)

    # x < 10 AND x > 3 (e.g. 4,5..9)
    intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3)
    test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none())
    # IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
    # Tdd.print_tdd(intersect_lt10_gt3)
    # Test a value within this intersection
    test_fn.(
      "int_5 <: (int_lt_10 & int_gt_3)",
      true,
      Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3)
    )

    # x == 5 AND x < 3
    intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3)
    test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none())

    IO.puts("\n--- Integer Union Tests ---")
    union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7)
    test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7))
    test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7))
    test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7))
    # IO.puts("Structure of int_5 | int_7:")
    # Tdd.print_tdd(union_5_7)

    # (int < 3) | (int > 10)
    union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)

    test_fn.(
      "int_eq(0) <: (int < 3 | int > 10)",
      true,
      Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges)
    )

    test_fn.(
      "int_eq(5) <: (int < 3 | int > 10)",
      false,
      Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges)
    )

    test_fn.(
      "int_eq(12) <: (int < 3 | int > 10)",
      true,
      Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
    )

    IO.inspect(Process.get(:test_failures, []))
  end
end

defmodule TupleTests do
  import Tdd

  def run(test_fn) do
    Process.put(:test_failures, [])
    # Re-init the system for a clean slate for these tests
    Tdd.init_tdd_system()
    IO.puts("\n--- Running TupleTests ---")

    # --- Basic Types for convenience ---
    t_atom = type_atom()
    t_int = type_integer()
    t_foo = type_atom_literal(:foo)
    t_bar = type_atom_literal(:bar)
    t_int_5 = type_int_eq(5)
    t_int_6 = type_int_eq(6)
    t_int_pos = type_int_gt(0)
    t_any = type_any()
    t_none = type_none()
    # any tuple
    t_tuple = type_tuple()
    t_empty_tuple = type_empty_tuple()

    # --- Specific Tuple Types ---
    # {atom(), integer()}
    tup_atom_int = type_tuple([t_atom, t_int])
    # {:foo, 5}
    tup_foo_5 = type_tuple([t_foo, t_int_5])
    # {pos_integer(), atom()}
    tup_pos_atom = type_tuple([t_int_pos, t_atom])
    # {atom(), any}
    tup_atom_any = type_tuple([t_atom, t_any])
    # {any, integer()}
    tup_any_int = type_tuple([t_any, t_int])
    # a tuple of size 2, {any, any}
    tup_s2_any = type_tuple_sized_any(2)
    # a tuple of size 3, {any, any, any}
    tup_s3_any = type_tuple_sized_any(3)
    # {integer(), atom()}
    tup_int_atom = type_tuple([t_int, t_atom])
    # {{:foo}}
    tup_nested_foo = type_tuple([type_tuple([t_foo])])
    # {{atom()}}
    tup_nested_atom = type_tuple([type_tuple([t_atom])])
    # {any, none} -> this should resolve to none
    tup_with_none = type_tuple([t_any, t_none])

    IO.puts("\n--- Section: Basic Subtyping ---")
    test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
    test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
    test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
    test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
    test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
    test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))

    IO.puts("\n--- Section: Size-related Subtyping ---")
    test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
    test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
    test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
    test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
    test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
    test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))

    IO.puts("\n--- Section: Intersection ---")
    # {atom, any} & {any, int} -> {atom, int}
    intersect1 = intersect(tup_atom_any, tup_any_int)
    test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)

    # {atom, int} & {int, atom} -> none
    intersect2 = intersect(tup_atom_int, tup_int_atom)
    test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)

    # tuple_size_2 & tuple_size_3 -> none
    intersect3 = intersect(tup_s2_any, tup_s3_any)
    test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)

    # tuple() & {atom, int} -> {atom, int}
    intersect4 = intersect(t_tuple, tup_atom_int)
    test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)

    IO.puts("\n--- Section: Union ---")
    # {:foo, 5} | {pos_int, atom}
    union1 = sum(tup_foo_5, tup_pos_atom)
    test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))

    test_fn.(
      "{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
      true,
      is_subtype(tup_pos_atom, union1)
    )

    test_fn.(
      "{atom, int} <: ({:foo, 5} | {pos_int, atom})",
      false,
      is_subtype(tup_atom_int, union1)
    )

    # {atom, any} | {any, int} -> a complex type, let's check subtyping against it
    union2 = sum(tup_atom_any, tup_any_int)
    # {atom, int} is in both parts of the union.
    test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
    # {:foo, :bar} is only in {atom, any}.
    test_fn.(
      "{:foo, :bar} <: ({atom,any} | {any,int})",
      true,
      is_subtype(type_tuple([t_foo, t_bar]), union2)
    )

    # {5, 6} is only in {any, int}.
    test_fn.(
      "{5, 6} <: ({atom,any} | {any,int})",
      true,
      is_subtype(type_tuple([t_int_5, t_int_6]), union2)
    )

    # {5, :foo} is in neither part of the union.
    test_fn.(
      "{5, :foo} <: ({atom,any} | {any,int})",
      false,
      is_subtype(type_tuple([t_int_5, t_foo]), union2)
    )

    IO.puts("\n--- Section: Negation and Type Difference ---")
    # atom is disjoint from tuple, so atom <: ¬tuple
    test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))

    # A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
    test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
    # {int, atom} is a subtype of ¬{atom, int} because their elements differ
    test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
    # tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
    test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))

    # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
    diff1 = intersect(tup_s2_any, negate(tup_atom_any))

    # {integer, integer} has a first element that is not an atom, so it should be in the difference.
    tup_int_int = type_tuple([t_int, t_int])
    test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))

    test_fn.(
      "{atom, int} <: (tuple_size_2 - {atom, any})",
      false,
      is_subtype(tup_atom_int, diff1)
    )

    IO.puts("\n--- Section: Nested Tuples ---")
    test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
    test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
    # Intersection of disjoint nested types: {{:foo}} & {{:bar}}
    intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
    test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
    # Union of nested types
    union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
    test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))

    test_fn.(
      "{{:bar}} <: ({{:foo}} | {{:bar}})",
      true,
      is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
    )

    test_fn.(
      "{{atom}} <: ({{:foo}} | {{:bar}})",
      false,
      is_subtype(tup_nested_atom, union_nested)
    )

    IO.puts("\n--- Section: Edge Cases (any, none) ---")
    # A type `{any, none}` should not be possible. The value `none` cannot exist.
    # The simplification logic should reduce this to `type_none`.
    test_fn.("{any, none} == none", true, tup_with_none == t_none)

    # Intersection with a tuple containing none should result in none
    intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
    test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)

    # Union with a tuple containing none should be a no-op
    union_with_none_tuple = sum(tup_atom_int, tup_with_none)
    test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)

    # --- Original tests from problem description for regression ---
    IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")

    test_fn.(
      "{1, :foo} <: {int_gt_0, :foo | :bar}",
      true,
      is_subtype(
        type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
      )
    )

    test_fn.(
      "{0, :foo} <: {int_gt_0, :foo | :bar}",
      false,
      is_subtype(
        type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
      )
    )

    test_fn.(
      "{1, :kek} <: {int_gt_0, :foo | :bar}",
      false,
      is_subtype(
        type_tuple([
          type_int_eq(1),
          type_atom_literal(:kek)
        ]),
        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
      )
    )

    IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
  end
end

defmodule ListTests do
  import Tdd

  def run(test_fn) do
    Process.put(:test_failures, [])
    Tdd.init_tdd_system()
    IO.puts("\n--- Running ListTests ---")

    # --- Basic Types ---
    t_atom = type_atom()
    t_int = type_integer()
    t_foo = type_atom_literal(:foo)
    t_bar = type_atom_literal(:bar)
    t_any = type_any()
    t_none = type_none()

    # --- List Types ---
    t_list = type_list()
    t_empty_list = type_empty_list()
    # [atom | list]
    t_cons_atom_list = type_cons(t_atom, t_list)
    # [:foo | []]
    t_cons_foo_empty = type_cons(t_foo, t_empty_list)
    # [atom | []]
    t_cons_atom_empty = type_cons(t_atom, t_empty_list)
    # [any | []]
    t_cons_any_empty = type_cons(t_any, t_empty_list)
    # [integer | list]
    t_cons_int_list = type_cons(t_int, t_list)

    IO.puts("\n--- Section: Basic List Subtyping ---")
    test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
    test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
    test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
    test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
    test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
    test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
    test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
    test_fn.("atom <: list", false, is_subtype(t_atom, t_list))

    IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
    # Head is a subtype
    test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
    test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
    # Tail is a subtype
    test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
    test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
    # Both are subtypes
    test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
    # Neither is a subtype
    test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
    # A list of length 1 is a subtype of a list of any element of length 1
    test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))

    IO.puts("\n--- Section: List Intersection ---")
    # [atom|list] & [integer|list] -> should be none due to head conflict
    intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
    test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)

    # [any|[]] & [atom|list] -> should be [atom|[]]
    intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
    test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)

    # [] & [atom|list] -> should be none because one is empty and one is not
    intersect3 = intersect(t_empty_list, t_cons_atom_list)
    test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)

    IO.puts("\n--- Section: List Union ---")
    # [] | [atom|[]]
    union1 = sum(t_empty_list, t_cons_atom_empty)
    test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
    test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))

    test_fn.(
      "[integer|[]] <: ([] | [atom|[]])",
      false,
      is_subtype(type_cons(t_int, t_empty_list), union1)
    )

    # [:foo|[]] | [:bar|[]]
    union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
    # This union is a subtype of [atom|[]]
    test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
    test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))

    IO.puts("\n--- Section: List Negation ---")
    # list is a subtype of not(atom)
    test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
    # A non-empty list is a subtype of not an empty list
    test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
    # [integer|list] is a subtype of not [atom|list]
    test_fn.(
      "[integer|list] <: ¬[atom|list]",
      true,
      is_subtype(t_cons_int_list, negate(t_cons_atom_list))
    )

    IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
  end
end

defmodule ListOfTests do
  import Tdd

  def run(test_fn) do
    Process.put(:test_failures, [])
    Tdd.init_tdd_system()
    IO.puts("\n--- Running ListOfTests ---")

    # --- Basic Types ---
    t_atom = type_atom()
    t_int = type_integer()
    t_pos_int = type_int_gt(0)
    t_int_5 = type_int_eq(5)

    # --- list(X) Types ---
    t_list_of_int = type_list_of(t_int)
    t_list_of_pos_int = type_list_of(t_pos_int)
    t_list_of_atom = type_list_of(t_atom)

    # --- Specific List Types ---
    t_list = type_list()
    t_empty_list = type_empty_list()
    # [5]
    t_list_one_int = type_cons(t_int_5, t_empty_list)
    # [:foo]
    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
    # [5, :foo]
    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))

    IO.puts("\n--- Section: Basic list(X) Subtyping ---")
    test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
    test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
    test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
    test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
    test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
    test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))

    test_fn.(
      "[5, :foo] <: list(any)",
      true,
      is_subtype(t_list_int_and_atom, type_list_of(type_any()))
    )

    IO.puts("\n--- Section: Covariance of list(X) ---")

    test_fn.(
      "list(pos_integer) <: list(integer)",
      true,
      is_subtype(t_list_of_pos_int, t_list_of_int)
    )

    test_fn.(
      "list(integer) <: list(pos_integer)",
      false,
      is_subtype(t_list_of_int, t_list_of_pos_int)
    )

    IO.puts("\n--- Section: Intersection of list(X) ---")
    # list(integer) & list(pos_integer) should be list(pos_integer)
    intersect1 = intersect(t_list_of_int, t_list_of_pos_int)

    test_fn.(
      "(list(int) & list(pos_int)) == list(pos_int)",
      true,
      intersect1 == t_list_of_pos_int
    )

    # list(integer) & list(atom) should be just [] (empty list is the only common member)
    # The system simplifies this intersection to a type that only accepts the empty list.
    intersect2 = intersect(t_list_of_int, t_list_of_atom)
    test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
    test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
    test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
    # It should be equivalent to `type_empty_list`
    test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)

    IO.puts("\n--- Section: Intersection of list(X) with cons ---")
    # list(integer) & [:foo | []] -> should be none
    intersect3 = intersect(t_list_of_int, t_list_one_atom)
    test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())

    # list(integer) & [5 | []] -> should be [5 | []]
    intersect4 = intersect(t_list_of_int, t_list_one_int)
    test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)

    # list(integer) & [5, :foo] -> should be none
    intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
    test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())

    IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
  end
end

defmodule AdhocTest do
  import Tdd

  def run(test_fn) do
    # --- Basic Types ---
    t_atom = type_atom()
    t_int = type_integer()
    t_pos_int = type_int_gt(0)
    t_int_5 = type_int_eq(5)

    # --- list(X) Types ---
    t_list_of_int = type_list_of(t_int)
    t_list_of_pos_int = type_list_of(t_pos_int)
    t_list_of_atom = type_list_of(t_atom)

    # --- Specific List Types ---
    t_list = type_list()
    t_empty_list = type_empty_list()
    # [5]
    t_list_one_int = type_cons(t_int_5, t_empty_list)
    # [:foo]
    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
    # [5, :foo]
    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
    intersect4 = intersect(t_list_of_int, t_list_one_int)
    IO.inspect("first_subtype")
    a = is_subtype(intersect4, t_list_one_int)
    IO.inspect("second_subtype")
    b = is_subtype(t_list_one_int, intersect4)
    test_fn.("list(integer) & [5] == [5]", true, a == b)
  end
end

# test_all.()
# IntegerTests.run(test)
# TupleTests.run(test)
# ListTests.run(test)
# ListOfTests.run(test)
AdhocTest.run(test)