Compare commits
5 Commits
92e741549f
...
3ff496e1d6
Author | SHA1 | Date | |
---|---|---|---|
3ff496e1d6 | |||
84c5229fbf | |||
a4af47435a | |||
01632f6ec3 | |||
696ede7a9c |
10
README.md
10
README.md
@ -3,17 +3,17 @@
|
|||||||
|
|
||||||
## Todo (pre-release):
|
## Todo (pre-release):
|
||||||
- Fix parser (call parentheses)
|
- 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
|
- Python files: installable, package list, etc
|
||||||
- $\alpha$-equivalence check
|
- $\alpha$-equivalence check
|
||||||
- Don't expand macros until you absolutely have to
|
|
||||||
- Versioning
|
- Versioning
|
||||||
- Clean up runner & printing
|
|
||||||
- Count reductions
|
|
||||||
|
|
||||||
## Todo:
|
## Todo:
|
||||||
- live syntax check
|
- live syntax check
|
||||||
- Command and macro autocomplete
|
- Command and macro autocomplete
|
||||||
- step-by-step reduction
|
- step-by-step reduction
|
||||||
- Documentation in README
|
- Documentation in README
|
||||||
- Maybe a better icon?
|
- 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
96
commands.py
Normal 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()
|
||||||
|
]
|
||||||
|
)
|
||||||
|
)
|
10
greeting.py
10
greeting.py
@ -1,6 +1,6 @@
|
|||||||
from prompt_toolkit.styles import Style
|
from prompt_toolkit.styles import Style
|
||||||
from prompt_toolkit.formatted_text import HTML, to_formatted_text
|
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",
|
"_l": "#FF6600 bold",
|
||||||
|
|
||||||
# Subtitle
|
# Subtitle
|
||||||
"_s": "#B4EC85 bold"
|
"_s": "#B4EC85 bold",
|
||||||
|
|
||||||
|
# :help message
|
||||||
|
"_p": "#AAAAAA"
|
||||||
})
|
})
|
||||||
|
|
||||||
html = HTML(f"""
|
html = HTML(f"""
|
||||||
@ -46,8 +49,9 @@ html = HTML(f"""
|
|||||||
`'._.--._.'
|
`'._.--._.'
|
||||||
|
|
||||||
<_s> A λ calculus engine</_s>
|
<_s> A λ calculus engine</_s>
|
||||||
|
<_p> Type :help for help</_p>
|
||||||
|
|
||||||
"""[1:-1])
|
"""[1:-1])
|
||||||
|
|
||||||
def show():
|
def show():
|
||||||
print_formatted_text(html, style = style)
|
printf(html, style = style)
|
40
main.py
40
main.py
@ -1,6 +1,6 @@
|
|||||||
from prompt_toolkit import PromptSession
|
from prompt_toolkit import PromptSession
|
||||||
from prompt_toolkit.completion import WordCompleter
|
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 FormattedText
|
||||||
from prompt_toolkit.formatted_text import to_plain_text
|
from prompt_toolkit.formatted_text import to_plain_text
|
||||||
from prompt_toolkit.key_binding import KeyBindings
|
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 pyparsing import exceptions as ppx
|
||||||
|
|
||||||
from parser import Parser
|
from parser import Parser
|
||||||
from runner import Runner
|
import runner
|
||||||
import tokens
|
import tokens
|
||||||
import greeting
|
import greeting
|
||||||
|
|
||||||
@ -27,12 +27,13 @@ session = PromptSession(
|
|||||||
)
|
)
|
||||||
|
|
||||||
|
|
||||||
|
printf("\n")
|
||||||
greeting.show()
|
greeting.show()
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
r = Runner()
|
r = runner.Runner()
|
||||||
|
|
||||||
r.run_lines([
|
r.run_lines([
|
||||||
"T = λa.λb.a",
|
"T = λa.λb.a",
|
||||||
@ -57,31 +58,50 @@ while True:
|
|||||||
|
|
||||||
# Catch Ctrl-C and Ctrl-D
|
# Catch Ctrl-C and Ctrl-D
|
||||||
except KeyboardInterrupt:
|
except KeyboardInterrupt:
|
||||||
print("")
|
printf("\n\nGoodbye.\n")
|
||||||
break
|
break
|
||||||
except EOFError:
|
except EOFError:
|
||||||
print("")
|
printf("\n\nGoodbye.\n")
|
||||||
break
|
break
|
||||||
|
|
||||||
|
# Skip empty lines
|
||||||
if i.strip() == "":
|
if i.strip() == "":
|
||||||
continue
|
continue
|
||||||
|
|
||||||
|
|
||||||
|
# Try to run an input line.
|
||||||
|
# Catch parse errors and point them out.
|
||||||
try:
|
try:
|
||||||
x = r.run(i)
|
x = r.run(i)
|
||||||
except ppx.ParseException as e:
|
except ppx.ParseException as e:
|
||||||
l = len(to_plain_text(session.message))
|
l = len(to_plain_text(session.message))
|
||||||
print_formatted_text(FormattedText([
|
printf(FormattedText([
|
||||||
("#FF0000", " "*(e.loc + l) + "^\n"),
|
("#FF0000", " "*(e.loc + l) + "^\n"),
|
||||||
("#FF0000", f"Syntax error at char {e.loc}."),
|
("#FF0000", f"Syntax error at char {e.loc}."),
|
||||||
("#FFFFFF", "\n")
|
("#FFFFFF", "\n")
|
||||||
]))
|
]))
|
||||||
continue
|
continue
|
||||||
|
|
||||||
|
# If this line defined a macro, print nothing.
|
||||||
|
if isinstance(x, runner.MacroStatus):
|
||||||
|
pass
|
||||||
|
|
||||||
print_formatted_text(FormattedText([
|
if isinstance(x, runner.CommandStatus):
|
||||||
("#00FF00", " = "),
|
printf(x.formatted_text)
|
||||||
("#FFFFFF", str(x))
|
|
||||||
]))
|
# 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("")
|
print("")
|
||||||
|
105
runner.py
105
runner.py
@ -1,50 +1,99 @@
|
|||||||
|
from prompt_toolkit.formatted_text import FormattedText
|
||||||
|
|
||||||
import tokens
|
import tokens
|
||||||
from parser import Parser
|
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:
|
class Runner:
|
||||||
def __init__(self):
|
def __init__(self):
|
||||||
self.macro_table = {}
|
self.macro_table = {}
|
||||||
self.expr = None
|
|
||||||
|
|
||||||
def exec_command(self, command: str):
|
# Maximum amount of reductions.
|
||||||
if command == "help":
|
# If None, no maximum is enforced.
|
||||||
print("This is a help message.")
|
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
|
# Apply a list of definitions
|
||||||
def run(self, line: str):
|
def run(self, line: str) -> RunStatus:
|
||||||
e = Parser.parse_line(line)
|
e = Parser.parse_line(line)
|
||||||
|
|
||||||
|
# If this line is a macro definition, save the macro.
|
||||||
if isinstance(e, tokens.macro_expression):
|
if isinstance(e, tokens.macro_expression):
|
||||||
if e.label in self.macro_table:
|
was_rewritten = e.label in self.macro_table
|
||||||
raise NameError(f"Label {e.label} exists!")
|
|
||||||
e.exp.bind_variables()
|
e.exp.bind_variables()
|
||||||
self.macro_table[e.label] = e.exp
|
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):
|
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:
|
else:
|
||||||
e.bind_variables()
|
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:
|
def run_lines(self, lines: list[str]):
|
||||||
#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:
|
for l in lines:
|
||||||
self.run(l)
|
self.run(l)
|
||||||
|
73
runstatus.py
Normal file
73
runstatus.py
Normal 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
|
46
tokens.py
46
tokens.py
@ -109,15 +109,36 @@ 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 reduce(
|
||||||
if self.name in macro_table:
|
self,
|
||||||
return ReductionStatus(
|
macro_table = {},
|
||||||
output = macro_table[self.name],
|
*,
|
||||||
reduction_type = ReductionType.MACRO_EXPAND,
|
# To keep output readable, we avoid expanding macros as often as possible.
|
||||||
was_reduced = True
|
# 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:
|
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 ReductionStatus(
|
||||||
output = free_variable(self.name),
|
output = free_variable(self.name),
|
||||||
@ -450,7 +471,16 @@ class lambda_apply(LambdaToken):
|
|||||||
# Otherwise, try to reduce self.fn.
|
# Otherwise, try to reduce self.fn.
|
||||||
# If that is impossible, try to reduce self.arg.
|
# If that is impossible, try to reduce self.arg.
|
||||||
else:
|
else:
|
||||||
r = self.fn.reduce(macro_table)
|
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,
|
# If a macro becomes a free variable,
|
||||||
# reduce twice.
|
# reduce twice.
|
||||||
if r.reduction_type == ReductionType.MACRO_TO_FREE:
|
if r.reduction_type == ReductionType.MACRO_TO_FREE:
|
||||||
|
Reference in New Issue
Block a user