defmodule Tdd do
  @moduledoc """
  Ternary decision diagram for set-theoretic types.
  """

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

  # --- State: Managed via module attributes (for simplicity in this example) ---
  # @nodes: Map from {var, yes_id, no_id, dc_id} -> node_id
  # @node_by_id: Map from node_id -> {var, yes_id, no_id, dc_id}
  # @next_id: Integer for the next available node ID
  # @op_cache: Cache for apply operations: {{op_name, id1, id2} -> result_id}

  defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id

  # Initialize state (call this once, or ensure it's idempotent)
  def init_tdd_system do
    # Node 0 represents FALSE, Node 1 represents TRUE.
    # These don't have var/children, so we represent them specially or handle them in functions.
    # For @node_by_id, we can store a marker.
    Process.put(:nodes, %{})
    Process.put(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal})
    Process.put(:next_id, 2) # Start after true/false
    Process.put(:op_cache, %{})
    IO.puts("TDD system initialized.")
  end

  # Helper to get current state
  defp get_state do
    %{
      nodes: Process.get(:nodes, %{}),
      node_by_id: Process.get(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal}),
      next_id: Process.get(:next_id, 2),
      op_cache: Process.get(:op_cache, %{})
    }
  end

  # Helper to update state
  defp update_state(changes) do
    current_state = get_state()
    new_state = Map.merge(current_state, changes)
    Process.put(:nodes, new_state.nodes)
    Process.put(:node_by_id, new_state.node_by_id)
    Process.put(:next_id, new_state.next_id)
    Process.put(:op_cache, new_state.op_cache)
  end

  # --- Node Creation and Reduction ---
  # This is the core function to get or create a node.
  # It implements the reduction rules.
  def make_node(variable, yes_id, no_id, dc_id) do
    # Reduction Rule: If all children are identical, this node is redundant.
    # (This is a strong form of reduction for TDDs)
    if yes_id == no_id && yes_id == dc_id do
      # IO.puts "Reduction (all children same): var #{inspect variable} -> #{yes_id}"
      yes_id
    else
      state = get_state()
      node_tuple = {variable, yes_id, no_id, dc_id}

      if Map.has_key?(state.nodes, node_tuple) do
        # Node already exists
        state.nodes[node_tuple]
      else
        # Create new node
        new_id = state.next_id
        # IO.puts "Creating node #{new_id}: #{inspect variable}, y:#{yes_id}, n:#{no_id}, d:#{dc_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

  # Get details of a node (useful for apply and debugging)
  def get_node_details(id) when is_terminal_id(id) do
    if id == @true_node_id, do: :true_terminal, else: :false_terminal
  end
  def get_node_details(id) do
    state = get_state()
    state.node_by_id[id] # Returns {var, yes, no, dc} or nil
  end


  # --- Variable Definitions (subset for now) ---
  # Category 0: Primary Type Discriminators
  @v_is_atom {0, :is_atom}
  @v_is_tuple {0, :is_tuple}
  # Add other primary types here in order, e.g., {0, :is_integer}, {0, :is_list}

  # Category 1: Atom-Specific Predicates
  def v_atom_eq(atom_val), do: {1, :value, atom_val}

  # Category 4: Tuple-Specific Predicates
  def v_tuple_size_eq(size), do: {4, :size, size}
  def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}

  # --- Basic Type Constructors ---
  # These construct TDDs representing specific types.
  # For simplicity, they assume an "empty" background (all other types are false).
  # `dc_id` is often `@false_node_id` in constructors because if a variable is "don't care"
  # for this specific type, it means it *could* be something that makes it NOT this type.

  def type_any, do: @true_node_id
  def type_none, do: @false_node_id

  # Represents the type `atom()` (any atom)
  def type_atom do
    # The variable order means we must consider @v_is_tuple *before* specific atom properties
    # if we were to build from a full list of variables.
    # However, for a simple constructor, we focus on the defining properties.
    # The `apply` algorithm will handle interactions with other types correctly due to variable ordering.

    # If it's an atom, it's true for this type.
    # If it's not an atom, it's false for this type.
    # If we "don't care" if it's an atom, it's not specific enough to be `type_atom`, so false.
    make_node(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
  end

  # Represents a specific atom literal, e.g., `:foo`
  def type_atom_literal(atom_val) do
    var_eq = v_atom_eq(atom_val) # e.g., {1, :value, :foo}

    # Node for specific atom value: if value matches, true; else false.
    atom_val_node = make_node(var_eq, @true_node_id, @false_node_id, @false_node_id)

    # Node for primary type: if is_atom, check value; else false.
    make_node(@v_is_atom, atom_val_node, @false_node_id, @false_node_id)
  end

  # Represents `tuple()` (any tuple)
  def type_tuple do
    make_node(@v_is_tuple, @true_node_id, @false_node_id, @false_node_id)
  end

  # Represents an empty tuple `{}`
  def type_empty_tuple do
    var_size_0 = v_tuple_size_eq(0)
    tuple_size_node = make_node(var_size_0, @true_node_id, @false_node_id, @false_node_id)
    make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
  end

  # Represents a tuple of a specific size with any elements, e.g., `{any, any}` for size 2
  def type_tuple_sized_any(size) do
    var_size = v_tuple_size_eq(size)
    # For element checks, 'any' means the element specific predicates would all go to their dc child,
    # which leads to true. So, for representing `tuple_of_size_N_with_any_elements`,
    # we only need to check the size after confirming it's a tuple.
    tuple_size_node = make_node(var_size, @true_node_id, @false_node_id, @false_node_id)
    make_node(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
  end

  # --- The APPLY Algorithm ---
  # apply(op_lambda, u1_id, u2_id)
  # op_lambda takes (terminal1_val, terminal2_val) and returns resulting terminal_val
  # e.g., for OR: fn :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal; _,_ -> :false_terminal end
  # which then maps to @true_node_id or @false_node_id.

  def apply(op_name, op_lambda, u1_id, u2_id) do
    state = get_state()
    # Ensure cache_key is canonical for commutative operations
    cache_key = {op_name, Enum.sort([u1_id, u2_id])}

    cond do
      # 1. Check cache first
      Map.has_key?(state.op_cache, cache_key) ->
        state.op_cache[cache_key]

      # 2. Base case: Both u1 and u2 are terminals
      is_terminal_id(u1_id) && is_terminal_id(u2_id) ->
        res_terminal_symbol = op_lambda.(get_node_details(u1_id), get_node_details(u2_id))
        # Result is a terminal ID, no need to cache these simple computations directly,
        # the calls leading to them will be cached.
        if res_terminal_symbol == :true_terminal, do: @true_node_id, else: @false_node_id

      # 3. Recursive case: At least one is non-terminal.
      #    Handle sub-cases where one is terminal and the other is not.
      true ->
        # Pre-check for terminal optimizations specific to the operation
        # This can make some operations (like sum with @true_node_id) much faster.
        # For sum:
        # if u1_id == @true_node_id or u2_id == @true_node_id, result is @true_node_id (if op is sum)
        # if u1_id == @false_node_id, result is u2_id (if op is sum)
        # if u2_id == @false_node_id, result is u1_id (if op is sum)
        # These are handled by op_lambda if both are terminals. If one is terminal,
        # the recursive calls below will hit that.

        u1_details = get_node_details(u1_id)
        u2_details = get_node_details(u2_id)

        result_id =
          cond do
            # Case 3a: u1 is terminal, u2 is not
            u1_details == :true_terminal or u1_details == :false_terminal ->
              {var2, y2, n2, d2} = u2_details # u2 must be a node
              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)

            # Case 3b: u2 is terminal, u1 is not
            u2_details == :true_terminal or u2_details == :false_terminal ->
              {var1, y1, n1, d1} = u1_details # u1 must be a node
              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, res_d)

            # Case 3c: Both u1 and u2 are non-terminal nodes
            true ->
              {var1, y1, n1, d1} = u1_details
              {var2, y2, n2, d2} = u2_details

              top_var =
                cond do
                  var1 == var2 -> var1
                  # Elixir's tuple comparison provides the global variable order
                  var1 < var2 -> var1
                  true -> var2 # var2 < var1
                end

              # Recursive calls: if a variable is not the top_var for a TDD,
              # that TDD is passed through unchanged to the next level of recursion.
              res_y =
                cond do
                  top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, y1, y2)
                  top_var == var1 -> apply(op_name, op_lambda, y1, u2_id)
                  true -> apply(op_name, op_lambda, u1_id, y2)
                end

              res_n =
                cond do
                  top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, n1, n2)
                  top_var == var1 -> apply(op_name, op_lambda, n1, u2_id)
                  true -> apply(op_name, op_lambda, u1_id, n2)
                end

              res_d =
                cond do
                  top_var == var1 && top_var == var2 -> apply(op_name, op_lambda, d1, d2)
                  top_var == var1 -> apply(op_name, op_lambda, d1, u2_id)
                  true -> apply(op_name, op_lambda, u1_id, d2)
                end
              make_node(top_var, res_y, res_n, res_d)
          end

        # Cache the result of this (op, u1, u2) call
        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
        result_id
    end
  end

  # --- Set Operations ---
  def sum(tdd1_id, tdd2_id) do
    op_lambda_sum = fn
      (:true_terminal, _) -> :true_terminal # true or X = true
      (_, :true_terminal) -> :true_terminal # X or true = true
      (:false_terminal, t2_val) -> t2_val   # false or X = X
      (t1_val, :false_terminal) -> t1_val   # X or false = X
    end
    apply(:sum, op_lambda_sum, tdd1_id, tdd2_id)
  end

  # Placeholder for intersect and negate
  # def intersect(one, two) do end
  # def negate(one) do end


  # --- Helper to inspect the TDD structure (for debugging) ---
  def print_tdd(id, indent \\ 0) do
    prefix = String.duplicate("  ", indent)
    details = get_node_details(id)
    IO.puts "#{prefix}ID #{id}: #{inspect details}"
    case details do
      {_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)
      :true_terminal -> :ok
      :false_terminal -> :ok
      nil -> IO.puts "#{prefix} Error: Unknown ID #{id}"
    end
  end

end

# --- Example Usage ---
# Initialize the system (important!)
Tdd.init_tdd_system()

IO.puts "\n--- TDD for :foo ---"
tdd_foo = Tdd.type_atom_literal(:foo)
Tdd.print_tdd(tdd_foo)
# Expected:
# ID 4: {{0, :is_atom}, 3, 0, 0}
#   Yes ->
#   ID 3: {{1, :value, :foo}, 1, 0, 0}
#     Yes ->
#     ID 1: :true_terminal
#     No  ->
#     ID 0: :false_terminal
#     DC  ->
#     ID 0: :false_terminal
#   No  ->
#   ID 0: :false_terminal
#   DC  ->
#   ID 0: :false_terminal

IO.puts "\n--- TDD for :bar ---"
tdd_bar = Tdd.type_atom_literal(:bar)
Tdd.print_tdd(tdd_bar)
# Similar structure, but with {1, :value, :bar} and different intermediate IDs like 6, 5.

IO.puts "\n--- TDD for :foo or :bar ---"
tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
Tdd.print_tdd(tdd_foo_or_bar)

# Expected structure for tdd_foo_or_bar (variable order matters):
# Top var: {0, :is_atom}
#   Yes branch: (node for :foo or :bar, given it's an atom)
#     Top var: {1, :value, :bar} (assuming :bar < :foo lexicographically for sorting example, or however Elixir sorts them)
#       Yes branch (:bar is true): true_terminal
#       No branch (:bar is false): (node for checking :foo)
#         Top var: {1, :value, :foo}
#           Yes branch (:foo is true): true_terminal
#           No branch (:foo is false): false_terminal
#           DC branch: false_terminal
#       DC branch: false_terminal (if value is don't care, it's not :bar)
#   No branch: false_terminal (not an atom)
#   DC branch: false_terminal (is_atom is don't care)

IO.puts "\n--- TDD for empty tuple {} ---"
tdd_empty_tuple = Tdd.type_empty_tuple()
Tdd.print_tdd(tdd_empty_tuple)
# Expected:
# ID X: {{0, :is_tuple}, Y, 0, 0}
#  Yes ->
#  ID Y: {{4, :size, 0}, 1, 0, 0}
#    ... leads to true/false ...
#  No -> ID 0
#  DC -> ID 0

IO.puts "\n--- TDD for :foo or {} ---"
tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
Tdd.print_tdd(tdd_foo_or_empty_tuple)
# Expected structure (variable order {0, :is_atom} < {0, :is_tuple}):
# Top var: {0, :is_atom}
#  Yes branch: (node for :foo, given it's an atom, and not a tuple)
#    ... (structure of tdd_foo, but false branch of {0, :is_tuple} might point here)
#  No branch: (node for {}, given it's not an atom)
#    ... (structure of tdd_empty_tuple, but false branch of {0, :is_atom} might point here)
#  DC branch: (complicated, depends on how dc propagates for sum)
#    For sum, if `is_atom` is dc for foo and for tuple, then result is dc.
#    Since our constructors use false for dc, `apply(:sum, false_id, false_id)` for dc branches yields `false_id`.
#    So, the DC branch of the root will be false.