package debruijn

// Shift increments all free variable indices in an expression by the given amount.
// A variable is free if its index is >= the cutoff (depth of nested abstractions).
// This is necessary when substituting an expression into a different binding context.
func Shift(expr Expression, amount int, cutoff int) Expression {
	switch e := expr.(type) {
	case *Variable:
		if e.index >= cutoff {
			return NewVariable(e.index+amount, e.label)
		}
		return e

	case *Abstraction:
		newBody := Shift(e.body, amount, cutoff+1)
		if newBody == e.body {
			return e
		}
		return NewAbstraction(newBody)

	case *Application:
		newAbs := Shift(e.abstraction, amount, cutoff)
		newArg := Shift(e.argument, amount, cutoff)
		if newAbs == e.abstraction && newArg == e.argument {
			return e
		}
		return NewApplication(newAbs, newArg)

	default:
		return expr
	}
}