Compare commits
No commits in common. "8558c484c54e989750a798c42535ca5a82586cf3" and "7a1077e3715e03a107a610347350c469ce06196c" have entirely different histories.
8558c484c5
...
7a1077e371
|
@ -1,9 +1,7 @@
|
||||||
{
|
{
|
||||||
"cSpell.words": [
|
"cSpell.words": [
|
||||||
"autochurch",
|
|
||||||
"freevar",
|
"freevar",
|
||||||
"pyparsing",
|
"pyparsing",
|
||||||
"runstatus",
|
|
||||||
"subvar"
|
"subvar"
|
||||||
],
|
],
|
||||||
"python.analysis.typeCheckingMode": "basic"
|
"python.analysis.typeCheckingMode": "basic"
|
||||||
|
|
|
@ -2,12 +2,15 @@
|
||||||
|
|
||||||
|
|
||||||
## Todo (pre-release):
|
## Todo (pre-release):
|
||||||
|
- Fix parser (call parentheses)
|
||||||
- Good command parsing (`:save`, `:load`, are a bare minimum)
|
- Good command parsing (`:save`, `:load`, are a bare minimum)
|
||||||
- Python files: installable, package list, etc
|
- Python files: installable, package list, etc
|
||||||
- $\alpha$-equivalence check
|
- $\alpha$-equivalence check
|
||||||
- Versioning
|
- Versioning
|
||||||
|
- Automatic church numerals
|
||||||
- Prettyprint functions (combine args, rename bound variables)
|
- Prettyprint functions (combine args, rename bound variables)
|
||||||
- Documentation in README
|
- Documentation in README
|
||||||
|
- Don't crash on errors
|
||||||
|
|
||||||
## Todo:
|
## Todo:
|
||||||
- live syntax check
|
- live syntax check
|
||||||
|
@ -17,8 +20,6 @@
|
||||||
- Warn when overwriting macro
|
- Warn when overwriting macro
|
||||||
- Syntax highlighting: parenthesis, bound variables, macros, etc
|
- Syntax highlighting: parenthesis, bound variables, macros, etc
|
||||||
- Pin header to top of screen
|
- Pin header to top of screen
|
||||||
- Parser is a bit slow. Maybe we can do better?
|
|
||||||
|
|
||||||
## Mention in Docs
|
## Mention in Docs
|
||||||
- lambda functions only work with single-letter arguments
|
- lambda functions only work with single-letter arguments
|
||||||
- church numerals
|
|
10
main.py
10
main.py
|
@ -43,7 +43,7 @@ r.run_lines([
|
||||||
"OR = λab.(a T b)",
|
"OR = λab.(a T b)",
|
||||||
"XOR = λab.(a (NOT a b) b)",
|
"XOR = λab.(a (NOT a b) b)",
|
||||||
"w = λx.(x x)",
|
"w = λx.(x x)",
|
||||||
"W = w w",
|
"W = (w w)",
|
||||||
"Y = λf.( (λx.(f (x x))) (λx.(f (x x))) )",
|
"Y = λf.( (λx.(f (x x))) (λx.(f (x x))) )",
|
||||||
"PAIR = λabi.( i a b )",
|
"PAIR = λabi.( i a b )",
|
||||||
"inc = λnfa.(f (n f a))",
|
"inc = λnfa.(f (n f a))",
|
||||||
|
@ -90,13 +90,7 @@ while True:
|
||||||
|
|
||||||
# If this line defined a macro, print nothing.
|
# If this line defined a macro, print nothing.
|
||||||
if isinstance(x, runner.MacroStatus):
|
if isinstance(x, runner.MacroStatus):
|
||||||
printf(FormattedText([
|
pass
|
||||||
("#FFFFFF", "Set "),
|
|
||||||
("#FF00FF", x.macro_label),
|
|
||||||
("#FFFFFF", " to "),
|
|
||||||
("#FFFFFF", str(x.macro_expr))
|
|
||||||
]))
|
|
||||||
|
|
||||||
|
|
||||||
if isinstance(x, runner.CommandStatus):
|
if isinstance(x, runner.CommandStatus):
|
||||||
printf(x.formatted_text)
|
printf(x.formatted_text)
|
||||||
|
|
70
parser.py
70
parser.py
|
@ -1,8 +1,17 @@
|
||||||
import pyparsing as pp
|
import pyparsing as pp
|
||||||
import tokens
|
import tokens
|
||||||
import utils
|
|
||||||
|
|
||||||
class Parser:
|
class Parser:
|
||||||
|
"""
|
||||||
|
Macro_def must be on its own line.
|
||||||
|
macro_def :: var = expr
|
||||||
|
|
||||||
|
var :: word
|
||||||
|
lambda_fun :: var -> expr
|
||||||
|
call :: '(' (var | expr) ')' +
|
||||||
|
expr :: define | var | call | '(' expr ')'
|
||||||
|
"""
|
||||||
|
|
||||||
lp = pp.Suppress("(")
|
lp = pp.Suppress("(")
|
||||||
rp = pp.Suppress(")")
|
rp = pp.Suppress(")")
|
||||||
|
|
||||||
|
@ -11,18 +20,6 @@ class Parser:
|
||||||
pp_macro = pp.Word(pp.alphas + "_")
|
pp_macro = pp.Word(pp.alphas + "_")
|
||||||
pp_macro.set_parse_action(tokens.macro.from_parse)
|
pp_macro.set_parse_action(tokens.macro.from_parse)
|
||||||
|
|
||||||
pp_church = pp.Word(pp.nums)
|
|
||||||
pp_church.set_parse_action(utils.autochurch)
|
|
||||||
|
|
||||||
# Function calls.
|
|
||||||
# `tokens.lambda_apply.from_parse` handles chained calls.
|
|
||||||
#
|
|
||||||
# <exp> <exp>
|
|
||||||
# <exp> <exp> <exp>
|
|
||||||
pp_call = pp.Forward()
|
|
||||||
pp_call <<= pp_expr[2, ...]
|
|
||||||
pp_call.set_parse_action(tokens.lambda_apply.from_parse)
|
|
||||||
|
|
||||||
# Function definitions.
|
# Function definitions.
|
||||||
# Right associative.
|
# Right associative.
|
||||||
#
|
#
|
||||||
|
@ -31,44 +28,41 @@ class Parser:
|
||||||
(pp.Suppress("λ") | pp.Suppress("\\")) +
|
(pp.Suppress("λ") | pp.Suppress("\\")) +
|
||||||
pp.Group(pp.Char(pp.alphas)[1, ...]) +
|
pp.Group(pp.Char(pp.alphas)[1, ...]) +
|
||||||
pp.Suppress(".") +
|
pp.Suppress(".") +
|
||||||
(pp_expr ^ pp_call)
|
pp_expr
|
||||||
)
|
)
|
||||||
pp_lambda_fun.set_parse_action(tokens.lambda_func.from_parse)
|
pp_lambda_fun.set_parse_action(tokens.lambda_func.from_parse)
|
||||||
|
|
||||||
# Assignment.
|
# Assignment.
|
||||||
# Can only be found at the start of a line.
|
# Can only be found at the start of a line.
|
||||||
#
|
#
|
||||||
# <name> = <exp>
|
# <var> = <exp>
|
||||||
pp_macro_def = (
|
pp_macro_def = pp.line_start() + pp_macro + pp.Suppress("=") + pp_expr
|
||||||
pp.line_start() +
|
|
||||||
pp_macro +
|
|
||||||
pp.Suppress("=") +
|
|
||||||
(pp_expr ^ pp_call)
|
|
||||||
)
|
|
||||||
pp_macro_def.set_parse_action(tokens.macro_expression.from_parse)
|
pp_macro_def.set_parse_action(tokens.macro_expression.from_parse)
|
||||||
|
|
||||||
pp_expr <<= (
|
# Function calls.
|
||||||
pp_church ^
|
# `tokens.lambda_func.from_parse` handles chained calls.
|
||||||
pp_lambda_fun ^
|
#
|
||||||
pp_macro ^
|
# <var>(<exp>)
|
||||||
(lp + pp_expr + rp) ^
|
# <var>(<exp>)(<exp>)(<exp>)
|
||||||
(lp + pp_call + rp)
|
# (<exp>)(<exp>)
|
||||||
)
|
# (<exp>)(<exp>)(<exp>)(<exp>)
|
||||||
|
pp_call = pp.Forward()
|
||||||
|
pp_call <<= pp_expr[2, ...]
|
||||||
|
pp_call.set_parse_action(tokens.lambda_apply.from_parse)
|
||||||
|
|
||||||
|
pp_expr <<= pp_lambda_fun ^ (lp + pp_expr + rp) ^ pp_macro ^ (lp + pp_call + rp)
|
||||||
|
pp_all = pp_expr | pp_macro_def
|
||||||
|
|
||||||
pp_command = pp.Suppress(":") + pp.Word(pp.alphas + "_")
|
pp_command = pp.Suppress(":") + pp.Word(pp.alphas + "_")
|
||||||
pp_command.set_parse_action(tokens.command.from_parse)
|
pp_command.set_parse_action(tokens.command.from_parse)
|
||||||
|
|
||||||
|
|
||||||
pp_all = (
|
|
||||||
pp_expr ^
|
|
||||||
pp_macro_def ^
|
|
||||||
pp_command ^
|
|
||||||
pp_call
|
|
||||||
)
|
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def parse_line(line):
|
def parse_line(line):
|
||||||
k = Parser.pp_all.parse_string(
|
k = (
|
||||||
|
Parser.pp_expr ^
|
||||||
|
Parser.pp_macro_def ^
|
||||||
|
Parser.pp_command ^ Parser.pp_call
|
||||||
|
).parse_string(
|
||||||
line,
|
line,
|
||||||
parse_all = True
|
parse_all = True
|
||||||
)[0]
|
)[0]
|
||||||
|
@ -77,4 +71,4 @@ class Parser:
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def run_tests(lines):
|
def run_tests(lines):
|
||||||
return Parser.pp_all.run_tests(lines)
|
return Parser.pp_macro_def.run_tests(lines)
|
15
runner.py
15
runner.py
|
@ -10,6 +10,10 @@ from runstatus import ReduceStatus
|
||||||
from runstatus import CommandStatus
|
from runstatus import CommandStatus
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
class Runner:
|
class Runner:
|
||||||
def __init__(self):
|
def __init__(self):
|
||||||
self.macro_table = {}
|
self.macro_table = {}
|
||||||
|
@ -39,7 +43,7 @@ class Runner:
|
||||||
i = 0
|
i = 0
|
||||||
macro_expansions = 0
|
macro_expansions = 0
|
||||||
|
|
||||||
while (self.reduction_limit is None) or (i < self.reduction_limit):
|
while i < self.reduction_limit:
|
||||||
r = expr.reduce(self.macro_table)
|
r = expr.reduce(self.macro_table)
|
||||||
expr = r.output
|
expr = r.output
|
||||||
|
|
||||||
|
@ -60,7 +64,7 @@ class Runner:
|
||||||
return ReduceStatus(
|
return ReduceStatus(
|
||||||
reduction_count = i - macro_expansions,
|
reduction_count = i - macro_expansions,
|
||||||
stop_reason = StopReason.MAX_EXCEEDED,
|
stop_reason = StopReason.MAX_EXCEEDED,
|
||||||
result = r.output # type: ignore
|
result = r.output
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
||||||
|
@ -77,8 +81,7 @@ class Runner:
|
||||||
|
|
||||||
return MacroStatus(
|
return MacroStatus(
|
||||||
was_rewritten = was_rewritten,
|
was_rewritten = was_rewritten,
|
||||||
macro_label = e.label,
|
macro_label = e.label
|
||||||
macro_expr = e.exp
|
|
||||||
)
|
)
|
||||||
|
|
||||||
# If this line is a command, do the command.
|
# If this line is a command, do the command.
|
||||||
|
@ -86,11 +89,9 @@ class Runner:
|
||||||
return self.exec_command(e.name)
|
return self.exec_command(e.name)
|
||||||
|
|
||||||
# If this line is a plain expression, reduce it.
|
# If this line is a plain expression, reduce it.
|
||||||
elif isinstance(e, tokens.LambdaToken):
|
else:
|
||||||
e.bind_variables()
|
e.bind_variables()
|
||||||
return self.reduce_expression(e)
|
return self.reduce_expression(e)
|
||||||
else:
|
|
||||||
raise TypeError(f"I don't know what to do with a {type(e)}")
|
|
||||||
|
|
||||||
|
|
||||||
def run_lines(self, lines: list[str]):
|
def run_lines(self, lines: list[str]):
|
||||||
|
|
|
@ -17,19 +17,16 @@ class MacroStatus(RunStatus):
|
||||||
Values:
|
Values:
|
||||||
`was_rewritten`: If true, an old macro was replaced.
|
`was_rewritten`: If true, an old macro was replaced.
|
||||||
`macro_label`: The name of the macro we just made.
|
`macro_label`: The name of the macro we just made.
|
||||||
`macro_expr`: The expr of the macro we just made.
|
|
||||||
"""
|
"""
|
||||||
|
|
||||||
def __init__(
|
def __init__(
|
||||||
self,
|
self,
|
||||||
*,
|
*,
|
||||||
was_rewritten: bool,
|
was_rewritten: bool,
|
||||||
macro_label: str,
|
macro_label: str
|
||||||
macro_expr
|
|
||||||
):
|
):
|
||||||
self.was_rewritten = was_rewritten
|
self.was_rewritten = was_rewritten
|
||||||
self.macro_label = macro_label
|
self.macro_label = macro_label
|
||||||
self.macro_expr = macro_expr
|
|
||||||
|
|
||||||
|
|
||||||
class StopReason(enum.Enum):
|
class StopReason(enum.Enum):
|
||||||
|
|
12
tokens.py
12
tokens.py
|
@ -302,9 +302,9 @@ class lambda_func(LambdaToken):
|
||||||
|
|
||||||
|
|
||||||
# Bind variables inside this function.
|
# Bind variables inside this function.
|
||||||
if isinstance(self.output, macro) and placeholder is not None:
|
if isinstance(self.output, macro):
|
||||||
if self.output == placeholder:
|
if self.output == placeholder:
|
||||||
self.output = val # type: ignore
|
self.output = val
|
||||||
elif isinstance(self.output, lambda_func):
|
elif isinstance(self.output, lambda_func):
|
||||||
self.output.bind_variables(placeholder, val)
|
self.output.bind_variables(placeholder, val)
|
||||||
elif isinstance(self.output, lambda_apply):
|
elif isinstance(self.output, lambda_apply):
|
||||||
|
@ -345,7 +345,7 @@ class lambda_func(LambdaToken):
|
||||||
calling_self = False
|
calling_self = False
|
||||||
if bound_var is None:
|
if bound_var is None:
|
||||||
calling_self = True
|
calling_self = True
|
||||||
bound_var = self.input # type: ignore
|
bound_var = self.input
|
||||||
new_out = self.output
|
new_out = self.output
|
||||||
if isinstance(self.output, bound_variable):
|
if isinstance(self.output, bound_variable):
|
||||||
if self.output == bound_var:
|
if self.output == bound_var:
|
||||||
|
@ -353,7 +353,7 @@ class lambda_func(LambdaToken):
|
||||||
elif isinstance(self.output, lambda_func):
|
elif isinstance(self.output, lambda_func):
|
||||||
new_out = self.output.apply(val, bound_var = bound_var)
|
new_out = self.output.apply(val, bound_var = bound_var)
|
||||||
elif isinstance(self.output, lambda_apply):
|
elif isinstance(self.output, lambda_apply):
|
||||||
new_out = self.output.sub_bound_var(val, bound_var = bound_var) # type: ignore
|
new_out = self.output.sub_bound_var(val, bound_var = bound_var)
|
||||||
|
|
||||||
# If we're applying THIS function,
|
# If we're applying THIS function,
|
||||||
# just give the output
|
# just give the output
|
||||||
|
@ -430,7 +430,7 @@ class lambda_apply(LambdaToken):
|
||||||
# everything below should still work as expected.
|
# everything below should still work as expected.
|
||||||
if isinstance(self.fn, macro) and placeholder is not None:
|
if isinstance(self.fn, macro) and placeholder is not None:
|
||||||
if self.fn == placeholder:
|
if self.fn == placeholder:
|
||||||
self.fn = val # type: ignore
|
self.fn = val
|
||||||
elif isinstance(self.fn, lambda_func):
|
elif isinstance(self.fn, lambda_func):
|
||||||
self.fn.bind_variables(placeholder, val)
|
self.fn.bind_variables(placeholder, val)
|
||||||
elif isinstance(self.fn, lambda_apply):
|
elif isinstance(self.fn, lambda_apply):
|
||||||
|
@ -438,7 +438,7 @@ class lambda_apply(LambdaToken):
|
||||||
|
|
||||||
if isinstance(self.arg, macro) and placeholder is not None:
|
if isinstance(self.arg, macro) and placeholder is not None:
|
||||||
if self.arg == placeholder:
|
if self.arg == placeholder:
|
||||||
self.arg = val # type: ignore
|
self.arg = val
|
||||||
elif isinstance(self.arg, lambda_func):
|
elif isinstance(self.arg, lambda_func):
|
||||||
self.arg.bind_variables(placeholder, val)
|
self.arg.bind_variables(placeholder, val)
|
||||||
elif isinstance(self.arg, lambda_apply):
|
elif isinstance(self.arg, lambda_apply):
|
||||||
|
|
24
utils.py
24
utils.py
|
@ -1,24 +0,0 @@
|
||||||
import tokens
|
|
||||||
|
|
||||||
def autochurch(results):
|
|
||||||
"""
|
|
||||||
Makes a church numeral from an integer.
|
|
||||||
"""
|
|
||||||
|
|
||||||
num = int(results[0])
|
|
||||||
|
|
||||||
f = tokens.bound_variable()
|
|
||||||
a = tokens.bound_variable()
|
|
||||||
|
|
||||||
chain = a
|
|
||||||
|
|
||||||
for i in range(num):
|
|
||||||
chain = tokens.lambda_apply(f, chain)
|
|
||||||
|
|
||||||
return tokens.lambda_func(
|
|
||||||
f,
|
|
||||||
tokens.lambda_func(
|
|
||||||
a,
|
|
||||||
chain
|
|
||||||
)
|
|
||||||
)
|
|
Reference in New Issue