Added a few commands
parent
84c5229fbf
commit
3ff496e1d6
|
@ -3,7 +3,7 @@
|
||||||
|
|
||||||
## Todo (pre-release):
|
## Todo (pre-release):
|
||||||
- Fix parser (call parentheses)
|
- Fix parser (call parentheses)
|
||||||
- Good command parsing (`:help`, `:save`, `:load`, `:macros`, `:clear` are 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
|
||||||
- Versioning
|
- Versioning
|
||||||
|
@ -16,3 +16,4 @@
|
||||||
- Maybe a better icon?
|
- Maybe a better icon?
|
||||||
- Warn when overwriting macro
|
- Warn when overwriting macro
|
||||||
- Syntax highlighting: parenthesis, bound variables, macros, etc
|
- 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.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)
|
3
main.py
3
main.py
|
@ -86,6 +86,9 @@ while True:
|
||||||
if isinstance(x, runner.MacroStatus):
|
if isinstance(x, runner.MacroStatus):
|
||||||
pass
|
pass
|
||||||
|
|
||||||
|
if isinstance(x, runner.CommandStatus):
|
||||||
|
printf(x.formatted_text)
|
||||||
|
|
||||||
# If this line was an expression, print reduction status
|
# If this line was an expression, print reduction status
|
||||||
elif isinstance(x, runner.ReduceStatus):
|
elif isinstance(x, runner.ReduceStatus):
|
||||||
printf(FormattedText([
|
printf(FormattedText([
|
||||||
|
|
74
runner.py
74
runner.py
|
@ -1,60 +1,17 @@
|
||||||
|
from prompt_toolkit.formatted_text import FormattedText
|
||||||
|
|
||||||
import tokens
|
import tokens
|
||||||
from parser import Parser
|
from parser import Parser
|
||||||
import enum
|
import commands
|
||||||
|
from runstatus import RunStatus
|
||||||
|
from runstatus import MacroStatus
|
||||||
|
from runstatus import StopReason
|
||||||
|
from runstatus import ReduceStatus
|
||||||
|
from runstatus import CommandStatus
|
||||||
|
|
||||||
|
|
||||||
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 Runner:
|
class Runner:
|
||||||
|
@ -65,9 +22,18 @@ class Runner:
|
||||||
# If None, no maximum is enforced.
|
# If None, no maximum is enforced.
|
||||||
self.reduction_limit: int | None = 300
|
self.reduction_limit: int | None = 300
|
||||||
|
|
||||||
def exec_command(self, command: str):
|
def exec_command(self, command: str) -> CommandStatus:
|
||||||
if command == "help":
|
if command in commands.commands:
|
||||||
print("This is a help message.")
|
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:
|
def reduce_expression(self, expr: tokens.LambdaToken) -> ReduceStatus:
|
||||||
|
|
||||||
|
|
|
@ -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
|
Reference in New Issue