Changed church handling
parent
6a8d057425
commit
31ce605674
|
@ -15,7 +15,7 @@ class Runner:
|
|||
self.parser = LambdaParser(
|
||||
action_command = tokens.command.from_parse,
|
||||
action_macro_def = tokens.macro_expression.from_parse,
|
||||
action_church = utils.autochurch(self),
|
||||
action_church = tokens.church_num.from_parse,
|
||||
action_func = tokens.lambda_func.from_parse,
|
||||
action_bound = tokens.macro.from_parse,
|
||||
action_macro = tokens.macro.from_parse,
|
||||
|
@ -24,7 +24,7 @@ class Runner:
|
|||
|
||||
# Maximum amount of reductions.
|
||||
# If None, no maximum is enforced.
|
||||
self.reduction_limit: int | None = 300
|
||||
self.reduction_limit: int | None = 1_000_000
|
||||
|
||||
# Ensure bound variables are unique.
|
||||
# This is automatically incremented whenever we make
|
||||
|
@ -38,16 +38,19 @@ class Runner:
|
|||
def reduce_expression(self, expr: tokens.LambdaToken) -> rs.ReduceStatus:
|
||||
|
||||
# Reduction Counter.
|
||||
# We also count macro expansions,
|
||||
# We also count macro (and church) expansions,
|
||||
# and subtract those from the final count.
|
||||
i = 0
|
||||
macro_expansions = 0
|
||||
|
||||
|
||||
while (self.reduction_limit is None) or (i < self.reduction_limit):
|
||||
print(repr(expr))
|
||||
r = expr.reduce()
|
||||
expr = r.output
|
||||
|
||||
#print(expr)
|
||||
#self.prompt()
|
||||
|
||||
# If we can't reduce this expression anymore,
|
||||
# it's in beta-normal form.
|
||||
if not r.was_reduced:
|
||||
|
@ -58,12 +61,17 @@ class Runner:
|
|||
)
|
||||
|
||||
# Count reductions
|
||||
i += 1
|
||||
if r.reduction_type == tokens.ReductionType.MACRO_EXPAND:
|
||||
#i += 1
|
||||
if (
|
||||
r.reduction_type == tokens.ReductionType.MACRO_EXPAND or
|
||||
r.reduction_type == tokens.ReductionType.AUTOCHURCH
|
||||
):
|
||||
macro_expansions += 1
|
||||
else:
|
||||
i += 1
|
||||
|
||||
return rs.ReduceStatus(
|
||||
reduction_count = i - macro_expansions,
|
||||
reduction_count = i, # - macro_expansions,
|
||||
stop_reason = rs.StopReason.MAX_EXCEEDED,
|
||||
result = r.output # type: ignore
|
||||
)
|
||||
|
|
|
@ -1,4 +1,5 @@
|
|||
import enum
|
||||
import lamb.utils as utils
|
||||
|
||||
class ReductionError(Exception):
|
||||
"""
|
||||
|
@ -13,6 +14,7 @@ class ReductionType(enum.Enum):
|
|||
MACRO_EXPAND = enum.auto()
|
||||
MACRO_TO_FREE = enum.auto()
|
||||
FUNCTION_APPLY = enum.auto()
|
||||
AUTOCHURCH = enum.auto()
|
||||
|
||||
|
||||
class ReductionStatus:
|
||||
|
@ -57,6 +59,39 @@ class LambdaToken:
|
|||
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 reduce(self, *, force_substitute = False) -> ReductionStatus:
|
||||
if force_substitute: # Only expand macros if we NEED to
|
||||
return ReductionStatus(
|
||||
output = utils.autochurch(
|
||||
self.runner,
|
||||
self.val
|
||||
),
|
||||
was_reduced = True,
|
||||
reduction_type = ReductionType.AUTOCHURCH
|
||||
)
|
||||
else: # Otherwise, do nothing.
|
||||
return ReductionStatus(
|
||||
output = self,
|
||||
was_reduced = False
|
||||
)
|
||||
|
||||
|
||||
class free_variable(LambdaToken):
|
||||
"""
|
||||
Represents a free variable.
|
||||
|
@ -148,7 +183,6 @@ class macro(LambdaToken):
|
|||
else: # Otherwise, do nothing.
|
||||
return ReductionStatus(
|
||||
output = self,
|
||||
reduction_type = ReductionType.MACRO_EXPAND,
|
||||
was_reduced = False
|
||||
)
|
||||
|
||||
|
@ -214,6 +248,9 @@ class bound_variable(LambdaToken):
|
|||
def __repr__(self):
|
||||
return f"<{self.original_name} {self.identifier}>"
|
||||
|
||||
def __str__(self):
|
||||
return self.original_name
|
||||
|
||||
class lambda_func(LambdaToken):
|
||||
"""
|
||||
Represents a function.
|
||||
|
@ -337,12 +374,6 @@ class lambda_func(LambdaToken):
|
|||
|
||||
r = self.output.reduce()
|
||||
|
||||
# If a macro becomes a free variable,
|
||||
# reduce twice.
|
||||
if r.reduction_type == ReductionType.MACRO_TO_FREE:
|
||||
self.output = r.output
|
||||
return self.reduce()
|
||||
|
||||
return ReductionStatus(
|
||||
was_reduced = r.was_reduced,
|
||||
reduction_type = r.reduction_type,
|
||||
|
@ -512,7 +543,7 @@ class lambda_apply(LambdaToken):
|
|||
# Otherwise, try to reduce self.fn.
|
||||
# If that is impossible, try to reduce self.arg.
|
||||
else:
|
||||
if isinstance(self.fn, macro):
|
||||
if isinstance(self.fn, macro) or isinstance(self.fn, church_num):
|
||||
# Macros must be reduced before we apply them as functions.
|
||||
# This is the only place we force substitution.
|
||||
r = self.fn.reduce(
|
||||
|
@ -521,12 +552,6 @@ class lambda_apply(LambdaToken):
|
|||
else:
|
||||
r = self.fn.reduce()
|
||||
|
||||
# If a macro becomes a free variable,
|
||||
# reduce twice.
|
||||
if r.reduction_type == ReductionType.MACRO_TO_FREE:
|
||||
self.fn = r.output
|
||||
return self.reduce()
|
||||
|
||||
if r.was_reduced:
|
||||
return ReductionStatus(
|
||||
was_reduced = True,
|
||||
|
@ -540,10 +565,6 @@ class lambda_apply(LambdaToken):
|
|||
else:
|
||||
r = self.arg.reduce()
|
||||
|
||||
if r.reduction_type == ReductionType.MACRO_TO_FREE:
|
||||
self.arg = r.output
|
||||
return self.reduce()
|
||||
|
||||
return ReductionStatus(
|
||||
was_reduced = r.was_reduced,
|
||||
reduction_type = r.reduction_type,
|
||||
|
|
|
@ -6,14 +6,11 @@ from importlib.metadata import version
|
|||
import lamb.tokens as tokens
|
||||
|
||||
|
||||
def autochurch(runner):
|
||||
def autochurch(runner, num):
|
||||
"""
|
||||
Makes a church numeral from an integer.
|
||||
"""
|
||||
|
||||
def inner(results):
|
||||
num = int(results[0])
|
||||
|
||||
f = tokens.bound_variable("f", runner = runner)
|
||||
a = tokens.bound_variable("a", runner = runner)
|
||||
|
||||
|
@ -29,7 +26,6 @@ def autochurch(runner):
|
|||
chain
|
||||
)
|
||||
)
|
||||
return inner
|
||||
|
||||
|
||||
style = Style.from_dict({ # type: ignore
|
||||
|
|
Reference in New Issue