Skip to content

Instantly share code, notes, and snippets.

@saulshanabrook

saulshanabrook/find_list_egglog.ipynb

Created December 5, 2023 23:48
Show Gist options
  • Save saulshanabrook/71e9d15cb63edc2b78b9e20739a44712 to your computer and use it in GitHub Desktop.
Save saulshanabrook/71e9d15cb63edc2b78b9e20739a44712 to your computer and use it in GitHub Desktop.
Download ZIP
Display the source blob
Display the rendered blob
Raw
find_list_egglog.ipynb
{
"cells": [
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"from __future__ import annotations\n",
"\n",
"from egglog import *\n",
"\n",
"egraph = EGraph()\n",
"\n",
"\n",
"@egraph.class_\n",
"class Num(Expr):\n",
" def __init__(self, value: i64Like) -> None:\n",
" ...\n",
"\n",
" @classmethod\n",
" def var(cls, name: StringLike) -> Num:\n",
" ...\n",
"\n",
" def __add__(self, other: Num) -> Num:\n",
" ...\n",
"\n",
" def __sub__(self, other: Num) -> Num:\n",
" ...\n",
"\n",
"\n",
"converter(i64, Num, Num)\n",
"converter(String, Num, Num.var)\n",
"\n",
"@egraph.class_\n",
"class OptionalNum(Expr):\n",
" def __init__(self, x: Num) -> None: ...\n",
"\n",
" @classmethod\n",
" def none(cls) -> OptionalNum: ...\n",
"\n",
" def incr(self) -> OptionalNum:\n",
" \"Increment if some\"\n",
" # could be replaced with `map` if we had higher order functions\n",
" \n",
"converter(Num, OptionalNum, OptionalNum)\n",
"converter(None, OptionalNum, lambda _: OptionalNum.none())\n",
"\n",
"\n",
"@egraph.class_\n",
"class NumList(Expr):\n",
" def __getitem__(self, index: Num) -> Num:\n",
" ...\n",
"\n",
" def index(self, value: Num) -> OptionalNum:\n",
" ...\n",
"\n",
"\n",
"@egraph.function\n",
"def nil() -> NumList:\n",
" ...\n",
"\n",
"\n",
"@egraph.function\n",
"def cons(x: Num, xs: NumList) -> NumList:\n",
" ...\n",
"\n",
"\n",
"converter(tuple, NumList, lambda t: nil() if not t else cons(t[0], t[1:]))\n",
"\n",
"\n",
"@egraph.register\n",
"def _rules(l: NumList, x: Num, i: i64, j: i64):\n",
" yield rewrite(Num(i) + Num(j)).to(Num(i + j))\n",
" yield rewrite(Num(i) - Num(j)).to(Num(i - j))\n",
"\n",
" yield rewrite(OptionalNum.none().incr()).to(OptionalNum.none())\n",
" yield rewrite(OptionalNum(x).incr()).to(OptionalNum(x + Num(1)))\n",
"\n",
" yield rewrite(cons(x, l)[Num(0)]).to(x)\n",
" yield rewrite(cons(x, l)[Num(i)]).to(l[i - Num(1)], i != i64(0))\n",
"\n",
" yield rewrite(cons(x, l).index(x)).to(OptionalNum(Num(0)))\n",
" yield rewrite(cons(Num(i), l).index(Num(j))).to(l.index(Num(j)).incr(), i != j)\n",
" yield rewrite(nil().index(x)).to(OptionalNum.none())"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<style>pre { line-height: 125%; }\n",
"td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
".output_html .hll { background-color: #ffffcc }\n",
".output_html { background: #f8f8f8; }\n",
".output_html .c { color: #3D7B7B; font-style: italic } /* Comment */\n",
".output_html .err { border: 1px solid #FF0000 } /* Error */\n",
".output_html .k { color: #008000; font-weight: bold } /* Keyword */\n",
".output_html .o { color: #666666 } /* Operator */\n",
".output_html .ch { color: #3D7B7B; font-style: italic } /* Comment.Hashbang */\n",
".output_html .cm { color: #3D7B7B; font-style: italic } /* Comment.Multiline */\n",
".output_html .cp { color: #9C6500 } /* Comment.Preproc */\n",
".output_html .cpf { color: #3D7B7B; font-style: italic } /* Comment.PreprocFile */\n",
".output_html .c1 { color: #3D7B7B; font-style: italic } /* Comment.Single */\n",
".output_html .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */\n",
".output_html .gd { color: #A00000 } /* Generic.Deleted */\n",
".output_html .ge { font-style: italic } /* Generic.Emph */\n",
".output_html .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */\n",
".output_html .gr { color: #E40000 } /* Generic.Error */\n",
".output_html .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
".output_html .gi { color: #008400 } /* Generic.Inserted */\n",
".output_html .go { color: #717171 } /* Generic.Output */\n",
".output_html .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
".output_html .gs { font-weight: bold } /* Generic.Strong */\n",
".output_html .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
".output_html .gt { color: #0044DD } /* Generic.Traceback */\n",
".output_html .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
".output_html .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
".output_html .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
".output_html .kp { color: #008000 } /* Keyword.Pseudo */\n",
".output_html .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
".output_html .kt { color: #B00040 } /* Keyword.Type */\n",
".output_html .m { color: #666666 } /* Literal.Number */\n",
".output_html .s { color: #BA2121 } /* Literal.String */\n",
".output_html .na { color: #687822 } /* Name.Attribute */\n",
".output_html .nb { color: #008000 } /* Name.Builtin */\n",
".output_html .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
".output_html .no { color: #880000 } /* Name.Constant */\n",
".output_html .nd { color: #AA22FF } /* Name.Decorator */\n",
".output_html .ni { color: #717171; font-weight: bold } /* Name.Entity */\n",
".output_html .ne { color: #CB3F38; font-weight: bold } /* Name.Exception */\n",
".output_html .nf { color: #0000FF } /* Name.Function */\n",
".output_html .nl { color: #767600 } /* Name.Label */\n",
".output_html .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
".output_html .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
".output_html .nv { color: #19177C } /* Name.Variable */\n",
".output_html .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
".output_html .w { color: #bbbbbb } /* Text.Whitespace */\n",
".output_html .mb { color: #666666 } /* Literal.Number.Bin */\n",
".output_html .mf { color: #666666 } /* Literal.Number.Float */\n",
".output_html .mh { color: #666666 } /* Literal.Number.Hex */\n",
".output_html .mi { color: #666666 } /* Literal.Number.Integer */\n",
".output_html .mo { color: #666666 } /* Literal.Number.Oct */\n",
".output_html .sa { color: #BA2121 } /* Literal.String.Affix */\n",
".output_html .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
".output_html .sc { color: #BA2121 } /* Literal.String.Char */\n",
".output_html .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
".output_html .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
".output_html .s2 { color: #BA2121 } /* Literal.String.Double */\n",
".output_html .se { color: #AA5D1F; font-weight: bold } /* Literal.String.Escape */\n",
".output_html .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
".output_html .si { color: #A45A77; font-weight: bold } /* Literal.String.Interpol */\n",
".output_html .sx { color: #008000 } /* Literal.String.Other */\n",
".output_html .sr { color: #A45A77 } /* Literal.String.Regex */\n",
".output_html .s1 { color: #BA2121 } /* Literal.String.Single */\n",
".output_html .ss { color: #19177C } /* Literal.String.Symbol */\n",
".output_html .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
".output_html .fm { color: #0000FF } /* Name.Function.Magic */\n",
".output_html .vc { color: #19177C } /* Name.Variable.Class */\n",
".output_html .vg { color: #19177C } /* Name.Variable.Global */\n",
".output_html .vi { color: #19177C } /* Name.Variable.Instance */\n",
".output_html .vm { color: #19177C } /* Name.Variable.Magic */\n",
".output_html .il { color: #666666 } /* Literal.Number.Integer.Long */</style><div class=\"highlight\"><pre><span></span><span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">1</span><span class=\"p\">),</span> <span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">2</span><span class=\"p\">),</span> <span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"o\">.</span><span class=\"n\">var</span><span class=\"p\">(</span><span class=\"s2\">&quot;x&quot;</span><span class=\"p\">),</span> <span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">nil</span><span class=\"p\">()))))</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{1}\\PY{p}{)}\\PY{p}{,} \\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{2}\\PY{p}{)}\\PY{p}{,} \\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{o}{.}\\PY{n}{var}\\PY{p}{(}\\PY{l+s+s2}{\\PYZdq{}}\\PY{l+s+s2}{x}\\PY{l+s+s2}{\\PYZdq{}}\\PY{p}{)}\\PY{p}{,} \\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{nil}\\PY{p}{(}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"cons(Num(1), cons(Num(2), cons(Num.var(\"x\"), cons(Num(3), nil()))))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"lst = convert((1, 2, \"x\", 3), NumList)\n",
"lst"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<style>pre { line-height: 125%; }\n",
"td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
".output_html .hll { background-color: #ffffcc }\n",
".output_html { background: #f8f8f8; }\n",
".output_html .c { color: #3D7B7B; font-style: italic } /* Comment */\n",
".output_html .err { border: 1px solid #FF0000 } /* Error */\n",
".output_html .k { color: #008000; font-weight: bold } /* Keyword */\n",
".output_html .o { color: #666666 } /* Operator */\n",
".output_html .ch { color: #3D7B7B; font-style: italic } /* Comment.Hashbang */\n",
".output_html .cm { color: #3D7B7B; font-style: italic } /* Comment.Multiline */\n",
".output_html .cp { color: #9C6500 } /* Comment.Preproc */\n",
".output_html .cpf { color: #3D7B7B; font-style: italic } /* Comment.PreprocFile */\n",
".output_html .c1 { color: #3D7B7B; font-style: italic } /* Comment.Single */\n",
".output_html .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */\n",
".output_html .gd { color: #A00000 } /* Generic.Deleted */\n",
".output_html .ge { font-style: italic } /* Generic.Emph */\n",
".output_html .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */\n",
".output_html .gr { color: #E40000 } /* Generic.Error */\n",
".output_html .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
".output_html .gi { color: #008400 } /* Generic.Inserted */\n",
".output_html .go { color: #717171 } /* Generic.Output */\n",
".output_html .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
".output_html .gs { font-weight: bold } /* Generic.Strong */\n",
".output_html .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
".output_html .gt { color: #0044DD } /* Generic.Traceback */\n",
".output_html .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
".output_html .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
".output_html .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
".output_html .kp { color: #008000 } /* Keyword.Pseudo */\n",
".output_html .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
".output_html .kt { color: #B00040 } /* Keyword.Type */\n",
".output_html .m { color: #666666 } /* Literal.Number */\n",
".output_html .s { color: #BA2121 } /* Literal.String */\n",
".output_html .na { color: #687822 } /* Name.Attribute */\n",
".output_html .nb { color: #008000 } /* Name.Builtin */\n",
".output_html .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
".output_html .no { color: #880000 } /* Name.Constant */\n",
".output_html .nd { color: #AA22FF } /* Name.Decorator */\n",
".output_html .ni { color: #717171; font-weight: bold } /* Name.Entity */\n",
".output_html .ne { color: #CB3F38; font-weight: bold } /* Name.Exception */\n",
".output_html .nf { color: #0000FF } /* Name.Function */\n",
".output_html .nl { color: #767600 } /* Name.Label */\n",
".output_html .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
".output_html .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
".output_html .nv { color: #19177C } /* Name.Variable */\n",
".output_html .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
".output_html .w { color: #bbbbbb } /* Text.Whitespace */\n",
".output_html .mb { color: #666666 } /* Literal.Number.Bin */\n",
".output_html .mf { color: #666666 } /* Literal.Number.Float */\n",
".output_html .mh { color: #666666 } /* Literal.Number.Hex */\n",
".output_html .mi { color: #666666 } /* Literal.Number.Integer */\n",
".output_html .mo { color: #666666 } /* Literal.Number.Oct */\n",
".output_html .sa { color: #BA2121 } /* Literal.String.Affix */\n",
".output_html .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
".output_html .sc { color: #BA2121 } /* Literal.String.Char */\n",
".output_html .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
".output_html .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
".output_html .s2 { color: #BA2121 } /* Literal.String.Double */\n",
".output_html .se { color: #AA5D1F; font-weight: bold } /* Literal.String.Escape */\n",
".output_html .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
".output_html .si { color: #A45A77; font-weight: bold } /* Literal.String.Interpol */\n",
".output_html .sx { color: #008000 } /* Literal.String.Other */\n",
".output_html .sr { color: #A45A77 } /* Literal.String.Regex */\n",
".output_html .s1 { color: #BA2121 } /* Literal.String.Single */\n",
".output_html .ss { color: #19177C } /* Literal.String.Symbol */\n",
".output_html .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
".output_html .fm { color: #0000FF } /* Name.Function.Magic */\n",
".output_html .vc { color: #19177C } /* Name.Variable.Class */\n",
".output_html .vg { color: #19177C } /* Name.Variable.Global */\n",
".output_html .vi { color: #19177C } /* Name.Variable.Instance */\n",
".output_html .vm { color: #19177C } /* Name.Variable.Magic */\n",
".output_html .il { color: #666666 } /* Literal.Number.Integer.Long */</style><div class=\"highlight\"><pre><span></span><span class=\"n\">OptionalNum</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">1</span><span class=\"p\">))</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{OptionalNum}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{1}\\PY{p}{)}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"OptionalNum(Num(1))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"egraph.simplify(lst.index(2), 20)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We aren't sure of this first index of `Num(3)` in the list because `Num.var(\"x\")` could become equal to `Num(3)` at some point in the future.\n"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<style>pre { line-height: 125%; }\n",
"td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
".output_html .hll { background-color: #ffffcc }\n",
".output_html { background: #f8f8f8; }\n",
".output_html .c { color: #3D7B7B; font-style: italic } /* Comment */\n",
".output_html .err { border: 1px solid #FF0000 } /* Error */\n",
".output_html .k { color: #008000; font-weight: bold } /* Keyword */\n",
".output_html .o { color: #666666 } /* Operator */\n",
".output_html .ch { color: #3D7B7B; font-style: italic } /* Comment.Hashbang */\n",
".output_html .cm { color: #3D7B7B; font-style: italic } /* Comment.Multiline */\n",
".output_html .cp { color: #9C6500 } /* Comment.Preproc */\n",
".output_html .cpf { color: #3D7B7B; font-style: italic } /* Comment.PreprocFile */\n",
".output_html .c1 { color: #3D7B7B; font-style: italic } /* Comment.Single */\n",
".output_html .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */\n",
".output_html .gd { color: #A00000 } /* Generic.Deleted */\n",
".output_html .ge { font-style: italic } /* Generic.Emph */\n",
".output_html .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */\n",
".output_html .gr { color: #E40000 } /* Generic.Error */\n",
".output_html .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
".output_html .gi { color: #008400 } /* Generic.Inserted */\n",
".output_html .go { color: #717171 } /* Generic.Output */\n",
".output_html .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
".output_html .gs { font-weight: bold } /* Generic.Strong */\n",
".output_html .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
".output_html .gt { color: #0044DD } /* Generic.Traceback */\n",
".output_html .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
".output_html .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
".output_html .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
".output_html .kp { color: #008000 } /* Keyword.Pseudo */\n",
".output_html .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
".output_html .kt { color: #B00040 } /* Keyword.Type */\n",
".output_html .m { color: #666666 } /* Literal.Number */\n",
".output_html .s { color: #BA2121 } /* Literal.String */\n",
".output_html .na { color: #687822 } /* Name.Attribute */\n",
".output_html .nb { color: #008000 } /* Name.Builtin */\n",
".output_html .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
".output_html .no { color: #880000 } /* Name.Constant */\n",
".output_html .nd { color: #AA22FF } /* Name.Decorator */\n",
".output_html .ni { color: #717171; font-weight: bold } /* Name.Entity */\n",
".output_html .ne { color: #CB3F38; font-weight: bold } /* Name.Exception */\n",
".output_html .nf { color: #0000FF } /* Name.Function */\n",
".output_html .nl { color: #767600 } /* Name.Label */\n",
".output_html .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
".output_html .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
".output_html .nv { color: #19177C } /* Name.Variable */\n",
".output_html .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
".output_html .w { color: #bbbbbb } /* Text.Whitespace */\n",
".output_html .mb { color: #666666 } /* Literal.Number.Bin */\n",
".output_html .mf { color: #666666 } /* Literal.Number.Float */\n",
".output_html .mh { color: #666666 } /* Literal.Number.Hex */\n",
".output_html .mi { color: #666666 } /* Literal.Number.Integer */\n",
".output_html .mo { color: #666666 } /* Literal.Number.Oct */\n",
".output_html .sa { color: #BA2121 } /* Literal.String.Affix */\n",
".output_html .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
".output_html .sc { color: #BA2121 } /* Literal.String.Char */\n",
".output_html .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
".output_html .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
".output_html .s2 { color: #BA2121 } /* Literal.String.Double */\n",
".output_html .se { color: #AA5D1F; font-weight: bold } /* Literal.String.Escape */\n",
".output_html .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
".output_html .si { color: #A45A77; font-weight: bold } /* Literal.String.Interpol */\n",
".output_html .sx { color: #008000 } /* Literal.String.Other */\n",
".output_html .sr { color: #A45A77 } /* Literal.String.Regex */\n",
".output_html .s1 { color: #BA2121 } /* Literal.String.Single */\n",
".output_html .ss { color: #19177C } /* Literal.String.Symbol */\n",
".output_html .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
".output_html .fm { color: #0000FF } /* Name.Function.Magic */\n",
".output_html .vc { color: #19177C } /* Name.Variable.Class */\n",
".output_html .vg { color: #19177C } /* Name.Variable.Global */\n",
".output_html .vi { color: #19177C } /* Name.Variable.Instance */\n",
".output_html .vm { color: #19177C } /* Name.Variable.Magic */\n",
".output_html .il { color: #666666 } /* Literal.Number.Integer.Long */</style><div class=\"highlight\"><pre><span></span><span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"o\">.</span><span class=\"n\">var</span><span class=\"p\">(</span><span class=\"s2\">&quot;x&quot;</span><span class=\"p\">),</span> <span class=\"n\">cons</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">nil</span><span class=\"p\">()))</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">Num</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">))</span><span class=\"o\">.</span><span class=\"n\">incr</span><span class=\"p\">()</span><span class=\"o\">.</span><span class=\"n\">incr</span><span class=\"p\">()</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{o}{.}\\PY{n}{var}\\PY{p}{(}\\PY{l+s+s2}{\\PYZdq{}}\\PY{l+s+s2}{x}\\PY{l+s+s2}{\\PYZdq{}}\\PY{p}{)}\\PY{p}{,} \\PY{n}{cons}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{nil}\\PY{p}{(}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{o}{.}\\PY{n}{index}\\PY{p}{(}\\PY{n}{Num}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{)}\\PY{o}{.}\\PY{n}{incr}\\PY{p}{(}\\PY{p}{)}\\PY{o}{.}\\PY{n}{incr}\\PY{p}{(}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"cons(Num.var(\"x\"), cons(Num(3), nil())).index(Num(3)).incr().incr()"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"egraph.simplify(lst.index(3), 20)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"However, if we have a list of all exact integer, we know when we don't have an item:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<style>pre { line-height: 125%; }\n",
"td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }\n",
"td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
"span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }\n",
".output_html .hll { background-color: #ffffcc }\n",
".output_html { background: #f8f8f8; }\n",
".output_html .c { color: #3D7B7B; font-style: italic } /* Comment */\n",
".output_html .err { border: 1px solid #FF0000 } /* Error */\n",
".output_html .k { color: #008000; font-weight: bold } /* Keyword */\n",
".output_html .o { color: #666666 } /* Operator */\n",
".output_html .ch { color: #3D7B7B; font-style: italic } /* Comment.Hashbang */\n",
".output_html .cm { color: #3D7B7B; font-style: italic } /* Comment.Multiline */\n",
".output_html .cp { color: #9C6500 } /* Comment.Preproc */\n",
".output_html .cpf { color: #3D7B7B; font-style: italic } /* Comment.PreprocFile */\n",
".output_html .c1 { color: #3D7B7B; font-style: italic } /* Comment.Single */\n",
".output_html .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */\n",
".output_html .gd { color: #A00000 } /* Generic.Deleted */\n",
".output_html .ge { font-style: italic } /* Generic.Emph */\n",
".output_html .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */\n",
".output_html .gr { color: #E40000 } /* Generic.Error */\n",
".output_html .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
".output_html .gi { color: #008400 } /* Generic.Inserted */\n",
".output_html .go { color: #717171 } /* Generic.Output */\n",
".output_html .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
".output_html .gs { font-weight: bold } /* Generic.Strong */\n",
".output_html .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
".output_html .gt { color: #0044DD } /* Generic.Traceback */\n",
".output_html .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
".output_html .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
".output_html .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
".output_html .kp { color: #008000 } /* Keyword.Pseudo */\n",
".output_html .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
".output_html .kt { color: #B00040 } /* Keyword.Type */\n",
".output_html .m { color: #666666 } /* Literal.Number */\n",
".output_html .s { color: #BA2121 } /* Literal.String */\n",
".output_html .na { color: #687822 } /* Name.Attribute */\n",
".output_html .nb { color: #008000 } /* Name.Builtin */\n",
".output_html .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
".output_html .no { color: #880000 } /* Name.Constant */\n",
".output_html .nd { color: #AA22FF } /* Name.Decorator */\n",
".output_html .ni { color: #717171; font-weight: bold } /* Name.Entity */\n",
".output_html .ne { color: #CB3F38; font-weight: bold } /* Name.Exception */\n",
".output_html .nf { color: #0000FF } /* Name.Function */\n",
".output_html .nl { color: #767600 } /* Name.Label */\n",
".output_html .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
".output_html .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
".output_html .nv { color: #19177C } /* Name.Variable */\n",
".output_html .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
".output_html .w { color: #bbbbbb } /* Text.Whitespace */\n",
".output_html .mb { color: #666666 } /* Literal.Number.Bin */\n",
".output_html .mf { color: #666666 } /* Literal.Number.Float */\n",
".output_html .mh { color: #666666 } /* Literal.Number.Hex */\n",
".output_html .mi { color: #666666 } /* Literal.Number.Integer */\n",
".output_html .mo { color: #666666 } /* Literal.Number.Oct */\n",
".output_html .sa { color: #BA2121 } /* Literal.String.Affix */\n",
".output_html .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
".output_html .sc { color: #BA2121 } /* Literal.String.Char */\n",
".output_html .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
".output_html .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
".output_html .s2 { color: #BA2121 } /* Literal.String.Double */\n",
".output_html .se { color: #AA5D1F; font-weight: bold } /* Literal.String.Escape */\n",
".output_html .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
".output_html .si { color: #A45A77; font-weight: bold } /* Literal.String.Interpol */\n",
".output_html .sx { color: #008000 } /* Literal.String.Other */\n",
".output_html .sr { color: #A45A77 } /* Literal.String.Regex */\n",
".output_html .s1 { color: #BA2121 } /* Literal.String.Single */\n",
".output_html .ss { color: #19177C } /* Literal.String.Symbol */\n",
".output_html .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
".output_html .fm { color: #0000FF } /* Name.Function.Magic */\n",
".output_html .vc { color: #19177C } /* Name.Variable.Class */\n",
".output_html .vg { color: #19177C } /* Name.Variable.Global */\n",
".output_html .vi { color: #19177C } /* Name.Variable.Instance */\n",
".output_html .vm { color: #19177C } /* Name.Variable.Magic */\n",
".output_html .il { color: #666666 } /* Literal.Number.Integer.Long */</style><div class=\"highlight\"><pre><span></span><span class=\"n\">OptionalNum</span><span class=\"o\">.</span><span class=\"n\">none</span><span class=\"p\">()</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{OptionalNum}\\PY{o}{.}\\PY{n}{none}\\PY{p}{(}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"OptionalNum.none()"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"lst = convert((1, 2, 3), NumList)\n",
"\n",
"egraph.simplify(lst.index(5), 20)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.10.12"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment