diff --git a/README.md b/README.md index cf14800..be1ee4a 100644 --- a/README.md +++ b/README.md @@ -16,4 +16,6 @@ - Command and macro autocomplete - step-by-step reduction - Documentation in README - - Maybe a better icon? \ No newline at end of file + - Maybe a better icon? + - Warn when overwriting macro + - Syntax highlighting: parenthesis, bound variables, macros, etc \ No newline at end of file diff --git a/main.py b/main.py index d2e8b2a..71042bc 100755 --- a/main.py +++ b/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,47 @@ 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 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("") diff --git a/runner.py b/runner.py index c8162ec..ac0e701 100644 --- a/runner.py +++ b/runner.py @@ -1,50 +1,133 @@ import tokens 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: def __init__(self): 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): if command == "help": 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 - 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)