Compare commits
5 Commits
92e741549f
...
3ff496e1d6
Author | SHA1 | Date |
---|---|---|
Mark | 3ff496e1d6 | |
Mark | 84c5229fbf | |
Mark | a4af47435a | |
Mark | 01632f6ec3 | |
Mark | 696ede7a9c |
|
@ -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
|
|
@ -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()
|
||||
]
|
||||
)
|
||||
)
|
10
greeting.py
10
greeting.py
|
@ -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
38
main.py
|
@ -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
105
runner.py
|
@ -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)
|
||||
|
|
|
@ -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
|
34
tokens.py
34
tokens.py
|
@ -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:
|
||||
|
|
Reference in New Issue