package lambda

import (
	"testing"

	"github.com/vic/godnet/pkg/deltanet"
)

// TestOptimalityProperty verifies that Delta-Nets achieves optimal reduction
// as claimed in the paper: "no reduction operation is applied which is rendered
// unnecessary later, and no reduction operation which is necessary is applied
// more than once."
//
// This means every normalizing term should reduce in the theoretical minimum
// number of steps. Perfect confluence guarantees that "every normalizing
// interaction order produces the same result in the same number of interactions."
//
// For each test case, we document the theoretical minimum based on:
// 1. Beta-reductions needed in lambda calculus
// 2. Additional fan/eraser interactions from the Delta-Net encoding
// 3. The paper's claim that Delta-Nets matches Lévy's optimal reduction
func TestOptimalityProperty(t *testing.T) {
	tests := []struct {
		name               string
		input              string
		expectedReductions uint64
		description        string
	}{
		{
			name:               "identity",
			input:              "(x: x)",
			expectedReductions: 0,
			description:        "No reductions needed - already in normal form",
		},
		{
			name:               "id_id",
			input:              "((x: x) (y: y))",
			expectedReductions: 4,
			description:        "1 beta reduction + 3 structural (fan annihilation from encoding)",
		},
		{
			name:               "K_combinator_1arg",
			input:              "(((x: (y: x)) a) b)",
			expectedReductions: 2,
			description:        "K a b → a: 2 beta reductions + erasure of b",
		},
		{
			name:               "K_combinator_2args",
			input:              "((x: (y: x)) a)",
			expectedReductions: 1,
			description:        "K a → λy.a: 1 beta reduction (optimal encoding)",
		},
		{
			name:               "church_zero",
			input:              "(((f: (x: x)) f) x)",
			expectedReductions: 2,
			description:        "Church zero application: (λf.λx.x) f x → x (optimal)",
		},
		{
			name:               "church_one",
			input:              "(((f: (x: (f x))) f) x)",
			expectedReductions: 2,
			description:        "Church one application: reduces to (f x)",
		},
		{
			name:               "church_two",
			input:              "(((f: (x: (f (f x)))) f) x)",
			expectedReductions: 2,
			description:        "Church two application: reduces to (f (f x))",
		},
		{
			name:               "simple_let",
			input:              "((x: x) y)",
			expectedReductions: 1,
			description:        "Simple beta reduction: (λx.x) y → y",
		},
		{
			name:               "boolean_true",
			input:              "((((x: (y: x)) a) b) c)",
			expectedReductions: 2,
			description:        "True combinator applied: returns first argument",
		},
		{
			name:               "boolean_false",
			input:              "((((x: (y: y)) a) b) c)",
			expectedReductions: 2,
			description:        "False combinator applied: returns second argument",
		},
	}

	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			term, err := Parse(tt.input)
			if err != nil {
				t.Fatalf("Parse error: %v", err)
			}

			net := deltanet.NewNetwork()
			root, port, _ := ToDeltaNet(term, net)

			output := net.NewVar()
			net.Link(root, port, output, 0)

			net.ReduceToNormalForm()

			stats := net.GetStats()

			if stats.TotalReductions != tt.expectedReductions {
				t.Errorf("%s: Expected %d reductions (optimal), got %d\nDescription: %s\nDelta: %+d",
					tt.name,
					tt.expectedReductions,
					stats.TotalReductions,
					tt.description,
					int64(stats.TotalReductions)-int64(tt.expectedReductions))
			} else {
				t.Logf("%s: ✓ Optimal - %d reductions\n  %s",
					tt.name,
					stats.TotalReductions,
					tt.description)
			}
		})
	}
}

// TestOptimalityComplexCases tests more complex terms where manual calculation
// of optimal reduction count is harder. These serve as regression tests - if
// counts change, we need to verify the change is correct.
//
// Note: The exact reduction count can vary slightly depending on how the
// let-bindings are encoded. The important property is that we don't exceed
// the theoretical minimum significantly. All tests below use let-bindings
// which add some overhead compared to direct application.
func TestOptimalityComplexCases(t *testing.T) {
	tests := []struct {
		name          string
		input         string
		maxReductions uint64 // Maximum acceptable reductions
		description   string
	}{
		{
			name:          "succ_zero",
			input:         "((succ: (n: (f: (x: (f ((n f) x)))))) (f: (x: x)))",
			maxReductions: 10,
			description:   "Successor of zero - with let-binding overhead",
		},
		{
			name:          "not_true",
			input:         "((not: (b: ((b (x: (y: y))) (x: (y: x))))) (x: (y: x)))",
			maxReductions: 12,
			description:   "Boolean NOT applied to TRUE",
		},
		{
			name:          "not_false",
			input:         "((not: (b: ((b (x: (y: y))) (x: (y: x))))) (x: (y: y)))",
			maxReductions: 12,
			description:   "Boolean NOT applied to FALSE",
		},
		{
			name:          "and_true_true",
			input:         "((and: (a: (b: ((a b) (x: (y: y)))))) ((x: (y: x)) (x: (y: x))))",
			maxReductions: 18,
			description:   "Boolean AND of TRUE and TRUE",
		},
		{
			name:          "and_true_false",
			input:         "((and: (a: (b: ((a b) (x: (y: y)))))) ((x: (y: x)) (x: (y: y))))",
			maxReductions: 18,
			description:   "Boolean AND of TRUE and FALSE",
		},
		{
			name:          "pair_fst",
			input:         "((pair: ((pair (x: (y: x))) a)) b)",
			maxReductions: 5,
			description:   "Extract first element from pair",
		},
		{
			name:          "pair_snd",
			input:         "((pair: ((pair (x: (y: y))) a)) b)",
			maxReductions: 5,
			description:   "Extract second element from pair",
		},
		{
			name:          "s_combinator_1arg",
			input:         "((((x: (y: (z: ((x z) (y z))))) (a: a)) (b: b)) (c: c))",
			maxReductions: 25,
			description:   "S combinator with identity functions: S I I c → c c",
		},
		{
			name:          "s_combinator_partial",
			input:         "(((x: (y: (z: ((x z) (y z))))) (a: a)) (b: b))",
			maxReductions: 12,
			description:   "S combinator partially applied",
		},
	}

	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			term, err := Parse(tt.input)
			if err != nil {
				t.Fatalf("Parse error: %v", err)
			}

			net := deltanet.NewNetwork()
			root, port, _ := ToDeltaNet(term, net)

			output := net.NewVar()
			net.Link(root, port, output, 0)

			net.ReduceToNormalForm()

			stats := net.GetStats()

			if stats.TotalReductions > tt.maxReductions {
				t.Errorf("%s: Exceeded maximum %d reductions, got %d (excess: +%d)\nDescription: %s",
					tt.name,
					tt.maxReductions,
					stats.TotalReductions,
					stats.TotalReductions-tt.maxReductions,
					tt.description)
			} else {
				t.Logf("%s: ✓ %d reductions (≤ %d max)\n  %s",
					tt.name,
					stats.TotalReductions,
					tt.maxReductions,
					tt.description)
			}
		})
	}
}

// TestOptimalityInvariant tests that the reduction count is invariant
// across multiple runs and different reduction orders (due to perfect confluence)
func TestOptimalityInvariant(t *testing.T) {
	input := "((x: x) (y: y))"

	term, err := Parse(input)
	if err != nil {
		t.Fatalf("Parse error: %v", err)
	}

	// Run reduction multiple times
	var counts []uint64
	for i := 0; i < 5; i++ {
		net := deltanet.NewNetwork()
		root, port, _ := ToDeltaNet(term, net)

		output := net.NewVar()
		net.Link(root, port, output, 0)

		net.ReduceToNormalForm()

		stats := net.GetStats()
		counts = append(counts, stats.TotalReductions)
	}

	// All counts should be identical due to perfect confluence
	first := counts[0]
	for i, count := range counts {
		if count != first {
			t.Errorf("Run %d: got %d reductions, expected %d (same as run 0)",
				i, count, first)
		}
	}

	t.Logf("Perfect confluence verified: all 5 runs produced exactly %d reductions", first)
}