Compare commits
3 Commits
7a1077e371
...
8558c484c5
Author | SHA1 | Date |
---|---|---|
Mark | 8558c484c5 | |
Mark | ee744b5245 | |
Mark | b5d97cf5c6 |
|
@ -1,7 +1,9 @@
|
||||||
{
|
{
|
||||||
"cSpell.words": [
|
"cSpell.words": [
|
||||||
|
"autochurch",
|
||||||
"freevar",
|
"freevar",
|
||||||
"pyparsing",
|
"pyparsing",
|
||||||
|
"runstatus",
|
||||||
"subvar"
|
"subvar"
|
||||||
],
|
],
|
||||||
"python.analysis.typeCheckingMode": "basic"
|
"python.analysis.typeCheckingMode": "basic"
|
||||||
|
|
|
@ -2,15 +2,12 @@
|
||||||
|
|
||||||
|
|
||||||
## 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
|
||||||
|
@ -20,6 +17,8 @@
|
||||||
- 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,7 +90,13 @@ 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):
|
||||||
pass
|
printf(FormattedText([
|
||||||
|
("#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,17 +1,8 @@
|
||||||
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(")")
|
||||||
|
|
||||||
|
@ -20,6 +11,18 @@ 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.
|
||||||
#
|
#
|
||||||
|
@ -28,41 +31,44 @@ 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_expr ^ pp_call)
|
||||||
)
|
)
|
||||||
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.
|
||||||
#
|
#
|
||||||
# <var> = <exp>
|
# <name> = <exp>
|
||||||
pp_macro_def = pp.line_start() + pp_macro + pp.Suppress("=") + pp_expr
|
pp_macro_def = (
|
||||||
|
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)
|
||||||
|
|
||||||
# Function calls.
|
pp_expr <<= (
|
||||||
# `tokens.lambda_func.from_parse` handles chained calls.
|
pp_church ^
|
||||||
#
|
pp_lambda_fun ^
|
||||||
# <var>(<exp>)
|
pp_macro ^
|
||||||
# <var>(<exp>)(<exp>)(<exp>)
|
(lp + pp_expr + rp) ^
|
||||||
# (<exp>)(<exp>)
|
(lp + pp_call + rp)
|
||||||
# (<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 = (
|
k = Parser.pp_all.parse_string(
|
||||||
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]
|
||||||
|
@ -71,4 +77,4 @@ class Parser:
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def run_tests(lines):
|
def run_tests(lines):
|
||||||
return Parser.pp_macro_def.run_tests(lines)
|
return Parser.pp_all.run_tests(lines)
|
15
runner.py
15
runner.py
|
@ -10,10 +10,6 @@ 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 = {}
|
||||||
|
@ -43,7 +39,7 @@ class Runner:
|
||||||
i = 0
|
i = 0
|
||||||
macro_expansions = 0
|
macro_expansions = 0
|
||||||
|
|
||||||
while i < self.reduction_limit:
|
while (self.reduction_limit is None) or (i < self.reduction_limit):
|
||||||
r = expr.reduce(self.macro_table)
|
r = expr.reduce(self.macro_table)
|
||||||
expr = r.output
|
expr = r.output
|
||||||
|
|
||||||
|
@ -64,7 +60,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
|
result = r.output # type: ignore
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
||||||
|
@ -81,7 +77,8 @@ 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.
|
||||||
|
@ -89,9 +86,11 @@ 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.
|
||||||
else:
|
elif isinstance(e, tokens.LambdaToken):
|
||||||
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,16 +17,19 @@ 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):
|
if isinstance(self.output, macro) and placeholder is not None:
|
||||||
if self.output == placeholder:
|
if self.output == placeholder:
|
||||||
self.output = val
|
self.output = val # type: ignore
|
||||||
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
|
bound_var = self.input # type: ignore
|
||||||
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)
|
new_out = self.output.sub_bound_var(val, bound_var = bound_var) # type: ignore
|
||||||
|
|
||||||
# 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
|
self.fn = val # type: ignore
|
||||||
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
|
self.arg = val # type: ignore
|
||||||
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):
|
||||||
|
|
|
@ -0,0 +1,24 @@
|
||||||
|
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