// Unicode text diagram
fmt.Println(lambda.Diagram(lambda.Y))
// ┌─────┬───╴
// ├─┬─┐ ├─┬─┐
// │ │ │ │ │ │
// │ ├─┘ │ ├─┘
// ├─┘   ├─┘
// └─────┘

// SVG with custom colors
svg := lambda.DiagramSVG(lambda.Y, &lambda.SVGOptions{
    CellSize:   20,
    Background: "#1a1a2e",
    Saturation: 0.8,
})

// Animated SVG showing beta-reduction steps
anim := lambda.DiagramAnimatedSVG(term, &lambda.AnimationOptions{
    Loop:         true,
    StepDuration: 2.0,
})

package main

import (
    "fmt"
    "github.com/KarpelesLab/lambda"
)

func main() {
    // Identity function: λx.x
    identity := lambda.Abstraction{
        Param: "x",
        Body:  lambda.Var{Name: "x"},
    }
    fmt.Println(identity) // λx.x

    // Apply identity to a variable: (λx.x) y
    applied := lambda.Application{
        Func: identity,
        Arg:  lambda.Var{Name: "y"},
    }
    fmt.Println(applied) // (λx.x) y

    // β-reduction
    result, _ := applied.BetaReduce()
    fmt.Println(result) // y
}

// Create Church numerals
zero := lambda.ChurchNumeral(0)   // λf.λx.x
three := lambda.ChurchNumeral(3)  // λf.λx.f (f (f x))

// Convert back to integers
fmt.Println(lambda.ToInt(three))  // 3

// Addition: 2 + 3
two := lambda.ChurchNumeral(2)
three := lambda.ChurchNumeral(3)

sum := lambda.Application{
    Func: lambda.Application{
        Func: lambda.PLUS,
        Arg:  two,
    },
    Arg: three,
}

// Reduce to normal form
for i := 0; i < 100; i++ {
    reduced, didReduce := sum.BetaReduce()
    if !didReduce {
        break
    }
    sum = reduced
}

fmt.Println(lambda.ToInt(sum)) // 5

// Calculate factorial(3)
three := lambda.ChurchNumeral(3)

result := lambda.Application{
    Func: lambda.FACTORIAL,
    Arg:  three,
}

// Reduce (may take multiple steps)
for i := 0; i < 1000; i++ {
    reduced, didReduce := result.BetaReduce()
    if !didReduce {
        break
    }
    result = reduced
}

fmt.Println(lambda.ToInt(result)) // 6

term := lambda.Abstraction{
    Param: "x",
    Body:  lambda.Var{Name: "x"},
}
renamed := term.AlphaConvert("x", "y") // λx.x → λy.y

// (λx.x) y → y
term := lambda.Application{
    Func: lambda.Abstraction{Param: "x", Body: lambda.Var{Name: "x"}},
    Arg:  lambda.Var{Name: "y"},
}
result, reduced := term.BetaReduce()
// result: y, reduced: true

// λx.(f x) → f (when x is not free in f)
term := lambda.Abstraction{
    Param: "x",
    Body: lambda.Application{
        Func: lambda.Var{Name: "f"},
        Arg:  lambda.Var{Name: "x"},
    },
}
result, converted := term.EtaConvert()
// result: f, converted: true

// (λy.x)[x := y] automatically renames y to avoid capture
abs := lambda.Abstraction{Param: "y", Body: lambda.Var{Name: "x"}}
result := abs.Substitute("x", lambda.Var{Name: "y"})
// Result is automatically renamed to avoid capture

term := lambda.Abstraction{
    Param: "x",
    Body:  lambda.Var{Name: "y"},
}
freeVars := term.FreeVars() // map[string]bool{"y": true}