fix: unbound substitutions, explanation tag
This commit is contained in:
1
.gitignore
vendored
1
.gitignore
vendored
@@ -25,3 +25,4 @@ go.work.sum
|
|||||||
# env file
|
# env file
|
||||||
.env
|
.env
|
||||||
|
|
||||||
|
*.log
|
||||||
|
|||||||
@@ -4,6 +4,7 @@ import (
|
|||||||
"errors"
|
"errors"
|
||||||
"fmt"
|
"fmt"
|
||||||
"os"
|
"os"
|
||||||
|
"time"
|
||||||
|
|
||||||
"git.maximhutz.com/max/lambda/internal/cli"
|
"git.maximhutz.com/max/lambda/internal/cli"
|
||||||
"git.maximhutz.com/max/lambda/pkg/lambda"
|
"git.maximhutz.com/max/lambda/pkg/lambda"
|
||||||
@@ -35,9 +36,21 @@ func main() {
|
|||||||
cli.HandleError(err)
|
cli.HandleError(err)
|
||||||
logger.Info("Parsed syntax tree.", "tree", lambda.Stringify(expression))
|
logger.Info("Parsed syntax tree.", "tree", lambda.Stringify(expression))
|
||||||
|
|
||||||
for lambda.ReduceOnce(&expression) {
|
start := time.Now()
|
||||||
logger.Info("Reduction.", "tree", lambda.Stringify(expression))
|
|
||||||
|
if options.Explanation {
|
||||||
|
fmt.Println(lambda.Stringify(expression))
|
||||||
}
|
}
|
||||||
|
|
||||||
|
for lambda.ReduceOnce(&expression) {
|
||||||
|
logger.Info("Reduction.", "tree", lambda.Stringify(expression))
|
||||||
|
if options.Explanation {
|
||||||
|
fmt.Println(" =", lambda.Stringify(expression))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
elapsed := time.Since(start).Milliseconds()
|
||||||
|
|
||||||
fmt.Println(lambda.Stringify(expression))
|
fmt.Println(lambda.Stringify(expression))
|
||||||
|
fmt.Fprintln(os.Stderr, "Time Spent:", elapsed, "ms")
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -6,13 +6,15 @@ import (
|
|||||||
)
|
)
|
||||||
|
|
||||||
type CLIOptions struct {
|
type CLIOptions struct {
|
||||||
Input string
|
Input string
|
||||||
Verbose bool
|
Verbose bool
|
||||||
|
Explanation bool
|
||||||
}
|
}
|
||||||
|
|
||||||
func ParseOptions(args []string) (*CLIOptions, error) {
|
func ParseOptions(args []string) (*CLIOptions, error) {
|
||||||
// Parse flags and arguments.
|
// Parse flags and arguments.
|
||||||
verbose := flag.Bool("v", false, "Verbosity. If set, the program will print logs.")
|
verbose := flag.Bool("v", false, "Verbosity. If set, the program will print logs.")
|
||||||
|
explanation := flag.Bool("x", false, "Explanation. Whether or not to show all reduction steps.")
|
||||||
flag.Parse()
|
flag.Parse()
|
||||||
|
|
||||||
if flag.NArg() == 0 {
|
if flag.NArg() == 0 {
|
||||||
@@ -22,7 +24,8 @@ func ParseOptions(args []string) (*CLIOptions, error) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
return &CLIOptions{
|
return &CLIOptions{
|
||||||
Input: flag.Arg(0),
|
Input: flag.Arg(0),
|
||||||
Verbose: *verbose,
|
Verbose: *verbose,
|
||||||
|
Explanation: *explanation,
|
||||||
}, nil
|
}, nil
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -20,7 +20,7 @@ func Substitute(e *Expression, target string, replacement Expression) {
|
|||||||
used := GetFreeVariables(typed.Body)
|
used := GetFreeVariables(typed.Body)
|
||||||
used.Union(replacement_free_vars)
|
used.Union(replacement_free_vars)
|
||||||
fresh_var := GenerateFreshName(used)
|
fresh_var := GenerateFreshName(used)
|
||||||
Rename(typed.Body, typed.Parameter, fresh_var)
|
Rename(typed, typed.Parameter, fresh_var)
|
||||||
Substitute(&typed.Body, target, replacement)
|
Substitute(&typed.Body, target, replacement)
|
||||||
case *Application:
|
case *Application:
|
||||||
Substitute(&typed.Abstraction, target, replacement)
|
Substitute(&typed.Abstraction, target, replacement)
|
||||||
|
|||||||
@@ -20,18 +20,23 @@ func ParseExpression(i *iterator.Iterator[tokenizer.Token]) (lambda.Expression,
|
|||||||
case tokenizer.TokenDot:
|
case tokenizer.TokenDot:
|
||||||
return nil, fmt.Errorf("Token '.' found without a corresponding slash (column %d).", token.Index)
|
return nil, fmt.Errorf("Token '.' found without a corresponding slash (column %d).", token.Index)
|
||||||
case tokenizer.TokenSlash:
|
case tokenizer.TokenSlash:
|
||||||
atom, atom_err := i.Next()
|
atoms := []string{}
|
||||||
if atom_err != nil {
|
|
||||||
return nil, fmt.Errorf("Could not find parameter of function: %w", atom_err)
|
for {
|
||||||
} else if atom.Type != tokenizer.TokenVariable {
|
atom, atom_err := i.Next()
|
||||||
return nil, fmt.Errorf("Expected function parameter, got '%v' (column %d).", atom.Value, atom.Index)
|
if atom_err != nil {
|
||||||
|
return nil, fmt.Errorf("Could not find parameter or terminator of function: %w", atom_err)
|
||||||
|
} else if atom.Type == tokenizer.TokenVariable {
|
||||||
|
atoms = append(atoms, atom.Value)
|
||||||
|
} else if atom.Type == tokenizer.TokenDot {
|
||||||
|
break
|
||||||
|
} else {
|
||||||
|
return nil, fmt.Errorf("Expected function parameter or terminator, got '%v' (column %d).", atom.Value, atom.Index)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
dot, dot_err := i.Next()
|
if len(atoms) == 0 {
|
||||||
if dot_err != nil {
|
return nil, fmt.Errorf("Every function must have atleast one parameter (column %d)", token.Index)
|
||||||
return nil, fmt.Errorf("Could not find function parameter terminator: %w", dot_err)
|
|
||||||
} else if dot.Type != tokenizer.TokenDot {
|
|
||||||
return nil, fmt.Errorf("Expected function parameter terminator, got '%v' (column %v).", dot.Value, dot.Index)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
body, body_err := ParseExpression(i)
|
body, body_err := ParseExpression(i)
|
||||||
@@ -39,16 +44,32 @@ func ParseExpression(i *iterator.Iterator[tokenizer.Token]) (lambda.Expression,
|
|||||||
return nil, fmt.Errorf("Could not parse function body: %w", body_err)
|
return nil, fmt.Errorf("Could not parse function body: %w", body_err)
|
||||||
}
|
}
|
||||||
|
|
||||||
return lambda.NewAbstraction(atom.Value, body), nil
|
// Construction.
|
||||||
|
result := body
|
||||||
|
for i := len(atoms) - 1; i >= 0; i-- {
|
||||||
|
result = lambda.NewAbstraction(atoms[i], result)
|
||||||
|
}
|
||||||
|
|
||||||
|
return result, nil
|
||||||
case tokenizer.TokenOpenParen:
|
case tokenizer.TokenOpenParen:
|
||||||
fn, fn_err := ParseExpression(i)
|
fn, fn_err := ParseExpression(i)
|
||||||
if fn_err != nil {
|
if fn_err != nil {
|
||||||
return nil, fmt.Errorf("Could not parse call function: %w", fn_err)
|
return nil, fmt.Errorf("Could not parse call function: %w", fn_err)
|
||||||
}
|
}
|
||||||
|
|
||||||
arg, arg_err := ParseExpression(i)
|
args := []lambda.Expression{}
|
||||||
if arg_err != nil {
|
|
||||||
return nil, fmt.Errorf("Could not parse call argument: %w", arg_err)
|
for {
|
||||||
|
if next, next_err := i.Peek(); next_err == nil && next.Type == tokenizer.TokenCloseParen {
|
||||||
|
break
|
||||||
|
}
|
||||||
|
|
||||||
|
arg, arg_err := ParseExpression(i)
|
||||||
|
if arg_err != nil {
|
||||||
|
return nil, fmt.Errorf("Could not parse call argument: %w", arg_err)
|
||||||
|
}
|
||||||
|
|
||||||
|
args = append(args, arg)
|
||||||
}
|
}
|
||||||
|
|
||||||
close, close_err := i.Next()
|
close, close_err := i.Next()
|
||||||
@@ -58,7 +79,13 @@ func ParseExpression(i *iterator.Iterator[tokenizer.Token]) (lambda.Expression,
|
|||||||
return nil, fmt.Errorf("Expected call terminating parenthesis, got '%v' (column %v).", close.Value, close.Index)
|
return nil, fmt.Errorf("Expected call terminating parenthesis, got '%v' (column %v).", close.Value, close.Index)
|
||||||
}
|
}
|
||||||
|
|
||||||
return lambda.NewApplication(fn, arg), nil
|
// Construction.
|
||||||
|
result := fn
|
||||||
|
for _, arg := range args {
|
||||||
|
result = lambda.NewApplication(result, arg)
|
||||||
|
}
|
||||||
|
|
||||||
|
return result, nil
|
||||||
case tokenizer.TokenCloseParen:
|
case tokenizer.TokenCloseParen:
|
||||||
return nil, fmt.Errorf("Token ')' found without a corresponding openning parenthesis (column %d).", token.Index)
|
return nil, fmt.Errorf("Token ')' found without a corresponding openning parenthesis (column %d).", token.Index)
|
||||||
default:
|
default:
|
||||||
|
|||||||
@@ -1 +1,16 @@
|
|||||||
(\add.(add (add (add \f.\x.x))) \n.\f.\x.(f ((n f) x)))
|
(\0.
|
||||||
|
(\inc.
|
||||||
|
(\add.
|
||||||
|
(\mult.
|
||||||
|
(\exp.
|
||||||
|
(exp (inc (inc (inc (inc (inc 0))))) (inc (inc (inc (inc (inc 0))))))
|
||||||
|
\n m.(m n)
|
||||||
|
)
|
||||||
|
\m n f.(m (n f))
|
||||||
|
)
|
||||||
|
\n m.(m inc n)
|
||||||
|
)
|
||||||
|
\n f x.(f (n f x))
|
||||||
|
)
|
||||||
|
\f x.x
|
||||||
|
)
|
||||||
Reference in New Issue
Block a user