Compare commits

...

5 Commits

Author SHA1 Message Date
Mark 3ff496e1d6
Added a few commands 2022-10-21 17:55:31 -07:00
Mark 84c5229fbf
Updated README 2022-10-21 17:14:20 -07:00
Mark a4af47435a
Improved macro reduction 2022-10-21 17:13:58 -07:00
Mark 01632f6ec3
Updated README 2022-10-21 17:13:35 -07:00
Mark 696ede7a9c
Added runstatus and prettified prompt 2022-10-21 17:05:25 -07:00
7 changed files with 326 additions and 54 deletions

View File

@ -3,13 +3,10 @@
## Todo (pre-release):
- Fix parser (call parentheses)
- Good command parsing (`:help`, `:save`, `:load`, `:macros` as a bare minimum)
- Good command parsing (`:save`, `:load`, are a bare minimum)
- Python files: installable, package list, etc
- $\alpha$-equivalence check
- Don't expand macros until you absolutely have to
- Versioning
- Clean up runner & printing
- Count reductions
## Todo:
- live syntax check
@ -17,3 +14,6 @@
- step-by-step reduction
- Documentation in README
- Maybe a better icon?
- Warn when overwriting macro
- Syntax highlighting: parenthesis, bound variables, macros, etc
- Pin header to top of screen

96
commands.py Normal file
View File

@ -0,0 +1,96 @@
from prompt_toolkit.formatted_text import FormattedText
from prompt_toolkit.shortcuts import clear as clear_screen
from runstatus import CommandStatus
import greeting
commands = {}
help_texts = {}
def lamb_command(*, help_text: str):
def inner(func):
commands[func.__name__] = func
help_texts[func.__name__] = help_text
return inner
def run(command, runner):
return commands[command](runner)
@lamb_command(help_text = "Show macros")
def macros(runner):
return CommandStatus(
formatted_text = FormattedText([
("#FF6600 bold", "\nDefined Macros:\n"),
] +
[
("#FFFFFF", f"\t{name} \t {exp}\n")
for name, exp in runner.macro_table.items()
]
)
)
@lamb_command(help_text = "Clear the screen")
def clear(runner):
clear_screen()
greeting.show()
@lamb_command(help_text = "Print this help")
def help(runner):
return CommandStatus(
formatted_text = FormattedText([
("#FF6600 bold", "\nUsage:\n"),
(
"#FFFFFF",
"\tWrite lambda expressions using your "
),
(
"#00FF00",
"\\"
),
(
"#FFFFFF",
" key.\n" +
"\tMacros can be defined using "
),
("#00FF00", "="),
(
"#FFFFFF",
", as in "
),
(
"#AAAAAA bold",
"T = λab.a\n"
),
(
"#FFFFFF",
"\tRun commands using "
),
(
"#00FF00",
":"
),
(
"#FFFFFF",
", for example "
),
(
"#AAAAAA bold",
":help"
),
("#FF6600 bold", "\n\nCommands:\n")
] +
[
("#FFFFFF", f"\t{name} \t {text}\n")
for name, text in help_texts.items()
]
)
)

View File

@ -1,6 +1,6 @@
from prompt_toolkit.styles import Style
from prompt_toolkit.formatted_text import HTML, to_formatted_text
from prompt_toolkit import print_formatted_text
from prompt_toolkit import print_formatted_text as printf
@ -30,7 +30,10 @@ style = Style.from_dict({
"_l": "#FF6600 bold",
# Subtitle
"_s": "#B4EC85 bold"
"_s": "#B4EC85 bold",
# :help message
"_p": "#AAAAAA"
})
html = HTML(f"""
@ -46,8 +49,9 @@ html = HTML(f"""
`'._.--._.'
<_s> A λ calculus engine</_s>
<_p> Type :help for help</_p>
"""[1:-1])
def show():
print_formatted_text(html, style = style)
printf(html, style = style)

38
main.py
View File

@ -1,6 +1,6 @@
from prompt_toolkit import PromptSession
from prompt_toolkit.completion import WordCompleter
from prompt_toolkit import print_formatted_text
from prompt_toolkit import print_formatted_text as printf
from prompt_toolkit.formatted_text import FormattedText
from prompt_toolkit.formatted_text import to_plain_text
from prompt_toolkit.key_binding import KeyBindings
@ -8,7 +8,7 @@ from prompt_toolkit.key_binding import KeyBindings
from pyparsing import exceptions as ppx
from parser import Parser
from runner import Runner
import runner
import tokens
import greeting
@ -27,12 +27,13 @@ session = PromptSession(
)
printf("\n")
greeting.show()
r = Runner()
r = runner.Runner()
r.run_lines([
"T = λa.λb.a",
@ -57,31 +58,50 @@ while True:
# Catch Ctrl-C and Ctrl-D
except KeyboardInterrupt:
print("")
printf("\n\nGoodbye.\n")
break
except EOFError:
print("")
printf("\n\nGoodbye.\n")
break
# Skip empty lines
if i.strip() == "":
continue
# Try to run an input line.
# Catch parse errors and point them out.
try:
x = r.run(i)
except ppx.ParseException as e:
l = len(to_plain_text(session.message))
print_formatted_text(FormattedText([
printf(FormattedText([
("#FF0000", " "*(e.loc + l) + "^\n"),
("#FF0000", f"Syntax error at char {e.loc}."),
("#FFFFFF", "\n")
]))
continue
# If this line defined a macro, print nothing.
if isinstance(x, runner.MacroStatus):
pass
print_formatted_text(FormattedText([
("#00FF00", " = "),
("#FFFFFF", str(x))
if isinstance(x, runner.CommandStatus):
printf(x.formatted_text)
# If this line was an expression, print reduction status
elif isinstance(x, runner.ReduceStatus):
printf(FormattedText([
("#00FF00 bold", f"\nExit reason: "),
x.stop_reason.value,
("#00FF00 bold", f"\nReduction count: "),
("#FFFFFF", str(x.reduction_count)),
("#00FF00 bold", "\n\n => "),
("#FFFFFF", str(x.result)),
]))
print("")

105
runner.py
View File

@ -1,50 +1,99 @@
from prompt_toolkit.formatted_text import FormattedText
import tokens
from parser import Parser
import commands
from runstatus import RunStatus
from runstatus import MacroStatus
from runstatus import StopReason
from runstatus import ReduceStatus
from runstatus import CommandStatus
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.")
# Maximum amount of reductions.
# If None, no maximum is enforced.
self.reduction_limit: int | None = 300
def exec_command(self, command: str) -> CommandStatus:
if command in commands.commands:
return commands.run(command, self)
# Handle unknown commands
else:
return CommandStatus(
formatted_text = FormattedText([
("#FFFF00", f"Unknown command \"{command}\"")
])
)
def reduce_expression(self, expr: tokens.LambdaToken) -> ReduceStatus:
# Reduction Counter.
# We also count macro expansions,
# and subtract those from the final count.
i = 0
macro_expansions = 0
while i < self.reduction_limit:
r = expr.reduce(self.macro_table)
expr = r.output
# If we can't reduce this expression anymore,
# it's in beta-normal form.
if not r.was_reduced:
return ReduceStatus(
reduction_count = i - macro_expansions,
stop_reason = StopReason.BETA_NORMAL,
result = r.output
)
# Count reductions
i += 1
if r.reduction_type == tokens.ReductionType.MACRO_EXPAND:
macro_expansions += 1
return ReduceStatus(
reduction_count = i - macro_expansions,
stop_reason = StopReason.MAX_EXCEEDED,
result = r.output
)
# Apply a list of definitions
def run(self, line: str):
def run(self, line: str) -> RunStatus:
e = Parser.parse_line(line)
# If this line is a macro definition, save the macro.
if isinstance(e, tokens.macro_expression):
if e.label in self.macro_table:
raise NameError(f"Label {e.label} exists!")
was_rewritten = e.label in self.macro_table
e.exp.bind_variables()
self.macro_table[e.label] = e.exp
return MacroStatus(
was_rewritten = was_rewritten,
macro_label = e.label
)
# If this line is a command, do the command.
elif isinstance(e, tokens.command):
self.exec_command(e.name)
return self.exec_command(e.name)
# If this line is a plain expression, reduce it.
else:
e.bind_variables()
self.expr = e
return self.reduce_expression(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):
def run_lines(self, lines: list[str]):
for l in lines:
self.run(l)

73
runstatus.py Normal file
View File

@ -0,0 +1,73 @@
import enum
import tokens
from prompt_toolkit.formatted_text import FormattedText
class RunStatus:
"""
Base class for run status.
These are returned whenever the runner does something.
"""
pass
class MacroStatus(RunStatus):
"""
Returned when a macro is defined.
Values:
`was_rewritten`: If true, an old macro was replaced.
`macro_label`: The name of the macro we just made.
"""
def __init__(
self,
*,
was_rewritten: bool,
macro_label: str
):
self.was_rewritten = was_rewritten
self.macro_label = macro_label
class StopReason(enum.Enum):
BETA_NORMAL = ("#FFFFFF", "β-normal form")
LOOP_DETECTED = ("#FFFF00", "loop detected")
MAX_EXCEEDED = ("#FFFF00", "too many reductions")
INTERRUPT = ("#FF0000", "user interrupt")
class ReduceStatus(RunStatus):
"""
Returned when an expression is reduced.
Values:
`reduction_count`: How many reductions were made.
`stop_reason`: Why we stopped. See `StopReason`.
"""
def __init__(
self,
*,
reduction_count: int,
stop_reason: StopReason,
result: tokens.LambdaToken
):
self.reduction_count = reduction_count
self.stop_reason = stop_reason
self.result = result
class CommandStatus(RunStatus):
"""
Returned when a command is executed.
Values:
`formatted_text`: What to print after this command is executed
"""
def __init__(
self,
*,
formatted_text: FormattedText
):
self.formatted_text = formatted_text

View File

@ -109,15 +109,36 @@ class macro(LambdaToken):
raise TypeError("Can only compare macro with macro")
return self.name == other.name
def reduce(self, macro_table = {}, *, auto_free_vars = True) -> ReductionStatus:
if self.name in macro_table:
def reduce(
self,
macro_table = {},
*,
# To keep output readable, we avoid expanding macros as often as possible.
# Macros are irreducible if force_substitute is false.
force_substitute = False,
# If this is false, error when macros aren't defined instead of
# invisibly making a free variable.
auto_free_vars = True
) -> ReductionStatus:
if (self.name in macro_table) and force_substitute:
if force_substitute: # Only expand macros if we NEED to
return ReductionStatus(
output = macro_table[self.name],
reduction_type = ReductionType.MACRO_EXPAND,
was_reduced = True
)
else: # Otherwise, do nothing.
return ReductionStatus(
output = self,
reduction_type = ReductionType.MACRO_EXPAND,
was_reduced = False
)
elif not auto_free_vars:
raise NameError(f"Name {self.name} is not defined!")
else:
return ReductionStatus(
output = free_variable(self.name),
@ -449,8 +470,17 @@ class lambda_apply(LambdaToken):
# Otherwise, try to reduce self.fn.
# If that is impossible, try to reduce self.arg.
else:
if isinstance(self.fn, macro):
# Macros must be reduced before we apply them as functions.
# This is the only place we force substitution.
r = self.fn.reduce(
macro_table,
force_substitute = True
)
else:
r = self.fn.reduce(macro_table)
# If a macro becomes a free variable,
# reduce twice.
if r.reduction_type == ReductionType.MACRO_TO_FREE: