Compare commits
2 Commits
main
...
feat/debru
| Author | SHA1 | Date | |
|---|---|---|---|
|
21ae2ca91c
|
|||
|
528956b033
|
@@ -7,7 +7,9 @@ import (
|
||||
"git.maximhutz.com/max/lambda/internal/config"
|
||||
"git.maximhutz.com/max/lambda/internal/plugins"
|
||||
"git.maximhutz.com/max/lambda/pkg/convert"
|
||||
"git.maximhutz.com/max/lambda/pkg/debruijn"
|
||||
"git.maximhutz.com/max/lambda/pkg/lambda"
|
||||
"git.maximhutz.com/max/lambda/pkg/reducer"
|
||||
"git.maximhutz.com/max/lambda/pkg/saccharine"
|
||||
)
|
||||
|
||||
@@ -33,35 +35,51 @@ func main() {
|
||||
compiled := convert.SaccharineToLambda(ast)
|
||||
logger.Info("compiled λ expression", "tree", compiled.String())
|
||||
|
||||
// Create reducer with the compiled expression.
|
||||
reducer := lambda.NewNormalOrderReducer(&compiled)
|
||||
// Create reducer based on the selected interpreter.
|
||||
var red reducer.Reducer
|
||||
switch options.Interpreter {
|
||||
case config.DeBruijnInterpreter:
|
||||
dbExpr := convert.LambdaToDeBruijn(compiled)
|
||||
logger.Info("converted to De Bruijn", "tree", dbExpr.String())
|
||||
red = debruijn.NewNormalOrderReducer(&dbExpr)
|
||||
default:
|
||||
red = lambda.NewNormalOrderReducer(&compiled)
|
||||
}
|
||||
|
||||
// If the user selected to track CPU performance, attach a profiler.
|
||||
if options.Profile != "" {
|
||||
plugins.NewPerformance(options.Profile, reducer)
|
||||
plugins.NewPerformance(options.Profile, red)
|
||||
}
|
||||
|
||||
// If the user selected to produce a step-by-step explanation, attach an
|
||||
// observer.
|
||||
if options.Explanation {
|
||||
plugins.NewExplanation(reducer)
|
||||
plugins.NewExplanation(red)
|
||||
}
|
||||
|
||||
// If the user opted to track statistics, attach a tracker.
|
||||
if options.Statistics {
|
||||
plugins.NewStatistics(reducer)
|
||||
plugins.NewStatistics(red)
|
||||
}
|
||||
|
||||
// If the user selected for verbose debug logs, attach a reduction tracker.
|
||||
if options.Verbose {
|
||||
plugins.NewLogs(logger, reducer)
|
||||
plugins.NewLogs(logger, red)
|
||||
}
|
||||
|
||||
// Run reduction.
|
||||
reducer.Reduce()
|
||||
red.Reduce()
|
||||
|
||||
// Return the final reduced result.
|
||||
result := reducer.Expression().String()
|
||||
// For De Bruijn, convert back to lambda for consistent output.
|
||||
var result string
|
||||
if options.Interpreter == config.DeBruijnInterpreter {
|
||||
dbExpr := red.Expression().(debruijn.Expression)
|
||||
lambdaExpr := convert.DeBruijnToLambda(dbExpr)
|
||||
result = lambdaExpr.String()
|
||||
} else {
|
||||
result = red.Expression().String()
|
||||
}
|
||||
err = options.Destination.Write(result)
|
||||
cli.HandleError(err)
|
||||
}
|
||||
|
||||
@@ -7,6 +7,7 @@ import (
|
||||
"testing"
|
||||
|
||||
"git.maximhutz.com/max/lambda/pkg/convert"
|
||||
"git.maximhutz.com/max/lambda/pkg/debruijn"
|
||||
"git.maximhutz.com/max/lambda/pkg/lambda"
|
||||
"git.maximhutz.com/max/lambda/pkg/saccharine"
|
||||
"github.com/stretchr/testify/assert"
|
||||
@@ -36,7 +37,36 @@ func runSample(samplePath string) (string, error) {
|
||||
return reducer.Expression().String() + "\n", nil
|
||||
}
|
||||
|
||||
// Test that all samples produce expected output.
|
||||
// Helper function to run a single sample through the De Bruijn interpreter.
|
||||
func runSampleDeBruijn(samplePath string) (string, error) {
|
||||
// Read the sample file.
|
||||
input, err := os.ReadFile(samplePath)
|
||||
if err != nil {
|
||||
return "", err
|
||||
}
|
||||
|
||||
// Parse code into syntax tree.
|
||||
ast, err := saccharine.Parse(string(input))
|
||||
if err != nil {
|
||||
return "", err
|
||||
}
|
||||
|
||||
// Compile expression to lambda calculus.
|
||||
compiled := convert.SaccharineToLambda(ast)
|
||||
|
||||
// Convert to De Bruijn and run reducer.
|
||||
dbExpr := convert.LambdaToDeBruijn(compiled)
|
||||
reducer := debruijn.NewNormalOrderReducer(&dbExpr)
|
||||
reducer.Reduce()
|
||||
|
||||
// Convert back to lambda for output.
|
||||
result := reducer.Expression().(debruijn.Expression)
|
||||
lambdaResult := convert.DeBruijnToLambda(result)
|
||||
|
||||
return lambdaResult.String() + "\n", nil
|
||||
}
|
||||
|
||||
// Test that all samples produce expected output with lambda interpreter.
|
||||
func TestSamplesValidity(t *testing.T) {
|
||||
// Discover all .test files in the tests directory.
|
||||
testFiles, err := filepath.Glob("../../tests/*.test")
|
||||
@@ -65,6 +95,35 @@ func TestSamplesValidity(t *testing.T) {
|
||||
}
|
||||
}
|
||||
|
||||
// Test that all samples produce expected output with De Bruijn interpreter.
|
||||
func TestSamplesValidityDeBruijn(t *testing.T) {
|
||||
// Discover all .test files in the tests directory.
|
||||
testFiles, err := filepath.Glob("../../tests/*.test")
|
||||
assert.NoError(t, err, "Failed to read tests directory.")
|
||||
assert.NotEmpty(t, testFiles, "No '*.test' files found in directory.")
|
||||
|
||||
for _, testPath := range testFiles {
|
||||
// Build expected file path.
|
||||
expectedPath := strings.TrimSuffix(testPath, filepath.Ext(testPath)) + ".expected"
|
||||
|
||||
name := strings.TrimSuffix(filepath.Base(testPath), filepath.Ext(testPath))
|
||||
|
||||
t.Run(name, func(t *testing.T) {
|
||||
// Run the sample and capture output.
|
||||
actual, err := runSampleDeBruijn(testPath)
|
||||
assert.NoError(t, err, "Failed to run sample.")
|
||||
|
||||
// Read expected output.
|
||||
expectedBytes, err := os.ReadFile(expectedPath)
|
||||
assert.NoError(t, err, "Failed to read expected output.")
|
||||
expected := string(expectedBytes)
|
||||
|
||||
// Compare outputs.
|
||||
assert.Equal(t, expected, actual, "Output does not match expected.")
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
// Benchmark all samples using sub-benchmarks.
|
||||
func BenchmarkSamples(b *testing.B) {
|
||||
// Discover all .test files in the tests directory.
|
||||
@@ -83,3 +142,22 @@ func BenchmarkSamples(b *testing.B) {
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
// Benchmark all samples using De Bruijn interpreter.
|
||||
func BenchmarkSamplesDeBruijn(b *testing.B) {
|
||||
// Discover all .test files in the tests directory.
|
||||
testFiles, err := filepath.Glob("../../tests/*.test")
|
||||
assert.NoError(b, err, "Failed to read tests directory.")
|
||||
assert.NotEmpty(b, testFiles, "No '*.test' files found in directory.")
|
||||
|
||||
for _, path := range testFiles {
|
||||
name := strings.TrimSuffix(filepath.Base(path), filepath.Ext(path))
|
||||
|
||||
b.Run(name, func(b *testing.B) {
|
||||
for b.Loop() {
|
||||
_, err := runSampleDeBruijn(path)
|
||||
assert.NoError(b, err, "Failed to run sample.")
|
||||
}
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,6 +1,14 @@
|
||||
// Package "config" parses ad handles the user settings given to the program.
|
||||
package config
|
||||
|
||||
// Interpreter specifies the reduction engine to use.
|
||||
type Interpreter string
|
||||
|
||||
const (
|
||||
LambdaInterpreter Interpreter = "lambda"
|
||||
DeBruijnInterpreter Interpreter = "debruijn"
|
||||
)
|
||||
|
||||
// Configuration settings for the program.
|
||||
type Config struct {
|
||||
Source Source // The source code given to the program.
|
||||
@@ -9,4 +17,5 @@ type Config struct {
|
||||
Explanation bool // Whether or not to print an explanation of the reduction.
|
||||
Profile string // If not nil, print a CPU profile during execution.
|
||||
Statistics bool // Whether or not to print statistics.
|
||||
Interpreter Interpreter // The interpreter engine to use.
|
||||
}
|
||||
|
||||
@@ -14,8 +14,20 @@ func FromArgs() (*Config, error) {
|
||||
profile := flag.String("p", "", "CPU profiling. If an output file is defined, the program will profile its execution and dump its results into it.")
|
||||
file := flag.String("f", "", "File. If set, read source from the specified file.")
|
||||
output := flag.String("o", "", "Output. If set, write result to the specified file. Use '-' for stdout (default).")
|
||||
interpreter := flag.String("i", "lambda", "Interpreter. The reduction engine to use: 'lambda' or 'debruijn'.")
|
||||
flag.Parse()
|
||||
|
||||
// Validate interpreter flag.
|
||||
var interpType Interpreter
|
||||
switch *interpreter {
|
||||
case "lambda":
|
||||
interpType = LambdaInterpreter
|
||||
case "debruijn":
|
||||
interpType = DeBruijnInterpreter
|
||||
default:
|
||||
return nil, fmt.Errorf("invalid interpreter: %s (must be 'lambda' or 'debruijn')", *interpreter)
|
||||
}
|
||||
|
||||
// Parse source type.
|
||||
var source Source
|
||||
if *file != "" {
|
||||
@@ -52,5 +64,6 @@ func FromArgs() (*Config, error) {
|
||||
Explanation: *explanation,
|
||||
Profile: *profile,
|
||||
Statistics: *statistics,
|
||||
Interpreter: interpType,
|
||||
}, nil
|
||||
}
|
||||
|
||||
82
pkg/convert/debruijn_to_lambda.go
Normal file
82
pkg/convert/debruijn_to_lambda.go
Normal file
@@ -0,0 +1,82 @@
|
||||
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
|
||||
}
|
||||
}
|
||||
}
|
||||
44
pkg/convert/lambda_to_debruijn.go
Normal file
44
pkg/convert/lambda_to_debruijn.go
Normal file
@@ -0,0 +1,44 @@
|
||||
package convert
|
||||
|
||||
import (
|
||||
"git.maximhutz.com/max/lambda/pkg/debruijn"
|
||||
"git.maximhutz.com/max/lambda/pkg/lambda"
|
||||
)
|
||||
|
||||
// LambdaToDeBruijn converts a lambda calculus expression to De Bruijn indexed form.
|
||||
// The context parameter tracks bound variables from outer abstractions.
|
||||
func LambdaToDeBruijn(expr lambda.Expression) debruijn.Expression {
|
||||
return lambdaToDeBruijnWithContext(expr, []string{})
|
||||
}
|
||||
|
||||
func lambdaToDeBruijnWithContext(expr lambda.Expression, context []string) debruijn.Expression {
|
||||
switch e := expr.(type) {
|
||||
case *lambda.Variable:
|
||||
name := e.Value()
|
||||
// Search for the variable in the context (innermost to outermost).
|
||||
for i := len(context) - 1; i >= 0; i-- {
|
||||
if context[i] == name {
|
||||
index := len(context) - 1 - i
|
||||
return debruijn.NewVariable(index, name)
|
||||
}
|
||||
}
|
||||
// Free variable: use a negative index to mark it.
|
||||
// We encode free variables with index = len(context) + position.
|
||||
// For simplicity, we use a large index that won't conflict.
|
||||
return debruijn.NewVariable(len(context), name)
|
||||
|
||||
case *lambda.Abstraction:
|
||||
// Add the parameter to the context.
|
||||
newContext := append(context, e.Parameter())
|
||||
body := lambdaToDeBruijnWithContext(e.Body(), newContext)
|
||||
return debruijn.NewAbstraction(body)
|
||||
|
||||
case *lambda.Application:
|
||||
abs := lambdaToDeBruijnWithContext(e.Abstraction(), context)
|
||||
arg := lambdaToDeBruijnWithContext(e.Argument(), context)
|
||||
return debruijn.NewApplication(abs, arg)
|
||||
|
||||
default:
|
||||
panic("unknown expression type")
|
||||
}
|
||||
}
|
||||
119
pkg/debruijn/expression.go
Normal file
119
pkg/debruijn/expression.go
Normal file
@@ -0,0 +1,119 @@
|
||||
// Package debruijn provides De Bruijn indexed lambda calculus expressions.
|
||||
// De Bruijn indices eliminate the need for variable names by using numeric
|
||||
// indices to refer to bound variables, avoiding capture issues during substitution.
|
||||
package debruijn
|
||||
|
||||
import "git.maximhutz.com/max/lambda/pkg/expr"
|
||||
|
||||
// Expression is the interface for all De Bruijn indexed expression types.
|
||||
// It embeds the general expr.Expression interface for cross-mode compatibility.
|
||||
type Expression interface {
|
||||
expr.Expression
|
||||
Accept(Visitor)
|
||||
}
|
||||
|
||||
/** ------------------------------------------------------------------------- */
|
||||
|
||||
// Abstraction represents a lambda abstraction without a named parameter.
|
||||
// In De Bruijn notation, the parameter is implicit and referenced by index 0
|
||||
// within the body.
|
||||
type Abstraction struct {
|
||||
body Expression
|
||||
}
|
||||
|
||||
// Body returns the body of the abstraction.
|
||||
func (a *Abstraction) Body() Expression {
|
||||
return a.body
|
||||
}
|
||||
|
||||
// Accept implements the Visitor pattern.
|
||||
func (a *Abstraction) Accept(v Visitor) {
|
||||
v.VisitAbstraction(a)
|
||||
}
|
||||
|
||||
// String returns the De Bruijn notation string representation.
|
||||
func (a *Abstraction) String() string {
|
||||
return Stringify(a)
|
||||
}
|
||||
|
||||
// NewAbstraction creates a new De Bruijn abstraction with the given body.
|
||||
func NewAbstraction(body Expression) *Abstraction {
|
||||
return &Abstraction{body: body}
|
||||
}
|
||||
|
||||
/** ------------------------------------------------------------------------- */
|
||||
|
||||
// Application represents the application of one expression to another.
|
||||
type Application struct {
|
||||
abstraction Expression
|
||||
argument Expression
|
||||
}
|
||||
|
||||
// Abstraction returns the function expression being applied.
|
||||
func (a *Application) Abstraction() Expression {
|
||||
return a.abstraction
|
||||
}
|
||||
|
||||
// Argument returns the argument expression.
|
||||
func (a *Application) Argument() Expression {
|
||||
return a.argument
|
||||
}
|
||||
|
||||
// Accept implements the Visitor pattern.
|
||||
func (a *Application) Accept(v Visitor) {
|
||||
v.VisitApplication(a)
|
||||
}
|
||||
|
||||
// String returns the De Bruijn notation string representation.
|
||||
func (a *Application) String() string {
|
||||
return Stringify(a)
|
||||
}
|
||||
|
||||
// NewApplication creates a new application expression.
|
||||
func NewApplication(abstraction Expression, argument Expression) *Application {
|
||||
return &Application{abstraction: abstraction, argument: argument}
|
||||
}
|
||||
|
||||
/** ------------------------------------------------------------------------- */
|
||||
|
||||
// Variable represents a De Bruijn indexed variable.
|
||||
// The index indicates how many binders to skip to find the binding abstraction.
|
||||
// The label is an optional hint for display purposes.
|
||||
type Variable struct {
|
||||
index int
|
||||
label string
|
||||
}
|
||||
|
||||
// Index returns the De Bruijn index.
|
||||
func (v *Variable) Index() int {
|
||||
return v.index
|
||||
}
|
||||
|
||||
// Label returns the optional variable label.
|
||||
func (v *Variable) Label() string {
|
||||
return v.label
|
||||
}
|
||||
|
||||
// Accept implements the Visitor pattern.
|
||||
func (v *Variable) Accept(visitor Visitor) {
|
||||
visitor.VisitVariable(v)
|
||||
}
|
||||
|
||||
// String returns the De Bruijn notation string representation.
|
||||
func (v *Variable) String() string {
|
||||
return Stringify(v)
|
||||
}
|
||||
|
||||
// NewVariable creates a new De Bruijn variable with the given index and label.
|
||||
func NewVariable(index int, label string) *Variable {
|
||||
return &Variable{index: index, label: label}
|
||||
}
|
||||
|
||||
/** ------------------------------------------------------------------------- */
|
||||
|
||||
// Visitor interface for traversing De Bruijn expressions.
|
||||
type Visitor interface {
|
||||
VisitAbstraction(*Abstraction)
|
||||
VisitApplication(*Application)
|
||||
VisitVariable(*Variable)
|
||||
}
|
||||
76
pkg/debruijn/iterator.go
Normal file
76
pkg/debruijn/iterator.go
Normal file
@@ -0,0 +1,76 @@
|
||||
package debruijn
|
||||
|
||||
// Iterator provides depth-first traversal of De Bruijn expressions.
|
||||
type Iterator struct {
|
||||
trace []*Expression
|
||||
}
|
||||
|
||||
// NewIterator creates a new iterator starting at the given expression.
|
||||
func NewIterator(expr *Expression) *Iterator {
|
||||
return &Iterator{[]*Expression{expr}}
|
||||
}
|
||||
|
||||
// Done returns true when the iterator has finished traversal.
|
||||
func (i *Iterator) Done() bool {
|
||||
return len(i.trace) == 0
|
||||
}
|
||||
|
||||
// Current returns a pointer to the current expression.
|
||||
func (i *Iterator) Current() *Expression {
|
||||
if i.Done() {
|
||||
return nil
|
||||
}
|
||||
|
||||
return i.trace[len(i.trace)-1]
|
||||
}
|
||||
|
||||
// Parent returns a pointer to the parent expression.
|
||||
func (i *Iterator) Parent() *Expression {
|
||||
if len(i.trace) < 2 {
|
||||
return nil
|
||||
}
|
||||
|
||||
return i.trace[len(i.trace)-2]
|
||||
}
|
||||
|
||||
// Swap replaces the current expression with the given expression.
|
||||
func (i *Iterator) Swap(with Expression) {
|
||||
current := i.Current()
|
||||
if current != nil {
|
||||
*current = with
|
||||
}
|
||||
}
|
||||
|
||||
// Back moves the iterator back to the parent expression.
|
||||
func (i *Iterator) Back() bool {
|
||||
if i.Done() {
|
||||
return false
|
||||
}
|
||||
|
||||
i.trace = i.trace[:len(i.trace)-1]
|
||||
return true
|
||||
}
|
||||
|
||||
// Next advances the iterator to the next expression in leftmost-outermost order.
|
||||
func (i *Iterator) Next() {
|
||||
switch typed := (*i.Current()).(type) {
|
||||
case *Abstraction:
|
||||
i.trace = append(i.trace, &typed.body)
|
||||
case *Application:
|
||||
i.trace = append(i.trace, &typed.abstraction)
|
||||
case *Variable:
|
||||
for len(i.trace) > 1 {
|
||||
if app, ok := (*i.Parent()).(*Application); ok {
|
||||
if app.abstraction == *i.Current() {
|
||||
i.Back()
|
||||
i.trace = append(i.trace, &app.argument)
|
||||
return
|
||||
}
|
||||
}
|
||||
|
||||
i.Back()
|
||||
}
|
||||
|
||||
i.trace = []*Expression{}
|
||||
}
|
||||
}
|
||||
66
pkg/debruijn/reducer.go
Normal file
66
pkg/debruijn/reducer.go
Normal file
@@ -0,0 +1,66 @@
|
||||
package debruijn
|
||||
|
||||
import (
|
||||
"git.maximhutz.com/max/lambda/pkg/emitter"
|
||||
"git.maximhutz.com/max/lambda/pkg/expr"
|
||||
"git.maximhutz.com/max/lambda/pkg/reducer"
|
||||
)
|
||||
|
||||
// NormalOrderReducer implements normal order (leftmost-outermost) reduction
|
||||
// for De Bruijn indexed lambda calculus expressions.
|
||||
type NormalOrderReducer struct {
|
||||
emitter.BaseEmitter[reducer.Event]
|
||||
expression *Expression
|
||||
}
|
||||
|
||||
// NewNormalOrderReducer creates a new normal order reducer.
|
||||
func NewNormalOrderReducer(expression *Expression) *NormalOrderReducer {
|
||||
return &NormalOrderReducer{
|
||||
BaseEmitter: *emitter.New[reducer.Event](),
|
||||
expression: expression,
|
||||
}
|
||||
}
|
||||
|
||||
// Expression returns the current expression state.
|
||||
func (r *NormalOrderReducer) Expression() expr.Expression {
|
||||
return *r.expression
|
||||
}
|
||||
|
||||
// isViable checks if an expression is a redex (reducible expression).
|
||||
// A redex is an application of an abstraction to an argument.
|
||||
func isViable(e *Expression) (*Abstraction, Expression, bool) {
|
||||
if e == nil {
|
||||
return nil, nil, false
|
||||
} else if app, appOk := (*e).(*Application); !appOk {
|
||||
return nil, nil, false
|
||||
} else if fn, fnOk := app.abstraction.(*Abstraction); !fnOk {
|
||||
return nil, nil, false
|
||||
} else {
|
||||
return fn, app.argument, true
|
||||
}
|
||||
}
|
||||
|
||||
// Reduce performs normal order reduction on a De Bruijn expression.
|
||||
func (r *NormalOrderReducer) Reduce() {
|
||||
r.Emit(reducer.StartEvent)
|
||||
it := NewIterator(r.expression)
|
||||
|
||||
for !it.Done() {
|
||||
if fn, arg, ok := isViable(it.Current()); !ok {
|
||||
it.Next()
|
||||
} else {
|
||||
// Substitute arg for variable 0 in the body.
|
||||
substituted := Substitute(fn.body, 0, Shift(arg, 1, 0))
|
||||
// Shift down to account for the removed abstraction.
|
||||
it.Swap(Shift(substituted, -1, 0))
|
||||
|
||||
r.Emit(reducer.StepEvent)
|
||||
|
||||
if _, _, ok := isViable(it.Parent()); ok {
|
||||
it.Back()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
r.Emit(reducer.StopEvent)
|
||||
}
|
||||
32
pkg/debruijn/shift.go
Normal file
32
pkg/debruijn/shift.go
Normal file
@@ -0,0 +1,32 @@
|
||||
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
|
||||
}
|
||||
}
|
||||
35
pkg/debruijn/stringify.go
Normal file
35
pkg/debruijn/stringify.go
Normal file
@@ -0,0 +1,35 @@
|
||||
package debruijn
|
||||
|
||||
import (
|
||||
"strconv"
|
||||
"strings"
|
||||
)
|
||||
|
||||
type stringifyVisitor struct {
|
||||
builder strings.Builder
|
||||
}
|
||||
|
||||
func (v *stringifyVisitor) VisitVariable(a *Variable) {
|
||||
v.builder.WriteString(strconv.Itoa(a.index))
|
||||
}
|
||||
|
||||
func (v *stringifyVisitor) VisitAbstraction(f *Abstraction) {
|
||||
v.builder.WriteRune('\\')
|
||||
v.builder.WriteRune('.')
|
||||
f.body.Accept(v)
|
||||
}
|
||||
|
||||
func (v *stringifyVisitor) VisitApplication(c *Application) {
|
||||
v.builder.WriteRune('(')
|
||||
c.abstraction.Accept(v)
|
||||
v.builder.WriteRune(' ')
|
||||
c.argument.Accept(v)
|
||||
v.builder.WriteRune(')')
|
||||
}
|
||||
|
||||
// Stringify converts a De Bruijn expression to its string representation.
|
||||
func Stringify(e Expression) string {
|
||||
b := &stringifyVisitor{builder: strings.Builder{}}
|
||||
e.Accept(b)
|
||||
return b.builder.String()
|
||||
}
|
||||
34
pkg/debruijn/substitute.go
Normal file
34
pkg/debruijn/substitute.go
Normal file
@@ -0,0 +1,34 @@
|
||||
package debruijn
|
||||
|
||||
// Substitute replaces the variable at the given index with the replacement expression.
|
||||
// The replacement is shifted appropriately as we descend into nested abstractions.
|
||||
func Substitute(expr Expression, index int, replacement Expression) Expression {
|
||||
switch e := expr.(type) {
|
||||
case *Variable:
|
||||
if e.index == index {
|
||||
return replacement
|
||||
}
|
||||
return e
|
||||
|
||||
case *Abstraction:
|
||||
// When entering an abstraction, increment the target index and shift the
|
||||
// replacement to account for the new binding context.
|
||||
shiftedReplacement := Shift(replacement, 1, 0)
|
||||
newBody := Substitute(e.body, index+1, shiftedReplacement)
|
||||
if newBody == e.body {
|
||||
return e
|
||||
}
|
||||
return NewAbstraction(newBody)
|
||||
|
||||
case *Application:
|
||||
newAbs := Substitute(e.abstraction, index, replacement)
|
||||
newArg := Substitute(e.argument, index, replacement)
|
||||
if newAbs == e.abstraction && newArg == e.argument {
|
||||
return e
|
||||
}
|
||||
return NewApplication(newAbs, newArg)
|
||||
|
||||
default:
|
||||
return expr
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user