2022-10-21 21:01:06 -07:00
|
|
|
from prompt_toolkit.styles import Style
|
|
|
|
from prompt_toolkit.formatted_text import HTML
|
2022-11-07 19:58:11 -08:00
|
|
|
from prompt_toolkit.lexers import Lexer
|
|
|
|
from prompt_toolkit.key_binding import KeyBindings
|
2022-10-21 21:01:06 -07:00
|
|
|
from prompt_toolkit import print_formatted_text as printf
|
|
|
|
from importlib.metadata import version
|
2022-11-11 17:04:05 -08:00
|
|
|
from prompt_toolkit.document import Document
|
2022-10-21 21:01:06 -07:00
|
|
|
|
2022-11-10 09:08:58 -08:00
|
|
|
import re
|
|
|
|
|
2022-10-21 21:01:06 -07:00
|
|
|
|
2022-10-22 12:59:42 -07:00
|
|
|
style = Style.from_dict({ # type: ignore
|
2022-10-22 08:37:19 -07:00
|
|
|
# Basic formatting
|
|
|
|
"text": "#FFFFFF",
|
2022-11-01 21:29:39 -07:00
|
|
|
"warn": "#FFA700",
|
|
|
|
"err": "#FF3809",
|
|
|
|
"prompt": "#05CFFF",
|
|
|
|
"ok": "#00EF7C",
|
2022-10-29 15:43:59 -07:00
|
|
|
"code": "#AAAAAA italic",
|
2022-10-28 19:47:50 -07:00
|
|
|
"muted": "#AAAAAA",
|
2022-10-22 08:37:19 -07:00
|
|
|
|
2022-11-07 19:58:11 -08:00
|
|
|
# Syntax highlighting colors
|
|
|
|
"syn_cmd": "#FFFFFF italic",
|
|
|
|
"syn_lambda": "#AAAAAA",
|
|
|
|
"syn_paren": "#AAAAAA",
|
|
|
|
|
2022-10-22 08:37:19 -07:00
|
|
|
# Command formatting
|
|
|
|
# cmd_h: section titles
|
|
|
|
# cmd_key: keyboard keys, usually one character
|
2022-11-01 21:29:39 -07:00
|
|
|
"cmd_h": "#FF3809 bold",
|
|
|
|
"cmd_key": "#00EF7C bold",
|
2022-10-22 08:37:19 -07:00
|
|
|
|
|
|
|
# Only used in greeting
|
2022-11-01 21:29:39 -07:00
|
|
|
"_v": "#00EF7C bold",
|
|
|
|
"_l": "#FF3809 bold",
|
|
|
|
"_s": "#00EF7C bold",
|
2022-10-22 08:37:19 -07:00
|
|
|
"_p": "#AAAAAA"
|
|
|
|
})
|
|
|
|
|
2022-10-21 21:01:06 -07:00
|
|
|
|
2022-11-07 19:58:11 -08:00
|
|
|
# Replace "\" with pretty "λ"s
|
|
|
|
bindings = KeyBindings()
|
|
|
|
@bindings.add("\\")
|
|
|
|
def _(event):
|
|
|
|
event.current_buffer.insert_text("λ")
|
|
|
|
|
|
|
|
# Simple lexer for highlighting.
|
|
|
|
# Improve this later.
|
|
|
|
class LambdaLexer(Lexer):
|
|
|
|
def lex_document(self, document):
|
|
|
|
def inner(line_no):
|
|
|
|
out = []
|
|
|
|
tmp_str = []
|
|
|
|
d = str(document.lines[line_no])
|
|
|
|
|
|
|
|
if d.startswith(":"):
|
|
|
|
return [
|
|
|
|
("class:syn_cmd", d)
|
|
|
|
]
|
|
|
|
|
|
|
|
for c in d:
|
|
|
|
if c in "\\λ.":
|
|
|
|
if len(tmp_str) != 0:
|
|
|
|
out.append(("class:text", "".join(tmp_str)))
|
|
|
|
out.append(("class:syn_lambda", c))
|
|
|
|
tmp_str = []
|
|
|
|
elif c in "()":
|
|
|
|
if len(tmp_str) != 0:
|
|
|
|
out.append(("class:text", "".join(tmp_str)))
|
|
|
|
out.append(("class:syn_paren", c))
|
|
|
|
tmp_str = []
|
|
|
|
else:
|
|
|
|
tmp_str.append(c)
|
|
|
|
|
|
|
|
if len(tmp_str) != 0:
|
|
|
|
out.append(("class:text", "".join(tmp_str)))
|
|
|
|
return out
|
|
|
|
return inner
|
|
|
|
|
|
|
|
|
2022-11-11 17:04:05 -08:00
|
|
|
|
|
|
|
def lex_str(s: str) -> list[tuple[str, str]]:
|
|
|
|
return LambdaLexer().lex_document(Document(s))(0)
|
|
|
|
|
2022-10-21 21:01:06 -07:00
|
|
|
def show_greeting():
|
|
|
|
# | _.._ _.|_
|
|
|
|
# |_(_|| | ||_)
|
|
|
|
# 0.0.0
|
|
|
|
#
|
|
|
|
# __ __
|
|
|
|
# ,-` `` `,
|
|
|
|
# (` \ )
|
|
|
|
# (` \ `)
|
|
|
|
# (, / \ _)
|
|
|
|
# (` / \ )
|
|
|
|
# `'._.--._.'
|
|
|
|
#
|
|
|
|
# A λ calculus engine
|
|
|
|
|
|
|
|
printf(HTML("\n".join([
|
|
|
|
"",
|
|
|
|
"<_h> | _.._ _.|_",
|
|
|
|
" |_(_|| | ||_)</_h>",
|
2022-11-11 18:19:38 -08:00
|
|
|
f" <_v>{version('lamb_engine')}</_v>",
|
2022-10-21 21:01:06 -07:00
|
|
|
" __ __",
|
|
|
|
" ,-` `` `,",
|
|
|
|
" (` <_l>\\</_l> )",
|
|
|
|
" (` <_l>\\</_l> `)",
|
|
|
|
" (, <_l>/ \\</_l> _)",
|
|
|
|
" (` <_l>/ \\</_l> )",
|
|
|
|
" `'._.--._.'",
|
|
|
|
"",
|
|
|
|
"<_s> A λ calculus engine</_s>",
|
|
|
|
"<_p> Type :help for help</_p>",
|
|
|
|
""
|
2022-10-29 13:25:37 -07:00
|
|
|
])), style = style)
|
|
|
|
|
2022-11-10 09:08:58 -08:00
|
|
|
def remove_sub(s: str):
|
|
|
|
return re.sub("[₀₁₂₃₄₅₆₈₉]*", "", s)
|
|
|
|
|
2022-11-10 08:02:28 -08:00
|
|
|
def base4(n: int):
|
|
|
|
if n == 0:
|
|
|
|
return [0]
|
|
|
|
digits = []
|
|
|
|
while n:
|
|
|
|
digits.append(n % 4)
|
|
|
|
n //= 4
|
|
|
|
return digits[::-1]
|
|
|
|
|
2022-10-29 13:25:37 -07:00
|
|
|
def subscript(num: int):
|
2022-11-10 08:02:28 -08:00
|
|
|
|
2022-11-10 09:08:58 -08:00
|
|
|
# unicode subscripts ₀₁₂₃ and ₄₅₆₈₉
|
|
|
|
# usually look different,
|
|
|
|
# so we'll use base 4.
|
2022-11-10 08:02:28 -08:00
|
|
|
qb = base4(num)
|
|
|
|
|
2022-10-29 13:25:37 -07:00
|
|
|
sub = {
|
|
|
|
"0": "₀",
|
|
|
|
"1": "₁",
|
|
|
|
"2": "₂",
|
|
|
|
"3": "₃",
|
|
|
|
"4": "₄",
|
|
|
|
"5": "₅",
|
|
|
|
"6": "₆",
|
|
|
|
"7": "₇",
|
|
|
|
"8": "₈",
|
|
|
|
"9": "₉"
|
|
|
|
}
|
|
|
|
|
|
|
|
sup = {
|
|
|
|
"0": "⁰",
|
|
|
|
"1": "¹",
|
|
|
|
"2": "²",
|
|
|
|
"3": "³",
|
|
|
|
"4": "⁴",
|
|
|
|
"5": "⁵",
|
|
|
|
"6": "⁶",
|
|
|
|
"7": "⁷",
|
|
|
|
"8": "⁸",
|
|
|
|
"9": "⁹"
|
|
|
|
}
|
|
|
|
|
|
|
|
return "".join(
|
2022-11-10 08:02:28 -08:00
|
|
|
[sub[str(x)] for x in qb]
|
2022-10-29 13:25:37 -07:00
|
|
|
)
|