defmodule TddSystemTest do
  # Most tests mutate Tdd.Store, so they cannot run concurrently.
  use ExUnit.Case, async: false

  alias Tdd.TypeSpec
  alias Tdd.Store
  alias Tdd.Variable
  alias Tdd.Compiler
  alias Tdd.Consistency.Engine
  alias Tdd.Algo

  # Helper to mimic the old test structure and provide better failure messages
  # for spec comparisons.
  defp assert_spec_normalized(expected, input_spec) do
    result = TypeSpec.normalize(input_spec)
    # The normalization process should produce a canonical, sorted form.
    assert expected == result, """
    Input Spec:
    #{inspect(input_spec, pretty: true)}

    Expected Normalized:
    #{inspect(expected, pretty: true)}

    Actual Normalized:
    #{inspect(result, pretty: true)}
    """
  end

  # Helper to check for equivalence by comparing TDD IDs.
  defmacro assert_equivalent_specs(spec1, spec2) do
    quote do
      assert Compiler.spec_to_id(unquote(spec1)) == Compiler.spec_to_id(unquote(spec2))
    end
  end

  # Helper to check for subtyping using the TDD compiler.
  defmacro assert_subtype(spec1, spec2) do
    quote do
      assert Compiler.is_subtype(unquote(spec1), unquote(spec2))
    end
  end

  defmacro refute_subtype(spec1, spec2) do
    quote do
      refute Compiler.is_subtype(unquote(spec1), unquote(spec2))
    end
  end

  # Setup block that initializes the Tdd.Store before each test.
  # This ensures that node IDs and caches are clean for every test case.
  setup do
    Tdd.Store.init()
    :ok
  end

  # ---
  # Tdd.Store Tests
  # These tests validate the lowest-level state management of the TDD system.
  # The Store is responsible for creating and storing the nodes of the decision diagram graph.
  # ---
  describe "Tdd.Store: Core state management for the TDD graph" do
    @doc """
    Tests that the store initializes with the correct, reserved IDs for the
    terminal nodes representing TRUE (:any) and FALSE (:none).
    """
    test "initialization and terminals" do
      assert Store.true_node_id() == 1
      assert Store.false_node_id() == 0
      assert Store.get_node(1) == {:ok, :true_terminal}
      assert Store.get_node(0) == {:ok, :false_terminal}
      assert Store.get_node(99) == {:error, :not_found}
    end

    @doc """
    Tests the core functionality of creating nodes. It verifies that new nodes receive
    incrementing IDs and that requesting an identical node reuses the existing one
    (structural sharing), which is fundamental to the efficiency of TDDs.
    """
    test "node creation and structural sharing" do
      var_a = {:is_atom}
      var_b = {:is_integer}
      true_id = Store.true_node_id()
      false_id = Store.false_node_id()

      # First created node gets ID 2 (after 0 and 1 are taken by terminals)
      id1 = Store.find_or_create_node(var_a, true_id, false_id, false_id)
      assert id1 == 2
      assert Store.get_node(id1) == {:ok, {var_a, true_id, false_id, false_id}}

      # Second, different node gets the next ID
      id2 = Store.find_or_create_node(var_b, id1, false_id, false_id)
      assert id2 == 3

      # Creating the first node again returns the same ID, not a new one
      id1_again = Store.find_or_create_node(var_a, true_id, false_id, false_id)
      assert id1_again == id1

      # Next new node gets the correct subsequent ID, proving no ID was wasted
      id3 = Store.find_or_create_node(var_b, true_id, false_id, false_id)
      assert id3 == 4
    end

    @doc """
    Tests a key reduction rule: if a node's 'yes', 'no', and 'don't care' branches
    all point to the same child node, the parent node is redundant and should be
    replaced by the child node itself.
    """
    test "node reduction rule for identical children" do
      var_a = {:is_atom}
      # from previous test logic
      id3 = 4
      id_redundant = Store.find_or_create_node(var_a, id3, id3, id3)
      assert id_redundant == id3
    end

    @doc """
    Tests the memoization cache for operations like 'apply', 'negate', etc.
    This ensures that repeated operations with the same inputs do not trigger
    redundant computations.
    """
    test "operation caching" do
      cache_key = {:my_op, 1, 2}
      assert Store.get_op_cache(cache_key) == :not_found

      Store.put_op_cache(cache_key, :my_result)
      assert Store.get_op_cache(cache_key) == {:ok, :my_result}

      Store.put_op_cache(cache_key, :new_result)
      assert Store.get_op_cache(cache_key) == {:ok, :new_result}
    end
  end

  # ---
  # Tdd.TypeSpec.normalize/1 Tests
  # These tests focus on ensuring the `normalize` function correctly transforms
  # any TypeSpec into its canonical, simplified form.
  # ---
  describe "Tdd.TypeSpec.normalize/1: Base & Simple Types" do
    @doc "Tests that normalizing already-simple specs doesn't change them (idempotency)."
    test "normalizing :any is idempotent" do
      assert_spec_normalized(:any, :any)
    end

    test "normalizing :none is idempotent" do
      assert_spec_normalized(:none, :none)
    end

    test "normalizing :atom is idempotent" do
      assert_spec_normalized(:atom, :atom)
    end

    test "normalizing a literal is idempotent" do
      assert_spec_normalized({:literal, :foo}, {:literal, :foo})
    end
  end

  describe "Tdd.TypeSpec.normalize/1: Double Negation" do
    @doc "Tests the logical simplification that ¬(¬A) is equivalent to A."
    test "¬(¬atom) simplifies to atom" do
      assert_spec_normalized(:atom, {:negation, {:negation, :atom}})
    end

    @doc "Tests that a single negation is preserved when it cannot be simplified further."
    test "A single negation is preserved" do
      assert_spec_normalized({:negation, :integer}, {:negation, :integer})
    end

    @doc "Tests that an odd number of negations simplifies to a single negation."
    test "¬(¬(¬atom)) simplifies to ¬atom" do
      assert_spec_normalized({:negation, :atom}, {:negation, {:negation, {:negation, :atom}}})
    end
  end

  describe "Tdd.TypeSpec.normalize/1: Union Normalization" do
    @doc """
    Tests that unions are canonicalized by flattening nested unions, sorting the members,
    and removing duplicates. e.g., `int | (list | atom | int)` becomes `(atom | int | list)`.
    """
    test "flattens, sorts, and uniques members" do
      input = {:union, [:integer, {:union, [:list, :atom, :integer]}]}
      expected = {:union, [:atom, :integer, :list]}
      assert_spec_normalized(expected, input)
    end

    @doc "Tests `A | none` simplifies to `A`, as `:none` is the identity for union."
    test "simplifies a union with :none (A | none -> A)" do
      assert_spec_normalized(:atom, {:union, [:atom, :none]})
    end

    @doc "Tests `A | any` simplifies to `any`, as `:any` is the absorbing element for union."
    test "simplifies a union with :any (A | any -> any)" do
      assert_spec_normalized(:any, {:union, [:atom, :any]})
    end

    @doc "An empty set of types is logically equivalent to `:none`."
    test "an empty union simplifies to :none" do
      assert_spec_normalized(:none, {:union, []})
    end

    @doc "A union containing just one type should simplify to that type itself."
    test "a union of a single element simplifies to the element itself" do
      assert_spec_normalized(:atom, {:union, [:atom]})
    end
  end

  describe "Tdd.TypeSpec.normalize/1: Intersection Normalization" do
    @doc "Tests that intersections are canonicalized like unions (flatten, sort, unique)."
    test "flattens, sorts, and uniques members" do
      input = {:intersect, [:integer, {:intersect, [:list, :atom, :integer]}]}
      expected = {:intersect, [:atom, :integer, :list]}
      assert_spec_normalized(expected, input)
    end

    @doc "Tests `A & any` simplifies to `A`, as `:any` is the identity for intersection."
    test "simplifies an intersection with :any (A & any -> A)" do
      assert_spec_normalized(:atom, {:intersect, [:atom, :any]})
    end

    @doc "Tests `A & none` simplifies to `none`, as `:none` is the absorbing element."
    test "simplifies an intersection with :none (A & none -> none)" do
      assert_spec_normalized(:none, {:intersect, [:atom, :none]})
    end

    @doc "An intersection of zero types is logically `any` (no constraints)."
    test "an empty intersection simplifies to :any" do
      assert_spec_normalized(:any, {:intersect, []})
    end

    @doc "An intersection of one type simplifies to the type itself."
    test "an intersection of a single element simplifies to the element itself" do
      assert_spec_normalized(:atom, {:intersect, [:atom]})
    end
  end

  describe "Tdd.TypeSpec.normalize/1: Subtype Reduction" do
    @doc """
    Tests a key simplification: if a union contains a type and its own subtype,
    the subtype is redundant and should be removed. E.g., `(1 | integer)` is just `integer`.
    Here, `:foo` and `:bar` are subtypes of `:atom`, so the union simplifies to `:atom`.
    """
    test "(:foo | :bar | atom) simplifies to atom" do
      input = {:union, [{:literal, :foo}, {:literal, :bar}, :atom]}
      expected = :atom
      assert_spec_normalized(expected, input)
    end
  end

  describe "Tdd.TypeSpec: Advanced Normalization (μ, Λ, Apply)" do
    @doc """
    Tests alpha-conversion for recursive types. The bound variable name (`:X`)
    should be renamed to a canonical name (`:m_var0`) to ensure structural equality
    regardless of the name chosen by the user.
    """
    test "basic alpha-conversion for μ-variable" do
      input = {:mu, :X, {:type_var, :X}}
      expected = {:mu, :m_var0, {:type_var, :m_var0}}
      assert_spec_normalized(expected, input)
    end

    @doc """
    Tests that the syntactic sugar `{:list_of, T}` is correctly desugared into
    its underlying recursive definition: `μT.[] | cons(T, μT)`.
    """
    test "list_of(integer) normalizes to a μ-expression with canonical var" do
      input = {:list_of, :integer}

      expected =
        {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :integer, {:type_var, :m_var0}}]}}

      assert_spec_normalized(expected, input)
    end

    @doc """
    Tests beta-reduction (function application). Applying the identity function
    `(ΛT.T)` to `integer` should result in `integer`.
    """
    test "simple application: (ΛT.T) integer -> integer" do
      input = {:type_apply, {:type_lambda, [:T], {:type_var, :T}}, [:integer]}
      expected = :integer
      assert_spec_normalized(expected, input)
    end

    @doc """
    Tests a more complex beta-reduction. Applying a list constructor lambda
    to `:atom` should produce the normalized form of `list_of(atom)`.
    """
    test "application with structure: (ΛT. list_of(T)) atom -> list_of(atom) (normalized form)" do
      input = {:type_apply, {:type_lambda, [:T], {:list_of, {:type_var, :T}}}, [:atom]}
      expected = {:mu, :m_var0, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :m_var0}}]}}
      assert_spec_normalized(expected, input)
    end
  end

  # ---
  # Tdd.Consistency.Engine Tests
  # These tests validate the logic that detects contradictions in a set of predicate assumptions.
  # ---
  describe "Tdd.Consistency.Engine: Logic for detecting contradictions" do
    # This setup is local to this describe block, which is fine.
    setup do
      Tdd.Store.init()
      id_atom = Tdd.Compiler.spec_to_id(:atom)
      %{id_atom: id_atom}
    end

    @doc "An empty set of assumptions has no contradictions."
    test "an empty assumption map is consistent" do
      assert Engine.check(%{}) == :consistent
    end

    @doc """
    Tests that the engine uses predicate traits to find implied contradictions.
    `v_atom_eq(:foo)` implies `v_is_atom()` is true, which contradicts the explicit
    assumption that `v_is_atom()` is false.
    """
    test "an implied contradiction is caught by expander" do
      assumptions = %{Variable.v_atom_eq(:foo) => true, Variable.v_is_atom() => false}
      assert Engine.check(assumptions) == :contradiction
    end

    @doc "A term cannot belong to two different primary types like :atom and :integer."
    test "two primary types cannot both be true" do
      assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true}
      assert Engine.check(assumptions) == :contradiction
    end

    @doc "A list cannot be empty and simultaneously have properties on its head (which wouldn't exist)."
    test "a list cannot be empty and have a head property", %{id_atom: id_atom} do
      assumptions = %{
        Variable.v_list_is_empty() => true,
        Variable.v_list_head_pred(id_atom) => true
      }

      assert Engine.check(assumptions) == :contradiction
    end

    @doc "Tests for logical contradictions in integer ranges."
    test "int < 10 AND int > 20 is a contradiction" do
      assumptions = %{
        Variable.v_int_lt(10) => true,
        Variable.v_int_gt(20) => true
      }

      assert Engine.check(assumptions) == :contradiction
    end
  end

  # ---
  # Compiler & Algo Integration Tests
  # These tests ensure that the high-level public APIs (`is_subtype`, `spec_to_id`)
  # work correctly by integrating the compiler and the graph algorithms.
  # ---
  describe "Tdd.Compiler and Tdd.Algo Integration: High-level API validation" do
    @doc "Verifies semantic equivalence of types using TDD IDs. e.g., `atom & any` is the same type as `atom`."
    test "basic equivalences" do
      assert_equivalent_specs({:intersect, [:atom, :any]}, :atom)
      assert_equivalent_specs({:union, [:atom, :none]}, :atom)
      assert_equivalent_specs({:intersect, [:atom, :integer]}, :none)
    end

    @doc "Tests the main `is_subtype` public API for simple, non-recursive types."
    test "basic subtyping" do
      assert_subtype({:literal, :foo}, :atom)
      refute_subtype(:atom, {:literal, :foo})
      assert_subtype(:none, :atom)
      assert_subtype(:atom, :any)
    end

    @doc "Tests that impossible type intersections compile to the `:none` (FALSE) node."
    test "contradictions" do
      assert Compiler.spec_to_id({:intersect, [:atom, :integer]}) == Store.false_node_id()

      assert Compiler.spec_to_id({:intersect, [{:literal, :foo}, {:literal, :bar}]}) ==
               Store.false_node_id()
    end
  end

  # ---
  # Tdd.Compiler Advanced Feature Tests
  # These tests target the most complex features: recursive and polymorphic types.
  # ---
  describe "Tdd.Compiler: Advanced Features (μ, Λ, Apply)" do
    test "list subtyping: list(int) <: list(any)" do
      int_list = {:list_of, :integer}
      any_list = {:list_of, :any}
      assert_subtype(:integer, :any)
      assert_subtype(int_list, any_list)
      assert_subtype({:cons, {:literal, 1}, {:literal, []}}, int_list)
    end

    test "list subtyping: list(any) <! list(integer)" do
      int_list = {:list_of, :integer}
      any_list = {:list_of, :any}
      assert_subtype(:integer, :any)
      refute_subtype({:cons, {:literal, :a}, {:literal, []}}, int_list)
      refute_subtype(any_list, int_list)
    end

    @doc "Tests that manually-defined recursive types (like a binary tree) can be compiled and checked correctly."
    test "explicit μ-types" do
      leaf_node = {:literal, :empty_tree}

      tree_spec =
        {:mu, :Tree,
         {:union,
          [
            leaf_node,
            {:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]}
          ]}}

      # Test that it compiles to a valid TDD ID
      assert is_integer(Compiler.spec_to_id(tree_spec))

      # Test that an instance of the tree is correctly identified as a subtype
      simple_tree_instance = {:tuple, [{:literal, :a}, leaf_node, leaf_node]}
      assert_subtype(simple_tree_instance, tree_spec)
    end

    @doc """
    Tests that a polymorphic type created via lambda application is equivalent
    to its manually specialized counterpart. e.g., `(List<T>)(int)` should be the
    same as `List<int>`.
    """
    test "polymorphism (Λ, Apply)" do
      gen_list_lambda = {:type_lambda, [:Tparam], {:list_of, {:type_var, :Tparam}}}
      list_of_int_from_apply = {:type_apply, gen_list_lambda, [:integer]}
      int_list = {:list_of, :integer}

      assert_equivalent_specs(list_of_int_from_apply, int_list)
    end

    test "negate list type" do
      refute_subtype({:negation, {:list_of, :integer}}, :none)
    end
  end
end