Compare commits

..

No commits in common. "1a4ed032c212e3b655dcc83834805dfabe94f681" and "94f8963436816aa6326797c8fb3efedb539d3ef9" have entirely different histories.

5 changed files with 216 additions and 328 deletions

View File

@ -1,53 +0,0 @@
from prompt_toolkit.styles import Style
from prompt_toolkit.formatted_text import HTML, to_formatted_text
from prompt_toolkit import print_formatted_text
# | _.._ _.|_
# |_(_|| | ||_)
# 1.1.0
#
# __ __
# ,-` `` `,
# (` \ )
# (` \ `)
# (, / \ _)
# (` / \ )
# `'._.--._.'
#
# A λ calculus engine
style = Style.from_dict({
# Heading
"_h": "#FFFFFF bold",
# Version
"_v": "#B4EC85 bold",
# Lambda
"_l": "#FF6600 bold",
# Subtitle
"_s": "#B4EC85 bold"
})
html = HTML(f"""
<_h> | _.._ _.|_
|_(_|| | ||_)</_h>
<_v>1.1.0</_v>
__ __
,-` `` `,
(` <_l>\\</_l> )
(` <_l>\\</_l> `)
(, <_l>/ \\</_l> _)
(` <_l>/ \\</_l> )
`'._.--._.'
<_s> A λ calculus engine</_s>
"""[1:-1])
def show():
print_formatted_text(html, style = style)

193
main.py
View File

@ -1,87 +1,146 @@
from prompt_toolkit import PromptSession
from prompt_toolkit.completion import WordCompleter
from prompt_toolkit import print_formatted_text
from prompt_toolkit.formatted_text import FormattedText
from prompt_toolkit.formatted_text import to_plain_text
from prompt_toolkit.key_binding import KeyBindings
from pyparsing import exceptions as ppx
from parser import Parser from parser import Parser
from runner import Runner
import tokens import tokens
import greeting import colorama as cr
# Replace "\" with a pretty "λ" in the prompt class lambda_runner:
bindings = KeyBindings() def __init__(self):
@bindings.add("\\") self.macro_table = {}
def _(event): self.expr = None
event.current_buffer.insert_text("λ")
session = PromptSession( # Apply a list of definitions
message = FormattedText([ def run_names(self, lines):
("#00FFFF", "~~> ") print("Added names:")
]), for l in lines:
key_bindings = bindings if isinstance(l, str):
) e = Parser.parse_assign(l)
else:
e = l
if e.label in self.macro_table:
raise NameError(f"Label {e.label} exists!")
greeting.show() e.exp.bind_variables()
self.macro_table[e.label] = e.exp
print(f"\t{e}")
print("\n")
def set_expr(self, expr: str | None = None):
if expr == None:
self.expr = None
print("Removed expression.\n")
return
self.expr = Parser.parse_expression(expr)
self.expr.bind_variables()
print(f"Set expression to {self.expr}\n")
def run(self):
if isinstance(self.expr, tokens.lambda_apply):
self.expr = self.expr.expand(self.macro_table)
elif isinstance(self.expr, tokens.lambda_func):
self.expr = self.expr.expand(self.macro_table)
else:
return None
return self.expr
"""
| _.._ _.|_
|_(_|| | ||_)
1.1.0
r = Runner() __ __
,-` `` `,
(` \ )
(` \ `)
(, / \ _)
(` / \ )
`'._.--._.'
r.run_lines([ A λ calculus engine
"T = λa.λb.a", """
"F = λa.λb.b",
"NOT = \\a.(a F T)", b = cr.Style.BRIGHT
#"AND = a -> b -> (a F b)", v = cr.Fore.GREEN + cr.Style.BRIGHT
#"OR = a -> b -> (a T b)", l = cr.Fore.RED + cr.Style.BRIGHT
#"XOR = a -> b -> (a (NOT a b) b)", n = cr.Style.RESET_ALL
#"w = x -> (x x)", t = cr.Fore.GREEN
#"W = (w w)",
#"Y = f -> ( (x -> (f (x x))) (x -> (f (x x))) )", print(f"""
#"l = if_true -> if_false -> which -> ( which if_true if_false )"
#"inc = n -> f -> x -> (f (n f x))", {b} | _.._ _.|_
#"zero = a -> x -> x", |_(_|| | ||_){n}
#"one = f -> x -> (f x)", {v}1.1.0{n}
__ __
,-` `` `,
(` {l}\{n} )
(` {l}\{n} `)
(, {l}/ \{n} _)
(` {l}/ \{n} )
`'._.--._.'
{t} A λ calculus engine{n}
"""[1:-1])
r = lambda_runner()
r.run_names([
"T = a -> b -> a",
"F = a -> b -> a",
"NOT = a -> (a F T)",
"AND = a -> b -> (a F b)",
"OR = a -> b -> (a T b)",
"XOR = a -> b -> (a (NOT a b) b)"
]) ])
r.run_names([
"w = x -> (x x)",
"W = (w w)",
"Y = f -> ( (x -> (f (x x))) (x -> (f (x x))) )",
#"l = if_true -> if_false -> which -> ( which if_true if_false )"
])
while True: r.run_names([
try: "inc = n -> f -> x -> (f (n f x))",
i = session.prompt() "zero = a -> x -> x",
"one = f -> x -> (f x)",
])
# Catch Ctrl-C and Ctrl-D print("\n")
except KeyboardInterrupt:
print("") #AND = r.run()
break #OR = r.run()
except EOFError: #XOR = r.run()
print("")
r.set_expr(
"(" +
"inc (inc (inc (zero)))"
+ ")"
)
print(repr(r.expr))
print("")
outs = [str(r.expr)]
for i in range(300):
x = r.run()
s = str(x)
p = s if len(s) < 100 else s[:97] + "..."
if s in outs:
print(p)
print("\nLoop detected, exiting.")
break break
if i.strip() == "": if x is None:
continue print("\nCannot evaluate any further.")
break
outs.append(s)
print(p)
try: print(f"Performed {i} {'operations' if i != 1 else 'operation'}.")
x = r.run(i)
except ppx.ParseException as e:
l = len(to_plain_text(session.message))
print_formatted_text(FormattedText([
("#FF0000", " "*(e.loc + l) + "^\n"),
("#FF0000", f"Syntax error at char {e.loc}."),
("#FFFFFF", "\n")
]))
continue
print_formatted_text(FormattedText([
("#00FF00", " = "),
("#FFFFFF", str(x))
]))
print("")

View File

@ -14,24 +14,26 @@ class Parser:
lp = pp.Suppress("(") lp = pp.Suppress("(")
rp = pp.Suppress(")") rp = pp.Suppress(")")
func_char = pp.Suppress("->")
macro_char = pp.Suppress("=")
# Simple tokens # Simple tokens
pp_expr = pp.Forward() pp_expr = pp.Forward()
pp_macro = pp.Word(pp.alphas + "_") pp_name = pp.Word(pp.alphas + "_")
pp_macro.set_parse_action(tokens.macro.from_parse) pp_name.set_parse_action(tokens.macro.from_parse)
# Function definitions. # Function definitions.
# Right associative. # Right associative.
# #
# <var> => <exp> # <var> => <exp>
pp_lambda_fun = (pp.Suppress("λ") | pp.Suppress("\\")) + pp_macro + pp.Suppress(".") + pp_expr pp_lambda_fun = pp_name + func_char + pp_expr
pp_lambda_fun.set_parse_action(tokens.lambda_func.from_parse) pp_lambda_fun.set_parse_action(tokens.lambda_func.from_parse)
# Assignment. # Assignment.
# Can only be found at the start of a line. # Can only be found at the start of a line.
# #
# <var> = <exp> # <var> = <exp>
pp_macro_def = pp.line_start() + pp_macro + pp.Suppress("=") + pp_expr pp_macro_def = pp.line_start() + pp_name + macro_char + pp_expr
pp_macro_def.set_parse_action(tokens.macro_expression.from_parse) pp_macro_def.set_parse_action(tokens.macro_expression.from_parse)
# Function calls. # Function calls.
@ -45,24 +47,18 @@ class Parser:
pp_call <<= pp_expr[2, ...] pp_call <<= pp_expr[2, ...]
pp_call.set_parse_action(tokens.lambda_apply.from_parse) pp_call.set_parse_action(tokens.lambda_apply.from_parse)
pp_expr <<= pp_lambda_fun ^ (lp + pp_expr + rp) ^ pp_macro ^ (lp + pp_call + rp) pp_expr <<= pp_lambda_fun ^ (lp + pp_expr + rp) ^ pp_name ^ (lp + pp_call + rp)
pp_all = pp_expr | pp_macro_def pp_all = pp_expr | pp_macro_def
pp_command = pp.Suppress(":") + pp.Word(pp.alphas + "_") @staticmethod
pp_command.set_parse_action(tokens.command.from_parse) def parse_expression(line):
return Parser.pp_expr.parse_string(line, parse_all = True)[0]
@staticmethod @staticmethod
def parse_line(line): def parse_assign(line):
k = ( return (
Parser.pp_expr ^ Parser.pp_macro_def
Parser.pp_macro_def ^ ).parse_string(line, parse_all = True)[0]
Parser.pp_command ^ Parser.pp_call
).parse_string(
line,
parse_all = True
)[0]
print(k)
return k
@staticmethod @staticmethod
def run_tests(lines): def run_tests(lines):

View File

@ -1,50 +0,0 @@
import tokens
from parser import Parser
class Runner:
def __init__(self):
self.macro_table = {}
self.expr = None
def exec_command(self, command: str):
if command == "help":
print("This is a help message.")
# Apply a list of definitions
def run(self, line: str):
e = Parser.parse_line(line)
if isinstance(e, tokens.macro_expression):
if e.label in self.macro_table:
raise NameError(f"Label {e.label} exists!")
e.exp.bind_variables()
self.macro_table[e.label] = e.exp
elif isinstance(e, tokens.command):
self.exec_command(e.name)
else:
e.bind_variables()
self.expr = e
outs = [str(e)]
for i in range(300):
r = self.expr.reduce(self.macro_table)
self.expr = r.output
s = str(r.output)
p = s if len(s) < 100 else s[:97] + "..."
#if s in outs:
#print(p)
#print("\nLoop detected, exiting.")
#break
if not r.was_reduced:
print("\nCannot evaluate any further.")
break
print(f"Performed {i} {'operations' if i != 1 else 'operation'}.")
return self.expr
def run_lines(self, lines):
for l in lines:
self.run(l)

216
tokens.py
View File

@ -1,53 +1,7 @@
from ast import Lambda from typing import Type
import enum
class ReductionType(enum.Enum):
MACRO_EXPAND = enum.auto()
MACRO_TO_FREE = enum.auto()
FUNCTION_APPLY = enum.auto()
class ReductionStatus: class free_variable:
"""
This object helps organize reduction output.
An instance is returned after every reduction step.
"""
def __init__(
self,
*,
output,
was_reduced: bool,
reduction_type: ReductionType | None = None
):
# The new expression
self.output = output
# What did we do?
# Will be None if was_reduced is false.
self.reduction_type = reduction_type
# Did this reduction change anything?
# If we try to reduce an irreducible expression,
# this will be false.
self.was_reduced = was_reduced
class LambdaToken:
"""
Base class for all lambda tokens.
"""
def bind_variables(self) -> None:
pass
def reduce(self, macro_table) -> ReductionStatus:
return ReductionStatus(
was_reduced = False,
output = self
)
class free_variable(LambdaToken):
""" """
Represents a free variable. Represents a free variable.
@ -68,22 +22,13 @@ class free_variable(LambdaToken):
def __str__(self): def __str__(self):
return f"{self.label}" return f"{self.label}"
class command:
@staticmethod
def from_parse(result):
return command(
result[0],
)
def __init__(self, name): class macro:
self.name = name
class macro(LambdaToken):
""" """
Represents a "macro" in lambda calculus, Represents a "macro" in lambda calculus,
a variable that reduces to an expression. a variable that expands to an expression.
These don't have any inherent logic, they These don't have inherent logic, they
just make writing and reading expressions just make writing and reading expressions
easier. easier.
@ -109,21 +54,14 @@ class macro(LambdaToken):
raise TypeError("Can only compare macro with macro") raise TypeError("Can only compare macro with macro")
return self.name == other.name return self.name == other.name
def reduce(self, macro_table = {}, *, auto_free_vars = True) -> ReductionStatus: def expand(self, macro_table = {}, *, auto_free_vars = True):
if self.name in macro_table: if self.name in macro_table:
return ReductionStatus( return macro_table[self.name]
output = macro_table[self.name],
reduction_type = ReductionType.MACRO_EXPAND,
was_reduced = True
)
elif not auto_free_vars: elif not auto_free_vars:
raise NameError(f"Name {self.name} is not defined!") raise NameError(f"Name {self.name} is not defined!")
else: else:
return ReductionStatus( return free_variable(self.name)
output = free_variable(self.name),
reduction_type = ReductionType.MACRO_TO_FREE,
was_reduced = True
)
class macro_expression: class macro_expression:
""" """
@ -142,7 +80,7 @@ class macro_expression:
result[1] result[1]
) )
def __init__(self, label: str, exp: LambdaToken): def __init__(self, label, exp):
self.label = label self.label = label
self.exp = exp self.exp = exp
@ -153,8 +91,11 @@ class macro_expression:
return f"{self.label} := {self.exp}" return f"{self.label} := {self.exp}"
bound_variable_counter = 0 bound_variable_counter = 0
class bound_variable(LambdaToken): class bound_variable:
def __init__(self, forced_id = None): def __init__(self, forced_id = None):
global bound_variable_counter global bound_variable_counter
@ -172,7 +113,7 @@ class bound_variable(LambdaToken):
def __repr__(self): def __repr__(self):
return f"<in {self.identifier}>" return f"<in {self.identifier}>"
class lambda_func(LambdaToken): class lambda_func:
""" """
Represents a function. Represents a function.
Defined like λa.aa Defined like λa.aa
@ -191,13 +132,9 @@ class lambda_func(LambdaToken):
result[1] result[1]
) )
def __init__( def __init__(self, input_var, output):
self, self.input = input_var
input_var: macro | bound_variable, self.output = output
output: LambdaToken
):
self.input: macro | bound_variable = input_var
self.output: LambdaToken = output
def __repr__(self) -> str: def __repr__(self) -> str:
return f"<{self.input!r}{self.output!r}>" return f"<{self.input!r}{self.output!r}>"
@ -205,6 +142,7 @@ class lambda_func(LambdaToken):
def __str__(self) -> str: def __str__(self) -> str:
return f"λ{self.input}.{self.output}" return f"λ{self.input}.{self.output}"
def bind_variables( def bind_variables(
self, self,
placeholder: macro | None = None, placeholder: macro | None = None,
@ -273,26 +211,30 @@ class lambda_func(LambdaToken):
elif isinstance(self.output, lambda_apply): elif isinstance(self.output, lambda_apply):
self.output.bind_variables(placeholder, val) self.output.bind_variables(placeholder, val)
def reduce(self, macro_table = {}) -> ReductionStatus: # Expand this function's output.
# For functions, this isn't done unless
# its explicitly asked for.
def expand(self, macro_table = {}):
new_out = self.output
if isinstance(self.output, macro):
new_out = self.output.expand(macro_table)
r = self.output.reduce(macro_table) # If the macro becomes a free variable, expand again.
if isinstance(new_out, free_variable):
lambda_func(
self.input,
new_out
).expand(macro_table)
# If a macro becomes a free variable, elif isinstance(self.output, lambda_func):
# reduce twice. new_out = self.output.expand(macro_table)
if r.reduction_type == ReductionType.MACRO_TO_FREE: elif isinstance(self.output, lambda_apply):
self.output = r.output new_out = self.output.expand(macro_table)
return self.reduce(macro_table) return lambda_func(
self.input,
return ReductionStatus( new_out
was_reduced = r.was_reduced,
reduction_type = r.reduction_type,
output = lambda_func(
self.input,
r.output
)
) )
def apply( def apply(
self, self,
val, val,
@ -317,6 +259,8 @@ class lambda_func(LambdaToken):
new_out = self.output.apply(val, bound_var = bound_var) new_out = self.output.apply(val, bound_var = bound_var)
elif isinstance(self.output, lambda_apply): elif isinstance(self.output, lambda_apply):
new_out = self.output.sub_bound_var(val, bound_var = bound_var) new_out = self.output.sub_bound_var(val, bound_var = bound_var)
else:
raise TypeError("Cannot apply a function to {self.output!r}")
# If we're applying THIS function, # If we're applying THIS function,
# just give the output # just give the output
@ -332,7 +276,7 @@ class lambda_func(LambdaToken):
) )
class lambda_apply(LambdaToken): class lambda_apply:
""" """
Represents a function application. Represents a function application.
Has two elements: fn, the function, Has two elements: fn, the function,
@ -359,11 +303,11 @@ class lambda_apply(LambdaToken):
def __init__( def __init__(
self, self,
fn: LambdaToken, fn,
arg: LambdaToken arg
): ):
self.fn: LambdaToken = fn self.fn = fn
self.arg: LambdaToken = arg self.arg = arg
def __repr__(self) -> str: def __repr__(self) -> str:
return f"<{self.fn!r} | {self.arg!r}>" return f"<{self.fn!r} | {self.arg!r}>"
@ -437,48 +381,40 @@ class lambda_apply(LambdaToken):
new_arg new_arg
) )
def reduce(self, macro_table = {}) -> ReductionStatus: def expand(self, macro_table = {}):
# If fn is a function, apply it.
# If we can directly apply self.fn, do so.
if isinstance(self.fn, lambda_func): if isinstance(self.fn, lambda_func):
return ReductionStatus( return self.fn.apply(self.arg)
was_reduced = True, # If fn is an application or macro, expand it.
reduction_type = ReductionType.FUNCTION_APPLY, elif isinstance(self.fn, macro):
output = self.fn.apply(self.arg) f = lambda_apply(
m := self.fn.expand(macro_table),
self.arg
) )
# Otherwise, try to reduce self.fn.
# If that is impossible, try to reduce self.arg.
else:
r = self.fn.reduce(macro_table)
# If a macro becomes a free variable, # If a macro becomes a free variable,
# reduce twice. # expand twice.
if r.reduction_type == ReductionType.MACRO_TO_FREE: if isinstance(m, free_variable):
self.fn = r.output return f.expand(macro_table)
return self.reduce(macro_table)
if r.was_reduced:
return ReductionStatus(
was_reduced = True,
reduction_type = r.reduction_type,
output = lambda_apply(
r.output,
self.arg
)
)
else: else:
r = self.arg.reduce(macro_table) return f
if r.reduction_type == ReductionType.MACRO_TO_FREE: elif isinstance(self.fn, lambda_apply):
self.arg = r.output return lambda_apply(
return self.reduce(macro_table) self.fn.expand(macro_table),
self.arg
)
return ReductionStatus( # If we get to this point, the function we're applying
was_reduced = r.was_reduced, # can't be expanded. That means it's a free or bound
reduction_type = r.reduction_type, # variable. If that happens, expand the arg instead.
output = lambda_apply( elif (
self.fn, isinstance(self.arg, lambda_apply) or
r.output isinstance(self.arg, lambda_func)
) ):
) return lambda_apply(
self.fn,
self.arg.expand(macro_table)
)
return self