Skip to content

Instantly share code, notes, and snippets.

@saulshanabrook

saulshanabrook/9.0.0-change.ipynb

Last active April 10, 2025 16:52
Show Gist options
  • Save saulshanabrook/4e3ae29b3382f0dcbbfbb1f8c0ba0d74 to your computer and use it in GitHub Desktop.
Save saulshanabrook/4e3ae29b3382f0dcbbfbb1f8c0ba0d74 to your computer and use it in GitHub Desktop.
Download ZIP
Display the source blob
Display the rendered blob
Raw
9.0.0-change.ipynb
{
"cells": [
{
"cell_type": "markdown",
"id": "84dfe599",
"metadata": {},
"source": [
"# 9.0.0 Changes\n"
]
},
{
"cell_type": "markdown",
"id": "f590b05b",
"metadata": {},
"source": [
"## Array API\n"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "6a5de151",
"metadata": {},
"outputs": [],
"source": [
"from __future__ import annotations\n",
"\n",
"from egglog import *\n",
"from egglog.exp.array_api import *\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "cfd3fd81",
"metadata": {},
"outputs": [],
"source": [
"@function(ruleset=array_api_ruleset, subsume=True)\n",
"def linalg_norm_v2(X: NDArrayLike, axis: TupleIntLike) -> NDArray:\n",
" X = cast(NDArray, X)\n",
" return NDArray(\n",
" X.shape.deselect(axis),\n",
" X.dtype,\n",
" lambda k: ndindex(X.shape.select(axis))\n",
" .foldl_value(lambda carry, i: carry + ((x := X.index(i + k)).conj() * x).real(), init=0.0)\n",
" .sqrt(),\n",
" )\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "188a393b",
"metadata": {},
"outputs": [],
"source": [
"X = constant(\"X\", NDArray)\n",
"assume_shape(X, (3, 2, 3, 4))\n",
"\n",
"res = linalg_norm_v2(X, (0, 1))"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "8a3dff44",
"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\">assume_shape</span><span class=\"p\">(</span><span class=\"n\">X</span><span class=\"p\">,</span> <span class=\"n\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">2</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">4</span><span class=\"p\">))))</span>\n",
"<span class=\"n\">linalg_norm_v2</span><span class=\"p\">(</span><span class=\"n\">X</span><span class=\"p\">,</span> <span class=\"n\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">0</span><span class=\"p\">),</span> <span class=\"n\">Int</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}{assume\\PYZus{}shape}\\PY{p}{(}\\PY{n}{X}\\PY{p}{,} \\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{2}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{4}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
"\\PY{n}{linalg\\PYZus{}norm\\PYZus{}v2}\\PY{p}{(}\\PY{n}{X}\\PY{p}{,} \\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{0}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{1}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"assume_shape(X, TupleInt.from_vec(Vec[Int](Int(3), Int(2), Int(3), Int(4))))\n",
"linalg_norm_v2(X, TupleInt.from_vec(Vec[Int](Int(0), Int(1))))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"res"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "cdf17a6d",
"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\">_NDArray_1</span> <span class=\"o\">=</span> <span class=\"n\">copy</span><span class=\"p\">(</span><span class=\"n\">X</span><span class=\"p\">)</span>\n",
"<span class=\"n\">assume_shape</span><span class=\"p\">(</span><span class=\"n\">_NDArray_1</span><span class=\"p\">,</span> <span class=\"n\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">2</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">4</span><span class=\"p\">))))</span>\n",
"<span class=\"n\">NDArray</span><span class=\"p\">(</span>\n",
" <span class=\"n\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">4</span><span class=\"p\">))),</span>\n",
" <span class=\"n\">X</span><span class=\"o\">.</span><span class=\"n\">dtype</span><span class=\"p\">,</span>\n",
" <span class=\"k\">lambda</span> <span class=\"n\">k</span><span class=\"p\">:</span> <span class=\"n\">ndindex</span><span class=\"p\">(</span><span class=\"n\">_NDArray_1</span><span class=\"o\">.</span><span class=\"n\">shape</span><span class=\"o\">.</span><span class=\"n\">select</span><span class=\"p\">(</span><span class=\"n\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">0</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">1</span><span class=\"p\">)))))</span>\n",
" <span class=\"o\">.</span><span class=\"n\">foldl_value</span><span class=\"p\">(</span><span class=\"k\">lambda</span> <span class=\"n\">carry</span><span class=\"p\">,</span> <span class=\"n\">i</span><span class=\"p\">:</span> <span class=\"n\">carry</span> <span class=\"o\">+</span> <span class=\"p\">(</span><span class=\"n\">_NDArray_1</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">i</span> <span class=\"o\">+</span> <span class=\"n\">k</span><span class=\"p\">)</span><span class=\"o\">.</span><span class=\"n\">conj</span><span class=\"p\">()</span> <span class=\"o\">*</span> <span class=\"n\">_NDArray_1</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">i</span> <span class=\"o\">+</span> <span class=\"n\">k</span><span class=\"p\">))</span><span class=\"o\">.</span><span class=\"n\">real</span><span class=\"p\">(),</span> <span class=\"n\">Value</span><span class=\"o\">.</span><span class=\"n\">float</span><span class=\"p\">(</span><span class=\"n\">Float</span><span class=\"p\">(</span><span class=\"mf\">0.0</span><span class=\"p\">)))</span>\n",
" <span class=\"o\">.</span><span class=\"n\">sqrt</span><span class=\"p\">(),</span>\n",
"<span class=\"p\">)</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{\\PYZus{}NDArray\\PYZus{}1} \\PY{o}{=} \\PY{n}{copy}\\PY{p}{(}\\PY{n}{X}\\PY{p}{)}\n",
"\\PY{n}{assume\\PYZus{}shape}\\PY{p}{(}\\PY{n}{\\PYZus{}NDArray\\PYZus{}1}\\PY{p}{,} \\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{2}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{4}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
"\\PY{n}{NDArray}\\PY{p}{(}\n",
" \\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{4}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{,}\n",
" \\PY{n}{X}\\PY{o}{.}\\PY{n}{dtype}\\PY{p}{,}\n",
" \\PY{k}{lambda} \\PY{n}{k}\\PY{p}{:} \\PY{n}{ndindex}\\PY{p}{(}\\PY{n}{\\PYZus{}NDArray\\PYZus{}1}\\PY{o}{.}\\PY{n}{shape}\\PY{o}{.}\\PY{n}{select}\\PY{p}{(}\\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{0}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{1}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
" \\PY{o}{.}\\PY{n}{foldl\\PYZus{}value}\\PY{p}{(}\\PY{k}{lambda} \\PY{n}{carry}\\PY{p}{,} \\PY{n}{i}\\PY{p}{:} \\PY{n}{carry} \\PY{o}{+} \\PY{p}{(}\\PY{n}{\\PYZus{}NDArray\\PYZus{}1}\\PY{o}{.}\\PY{n}{index}\\PY{p}{(}\\PY{n}{i} \\PY{o}{+} \\PY{n}{k}\\PY{p}{)}\\PY{o}{.}\\PY{n}{conj}\\PY{p}{(}\\PY{p}{)} \\PY{o}{*} \\PY{n}{\\PYZus{}NDArray\\PYZus{}1}\\PY{o}{.}\\PY{n}{index}\\PY{p}{(}\\PY{n}{i} \\PY{o}{+} \\PY{n}{k}\\PY{p}{)}\\PY{p}{)}\\PY{o}{.}\\PY{n}{real}\\PY{p}{(}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Value}\\PY{o}{.}\\PY{n}{float}\\PY{p}{(}\\PY{n}{Float}\\PY{p}{(}\\PY{l+m+mf}{0.0}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
" \\PY{o}{.}\\PY{n}{sqrt}\\PY{p}{(}\\PY{p}{)}\\PY{p}{,}\n",
"\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"_NDArray_1 = copy(X)\n",
"assume_shape(_NDArray_1, TupleInt.from_vec(Vec[Int](Int(3), Int(2), Int(3), Int(4))))\n",
"NDArray(\n",
" TupleInt.from_vec(Vec[Int](Int(3), Int(4))),\n",
" X.dtype,\n",
" lambda k: ndindex(_NDArray_1.shape.select(TupleInt.from_vec(Vec[Int](Int(0), Int(1)))))\n",
" .foldl_value(lambda carry, i: carry + (_NDArray_1.index(i + k).conj() * _NDArray_1.index(i + k)).real(), Value.float(Float(0.0)))\n",
" .sqrt(),\n",
")"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"egraph = EGraph(save_egglog_string=True)\n",
"\n",
"egraph.simplify(res, array_api_schedule)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "2fd78732",
"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\">TupleInt</span><span class=\"o\">.</span><span class=\"n\">from_vec</span><span class=\"p\">(</span><span class=\"n\">Vec</span><span class=\"p\">[</span><span class=\"n\">Int</span><span class=\"p\">](</span><span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">),</span> <span class=\"n\">Int</span><span class=\"p\">(</span><span class=\"mi\">4</span><span class=\"p\">)))</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{TupleInt}\\PY{o}{.}\\PY{n}{from\\PYZus{}vec}\\PY{p}{(}\\PY{n}{Vec}\\PY{p}{[}\\PY{n}{Int}\\PY{p}{]}\\PY{p}{(}\\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Int}\\PY{p}{(}\\PY{l+m+mi}{4}\\PY{p}{)}\\PY{p}{)}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"TupleInt.from_vec(Vec[Int](Int(3), Int(4)))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"shape = EGraph().simplify(res.shape, array_api_schedule)\n",
"shape"
]
},
{
"cell_type": "code",
"execution_count": 30,
"id": "72d7091b",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(ruleset array_api_ruleset)\n",
"(sort TupleInt)\n",
"(sort Int)\n",
"(constructor i-TupleInt__-Int_i (TupleInt Int) TupleInt)\n",
"(rewrite (i-TupleInt__-Int_i i _) i :subsume :ruleset array_api_ruleset)\n",
"(sort TupleTupleInt)\n",
"(constructor TupleTupleInt_single (TupleInt) TupleTupleInt)\n",
"(sort UnstableFn_TupleInt_Int (UnstableFn (Int ) TupleInt))\n",
"(constructor TupleTupleInt___init__ (Int UnstableFn_TupleInt_Int) TupleTupleInt)\n",
"(constructor Int___init__ (i64) Int)\n",
"(rewrite (TupleTupleInt_single i) (TupleTupleInt___init__ (Int___init__ 1) (unstable-fn \"i-TupleInt__-Int_i\" i)) :subsume :ruleset array_api_ruleset)\n",
"(sort Value)\n",
"(sort TupleValue)\n",
"(sort Boolean)\n",
"(constructor Value_if_ (Boolean Value Value) Value)\n",
"(constructor Int___lt__ (Int Int) Boolean)\n",
"(constructor TupleValue_length (TupleValue) Int)\n",
"(constructor TupleValue___getitem__ (TupleValue Int) Value)\n",
"(constructor Int___sub__ (Int Int) Int)\n",
"(constructor other-TupleValue_self-TupleValue_i-Int__Value_if___Int___lt___i__TupleValue_length_self____TupleValue___getitem___self_i___TupleValue___getitem___other__Int___sub___i__TupleValue_length_self____ (TupleValue TupleValue Int) Value)\n",
"(rewrite (other-TupleValue_self-TupleValue_i-Int__Value_if___Int___lt___i__TupleValue_length_self____TupleValue___getitem___self_i___TupleValue___getitem___other__Int___sub___i__TupleValue_length_self____ other self i) (Value_if_ (Int___lt__ i (TupleValue_length self)) (TupleValue___getitem__ self i) (TupleValue___getitem__ other (Int___sub__ i (TupleValue_length self)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleValue___add__ (TupleValue TupleValue) TupleValue)\n",
"(sort UnstableFn_Value_Int (UnstableFn (Int ) Value))\n",
"(constructor TupleValue___init__ (Int UnstableFn_Value_Int) TupleValue)\n",
"(constructor Int___add__ (Int Int) Int)\n",
"(rewrite (TupleValue___add__ self other) (TupleValue___init__ (Int___add__ (TupleValue_length self) (TupleValue_length other)) (unstable-fn \"other-TupleValue_self-TupleValue_i-Int__Value_if___Int___lt___i__TupleValue_length_self____TupleValue___getitem___self_i___TupleValue___getitem___other__Int___sub___i__TupleValue_length_self____\" other self)) :ruleset array_api_ruleset)\n",
"(constructor Boolean___or__ (Boolean Boolean) Boolean)\n",
"(constructor Value___eq__ (Value Value) Boolean)\n",
"(constructor value-Value_acc-Boolean_j-Value__Boolean___or___acc__Value___eq___value_j__ (Value Boolean Value) Boolean)\n",
"(rewrite (value-Value_acc-Boolean_j-Value__Boolean___or___acc__Value___eq___value_j__ value acc j) (Boolean___or__ acc (Value___eq__ value j)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleValue_contains (TupleValue Value) Boolean)\n",
"(sort UnstableFn_Boolean_Boolean_Value (UnstableFn (Boolean Value) Boolean))\n",
"(constructor TupleValue_foldl_boolean (TupleValue UnstableFn_Boolean_Boolean_Value Boolean) Boolean)\n",
"(constructor Boolean___init__ (bool) Boolean)\n",
"(rewrite (TupleValue_contains self value) (TupleValue_foldl_boolean self (unstable-fn \"value-Value_acc-Boolean_j-Value__Boolean___or___acc__Value___eq___value_j__\" value) (Boolean___init__ false)) :ruleset array_api_ruleset)\n",
"(constructor Value_int (Int) Value)\n",
"(constructor TupleInt___getitem__ (TupleInt Int) Int)\n",
"(constructor ti-TupleInt_i-Int__Value_int__TupleInt___getitem___ti_i__ (TupleInt Int) Value)\n",
"(rewrite (ti-TupleInt_i-Int__Value_int__TupleInt___getitem___ti_i__ ti i) (Value_int (TupleInt___getitem__ ti i)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleValue_from_tuple_int (TupleInt) TupleValue)\n",
"(constructor TupleInt_length (TupleInt) Int)\n",
"(rewrite (TupleValue_from_tuple_int ti) (TupleValue___init__ (TupleInt_length ti) (unstable-fn \"ti-TupleInt_i-Int__Value_int__TupleInt___getitem___ti_i__\" ti)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_if_ (Boolean TupleInt TupleInt) TupleInt)\n",
"(constructor TupleTupleInt_length (TupleTupleInt) Int)\n",
"(constructor TupleTupleInt___getitem__ (TupleTupleInt Int) TupleInt)\n",
"(constructor other-TupleTupleInt_self-TupleTupleInt_i-Int__TupleInt_if___Int___lt___i__TupleTupleInt_length_self____TupleTupleInt___getitem___self_i___TupleTupleInt___getitem___other__Int___sub___i__TupleTupleInt_length_self____ (TupleTupleInt TupleTupleInt Int) TupleInt)\n",
"(rewrite (other-TupleTupleInt_self-TupleTupleInt_i-Int__TupleInt_if___Int___lt___i__TupleTupleInt_length_self____TupleTupleInt___getitem___self_i___TupleTupleInt___getitem___other__Int___sub___i__TupleTupleInt_length_self____ other self i) (TupleInt_if_ (Int___lt__ i (TupleTupleInt_length self)) (TupleTupleInt___getitem__ self i) (TupleTupleInt___getitem__ other (Int___sub__ i (TupleTupleInt_length self)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt___add__ (TupleTupleInt TupleTupleInt) TupleTupleInt)\n",
"(rewrite (TupleTupleInt___add__ self other) (TupleTupleInt___init__ (Int___add__ (TupleTupleInt_length self) (TupleTupleInt_length other)) (unstable-fn \"other-TupleTupleInt_self-TupleTupleInt_i-Int__TupleInt_if___Int___lt___i__TupleTupleInt_length_self____TupleTupleInt___getitem___self_i___TupleTupleInt___getitem___other__Int___sub___i__TupleTupleInt_length_self____\" other self)) :ruleset array_api_ruleset)\n",
"(constructor n-Int_self-TupleTupleInt_i-Int__TupleTupleInt___getitem___self__Int___add___i_n__ (Int TupleTupleInt Int) TupleInt)\n",
"(rewrite (n-Int_self-TupleTupleInt_i-Int__TupleTupleInt___getitem___self__Int___add___i_n__ n self i) (TupleTupleInt___getitem__ self (Int___add__ i n)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt_drop (TupleTupleInt Int) TupleTupleInt)\n",
"(rewrite (TupleTupleInt_drop self n) (TupleTupleInt___init__ (Int___sub__ (TupleTupleInt_length self) n) (unstable-fn \"n-Int_self-TupleTupleInt_i-Int__TupleTupleInt___getitem___self__Int___add___i_n__\" n self)) :ruleset array_api_ruleset)\n",
"(sort UnstableFn_Int_TupleInt (UnstableFn (TupleInt ) Int))\n",
"(constructor f-UnstableFn_Int_TupleInt_self-TupleTupleInt_i-Int__unstable-app_f__TupleTupleInt___getitem___self_i__ (UnstableFn_Int_TupleInt TupleTupleInt Int) Int)\n",
"(rewrite (f-UnstableFn_Int_TupleInt_self-TupleTupleInt_i-Int__unstable-app_f__TupleTupleInt___getitem___self_i__ f self i) (unstable-app f (TupleTupleInt___getitem__ self i)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt_map_int (TupleTupleInt UnstableFn_Int_TupleInt) TupleInt)\n",
"(sort UnstableFn_Int_Int (UnstableFn (Int ) Int))\n",
"(constructor TupleInt___init__ (Int UnstableFn_Int_Int) TupleInt)\n",
"(rewrite (TupleTupleInt_map_int self f) (TupleInt___init__ (TupleTupleInt_length self) (unstable-fn \"f-UnstableFn_Int_TupleInt_self-TupleTupleInt_i-Int__unstable-app_f__TupleTupleInt___getitem___self_i__\" f self)) :ruleset array_api_ruleset)\n",
"(constructor x-TupleInt__TupleInt_length_x_ (TupleInt) Int)\n",
"(rewrite (x-TupleInt__TupleInt_length_x_ x) (TupleInt_length x) :subsume :ruleset array_api_ruleset)\n",
"(constructor Int___mod__ (Int Int) Int)\n",
"(constructor Int___floordiv__ (Int Int) Int)\n",
"(constructor TupleInt_product (TupleInt) Int)\n",
"(constructor i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j____ (Int TupleTupleInt Int) Int)\n",
"(rewrite (i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j____ i self j) (TupleInt___getitem__ (TupleTupleInt___getitem__ self j) (Int___mod__ (Int___floordiv__ i (TupleInt_product (TupleTupleInt_map_int (TupleTupleInt_drop self (Int___add__ j (Int___init__ 1))) (unstable-fn \"x-TupleInt__TupleInt_length_x_\")))) (TupleInt_length (TupleTupleInt___getitem__ self j)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor self-TupleTupleInt_i-Int__TupleInt___init____TupleTupleInt_length_self___unstable-fn__i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j______i_self__ (TupleTupleInt Int) TupleInt)\n",
"(rewrite (self-TupleTupleInt_i-Int__TupleInt___init____TupleTupleInt_length_self___unstable-fn__i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j______i_self__ self i) (TupleInt___init__ (TupleTupleInt_length self) (unstable-fn \"i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j____\" i self)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt_product (TupleTupleInt) TupleTupleInt)\n",
"(rewrite (TupleTupleInt_product self) (TupleTupleInt___init__ (TupleInt_product (TupleTupleInt_map_int self (unstable-fn \"x-TupleInt__TupleInt_length_x_\"))) (unstable-fn \"self-TupleTupleInt_i-Int__TupleInt___init____TupleTupleInt_length_self___unstable-fn__i-Int_self-TupleTupleInt_j-Int__TupleInt___getitem____TupleTupleInt___getitem___self_j___Int___mod____Int___floordiv___i__TupleInt_product__TupleTupleInt_map_int__TupleTupleInt_drop_self__Int___add___j__Int___init___1_____unstable-fn__x-TupleInt__TupleInt_length_x________TupleInt_length__TupleTupleInt___getitem___self_j______i_self__\" self)) :subsume :ruleset array_api_ruleset)\n",
"(constructor i-Int__-Int_i (Int Int) Int)\n",
"(rewrite (i-Int__-Int_i i _) i :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_single (Int) TupleInt)\n",
"(rewrite (TupleInt_single i) (TupleInt___init__ (Int___init__ 1) (unstable-fn \"i-Int__-Int_i\" i)) :ruleset array_api_ruleset)\n",
"(constructor i-Int_i (Int) Int)\n",
"(rewrite (i-Int_i i) i :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_range (Int) TupleInt)\n",
"(rewrite (TupleInt_range stop) (TupleInt___init__ stop (unstable-fn \"i-Int_i\")) :subsume :ruleset array_api_ruleset)\n",
"(constructor Int_if_ (Boolean Int Int) Int)\n",
"(constructor other-TupleInt_self-TupleInt_i-Int__Int_if___Int___lt___i__TupleInt_length_self____TupleInt___getitem___self_i___TupleInt___getitem___other__Int___sub___i__TupleInt_length_self____ (TupleInt TupleInt Int) Int)\n",
"(rewrite (other-TupleInt_self-TupleInt_i-Int__Int_if___Int___lt___i__TupleInt_length_self____TupleInt___getitem___self_i___TupleInt___getitem___other__Int___sub___i__TupleInt_length_self____ other self i) (Int_if_ (Int___lt__ i (TupleInt_length self)) (TupleInt___getitem__ self i) (TupleInt___getitem__ other (Int___sub__ i (TupleInt_length self)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt___add__ (TupleInt TupleInt) TupleInt)\n",
"(rewrite (TupleInt___add__ self other) (TupleInt___init__ (Int___add__ (TupleInt_length self) (TupleInt_length other)) (unstable-fn \"other-TupleInt_self-TupleInt_i-Int__Int_if___Int___lt___i__TupleInt_length_self____TupleInt___getitem___self_i___TupleInt___getitem___other__Int___sub___i__TupleInt_length_self____\" other self)) :ruleset array_api_ruleset)\n",
"(constructor Int___eq__ (Int Int) Boolean)\n",
"(constructor i-Int_acc-Boolean_j-Int__Boolean___or___acc__Int___eq___i_j__ (Int Boolean Int) Boolean)\n",
"(rewrite (i-Int_acc-Boolean_j-Int__Boolean___or___acc__Int___eq___i_j__ i acc j) (Boolean___or__ acc (Int___eq__ i j)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_contains (TupleInt Int) Boolean)\n",
"(sort UnstableFn_Boolean_Boolean_Int (UnstableFn (Boolean Int) Boolean))\n",
"(constructor TupleInt_foldl_boolean (TupleInt UnstableFn_Boolean_Boolean_Int Boolean) Boolean)\n",
"(rewrite (TupleInt_contains self i) (TupleInt_foldl_boolean self (unstable-fn \"i-Int_acc-Boolean_j-Int__Boolean___or___acc__Int___eq___i_j__\" i) (Boolean___init__ false)) :subsume :ruleset array_api_ruleset)\n",
"(sort UnstableFn_Boolean_Int (UnstableFn (Int ) Boolean))\n",
"(constructor TupleInt_append (TupleInt Int) TupleInt)\n",
"(constructor f-UnstableFn_Boolean_Int_acc-TupleInt_v-Int__TupleInt_if___unstable-app_f_v___TupleInt_append_acc_v__acc_ (UnstableFn_Boolean_Int TupleInt Int) TupleInt)\n",
"(rewrite (f-UnstableFn_Boolean_Int_acc-TupleInt_v-Int__TupleInt_if___unstable-app_f_v___TupleInt_append_acc_v__acc_ f acc v) (TupleInt_if_ (unstable-app f v) (TupleInt_append acc v) acc) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_filter (TupleInt UnstableFn_Boolean_Int) TupleInt)\n",
"(sort UnstableFn_TupleInt_TupleInt_Int (UnstableFn (TupleInt Int) TupleInt))\n",
"(constructor TupleInt_foldl_tuple_int (TupleInt UnstableFn_TupleInt_TupleInt_Int TupleInt) TupleInt)\n",
"(constructor TupleInt_EMPTY () TupleInt)\n",
"(rewrite (TupleInt_filter self f) (TupleInt_foldl_tuple_int self (unstable-fn \"f-UnstableFn_Boolean_Int_acc-TupleInt_v-Int__TupleInt_if___unstable-app_f_v___TupleInt_append_acc_v__acc_\" f) (TupleInt_EMPTY )) :subsume :ruleset array_api_ruleset)\n",
"(constructor f-UnstableFn_Int_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__ (UnstableFn_Int_Int TupleInt Int) Int)\n",
"(rewrite (f-UnstableFn_Int_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__ f self i) (unstable-app f (TupleInt___getitem__ self i)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_map (TupleInt UnstableFn_Int_Int) TupleInt)\n",
"(rewrite (TupleInt_map self f) (TupleInt___init__ (TupleInt_length self) (unstable-fn \"f-UnstableFn_Int_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__\" f self)) :subsume :ruleset array_api_ruleset)\n",
"(constructor n-Int_self-TupleInt_i-Int__TupleInt___getitem___self__Int___add___i_n__ (Int TupleInt Int) Int)\n",
"(rewrite (n-Int_self-TupleInt_i-Int__TupleInt___getitem___self__Int___add___i_n__ n self i) (TupleInt___getitem__ self (Int___add__ i n)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_drop (TupleInt Int) TupleInt)\n",
"(rewrite (TupleInt_drop self n) (TupleInt___init__ (Int___sub__ (TupleInt_length self) n) (unstable-fn \"n-Int_self-TupleInt_i-Int__TupleInt___getitem___self__Int___add___i_n__\" n self)) :ruleset array_api_ruleset)\n",
"(constructor Int___mul__ (Int Int) Int)\n",
"(constructor acc-Int_i-Int__Int___mul___acc_i_ (Int Int) Int)\n",
"(rewrite (acc-Int_i-Int__Int___mul___acc_i_ acc i) (Int___mul__ acc i) :subsume :ruleset array_api_ruleset)\n",
"(sort UnstableFn_Int_Int_Int (UnstableFn (Int Int) Int))\n",
"(constructor TupleInt_foldl (TupleInt UnstableFn_Int_Int_Int Int) Int)\n",
"(rewrite (TupleInt_product self) (TupleInt_foldl self (unstable-fn \"acc-Int_i-Int__Int___mul___acc_i_\") (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(constructor f-UnstableFn_TupleInt_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__ (UnstableFn_TupleInt_Int TupleInt Int) TupleInt)\n",
"(rewrite (f-UnstableFn_TupleInt_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__ f self i) (unstable-app f (TupleInt___getitem__ self i)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_map_tuple_int (TupleInt UnstableFn_TupleInt_Int) TupleTupleInt)\n",
"(rewrite (TupleInt_map_tuple_int self f) (TupleTupleInt___init__ (TupleInt_length self) (unstable-fn \"f-UnstableFn_TupleInt_Int_self-TupleInt_i-Int__unstable-app_f__TupleInt___getitem___self_i__\" f self)) :ruleset array_api_ruleset)\n",
"(constructor self-TupleInt_i-Int__TupleInt___getitem___self_i_ (TupleInt Int) Int)\n",
"(rewrite (self-TupleInt_i-Int__TupleInt___getitem___self_i_ self i) (TupleInt___getitem__ self i) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_select (TupleInt TupleInt) TupleInt)\n",
"(rewrite (TupleInt_select self indices) (TupleInt_map indices (unstable-fn \"self-TupleInt_i-Int__TupleInt___getitem___self_i_\" self)) :ruleset array_api_ruleset)\n",
"(constructor Boolean___invert__ (Boolean) Boolean)\n",
"(constructor indices-TupleInt_i-Int__Boolean___invert____TupleInt_contains_indices_i__ (TupleInt Int) Boolean)\n",
"(rewrite (indices-TupleInt_i-Int__Boolean___invert____TupleInt_contains_indices_i__ indices i) (Boolean___invert__ (TupleInt_contains indices i)) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleInt_deselect (TupleInt TupleInt) TupleInt)\n",
"(rewrite (TupleInt_deselect self indices) (TupleInt_map (TupleInt_filter (TupleInt_range (TupleInt_length self)) (unstable-fn \"indices-TupleInt_i-Int__Boolean___invert____TupleInt_contains_indices_i__\" indices)) (unstable-fn \"self-TupleInt_i-Int__TupleInt___getitem___self_i_\" self)) :ruleset array_api_ruleset)\n",
"(constructor value-Value__-TupleInt_value (Value TupleInt) Value)\n",
"(rewrite (value-Value__-TupleInt_value value _) value :subsume :ruleset array_api_ruleset)\n",
"(sort NDArray)\n",
"(constructor NDArray_scalar (Value) NDArray)\n",
"(sort DType)\n",
"(sort UnstableFn_Value_TupleInt (UnstableFn (TupleInt ) Value))\n",
"(constructor NDArray___init__ (TupleInt DType UnstableFn_Value_TupleInt) NDArray)\n",
"(constructor Value_dtype (Value) DType)\n",
"(rewrite (NDArray_scalar value) (NDArray___init__ (TupleInt_EMPTY ) (Value_dtype value) (unstable-fn \"value-Value__-TupleInt_value\" value)) :ruleset array_api_ruleset)\n",
"(sort TupleNDArray)\n",
"(constructor NDArray_if_ (Boolean NDArray NDArray) NDArray)\n",
"(constructor TupleNDArray_length (TupleNDArray) Int)\n",
"(constructor TupleNDArray___getitem__ (TupleNDArray Int) NDArray)\n",
"(constructor other-TupleNDArray_self-TupleNDArray_i-Int__NDArray_if___Int___lt___i__TupleNDArray_length_self____TupleNDArray___getitem___self_i___TupleNDArray___getitem___other__Int___sub___i__TupleNDArray_length_self____ (TupleNDArray TupleNDArray Int) NDArray)\n",
"(rewrite (other-TupleNDArray_self-TupleNDArray_i-Int__NDArray_if___Int___lt___i__TupleNDArray_length_self____TupleNDArray___getitem___self_i___TupleNDArray___getitem___other__Int___sub___i__TupleNDArray_length_self____ other self i) (NDArray_if_ (Int___lt__ i (TupleNDArray_length self)) (TupleNDArray___getitem__ self i) (TupleNDArray___getitem__ other (Int___sub__ i (TupleNDArray_length self)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor TupleNDArray___add__ (TupleNDArray TupleNDArray) TupleNDArray)\n",
"(sort UnstableFn_NDArray_Int (UnstableFn (Int ) NDArray))\n",
"(constructor TupleNDArray___init__ (Int UnstableFn_NDArray_Int) TupleNDArray)\n",
"(rewrite (TupleNDArray___add__ self other) (TupleNDArray___init__ (Int___add__ (TupleNDArray_length self) (TupleNDArray_length other)) (unstable-fn \"other-TupleNDArray_self-TupleNDArray_i-Int__NDArray_if___Int___lt___i__TupleNDArray_length_self____TupleNDArray___getitem___self_i___TupleNDArray___getitem___other__Int___sub___i__TupleNDArray_length_self____\" other self)) :ruleset array_api_ruleset)\n",
"(constructor ndindex (TupleInt) TupleTupleInt)\n",
"(rewrite (ndindex shape) (TupleTupleInt_product (TupleInt_map_tuple_int shape (unstable-fn \"TupleInt_range\"))) :ruleset array_api_ruleset)\n",
"(constructor Value___add__ (Value Value) Value)\n",
"(constructor Value_real (Value) Value)\n",
"(constructor Value___mul__ (Value Value) Value)\n",
"(constructor Value_conj (Value) Value)\n",
"(constructor NDArray_index (NDArray TupleInt) Value)\n",
"(constructor X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_____ (NDArray TupleInt Value TupleInt) Value)\n",
"(rewrite (X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_____ X k carry i) (Value___add__ carry (Value_real (Value___mul__ (Value_conj (NDArray_index X (TupleInt___add__ i k))) (NDArray_index X (TupleInt___add__ i k))))) :subsume :ruleset array_api_ruleset)\n",
"(constructor Value_sqrt (Value) Value)\n",
"(sort UnstableFn_Value_Value_TupleInt (UnstableFn (Value TupleInt) Value))\n",
"(constructor TupleTupleInt_foldl_value (TupleTupleInt UnstableFn_Value_Value_TupleInt Value) Value)\n",
"(constructor NDArray_shape (NDArray) TupleInt)\n",
"(sort Float)\n",
"(constructor Value_float (Float) Value)\n",
"(constructor Float___init__ (f64) Float :cost 3)\n",
"(constructor X-NDArray_axis-TupleInt_k-TupleInt__Value_sqrt__TupleTupleInt_foldl_value__ndindex__TupleInt_select__NDArray_shape_X__axis____unstable-fn__X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_______X_k___Value_float__Float___init___0_0____ (NDArray TupleInt TupleInt) Value)\n",
"(rewrite (X-NDArray_axis-TupleInt_k-TupleInt__Value_sqrt__TupleTupleInt_foldl_value__ndindex__TupleInt_select__NDArray_shape_X__axis____unstable-fn__X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_______X_k___Value_float__Float___init___0_0____ X axis k) (Value_sqrt (TupleTupleInt_foldl_value (ndindex (TupleInt_select (NDArray_shape X) axis)) (unstable-fn \"X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_____\" X k) (Value_float (Float___init__ 0.0)))) :subsume :ruleset array_api_ruleset)\n",
"(constructor linalg_norm_v2 (NDArray TupleInt) NDArray)\n",
"(constructor NDArray_dtype (NDArray) DType)\n",
"(rewrite (linalg_norm_v2 X axis) (NDArray___init__ (TupleInt_deselect (NDArray_shape X) axis) (NDArray_dtype X) (unstable-fn \"X-NDArray_axis-TupleInt_k-TupleInt__Value_sqrt__TupleTupleInt_foldl_value__ndindex__TupleInt_select__NDArray_shape_X__axis____unstable-fn__X-NDArray_k-TupleInt_carry-Value_i-TupleInt__Value___add___carry__Value_real__Value___mul____Value_conj__NDArray_index_X__TupleInt___add___i_k_____NDArray_index_X__TupleInt___add___i_k_______X_k___Value_float__Float___init___0_0____\" X axis)) :subsume :ruleset array_api_ruleset)\n",
"(constructor NDArray_size (NDArray) Int)\n",
"(rewrite (NDArray_size x) (TupleInt_foldl (NDArray_shape x) (unstable-fn \"Int___mul__\") (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(constructor unique_values (NDArray) NDArray)\n",
"(constructor NDArray_vector (TupleValue) NDArray)\n",
"(constructor possible_values (Value) TupleValue)\n",
"(constructor ALL_INDICES () TupleInt)\n",
"(rewrite (unique_values a) (NDArray_vector (possible_values (NDArray_index a (ALL_INDICES )))) :ruleset array_api_ruleset)\n",
"(constructor Value_isfinite (Value) Boolean)\n",
"(rewrite (Value_isfinite (Value_int i)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(constructor Value_bool (Boolean) Value)\n",
"(rewrite (Value_isfinite (Value_bool b)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (Value_isfinite (Value_float (Float___init__ f))) (Boolean___init__ true) :when ((!= f NaN)) :ruleset array_api_ruleset)\n",
"(constructor isfinite (NDArray) NDArray)\n",
"(sort OptionalIntOrTuple)\n",
"(constructor sum (NDArray OptionalIntOrTuple) NDArray)\n",
"(constructor OptionalIntOrTuple_none () OptionalIntOrTuple)\n",
"(rewrite (isfinite (sum arr (OptionalIntOrTuple_none ))) (NDArray_scalar (Value_bool (Value_isfinite (NDArray_index arr (ALL_INDICES ))))) :ruleset array_api_ruleset)\n",
"(constructor assume_value_one_of (NDArray TupleValue) NDArray)\n",
"(rewrite (NDArray_shape (assume_value_one_of x vs)) (NDArray_shape x) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (assume_value_one_of x vs)) (NDArray_dtype x) :ruleset array_api_ruleset)\n",
"(rule ((= v (NDArray_index (assume_value_one_of x vs) idx)))\n",
" ((union v (NDArray_index x idx))\n",
" (union (possible_values v) vs))\n",
" :ruleset array_api_ruleset )\n",
"(constructor assume_isfinite (NDArray) NDArray)\n",
"(rewrite (NDArray_shape (assume_isfinite x)) (NDArray_shape x) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (assume_isfinite x)) (NDArray_dtype x) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (assume_isfinite x) ti) (NDArray_index x ti) :ruleset array_api_ruleset)\n",
"(rewrite (Value_isfinite (NDArray_index (assume_isfinite x) ti)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(constructor assume_shape (NDArray TupleInt) NDArray)\n",
"(rewrite (NDArray_shape (assume_shape x shape)) shape :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (assume_shape x shape)) (NDArray_dtype x) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (assume_shape x shape) idx) (NDArray_index x idx) :ruleset array_api_ruleset)\n",
"(constructor assume_dtype (NDArray DType) NDArray)\n",
"(rewrite (NDArray_dtype (assume_dtype x dtype)) dtype :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_shape (assume_dtype x dtype)) (NDArray_shape x) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (assume_dtype x dtype) idx) (NDArray_index x idx) :ruleset array_api_ruleset)\n",
"(sort IndexKey)\n",
"(constructor NDArray___getitem__ (NDArray IndexKey) NDArray)\n",
"(constructor IndexKey_int (Int) IndexKey)\n",
"(rewrite (NDArray___getitem__ x (IndexKey_int i)) (NDArray_scalar (NDArray_index x (TupleInt_single i))) :ruleset array_api_ruleset)\n",
"(sort OptionalBool)\n",
"(constructor reshape (NDArray TupleInt OptionalBool) NDArray)\n",
"(rule ((= __a (reshape x shape copy)))\n",
" ((NDArray_shape x)\n",
" (TupleInt_length (NDArray_shape x)))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((reshape x shape copy))\n",
" ((TupleInt_length shape)\n",
" (TupleInt___getitem__ shape (Int___init__ 0)))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (reshape x shape copy) x :when ((= (TupleInt_length (NDArray_shape x)) (Int___init__ 1)) (= (TupleInt_length shape) (Int___init__ 1)) (= (TupleInt___getitem__ shape (Int___init__ 0)) (Int___init__ -1))) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_shape (NDArray_vector vs)) (TupleInt_single (TupleValue_length vs)) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (NDArray_vector vs)) (Value_dtype (TupleValue___getitem__ vs (Int___init__ 0))) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (NDArray_vector vs) ti) (TupleValue___getitem__ vs (TupleInt___getitem__ ti (Int___init__ 0))) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_shape (NDArray_scalar v)) (TupleInt_EMPTY ) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (NDArray_scalar v)) (Value_dtype v) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (NDArray_scalar v) (TupleInt_EMPTY )) v :ruleset array_api_ruleset)\n",
"(constructor any (NDArray) NDArray)\n",
"(constructor Value_to_truthy_value (Value) Value)\n",
"(rewrite (any x) (NDArray_scalar (Value_bool (TupleValue_contains (possible_values (Value_to_truthy_value (NDArray_index x (ALL_INDICES )))) (Value_bool (Boolean___init__ true))))) :ruleset array_api_ruleset)\n",
"(constructor NDArray___lt__ (NDArray NDArray) NDArray)\n",
"(constructor Value___lt__ (Value Value) Value)\n",
"(constructor broadcast_index (TupleInt TupleInt TupleInt) TupleInt)\n",
"(constructor broadcast_shapes (TupleInt TupleInt) TupleInt)\n",
"(rewrite (NDArray_index (NDArray___lt__ x y) idx) (Value___lt__ (NDArray_index x (broadcast_index (NDArray_shape x) (broadcast_shapes (NDArray_shape x) (NDArray_shape y)) idx)) (NDArray_index y (broadcast_index (NDArray_shape y) (broadcast_shapes (NDArray_shape x) (NDArray_shape y)) idx))) :ruleset array_api_ruleset)\n",
"(constructor NDArray___truediv__ (NDArray NDArray) NDArray)\n",
"(constructor Value___truediv__ (Value Value) Value)\n",
"(rewrite (NDArray_index (NDArray___truediv__ x y) idx) (Value___truediv__ (NDArray_index x (broadcast_index (NDArray_shape x) (broadcast_shapes (NDArray_shape x) (NDArray_shape y)) idx)) (NDArray_index y (broadcast_index (NDArray_shape y) (broadcast_shapes (NDArray_shape x) (NDArray_shape y)) idx))) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (NDArray_scalar v) idx) v :ruleset array_api_ruleset)\n",
"(constructor astype (NDArray DType) NDArray)\n",
"(constructor Value_astype (Value DType) Value)\n",
"(rewrite (NDArray_index (astype x dtype) idx) (Value_astype (NDArray_index x idx) dtype) :ruleset array_api_ruleset)\n",
"(relation greater_zero (Value))\n",
"(constructor unique_counts (NDArray) TupleNDArray)\n",
"(rule ((= v (NDArray_index (TupleNDArray___getitem__ (unique_counts x) (Int___init__ 1)) idx)))\n",
" ((greater_zero v))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((greater_zero v)\n",
" (= v1 (Value_astype v dtype)))\n",
" ((greater_zero v1))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= v (Value_float (Float___init__ f)))\n",
" (> f 0.0))\n",
" ((greater_zero v))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= v (Value_int (Int___init__ i)))\n",
" (> i 0))\n",
" ((greater_zero v))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((greater_zero v)\n",
" (greater_zero v1)\n",
" (= v2 (Value___truediv__ v v1)))\n",
" ((greater_zero v2))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((greater_zero v)\n",
" (= v1 (Value___lt__ v (Value_int (Int___init__ 0)))))\n",
" ((union v1 (Value_bool (Boolean___init__ false))))\n",
" :ruleset array_api_ruleset )\n",
"(constructor TupleValue_append (TupleValue Value) TupleValue)\n",
"(constructor TupleValue_EMPTY () TupleValue)\n",
"(rewrite (possible_values (Value_bool b)) (TupleValue_append (TupleValue_EMPTY ) (Value_bool b)) :ruleset array_api_ruleset)\n",
"(rule ((= v1 (Value_astype v dtype))\n",
" (greater_zero v))\n",
" ((greater_zero v1))\n",
" :ruleset array_api_ruleset )\n",
"(constructor svd (NDArray Boolean) TupleNDArray)\n",
"(rewrite (svd x full_matrices) (TupleNDArray___init__ (Int___init__ 3) (unstable-fn \"TupleNDArray___getitem__\" (svd x full_matrices))) :ruleset array_api_ruleset)\n",
"(constructor unique_inverse (NDArray) TupleNDArray)\n",
"(rewrite (unique_inverse x) (TupleNDArray___init__ (Int___init__ 2) (unstable-fn \"TupleNDArray___getitem__\" (unique_inverse x))) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray___getitem__ (unique_inverse x) (Int___init__ 0)) (unique_values x) :ruleset array_api_ruleset)\n",
"(constructor ndarray-abs (NDArray) NDArray)\n",
"(constructor Float_abs (Float) Float)\n",
"(rewrite (ndarray-abs (NDArray_scalar (Value_float f))) (NDArray_scalar (Value_float (Float_abs f))) :ruleset array_api_ruleset)\n",
"(rewrite (unique_counts x) (TupleNDArray___init__ (Int___init__ 2) (unstable-fn \"TupleNDArray___getitem__\" (unique_counts x))) :ruleset array_api_ruleset)\n",
"(rewrite (sum (TupleNDArray___getitem__ (unique_counts x) (Int___init__ 1)) (OptionalIntOrTuple_none )) (NDArray_scalar (Value_int (NDArray_size x))) :ruleset array_api_ruleset)\n",
"(rewrite (sum (astype (TupleNDArray___getitem__ (unique_counts x) (Int___init__ 1)) dtype) (OptionalIntOrTuple_none )) (astype (NDArray_scalar (Value_int (NDArray_size x))) dtype) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (astype x dtype)) dtype :ruleset array_api_ruleset)\n",
"(constructor DType_float64 () DType)\n",
"(rewrite (astype (NDArray_scalar (Value_int (Int___init__ i))) (DType_float64 )) (NDArray_scalar (Value_float (Float___init__ (to-f64 i)))) :ruleset array_api_ruleset)\n",
"(sort OptionalInt)\n",
"(constructor concat (TupleNDArray OptionalInt) NDArray)\n",
"(constructor TupleNDArray_append (TupleNDArray NDArray) TupleNDArray)\n",
"(constructor TupleNDArray_EMPTY () TupleNDArray)\n",
"(constructor OptionalInt_none () OptionalInt)\n",
"(rewrite (concat (TupleNDArray_append (TupleNDArray_EMPTY ) x) (OptionalInt_none )) x :ruleset array_api_ruleset)\n",
"(rewrite (unique_values (unique_values x)) (unique_values x) :ruleset array_api_ruleset)\n",
"(rewrite (sum (NDArray___truediv__ x (NDArray_scalar v)) (OptionalIntOrTuple_none )) (NDArray___truediv__ (sum x (OptionalIntOrTuple_none )) (NDArray_scalar v)) :ruleset array_api_ruleset)\n",
"(constructor NDArray_ndim (NDArray) Int)\n",
"(sort OptionalDType)\n",
"(sort OptionalDevice)\n",
"(constructor asarray (NDArray OptionalDType OptionalBool OptionalDevice) NDArray)\n",
"(constructor OptionalDevice_none () OptionalDevice)\n",
"(rewrite (NDArray_ndim (asarray a d ob (OptionalDevice_none ))) (NDArray_ndim a) :ruleset array_api_ruleset)\n",
"(constructor OptionalDType_none () OptionalDType)\n",
"(constructor OptionalBool_none () OptionalBool)\n",
"(rewrite (asarray a (OptionalDType_none ) (OptionalBool_none ) (OptionalDevice_none )) a :ruleset array_api_ruleset)\n",
"(constructor check_index (Int Int) Int)\n",
"(constructor Boolean___and__ (Boolean Boolean) Boolean)\n",
"(constructor Int___ge__ (Int Int) Boolean)\n",
"(constructor Int_NEVER () Int)\n",
"(rewrite (check_index length idx) (Int_if_ (Boolean___and__ (Int___ge__ idx (Int___init__ 0)) (Int___lt__ idx length)) idx (Int_NEVER )) :ruleset array_api_ruleset)\n",
"(sort Vec_NDArray (Vec NDArray))\n",
"(function TupleNDArray_to_vec (TupleNDArray) Vec_NDArray :no-merge)\n",
"(constructor TupleNDArray_from_vec (Vec_NDArray) TupleNDArray)\n",
"(rule ((= tv (TupleNDArray_from_vec vs)))\n",
" ((set (TupleNDArray_to_vec tv) vs))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (TupleNDArray_length (TupleNDArray___init__ length idx_fn)) length :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray___getitem__ (TupleNDArray___init__ length idx_fn) idx) (unstable-app idx_fn (check_index idx length)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray_length (TupleNDArray_EMPTY )) (Int___init__ 0) :ruleset array_api_ruleset)\n",
"(constructor NDArray_NEVER () NDArray)\n",
"(rewrite (TupleNDArray___getitem__ (TupleNDArray_EMPTY ) idx) (NDArray_NEVER ) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray_length (TupleNDArray_append tv v)) (Int___add__ (TupleNDArray_length tv) (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray___getitem__ (TupleNDArray_append tv v) idx) (NDArray_if_ (Int___eq__ idx (TupleNDArray_length tv)) v (TupleNDArray___getitem__ tv idx)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray___init__ (Int___init__ 0) idx_fn) (TupleNDArray_EMPTY ) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray___init__ (Int___init__ k) idx_fn) (TupleNDArray_append (TupleNDArray___init__ (Int___init__ (- k 1)) idx_fn) (unstable-app idx_fn (Int___init__ (- k 1)))) :subsume :when ((> k 0)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray_EMPTY ) (TupleNDArray_from_vec (vec-of )) :ruleset array_api_ruleset)\n",
"(rewrite (TupleNDArray_append (TupleNDArray_from_vec vs) v) (TupleNDArray_from_vec (vec-append vs (vec-of v))) :ruleset array_api_ruleset)\n",
"(rule ((= (TupleNDArray_append tv v) (TupleNDArray_append tv1 v1)))\n",
" ((union tv tv1)\n",
" (union v v1))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (NDArray_shape (NDArray___init__ shape dtype idx_fn)) shape :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_dtype (NDArray___init__ shape dtype idx_fn)) dtype :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_index (NDArray___init__ shape dtype idx_fn) idx) (unstable-app idx_fn idx) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_ndim x) (TupleInt_length (NDArray_shape x)) :ruleset array_api_ruleset)\n",
"(constructor NDArray_to_value (NDArray) Value)\n",
"(rewrite (NDArray_to_value x) (NDArray_index x (TupleInt_EMPTY )) :ruleset array_api_ruleset)\n",
"(constructor NDArray_to_values (NDArray) TupleValue)\n",
"(rewrite (NDArray_to_values (NDArray_vector tv)) tv :ruleset array_api_ruleset)\n",
"(rewrite (NDArray___truediv__ (NDArray_scalar (Value_float f)) (NDArray_scalar (Value_float f))) (NDArray_scalar (Value_float (Float___init__ 1.0))) :ruleset array_api_ruleset)\n",
"(constructor NDArray___sub__ (NDArray NDArray) NDArray)\n",
"(rewrite (NDArray___sub__ (NDArray_scalar (Value_float f)) (NDArray_scalar (Value_float f))) (NDArray_scalar (Value_float (Float___init__ 0.0))) :ruleset array_api_ruleset)\n",
"(constructor NDArray___gt__ (NDArray NDArray) NDArray)\n",
"(rewrite (NDArray___gt__ (NDArray_scalar (Value_float (Float___init__ fi1))) (NDArray_scalar (Value_float (Float___init__ fi2)))) (NDArray_scalar (Value_bool (Boolean___init__ true))) :when ((> fi1 fi2)) :ruleset array_api_ruleset)\n",
"(rewrite (NDArray___gt__ (NDArray_scalar (Value_float (Float___init__ fi1))) (NDArray_scalar (Value_float (Float___init__ fi2)))) (NDArray_scalar (Value_bool (Boolean___init__ false))) :when ((<= fi1 fi2)) :ruleset array_api_ruleset)\n",
"(constructor NDArray_T (NDArray) NDArray)\n",
"(rewrite (NDArray_T (NDArray_T x)) x :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_if_ (Boolean___init__ true) x x1) x :ruleset array_api_ruleset)\n",
"(rewrite (NDArray_if_ (Boolean___init__ false) x x1) x1 :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_length (TupleValue___init__ length idx_fn)) length :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue___getitem__ (TupleValue___init__ length idx_fn) idx) (unstable-app idx_fn (check_index idx length)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_length (TupleValue_EMPTY )) (Int___init__ 0) :ruleset array_api_ruleset)\n",
"(constructor Value_NEVER () Value)\n",
"(rewrite (TupleValue___getitem__ (TupleValue_EMPTY ) idx) (Value_NEVER ) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_length (TupleValue_append tv v)) (Int___add__ (TupleValue_length tv) (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue___getitem__ (TupleValue_append tv v) idx) (Value_if_ (Int___eq__ idx (TupleValue_length tv)) v (TupleValue___getitem__ tv idx)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue___init__ (Int___init__ 0) idx_fn) (TupleValue_EMPTY ) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue___init__ (Int___init__ k) idx_fn) (TupleValue_append (TupleValue___init__ (Int___init__ (- k 1)) idx_fn) (unstable-app idx_fn (Int___init__ (- k 1)))) :subsume :when ((> k 0)) :ruleset array_api_ruleset)\n",
"(sort Vec_Value (Vec Value))\n",
"(constructor TupleValue_from_vec (Vec_Value) TupleValue)\n",
"(rewrite (TupleValue_EMPTY ) (TupleValue_from_vec (vec-of )) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_append (TupleValue_from_vec vs) v) (TupleValue_from_vec (vec-append vs (vec-of v))) :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_foldl_boolean (TupleValue_EMPTY ) bool_f b) b :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleValue_foldl_boolean (TupleValue_append tv v) bool_f b) (unstable-app bool_f (TupleValue_foldl_boolean tv bool_f b) v) :subsume :ruleset array_api_ruleset)\n",
"(rule ((= (TupleValue_append tv v) (TupleValue_append tv1 v1)))\n",
" ((union tv tv1)\n",
" (union v v1))\n",
" :ruleset array_api_ruleset )\n",
"(constructor DType_int64 () DType)\n",
"(rewrite (Value_dtype (Value_int i)) (DType_int64 ) :ruleset array_api_ruleset)\n",
"(rewrite (Value_dtype (Value_float f)) (DType_float64 ) :ruleset array_api_ruleset)\n",
"(constructor DType_bool () DType)\n",
"(rewrite (Value_dtype (Value_bool b)) (DType_bool ) :ruleset array_api_ruleset)\n",
"(constructor Value_to_bool (Value) Boolean)\n",
"(rewrite (Value_to_bool (Value_bool b)) b :ruleset array_api_ruleset)\n",
"(constructor Value_to_int (Value) Int)\n",
"(rewrite (Value_to_int (Value_int i)) i :ruleset array_api_ruleset)\n",
"(rewrite (Value_to_truthy_value (Value_bool b)) (Value_bool b) :ruleset array_api_ruleset)\n",
"(rewrite (Value_conj (Value_float f)) (Value_float f) :ruleset array_api_ruleset)\n",
"(rewrite (Value_real (Value_float f)) (Value_float f) :ruleset array_api_ruleset)\n",
"(rewrite (Value_real (Value_int i)) (Value_int i) :ruleset array_api_ruleset)\n",
"(rewrite (Value_conj (Value_int i)) (Value_int i) :ruleset array_api_ruleset)\n",
"(constructor Float___pow__ (Float Float) Float)\n",
"(rewrite (Value_sqrt (Value_float f)) (Value_float (Float___pow__ f (Float___init__ 0.5))) :ruleset array_api_ruleset)\n",
"(constructor Float_rational (BigRat) Float :cost 2)\n",
"(rewrite (Value___add__ (Value_float (Float_rational (bigrat (bigint 0) (bigint 1)))) v) v :ruleset array_api_ruleset)\n",
"(rewrite (Value_if_ (Boolean___init__ true) v v1) v :ruleset array_api_ruleset)\n",
"(rewrite (Value_if_ (Boolean___init__ false) v v1) v1 :ruleset array_api_ruleset)\n",
"(rewrite (Value___eq__ (Value_int i) (Value_int i1)) (Int___eq__ i i1) :ruleset array_api_ruleset)\n",
"(constructor Float___eq__ (Float Float) Boolean)\n",
"(rewrite (Value___eq__ (Value_float f) (Value_float f1)) (Float___eq__ f f1) :ruleset array_api_ruleset)\n",
"(constructor Boolean___eq__ (Boolean Boolean) Boolean)\n",
"(rewrite (Value___eq__ (Value_bool b) (Value_bool b1)) (Boolean___eq__ b b1) :ruleset array_api_ruleset)\n",
"(sort IsDtypeKind)\n",
"(constructor isdtype (DType IsDtypeKind) Boolean)\n",
"(constructor DType_float32 () DType)\n",
"(constructor IsDtypeKind_string (String) IsDtypeKind)\n",
"(rewrite (isdtype (DType_float32 ) (IsDtypeKind_string \"integral\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_float64 ) (IsDtypeKind_string \"integral\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(constructor DType_object () DType)\n",
"(rewrite (isdtype (DType_object ) (IsDtypeKind_string \"integral\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_int64 ) (IsDtypeKind_string \"integral\")) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(constructor DType_int32 () DType)\n",
"(rewrite (isdtype (DType_int32 ) (IsDtypeKind_string \"integral\")) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_float32 ) (IsDtypeKind_string \"real floating\")) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_float64 ) (IsDtypeKind_string \"real floating\")) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_object ) (IsDtypeKind_string \"real floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_int64 ) (IsDtypeKind_string \"real floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_int32 ) (IsDtypeKind_string \"real floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_float32 ) (IsDtypeKind_string \"complex floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_float64 ) (IsDtypeKind_string \"complex floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_object ) (IsDtypeKind_string \"complex floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_int64 ) (IsDtypeKind_string \"complex floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (isdtype (DType_int32 ) (IsDtypeKind_string \"complex floating\")) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(constructor IsDtypeKind_NULL () IsDtypeKind)\n",
"(rewrite (isdtype d (IsDtypeKind_NULL )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(constructor IsDtypeKind_dtype (DType) IsDtypeKind)\n",
"(rewrite (isdtype d (IsDtypeKind_dtype d)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(constructor IsDtypeKind___or__ (IsDtypeKind IsDtypeKind) IsDtypeKind :cost 10)\n",
"(rewrite (isdtype d (IsDtypeKind___or__ k1 k2)) (Boolean___or__ (isdtype d k1) (isdtype d k2)) :ruleset array_api_ruleset)\n",
"(rewrite (IsDtypeKind___or__ k1 (IsDtypeKind_NULL )) k1 :ruleset array_api_ruleset)\n",
"(constructor DType___eq__ (DType DType) Boolean)\n",
"(rewrite (DType___eq__ (DType_float64 ) (DType_float64 )) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float64 ) (DType_float32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float64 ) (DType_int32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float64 ) (DType_int64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float64 ) (DType_object )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float32 ) (DType_float64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float32 ) (DType_float32 )) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float32 ) (DType_int32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float32 ) (DType_int64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_float32 ) (DType_object )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int32 ) (DType_float64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int32 ) (DType_float32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int32 ) (DType_int32 )) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int32 ) (DType_int64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int32 ) (DType_object )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int64 ) (DType_float64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int64 ) (DType_float32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int64 ) (DType_int32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int64 ) (DType_int64 )) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_int64 ) (DType_object )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_object ) (DType_float64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_object ) (DType_float32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_object ) (DType_int32 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_object ) (DType_int64 )) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (DType___eq__ (DType_object ) (DType_object )) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(sort Vec_TupleInt (Vec TupleInt))\n",
"(function TupleTupleInt_to_vec (TupleTupleInt) Vec_TupleInt :no-merge)\n",
"(constructor TupleTupleInt_from_vec (Vec_TupleInt) TupleTupleInt)\n",
"(rule ((= tti (TupleTupleInt_from_vec vs)))\n",
" ((set (TupleTupleInt_to_vec tti) vs))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (TupleTupleInt_length (TupleTupleInt___init__ length idx_fn)) length :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt___getitem__ (TupleTupleInt___init__ length idx_fn) idx) (unstable-app idx_fn (check_index idx length)) :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt_EMPTY () TupleTupleInt)\n",
"(rewrite (TupleTupleInt_length (TupleTupleInt_EMPTY )) (Int___init__ 0) :ruleset array_api_ruleset)\n",
"(constructor TupleInt_NEVER () TupleInt)\n",
"(rewrite (TupleTupleInt___getitem__ (TupleTupleInt_EMPTY ) idx) (TupleInt_NEVER ) :ruleset array_api_ruleset)\n",
"(constructor TupleTupleInt_append (TupleTupleInt TupleInt) TupleTupleInt)\n",
"(rewrite (TupleTupleInt_length (TupleTupleInt_append tti ti)) (Int___add__ (TupleTupleInt_length tti) (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt___getitem__ (TupleTupleInt_append tti ti) idx) (TupleInt_if_ (Int___eq__ idx (TupleTupleInt_length tti)) ti (TupleTupleInt___getitem__ tti idx)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt___init__ (Int___init__ 0) idx_fn) (TupleTupleInt_EMPTY ) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt___init__ (Int___init__ k) idx_fn) (TupleTupleInt_append (TupleTupleInt___init__ (Int___init__ (- k 1)) idx_fn) (unstable-app idx_fn (Int___init__ (- k 1)))) :subsume :when ((> k 0)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt_EMPTY ) (TupleTupleInt_from_vec (vec-of )) :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt_append (TupleTupleInt_from_vec vs) ti) (TupleTupleInt_from_vec (vec-append vs (vec-of ti))) :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt_foldl_value (TupleTupleInt_EMPTY ) f i) i :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleTupleInt_foldl_value (TupleTupleInt_append tti ti) f i) (unstable-app f (TupleTupleInt_foldl_value tti f i) ti) :subsume :ruleset array_api_ruleset)\n",
"(rule ((= (TupleTupleInt_append tti ti) (TupleTupleInt_append tti1 ti1)))\n",
" ((union tti tti1)\n",
" (union ti ti1))\n",
" :ruleset array_api_ruleset )\n",
"(sort Vec_Int (Vec Int))\n",
"(function TupleInt_to_vec (TupleInt) Vec_Int :no-merge)\n",
"(constructor TupleInt_from_vec (Vec_Int) TupleInt)\n",
"(rule ((= ti (TupleInt_from_vec vs)))\n",
" ((set (TupleInt_to_vec ti) vs))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (TupleInt_length (TupleInt___init__ i idx_fn)) i :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt___getitem__ (TupleInt___init__ i idx_fn) i2) (unstable-app idx_fn (check_index i i2)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_length (TupleInt_EMPTY )) (Int___init__ 0) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt___getitem__ (TupleInt_EMPTY ) i) (Int_NEVER ) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_length (TupleInt_append ti i)) (Int___add__ (TupleInt_length ti) (Int___init__ 1)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt___getitem__ (TupleInt_append ti i) i2) (Int_if_ (Int___eq__ i2 (TupleInt_length ti)) i (TupleInt___getitem__ ti i2)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt___init__ (Int___init__ 0) idx_fn) (TupleInt_EMPTY ) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt___init__ (Int___init__ k) idx_fn) (TupleInt_append (TupleInt___init__ (Int___init__ (- k 1)) idx_fn) (unstable-app idx_fn (Int___init__ (- k 1)))) :subsume :when ((> k 0)) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_EMPTY ) (TupleInt_from_vec (vec-of )) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_append (TupleInt_from_vec vs) i) (TupleInt_from_vec (vec-append vs (vec-of i))) :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl (TupleInt_EMPTY ) f i) i :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl (TupleInt_append ti i2) f i) (unstable-app f (TupleInt_foldl ti f i) i2) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl_boolean (TupleInt_EMPTY ) bool_f b) b :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl_boolean (TupleInt_append ti i2) bool_f b) (unstable-app bool_f (TupleInt_foldl_boolean ti bool_f b) i2) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl_tuple_int (TupleInt_EMPTY ) tuple_int_f ti) ti :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_foldl_tuple_int (TupleInt_append ti i2) tuple_int_f ti2) (unstable-app tuple_int_f (TupleInt_foldl_tuple_int ti tuple_int_f ti2) i2) :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_if_ (Boolean___init__ true) ti ti2) ti :subsume :ruleset array_api_ruleset)\n",
"(rewrite (TupleInt_if_ (Boolean___init__ false) ti ti2) ti2 :subsume :ruleset array_api_ruleset)\n",
"(rule ((= (TupleInt_append ti i) (TupleInt_append ti2 i2)))\n",
" ((union ti ti2)\n",
" (union i i2))\n",
" :ruleset array_api_ruleset )\n",
"(function Float_to_f64 (Float) f64 :no-merge)\n",
"(rule ((= fl (Float___init__ f)))\n",
" ((set (Float_to_f64 fl) f))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Float_abs (Float___init__ f)) (Float___init__ f) :when ((>= f 0.0)) :ruleset array_api_ruleset)\n",
"(rewrite (Float_abs (Float___init__ f)) (Float___init__ (neg f)) :when ((< f 0.0)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___init__ f) (Float_rational (bigrat (bigint (to-i64 f)) (bigint 1))) :when ((= (to-f64 (to-i64 f)) f)) :ruleset array_api_ruleset)\n",
"(constructor Float_from_int (Int) Float)\n",
"(rewrite (Float_from_int (Int___init__ i)) (Float_rational (bigrat (bigint i) (bigint 1))) :ruleset array_api_ruleset)\n",
"(constructor Float___add__ (Float Float) Float)\n",
"(rewrite (Float___add__ (Float___init__ f) (Float___init__ f2)) (Float___init__ (+ f f2)) :ruleset array_api_ruleset)\n",
"(constructor Float___sub__ (Float Float) Float)\n",
"(rewrite (Float___sub__ (Float___init__ f) (Float___init__ f2)) (Float___init__ (- f f2)) :ruleset array_api_ruleset)\n",
"(constructor Float___mul__ (Float Float) Float)\n",
"(rewrite (Float___mul__ (Float___init__ f) (Float___init__ f2)) (Float___init__ (* f f2)) :ruleset array_api_ruleset)\n",
"(constructor Float___truediv__ (Float Float) Float)\n",
"(rewrite (Float___truediv__ (Float_rational r) (Float_rational r1)) (Float_rational (/ r r1)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___add__ (Float_rational r) (Float_rational r1)) (Float_rational (+ r r1)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___sub__ (Float_rational r) (Float_rational r1)) (Float_rational (- r r1)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___mul__ (Float_rational r) (Float_rational r1)) (Float_rational (* r r1)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___pow__ (Float___init__ f) (Float___init__ f2)) (Float___init__ (^ f f2)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___eq__ (Float___init__ f) (Float___init__ f)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (Float___eq__ (Float___init__ f) (Float___init__ f2)) (Boolean___init__ false) :when ((!= f f2)) :ruleset array_api_ruleset)\n",
"(rewrite (Float___eq__ (Float_rational r) (Float_rational r)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (Float___eq__ (Float_rational r) (Float_rational r1)) (Boolean___init__ false) :when ((!= r r1)) :ruleset array_api_ruleset)\n",
"(rewrite (Int___eq__ (Int___init__ i) (Int___init__ i)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rule ((= r (Int___eq__ (Int___init__ i) (Int___init__ j)))\n",
" (!= i j))\n",
" ((union r (Boolean___init__ false)))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Int___ge__ (Int___init__ i) (Int___init__ i)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rule ((= r (Int___ge__ (Int___init__ i) (Int___init__ j)))\n",
" (> i j))\n",
" ((union r (Boolean___init__ true)))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= r (Int___ge__ (Int___init__ i) (Int___init__ j)))\n",
" (< i j))\n",
" ((union r (Boolean___init__ false)))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Int___lt__ (Int___init__ i) (Int___init__ i)) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rule ((= r (Int___lt__ (Int___init__ i) (Int___init__ j)))\n",
" (< i j))\n",
" ((union r (Boolean___init__ true)))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= r (Int___lt__ (Int___init__ i) (Int___init__ j)))\n",
" (> i j))\n",
" ((union r (Boolean___init__ false)))\n",
" :ruleset array_api_ruleset )\n",
"(constructor Int___gt__ (Int Int) Boolean)\n",
"(rewrite (Int___gt__ (Int___init__ i) (Int___init__ i)) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rule ((= r (Int___gt__ (Int___init__ i) (Int___init__ j)))\n",
" (> i j))\n",
" ((union r (Boolean___init__ true)))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= r (Int___gt__ (Int___init__ i) (Int___init__ j)))\n",
" (< i j))\n",
" ((union r (Boolean___init__ false)))\n",
" :ruleset array_api_ruleset )\n",
"(function Int_to_i64 (Int) i64 :no-merge)\n",
"(rule ((= o (Int___init__ j)))\n",
" ((set (Int_to_i64 o) j))\n",
" :ruleset array_api_ruleset )\n",
"(rule ((= (Int___init__ i) (Int___init__ j))\n",
" (!= i j))\n",
" ((panic \"Real ints cannot be equal to different ints\"))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Int___add__ (Int___init__ i) (Int___init__ j)) (Int___init__ (+ i j)) :ruleset array_api_ruleset)\n",
"(rewrite (Int___sub__ (Int___init__ i) (Int___init__ j)) (Int___init__ (- i j)) :ruleset array_api_ruleset)\n",
"(rewrite (Int___mul__ (Int___init__ i) (Int___init__ j)) (Int___init__ (* i j)) :ruleset array_api_ruleset)\n",
"(rewrite (Int___floordiv__ (Int___init__ i) (Int___init__ j)) (Int___init__ (/ i j)) :ruleset array_api_ruleset)\n",
"(rewrite (Int___mod__ (Int___init__ i) (Int___init__ j)) (Int___init__ (% i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___and__ (Int Int) Int)\n",
"(rewrite (Int___and__ (Int___init__ i) (Int___init__ j)) (Int___init__ (& i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___or__ (Int Int) Int)\n",
"(rewrite (Int___or__ (Int___init__ i) (Int___init__ j)) (Int___init__ (| i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___xor__ (Int Int) Int)\n",
"(rewrite (Int___xor__ (Int___init__ i) (Int___init__ j)) (Int___init__ (^ i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___lshift__ (Int Int) Int)\n",
"(rewrite (Int___lshift__ (Int___init__ i) (Int___init__ j)) (Int___init__ (<< i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___rshift__ (Int Int) Int)\n",
"(rewrite (Int___rshift__ (Int___init__ i) (Int___init__ j)) (Int___init__ (>> i j)) :ruleset array_api_ruleset)\n",
"(constructor Int___invert__ (Int) Int)\n",
"(rewrite (Int___invert__ (Int___init__ i)) (Int___init__ (not-i64 i)) :ruleset array_api_ruleset)\n",
"(rewrite (Int_if_ (Boolean___init__ true) o b) o :subsume :ruleset array_api_ruleset)\n",
"(rewrite (Int_if_ (Boolean___init__ false) o b) b :subsume :ruleset array_api_ruleset)\n",
"(rule ((= (Int_NEVER ) (Int___init__ i)))\n",
" ((panic \"Int.NEVER cannot be equal to any real int\"))\n",
" :ruleset array_api_ruleset )\n",
"(function Boolean_to_bool (Boolean) bool :no-merge)\n",
"(rule ((= x (Boolean___init__ b)))\n",
" ((set (Boolean_to_bool x) b))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Boolean___or__ (Boolean___init__ true) x) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___or__ (Boolean___init__ false) x) x :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___and__ (Boolean___init__ true) x) x :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___and__ (Boolean___init__ false) x) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___invert__ (Boolean___init__ true)) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___invert__ (Boolean___init__ false)) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rule ((= (Boolean___init__ false) (Boolean___init__ true)))\n",
" ((panic \"False cannot equal True\"))\n",
" :ruleset array_api_ruleset )\n",
"(rewrite (Boolean___eq__ x x) (Boolean___init__ true) :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___eq__ (Boolean___init__ false) (Boolean___init__ true)) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(rewrite (Boolean___eq__ (Boolean___init__ true) (Boolean___init__ false)) (Boolean___init__ false) :ruleset array_api_ruleset)\n",
"(ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleInt_from_vec vs) (TupleInt_EMPTY ) :when ((= (vec-length vs) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleInt_from_vec vs) (TupleInt_append (TupleInt_from_vec (vec-remove vs (- (vec-length vs) 1))) (vec-get vs (- (vec-length vs) 1))) :when ((!= (vec-length vs) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleValue_from_vec vv) (TupleValue_EMPTY ) :when ((= (vec-length vv) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleValue_from_vec vv) (TupleValue_append (TupleValue_from_vec (vec-remove vv (- (vec-length vv) 1))) (vec-get vv (- (vec-length vv) 1))) :when ((!= (vec-length vv) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleTupleInt_from_vec vt) (TupleTupleInt_EMPTY ) :when ((= (vec-length vt) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleTupleInt_from_vec vt) (TupleTupleInt_append (TupleTupleInt_from_vec (vec-remove vt (- (vec-length vt) 1))) (vec-get vt (- (vec-length vt) 1))) :when ((!= (vec-length vt) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleNDArray_from_vec vn) (TupleNDArray_EMPTY ) :when ((= (vec-length vn) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(rewrite (TupleNDArray_from_vec vn) (TupleNDArray_append (TupleNDArray_from_vec (vec-remove vn (- (vec-length vn) 1))) (vec-get vn (- (vec-length vn) 1))) :when ((!= (vec-length vn) 0)) :ruleset array_api_vec_to_cons_ruleset)\n",
"(unstable-combined-ruleset combined_ruleset_4715589712 array_api_ruleset array_api_vec_to_cons_ruleset)\n",
"(constructor X () NDArray)\n",
"(constructor i () Int)\n",
"(constructor j () Int)\n",
"(simplify (saturate (run combined_ruleset_4715589712)) (NDArray_index (linalg_norm_v2 (assume_shape (X ) (TupleInt_from_vec (vec-of (Int___init__ 3) (Int___init__ 2) (Int___init__ 3) (Int___init__ 4)))) (TupleInt_from_vec (vec-of (Int___init__ 0) (Int___init__ 1)))) (TupleInt_from_vec (vec-of (i ) (j )))))\n",
"\n"
]
}
],
"source": [
"egraph = EGraph(save_egglog_string=True)\n",
"\n",
"i = constant(\"i\", Int)\n",
"j = constant(\"j\", Int)\n",
"egraph.simplify(res.index((i, j)), array_api_schedule)\n",
"print(egraph.as_egglog_string)"
]
},
{
"cell_type": "markdown",
"id": "2b963670",
"metadata": {},
"source": []
},
{
"cell_type": "markdown",
"id": "a5615583",
"metadata": {},
"source": [
"## Primites\n"
]
},
{
"cell_type": "code",
"execution_count": 22,
"id": "2a0d67c6",
"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\">Vec</span><span class=\"p\">(</span><span class=\"n\">Math</span><span class=\"p\">(</span><span class=\"mi\">1</span><span class=\"p\">),</span> <span class=\"n\">Math</span><span class=\"p\">(</span><span class=\"mi\">2</span><span class=\"p\">),</span> <span class=\"n\">Math</span><span class=\"p\">(</span><span class=\"mi\">3</span><span class=\"p\">))</span>\n",
"</pre></div>\n"
],
"text/latex": [
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]\n",
"\\PY{n}{Vec}\\PY{p}{(}\\PY{n}{Math}\\PY{p}{(}\\PY{l+m+mi}{1}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Math}\\PY{p}{(}\\PY{l+m+mi}{2}\\PY{p}{)}\\PY{p}{,} \\PY{n}{Math}\\PY{p}{(}\\PY{l+m+mi}{3}\\PY{p}{)}\\PY{p}{)}\n",
"\\end{Verbatim}\n"
],
"text/plain": [
"Vec(Math(1), Math(2), Math(3))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"class Math(Expr):\n",
" def __init__(self, x: i64Like) -> None: ...\n",
"\n",
"\n",
"xs = Vec(Math(1), Math(2), Math(3))\n",
"xs"
]
},
{
"cell_type": "markdown",
"id": "70ee7804",
"metadata": {},
"source": [
"Primitives now can be turned into Python values without an e-graph, by looking at evaluating the primitives expression in Python. They must be in the form that they are extracted in.\n"
]
},
{
"cell_type": "code",
"execution_count": 23,
"id": "8cacf94f",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[Math(1), Math(2), Math(3)]"
]
},
"execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"list(xs)"
]
},
{
"cell_type": "code",
"execution_count": 24,
"id": "29a055c8",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"100"
]
},
"execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# instead of EGraph().eval(i64(100)) you can now do:\n",
"int(i64(100))"
]
},
{
"cell_type": "markdown",
"id": "1cc8dd18",
"metadata": {},
"source": [
"Adding an Equality fact or a != expression is now easier too, by using the `__eq__` builtin:\n"
]
},
{
"cell_type": "markdown",
"id": "c117861a",
"metadata": {},
"source": []
},
{
"cell_type": "code",
"execution_count": 27,
"id": "d7f1b644",
"metadata": {},
"outputs": [],
"source": [
"e = EGraph()\n",
"e.register(xs)\n",
"e.check(xs == Vec(Math(1), Math(2), Math(3)))\n",
"# instead of\n",
"# e.check(eq(xs).to(Vec(Math(1), Math(2), Math(3))))"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "9d3369a6",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": ".venv",
"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.12.5"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment