Added runstatus and prettified prompt

master
Mark 2022-10-21 17:05:25 -07:00
parent 92e741549f
commit 696ede7a9c
Signed by: Mark
GPG Key ID: AD62BB059C2AAEE4
3 changed files with 138 additions and 36 deletions

View File

@ -17,3 +17,5 @@
- 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

37
main.py
View File

@ -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,47 @@ 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 this line was an expression, print reduction status
("#00FF00", " = "), elif isinstance(x, runner.ReduceStatus):
("#FFFFFF", str(x)) 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("")

133
runner.py
View File

@ -1,50 +1,133 @@
import tokens import tokens
from parser import Parser from parser import Parser
import enum
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:
def __init__(self): def __init__(self):
self.macro_table = {} self.macro_table = {}
self.expr = None
# Maximum amount of reductions.
# If None, no maximum is enforced.
self.reduction_limit: int | None = 300
def exec_command(self, command: str): def exec_command(self, command: str):
if command == "help": if command == "help":
print("This is a help message.") print("This is a help message.")
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)