Added a few commands

README.md

@@ -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

commands.py

@@ -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()
+		]
+		)
+	)

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)

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("")

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)

runstatus.py

@@ -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

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:
-			return ReductionStatus(
-				output = macro_table[self.name],
-				reduction_type = ReductionType.MACRO_EXPAND,
-				was_reduced = True
-			)
+	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),
@@ -450,7 +471,16 @@ class lambda_apply(LambdaToken):
 		# Otherwise, try to reduce self.fn.
 		# If that is impossible, try to reduce self.arg.
 		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,
 			# reduce twice.
 			if r.reduction_type == ReductionType.MACRO_TO_FREE: