Add let statements

genir.py

@@ -3,7 +3,7 @@ from typing import *
 
 from silly_thing import *
 from pattern import lex_and_parse_pattern
-from ir import Function, Application, Int, Variable
+from ir import Function, Application, Int, Variable, LetBinding, Unit
 
 import json
 
@@ -19,6 +19,11 @@ def json_to_ir(j: JsonType) -> Expression:
 	elif isinstance(j, str):
 		return Variable(j)
 	elif isinstance(j, Sequence):
-		return Application([json_to_ir(e) for e in j])
+		match j:
+			case [first, *rest]:
+				return Application(json_to_ir(first), [json_to_ir(a) for a in rest])
+			case []:
+				return Unit()
+		raise Exception('Unreachable')
 	else:
 		return Int(j)

ir.py

@@ -3,7 +3,7 @@ from emis_funky_funktions import *
 from typing import Mapping, Sequence, Tuple, TypeAlias
 
 
-Expression: TypeAlias = 'Function | Application | Int | Variable | Builtin'
+Expression: TypeAlias = 'Function | Application | Int | Variable | Builtin | LetBinding | Unit'
 Pattern: TypeAlias = 'NamePattern | IntPattern | SPattern | IgnorePattern'
 
 @dataclass(frozen=True)
@@ -118,6 +118,20 @@ class SPattern:
 	def __repr__(self) -> str:
 		return 'S ' + repr(self.pred)
 
+@dataclass(frozen=True)
+class Unit:
+	def subst(self, expression: Expression, variable: str) -> Expression:
+		return self
+
+	def is_value(self) -> bool:
+		return True
+
+	def step(self) -> Option[Expression]:
+		return None
+
+	def __repr__(self) -> str:
+		return "[]"
+
 @dataclass(frozen=True)
 class Builtin:
 	name: str
@@ -189,48 +203,92 @@ class Function:
 		return '{ ' + ', '.join('"' + repr(repr(p))[1:-1] + '" : ' + repr(e) for (p, e) in self.forms) + ' }'
 
 @dataclass
-class Application:
-	expressions: Sequence[Expression]
+class LetBinding:
+	lhs: str
+	rhs: Expression
+	body: Expression
 
 	def subst(self, expression: Expression, variable: str) -> Expression:
-		return Application([
-			e.subst(expression, variable)
-			for e in self.expressions
-		])
+		if self.lhs == variable:
+			return self
+		else:
+			return LetBinding(
+				self.lhs,
+				self.rhs.subst(expression, variable),
+				self.body.subst(expression, variable)
+			)
 
 	def is_value(self) -> bool:
-		return not len(self.expressions)
+		return False
 
 	def step(self) -> Option[Expression]:
-		match self.expressions:
+		if self.rhs.is_value():
+			return Some(self.body.subst(
+				self.rhs.subst(
+					LetBinding(self.lhs, self.rhs, Variable(self.lhs)),
+					self.lhs
+				),
+				self.lhs
+			))
+		else:
+			return map_opt(lambda rhs_step:
+				LetBinding(self.lhs, rhs_step, self.body),
+				self.rhs.step()
+			)
+
+	def __repr__(self) -> str:
+		if isinstance(self.body, LetBinding) or isinstance(self.body, Application):
+			return f'L[ {repr(self.lhs)}, {repr(self.rhs)},{repr(self.body)[1:-1]}]'
+		else:
+			return f'L[ {repr(self.lhs)}, {repr(self.rhs)}, {repr(self.body)}]'
+
+@dataclass
+class Application:
+	first: Expression
+	args: Sequence[Expression]
+
+	def subst(self, expression: Expression, variable: str) -> Expression:
+		return Application(
+			self.first.subst(expression, variable),
+			[r.subst(expression, variable) for r in self.args]
+		)
+
+	def is_value(self) -> bool:
+		return False
+
+	def step(self) -> Option[Expression]:
+		match self.args:
 			case []:
-				return None
-			case [e]:
-				return Some(e)
-			case [f, a, *rest]:
-				if f.is_value():
-					if a.is_value():
-						if isinstance(f, Function) or isinstance(f, Builtin):
-							return map_opt(
-								lambda maybe_f_sub: Application([maybe_f_sub, *rest]),
-								f.try_apply(a)
-							)
-						else:
-							return None
-					else:
-						return map_opt(
-							lambda next_a: Application([f, next_a, *rest]),
-							a.step()
-						)
-				else:
-					return map_opt(
-						lambda next_f: Application([next_f, a, *rest]),
-						f.step()
-					)
+				return Some(self.first)
+			case [a, *rest]:
+				match self.first.step():
+					case Some(first_stepped):
+						return Some(Application(first_stepped, self.args))
+					case None:
+						match a.step():
+							case Some(a_stepped):
+								return Some(Application(self.first, [a_stepped, *rest]))
+							case None:
+								if isinstance(self.first, Function) or isinstance(self.first, Builtin):
+									return map_opt(
+										lambda f_sub: Application(f_sub, rest),
+										self.first.try_apply(a)
+									)
+								elif isinstance(self.first, Variable):
+									lhs = self.first.name
+									rhs = a
+									body = rest
+									match body:
+										case []:
+											return Some(Unit())
+										case [body_first, *body_rest]:
+											return Some(LetBinding(lhs, rhs, Application(body_first, body_rest)))
+								else:
+									return None
 		raise Exception('Unreachable')
 
 	def __repr__(self) -> str:
-		return '[ ' + ', '.join(repr(e) for e in self.expressions) + ' ]'
+		return f'[ {repr(self.first)}, ' + ', '.join(repr(e) for e in self.args) + ' ]'
 
 @dataclass
 class Int: