Added variable binding

README.md

@@ -3,7 +3,7 @@
 
 ## Todo (pre-release):
  - $\alpha$-equivalence check
- - Prettyprint functions (combine args, rename bound variables)
+ - Prettyprint functions (rename bound variables)
  - Write a nice README
  - Handle or avoid recursion errors
  - Fix colors

lamb/__main__.py

@@ -7,10 +7,9 @@ from prompt_toolkit.key_binding import KeyBindings
 from prompt_toolkit.lexers import Lexer
 
 from pyparsing import exceptions as ppx
+import enum
 
 import lamb.parser
-import lamb.runner as runner
-import lamb.tokens as tokens
 import lamb.utils as utils
 
 
@@ -47,44 +46,58 @@ r = runner.Runner(
 )
 """
 
+class Direction(enum.Enum):
+	UP		= enum.auto()
+	LEFT	= enum.auto()
+	RIGHT	= enum.auto()
+
+class ReductionError(Exception):
+	"""
+	Raised when we encounter an error while reducing.
+
+	These should be caught and elegantly presented to the user.
+	"""
+	def __init__(self, msg: str):
+		self.msg = msg
+
 class Node:
 	def __init__(self):
 		# The node this one is connected to.
 		# None if this is the top node.
 		self.parent: Node | None = None
 
-		# True if we're connected to the left side
+		# What direction this is relative to the parent.
-		# of the parent, False otherwise.
+		# Left of Right.
-		self.parent_left: bool | None = None
+		self.parent_side: Direction | None = None
 
 		# Left and right nodes, None if empty
 		self.left: Node | None = None
 		self.right: Node | None = None
 
-	def set_parent(self, parent, is_left):
+	def set_parent(self, parent, side: Direction):
 		self.parent = parent
-		self.parent_left = is_left
+		self.parent_side = side
 
 	def go_left(self):
 		if self.left is None:
 			raise Exception("Can't go left when left is None")
-		return None, self.left
+		return Direction.UP, self.left
 
 	def go_right(self):
 		if self.right is None:
 			raise Exception("Can't go right when right is None")
-		return None, self.right
+		return Direction.UP, self.right
 
 	def go_up(self):
 		if self.parent is None:
 			raise Exception("Can't go up when parent is None")
-		return self.parent_left, self.parent
+		return self.parent_side, self.parent
 
-def to_node(result_pair) -> Node:
+class EndNode:
-	return result_pair[0].from_parse(result_pair[1])
+	def print_value(self):
+		raise NotImplementedError("EndNodes MUST have a print_value method!")
 
-
+class Macro(Node, EndNode):
-class Macro(Node):
 	@staticmethod
 	def from_parse(results):
 		return Macro(results[0])
@@ -98,29 +111,98 @@ class Macro(Node):
 	def __repr__(self):
 		return f"<macro {self.name}>"
 
+	def print_value(self):
+		return self.name
+
+class Church(Node, EndNode):
+	@staticmethod
+	def from_parse(results):
+		return Church(results[0])
+
+	def __init__(self, value: int) -> None:
+		super().__init__()
+		self.value = value
+		self.left = None
+		self.right = None
+
+	def __repr__(self):
+		return f"<church {self.value}>"
+
+	def print_value(self):
+		return str(self.value)
+
+	def to_church(self):
+		"""
+		Return this number as an expanded church numeral.
+		"""
+		f = Bound("f")
+		a = Bound("a")
+		chain = a
+
+		for i in range(self.value):
+			chain = Call(f, chain)
+
+		return Func(
+			f,
+			Func(a, chain)
+		)
+
+
+bound_counter = 0
+class Bound(Node, EndNode):
+	def __init__(self, name: str, *, forced_id = None):
+		self.name = name
+		global bound_counter
+
+		if forced_id is None:
+			self.identifier = bound_counter
+			bound_counter += 1
+		else:
+			self.identifier = forced_id
+
+	def clone(self):
+		"""
+		Return a new bound variable equivalent to this one.
+		"""
+		return Bound(
+			self.name,
+			forced_id = self.identifier
+		)
+
+	def __eq__(self, other):
+		if not isinstance(other, Bound):
+			raise TypeError(f"Cannot compare bound_variable with {type(other)}")
+		return self.identifier == other.identifier
+
+	def __repr__(self):
+		return f"<{self.name} {self.identifier}>"
+
+	def print_value(self):
+		return self.name
+
 class Func(Node):
 	@staticmethod
 	def from_parse(result):
 		if len(result[0]) == 1:
-			i = to_node(result[0][0])
+			i = result[0][0]
-			below = to_node(result[1])
+			below = result[1]
 			this = Func(i, below) # type: ignore
 
-			below.set_parent(this, True)
+			below.set_parent(this, Direction.LEFT)
 			return this
 		else:
-			i = to_node(result[0].pop(0))
+			i = result[0].pop(0)
 			below = Func.from_parse(result)
 			this = Func(i, below) # type: ignore
 
-			below.set_parent(this, True)
+			below.set_parent(this, Direction.LEFT)
 			return this
 
-	def __init__(self, input: Macro, output: Node) -> None:
+	def __init__(self, input: Macro | Bound, output: Node) -> None:
 		super().__init__()
-		self.input = input
+		self.input: Macro | Bound = input
-		self.left = output
+		self.left: Node = output
-		self.right = None
+		self.right: None = None
 
 	def __repr__(self):
 		return f"<func {self.input!r} {self.left!r}>"
@@ -130,93 +212,203 @@ class Call(Node):
 	def from_parse(results):
 		if len(results) == 2:
 			left = results[0]
-			if not isinstance(left, Node):
+			right = results[1]
-				left = to_node(left)
-
-			right = to_node(results[1])
 			this = Call(left, right)
 
-			left.set_parent(this, True)
+			left.set_parent(this, Direction.LEFT)
-			right.set_parent(this, False)
+			right.set_parent(this, Direction.RIGHT)
 			return this
 		else:
 			left = results[0]
-			if not isinstance(left, Node):
+			right = results[1]
-				left = to_node(left)
-
-			right = to_node(results[1])
 			this = Call(left, right)
 
-			left.set_parent(this, True)
+			left.set_parent(this, Direction.LEFT)
-			right.set_parent(this, False)
+			right.set_parent(this, Direction.RIGHT)
 			return Call.from_parse(
 				[this] + results[2:]
 			)
 
 	def __init__(self, fn: Node, arg: Node) -> None:
 		super().__init__()
-		self.left = fn
+		self.left: Node = fn
-		self.right = arg
+		self.right: Node = arg
 
 	def __repr__(self):
 		return f"<call {self.left!r} {self.right!r}>"
 
+class MacroDef:
+	@staticmethod
+	def from_parse(result):
+		return MacroDef(
+			result[0].name,
+			result[1]
+		)
+
+	def __init__(self, label: str, expr: Node):
+		self.label = label
+		self.expr = expr
+
+	def __repr__(self):
+		return f"<{self.label} := {self.expr!r}>"
+
+	def __str__(self):
+		return f"{self.label} := {self.expr}"
+
+class Command:
+	@staticmethod
+	def from_parse(result):
+		return Command(
+			result[0],
+			result[1:]
+		)
+
+	def __init__(self, name, args):
+		self.name = name
+		self.args = args
+
 p = lamb.parser.LambdaParser(
-	action_func = lambda x: (Func, x),
+	action_func = Func.from_parse,
-	action_bound = lambda x: (Macro, x),
+	action_bound = Macro.from_parse,
-	action_macro = lambda x: (Macro, x),
+	action_macro = Macro.from_parse,
-	action_call = lambda x: (Call, x)
+	action_call = Call.from_parse,
+	action_church = Church.from_parse,
+	action_macro_def = MacroDef.from_parse,
+	action_command = Command.from_parse
 )
 
 
-def traverse(node: Node):
+def print_expr(expr) -> str:
-	ptr = node
-	back_from_left = None
 
-	out = ""
+	if isinstance(expr, MacroDef):
+		return f"{expr.label} = {print_expr(expr.expr)}"
 
-	while True:
+	elif isinstance(expr, Node):
-		if isinstance(ptr, Macro):
+		ptr = expr
-			out += ptr.name
+		from_side = Direction.UP
-			back_from_left, ptr = ptr.go_up()
-		if isinstance(ptr, Func):
-			if back_from_left is None:
-				if isinstance(ptr.parent, Func):
-					out += ptr.input.name
-				else:
-					out += "λ" + ptr.input.name
-				if not isinstance(ptr.left, Func):
-					out += "."
-				back_from_left, ptr = ptr.go_left()
-			elif back_from_left is True:
-				back_from_left, ptr = ptr.go_up()
-		if isinstance(ptr, Call):
-			if back_from_left is None:
-				out += "("
-				back_from_left, ptr = ptr.go_left()
-			elif back_from_left is True:
-				out += " "
-				back_from_left, ptr = ptr.go_right()
-			elif back_from_left is False:
-				out += ")"
-				back_from_left, ptr = ptr.go_up()
 
-		if ptr.parent is None:
+		out = ""
-			break
+
-	return out
+		while True:
+			if isinstance(ptr, EndNode):
+				out += ptr.print_value()
+				if ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+			elif isinstance(ptr, Func):
+				if from_side == Direction.UP:
+					if isinstance(ptr.parent, Func):
+						out += ptr.input.name
+					else:
+						out += "λ" + ptr.input.name
+					if not isinstance(ptr.left, Func):
+						out += "."
+					from_side, ptr = ptr.go_left()
+				elif from_side == Direction.LEFT:
+					if ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+			elif isinstance(ptr, Call):
+				if from_side == Direction.UP:
+					out += "("
+					from_side, ptr = ptr.go_left()
+				elif from_side == Direction.LEFT:
+					out += " "
+					from_side, ptr = ptr.go_right()
+				elif from_side == Direction.RIGHT:
+					out += ")"
+					if ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+			if ptr.parent is None:
+				break
+		return out
+
+	else:
+		raise TypeError(f"I don't know what to do with a {type(expr)}")
+
+def bind_variables(expr) -> None:
+
+	if isinstance(expr, MacroDef):
+		bind_variables(expr.expr)
+
+	elif isinstance(expr, Node):
+		ptr = expr
+		from_side = Direction.UP
+
+		bound_variables = {}
+
+		while True:
+			if isinstance(ptr, Func):
+				if from_side == Direction.UP:
+					# Add this function's input to the table of bound variables.
+					# If it is already there, raise an error.
+					if (ptr.input.name in bound_variables):
+						raise ReductionError(f"Bound variable name conflict: \"{ptr.input.name}\"")
+					else:
+						bound_variables[ptr.input.name] = Bound(ptr.input.name)
+						ptr.input = bound_variables[ptr.input.name]
+
+					# If output is a macro, swap it with a bound variable.
+					if isinstance(ptr.left, Macro):
+						if ptr.left.name in bound_variables:
+							ptr.left = bound_variables[ptr.left.name].clone()
+							ptr.left.set_parent(ptr, Direction.LEFT)
+
+					# If we can't move down the tree, move up.
+					if isinstance(ptr.left, EndNode):
+						del bound_variables[ptr.input.name]
+						if ptr.parent is not None:
+							from_side, ptr = ptr.go_up()
+					else:
+						from_side, ptr = ptr.go_left()
+
+				elif from_side == Direction.LEFT:
+					del bound_variables[ptr.input.name]
+					if ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+			elif isinstance(ptr, Call):
+				if from_side == Direction.UP:
+					# Bind macros
+					if isinstance(ptr.left, Macro):
+						if ptr.left.name in bound_variables:
+							ptr.left = bound_variables[ptr.left.name].clone()
+							ptr.left.set_parent(ptr, Direction.LEFT)
+					if isinstance(ptr.right, Macro):
+						if ptr.right.name in bound_variables:
+							ptr.right = bound_variables[ptr.right.name].clone()
+							ptr.right.set_parent(ptr, Direction.RIGHT)
+
+					if not isinstance(ptr.left, EndNode):
+						from_side, ptr = ptr.go_left()
+					elif not isinstance(ptr.right, EndNode):
+						from_side, ptr = ptr.go_right()
+					elif ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+				elif from_side == Direction.LEFT:
+					if isinstance(ptr.right, Macro):
+						if ptr.right.name in bound_variables:
+							ptr.right = bound_variables[ptr.right.name].clone()
+							ptr.right.set_parent(ptr, Direction.RIGHT)
+
+					if not isinstance(ptr.right, EndNode):
+						from_side, ptr = ptr.go_right()
+					elif ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+				elif from_side == Direction.RIGHT:
+					if ptr.parent is not None:
+						from_side, ptr = ptr.go_up()
+
+			if ptr.parent is None:
+				break
+
+	else:
+		raise TypeError(f"I don't know what to do with a {type(expr)}")
 
 for l in [
-	"λab.(a (NOT a b) b)",
-	"λnmf.n (m f)",
-	"λf.(λx. f(x x))(λx.f(x x))",
-]:
-	i = p.parse_line(l)
-	#print(i)
-	n = to_node(i)
-	#print(n)
-	print(traverse(n))
-
-"""
 	"NOT = λa.(a F T)",
 	"AND = λab.(a F b)",
 	"OR = λab.(a T b)",
@@ -228,5 +420,8 @@ for l in [
 	"S = λnfa.(f (n f a))",
 	"Z = λn.n (λa.F) T",
 	"MULT = λnmf.n (m f)",
-	"H = λp.((PAIR (p F)) (S (p F)))",
+	"H = λp.((PAIR (p F)) (S (p F)))"
-])"""
+]:
+	n = p.parse_line(l)
+	bind_variables(n)
+	print(print_expr(n))

lamb/parser.py

@@ -67,9 +67,9 @@ class LambdaParser:
 	def __init__(
 			self,
 			*,
-			#action_command,
+			action_command,
-			#action_macro_def,
+			action_macro_def,
-			#action_church,
+			action_church,
 			action_func,
 			action_bound,
 			action_macro,
@@ -78,9 +78,9 @@ class LambdaParser:
 
 		self.make_parser()
 
-		#self.pp_command.set_parse_action(action_command)
+		self.pp_command.set_parse_action(action_command)
-		#self.pp_macro_def.set_parse_action(action_macro_def)
+		self.pp_macro_def.set_parse_action(action_macro_def)
-		#self.pp_church.set_parse_action(action_church)
+		self.pp_church.set_parse_action(action_church)
 		self.pp_lambda_fun.set_parse_action(action_func)
 		self.pp_macro.set_parse_action(action_macro)
 		self.pp_bound.set_parse_action(action_bound)

lamb/tokens.py

@@ -1,14 +1,7 @@
 import enum
 import lamb.utils as utils
 
-class ReductionError(Exception):
-	"""
-	Raised when we encounter an error while reducing.
 
-	These should be caught and elegantly presented to the user.
-	"""
-	def __init__(self, msg: str):
-		self.msg = msg
 
 class ReductionType(enum.Enum):
 	MACRO_EXPAND	= enum.auto()
@@ -42,56 +35,8 @@ class ReductionStatus:
 		# this will be false.
 		self.was_reduced = was_reduced
 
-class LambdaToken:
-	"""
-	Base class for all lambda tokens.
-	"""
-
-	def set_runner(self, runner):
-		self.runner = runner
-
-	def bind_variables(self, *, ban_macro_name: str | None = None) -> None:
-		pass
-
-	def reduce(self) -> ReductionStatus:
-		return ReductionStatus(
-			was_reduced = False,
-			output = self
-		)
 
 class church_num(LambdaToken):
-	"""
-	Represents a Church numeral.
-	"""
-	@staticmethod
-	def from_parse(result):
-		return church_num(
-			int(result[0]),
-		)
-
-	def __init__(self, val):
-		self.val = val
-	def __repr__(self):
-		return f"<{self.val}>"
-	def __str__(self):
-		return f"{self.val}"
-
-	def to_church(self):
-		"""
-		Return this number as an expanded church numeral.
-		"""
-		f = bound_variable("f", runner = self.runner)
-		a = bound_variable("a", runner = self.runner)
-		chain = a
-
-		for i in range(self.val):
-			chain = lambda_apply(f, chain)
-
-		return lambda_func(
-			f,
-			lambda_func(a, chain)
-		)
-
 	def reduce(self, *, force_substitute = False) -> ReductionStatus:
 		if force_substitute: # Only expand macros if we NEED to
 			return ReductionStatus(
@@ -127,53 +72,7 @@ class free_variable(LambdaToken):
 	def __str__(self):
 		return f"{self.label}"
 
-class command(LambdaToken):
-	@staticmethod
-	def from_parse(result):
-		return command(
-			result[0],
-			result[1:]
-		)
-
-	def __init__(self, name, args):
-		self.name = name
-		self.args = args
-
 class macro(LambdaToken):
-	"""
-	Represents a "macro" in lambda calculus,
-	a variable that reduces to an expression.
-
-	These don't have any inherent logic, they
-	just make writing and reading expressions
-	easier.
-
-	These are defined as follows:
-	<macro name> = <expression>
-	"""
-
-	@staticmethod
-	def from_parse(result):
-		return macro(
-			result[0],
-		)
-
-	def __init__(self, name):
-		self.name = name
-	def __repr__(self):
-		return f"<{self.name}>"
-	def __str__(self):
-		return self.name
-
-	def __eq__(self, other):
-		if not isinstance(other, macro):
-			raise TypeError("Can only compare macro with macro")
-		return self.name == other.name
-
-	def bind_variables(self, *, ban_macro_name=None) -> None:
-		if self.name == ban_macro_name:
-			raise ReductionError(f"Cannot use macro \"{ban_macro_name}\" here.")
-
 	def reduce(
 			self,
 			*,
@@ -209,185 +108,8 @@ class macro(LambdaToken):
 				was_reduced = True
 			)
 
-class macro_expression(LambdaToken):
-	"""
-	Represents a line that looks like
-		<name> = <expression>
-
-	Doesn't do anything particularly interesting,
-	just holds an expression until it is stored
-	in the runner's macro table.
-	"""
-
-	@staticmethod
-	def from_parse(result):
-		return macro_expression(
-			result[0].name,
-			result[1]
-		)
-
-	def set_runner(self, runner):
-		self.expr.set_runner(runner)
-
-	def bind_variables(self, *, ban_macro_name: str | None = None):
-		self.expr.bind_variables(ban_macro_name = ban_macro_name)
-
-	def __init__(self, label: str, expr: LambdaToken):
-		self.label = label
-		self.expr = expr
-
-	def __repr__(self):
-		return f"<{self.label} := {self.expr!r}>"
-
-	def __str__(self):
-		return f"{self.label} := {self.expr}"
-
-
-class bound_variable(LambdaToken):
-	def __init__(self, name: str, *, runner, forced_id = None):
-		self.original_name = name
-		self.runner = runner
-
-		if forced_id is None:
-			self.identifier = self.runner.bound_variable_counter
-			self.runner.bound_variable_counter += 1
-		else:
-			self.identifier = forced_id
-
-	def __eq__(self, other):
-		if not isinstance(other, bound_variable):
-			raise TypeError(f"Cannot compare bound_variable with {type(other)}")
-		return self.identifier == other.identifier
-
-	def __repr__(self):
-		return f"<{self.original_name} {self.identifier}>"
-
-	def __str__(self):
-		return self.original_name
 
 class lambda_func(LambdaToken):
-	"""
-	Represents a function.
-		Defined like λa.aa
-
-	After being created by the parser, a function
-	needs to have its variables bound. This cannot
-	happen during parsing, since the parser creates
-	functions "inside-out," and we need all inner
-	functions before we bind variables.
-	"""
-
-	@staticmethod
-	def from_parse(result):
-		if len(result[0]) == 1:
-			return lambda_func(
-				result[0][0],
-				result[1]
-			)
-		else:
-			return lambda_func(
-				result[0].pop(0),
-				lambda_func.from_parse(result)
-			)
-
-	def set_runner(self, runner):
-		self.runner = runner
-		self.input.set_runner(runner)
-		self.output.set_runner(runner)
-
-	def __init__(
-			self,
-			input_var: macro | bound_variable,
-			output: LambdaToken
-		):
-		self.input: macro | bound_variable = input_var
-		self.output: LambdaToken = output
-
-	def __repr__(self) -> str:
-		return f"<{self.input!r} → {self.output!r}>"
-
-	def __str__(self) -> str:
-		return f"λ{self.input}.{self.output}"
-
-	def bind_variables(
-			self,
-			placeholder: macro | None = None,
-			val: bound_variable | None = None,
-			*,
-			binding_self: bool = False,
-			ban_macro_name: str | None = None
-		) -> None:
-		"""
-		Go through this function and all the functions inside it,
-		and replace the strings generated by the parser with bound
-		variables or free variables.
-
-		If values are passed to `placeholder` and `val,`
-		we're binding the variable of a function containing
-		this one. If they are both none, start the binding
-		chain with this function.
-
-		If only one of those arguments is None, something is very wrong.
-
-		`placeholder` is a macro, NOT A STRING!
-		The parser assumes all names are macros at first, variable
-		binding fixes those that are actually bound variables.
-
-		If `binding_self` is True, don't throw an error on a name conflict
-		and don't bind this function's input variable.
-		This is used when we're calling this method to bind this function's
-		variable.
-		"""
-
-
-		if (placeholder is None) and (val != placeholder):
-			raise Exception(
-				"Error while binding variables: placeholder and val are both None."
-			)
-
-		# We only need to check for collisions if we're
-		# binding another function's variable. If this
-		# function starts the bind chain, skip that step.
-		if placeholder is not None:
-			if not binding_self and isinstance(self.input, macro):
-				if self.input == placeholder:
-					raise ReductionError(f"Bound variable name conflict: \"{self.input.name}\"")
-
-				if self.input.name in self.runner.macro_table:
-					raise ReductionError(f"Bound variable name conflict: \"{self.input.name}\" is a macro")
-
-
-		# If this function's variables haven't been bound yet,
-		# bind them BEFORE binding the outer function's.
-		#
-		# If we bind inner functions' variables before outer
-		# functions' variables, we won't be able to detect
-		# name conflicts.
-		if isinstance(self.input, macro) and not binding_self:
-			new_bound_var = bound_variable(
-				self.input.name,
-				runner = self.runner
-			)
-			self.bind_variables(
-				self.input,
-				new_bound_var,
-				binding_self = True,
-				ban_macro_name = ban_macro_name
-			)
-			self.input = new_bound_var
-
-
-		# Bind variables inside this function.
-		if isinstance(self.output, macro) and placeholder is not None:
-			if self.output.name == ban_macro_name:
-				raise ReductionError(f"Cannot use macro \"{ban_macro_name}\" here.")
-			if self.output == placeholder:
-				self.output = val # type: ignore
-		elif isinstance(self.output, lambda_func):
-			self.output.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-		elif isinstance(self.output, lambda_apply):
-			self.output.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-
 	def reduce(self) -> ReductionStatus:
 
 		r = self.output.reduce()
@@ -442,88 +164,6 @@ class lambda_func(LambdaToken):
 
 
 class lambda_apply(LambdaToken):
-	"""
-	Represents a function application.
-	Has two elements: fn, the function,
-	and arg, the thing it acts upon.
-
-	Parentheses are handled by the parser, and
-	chained functions are handled by from_parse.
-	"""
-
-	@staticmethod
-	def from_parse(result):
-		if len(result) == 2:
-			return lambda_apply(
-				result[0],
-				result[1]
-			)
-		elif len(result) > 2:
-			return lambda_apply.from_parse([
-				lambda_apply(
-					result[0],
-					result[1]
-				)] + result[2:]
-			)
-
-	def set_runner(self, runner):
-		self.runner = runner
-		self.fn.set_runner(runner)
-		self.arg.set_runner(runner)
-
-	def __init__(
-			self,
-			fn: LambdaToken,
-			arg: LambdaToken
-		):
-		self.fn: LambdaToken = fn
-		self.arg: LambdaToken = arg
-
-	def __repr__(self) -> str:
-		return f"<{self.fn!r} | {self.arg!r}>"
-
-	def __str__(self) -> str:
-		return f"({self.fn} {self.arg})"
-
-	def bind_variables(
-			self,
-			placeholder: macro | None = None,
-			val: bound_variable | None = None,
-			*,
-			ban_macro_name: str | None = None
-		) -> None:
-		"""
-		Does exactly what lambda_func.bind_variables does,
-		but acts on applications instead.
-		"""
-
-		if (placeholder is None) and (val != placeholder):
-			raise Exception(
-				"Error while binding variables: placeholder and val are both None."
-			)
-
-		# If val and placeholder are None,
-		# everything below should still work as expected.
-		if isinstance(self.fn, macro) and placeholder is not None:
-			if self.fn.name == ban_macro_name:
-				raise ReductionError(f"Cannot use macro \"{ban_macro_name}\" here.")
-			if self.fn == placeholder:
-				self.fn = val # type: ignore
-		elif isinstance(self.fn, lambda_func):
-			self.fn.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-		elif isinstance(self.fn, lambda_apply):
-			self.fn.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-
-		if isinstance(self.arg, macro) and placeholder is not None:
-			if self.arg.name == ban_macro_name:
-				raise ReductionError(f"Cannot use macro \"{ban_macro_name}\" here.")
-			if self.arg == placeholder:
-				self.arg = val # type: ignore
-		elif isinstance(self.arg, lambda_func):
-			self.arg.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-		elif isinstance(self.arg, lambda_apply):
-			self.arg.bind_variables(placeholder, val, ban_macro_name = ban_macro_name)
-
 	def sub_bound_var(
 		self,
 		val,