M.V. Hutz
528956b033
Add a new interpreter option (-i debruijn) that uses De Bruijn indices for variable representation, eliminating the need for variable renaming during substitution. - Add -i flag to select interpreter (lambda or debruijn) - Create debruijn package with Expression types (Variable with index, Abstraction without parameter, Application) - Implement shift and substitute operations for De Bruijn indices - Add conversion functions between lambda and De Bruijn representations - Update CLI to support switching between interpreters - Add De Bruijn tests to verify all samples pass Closes #26
83 lines
2.3 KiB
Go
83 lines
2.3 KiB
Go
package convert
|
|
|
|
import (
|
|
"fmt"
|
|
|
|
"git.maximhutz.com/max/lambda/pkg/debruijn"
|
|
"git.maximhutz.com/max/lambda/pkg/lambda"
|
|
"git.maximhutz.com/max/lambda/pkg/set"
|
|
)
|
|
|
|
// DeBruijnToLambda converts a De Bruijn indexed expression back to named lambda calculus.
|
|
func DeBruijnToLambda(expr debruijn.Expression) lambda.Expression {
|
|
return deBruijnToLambdaWithContext(expr, []string{})
|
|
}
|
|
|
|
func deBruijnToLambdaWithContext(expr debruijn.Expression, context []string) lambda.Expression {
|
|
switch e := expr.(type) {
|
|
case *debruijn.Variable:
|
|
index := e.Index()
|
|
if index < len(context) {
|
|
// Bound variable: look up name in context.
|
|
name := context[len(context)-1-index]
|
|
return lambda.NewVariable(name)
|
|
}
|
|
// Free variable: use the label if available.
|
|
if e.Label() != "" {
|
|
return lambda.NewVariable(e.Label())
|
|
}
|
|
// Generate a name for free variables without labels.
|
|
return lambda.NewVariable(fmt.Sprintf("free%d", index))
|
|
|
|
case *debruijn.Abstraction:
|
|
// Generate a fresh parameter name.
|
|
used := collectUsedNames(e.Body(), context)
|
|
paramName := generateFreshName(used)
|
|
newContext := append(context, paramName)
|
|
body := deBruijnToLambdaWithContext(e.Body(), newContext)
|
|
return lambda.NewAbstraction(paramName, body)
|
|
|
|
case *debruijn.Application:
|
|
abs := deBruijnToLambdaWithContext(e.Abstraction(), context)
|
|
arg := deBruijnToLambdaWithContext(e.Argument(), context)
|
|
return lambda.NewApplication(abs, arg)
|
|
|
|
default:
|
|
panic("unknown expression type")
|
|
}
|
|
}
|
|
|
|
// collectUsedNames gathers all variable labels used in an expression.
|
|
func collectUsedNames(expr debruijn.Expression, context []string) *set.Set[string] {
|
|
used := set.New[string]()
|
|
for _, name := range context {
|
|
used.Add(name)
|
|
}
|
|
collectUsedNamesHelper(expr, used)
|
|
return used
|
|
}
|
|
|
|
func collectUsedNamesHelper(expr debruijn.Expression, used *set.Set[string]) {
|
|
switch e := expr.(type) {
|
|
case *debruijn.Variable:
|
|
if e.Label() != "" {
|
|
used.Add(e.Label())
|
|
}
|
|
case *debruijn.Abstraction:
|
|
collectUsedNamesHelper(e.Body(), used)
|
|
case *debruijn.Application:
|
|
collectUsedNamesHelper(e.Abstraction(), used)
|
|
collectUsedNamesHelper(e.Argument(), used)
|
|
}
|
|
}
|
|
|
|
// generateFreshName creates a fresh variable name not in the used set.
|
|
func generateFreshName(used *set.Set[string]) string {
|
|
for i := 0; ; i++ {
|
|
name := fmt.Sprintf("_%d", i)
|
|
if !used.Has(name) {
|
|
return name
|
|
}
|
|
}
|
|
}
|