build based on 322be51

dev/egraphs/index.html

@@ -134,4 +134,4 @@
 custom_analysis(:(2*a)) # :even
 custom_analysis(:(3*3)) # :odd
 custom_analysis(:(3*(2+a)*2)) # :even
-custom_analysis(:(3y * (2x*y))) # :even</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../rewrite/">« Classical Term Rewriting</a><a class="docs-footer-nextpage" href="../api/">API Documentation »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Wednesday 31 May 2023 16:13">Wednesday 31 May 2023</span>. Using Julia version 1.8.5.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+custom_analysis(:(3y * (2x*y))) # :even</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../rewrite/">« Classical Term Rewriting</a><a class="docs-footer-nextpage" href="../api/">API Documentation »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Monday 7 August 2023 12:40">Monday 7 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>

dev/index.html

@@ -5,4 +5,4 @@
 <a href="https://planting.space"> 
     <img width="300px" src="https://raw.githubusercontent.com/juliasymbolics/Metatheory.jl/master/.github/plantingspace.png"/>
 </a>
-</p></article><nav class="docs-footer"><a class="docs-footer-nextpage" href="rewrite/">Classical Term Rewriting »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Wednesday 31 May 2023 16:13">Wednesday 31 May 2023</span>. Using Julia version 1.8.5.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+</p></article><nav class="docs-footer"><a class="docs-footer-nextpage" href="rewrite/">Classical Term Rewriting »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Monday 7 August 2023 12:40">Monday 7 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>

dev/rewrite/index.html

@@ -34,4 +34,4 @@
 distrib = @theory a b c begin
     a * (b + c) => (a * b) + (a * c)
 end
-t = comm_monoid ∪ comm_group ∪ distrib</code></pre><h2 id="Composing-rewriters"><a class="docs-heading-anchor" href="#Composing-rewriters">Composing rewriters</a><a id="Composing-rewriters-1"></a><a class="docs-heading-anchor-permalink" href="#Composing-rewriters" title="Permalink"></a></h2><p>Rules may be <em>chained together</em> into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object which takes an expression and returns an expression or <code>nothing</code>. If <code>nothing</code> is returned that means there was no changes applicable to the input expression. The Rules we created above are rewriters.</p><p>The <code>Metatheory.Rewriters</code> module contains some types which create and transform rewriters.</p><ul><li><code>Empty()</code> is a rewriter which always returns <code>nothing</code></li><li><code>Chain(itr)</code> chain an iterator of rewriters into a single rewriter which applies  each chained rewriter in the given order.  If a rewriter returns <code>nothing</code> this is treated as a no-change.</li><li><code>RestartedChain(itr)</code> like <code>Chain(itr)</code> but restarts from the first rewriter once on the  first successful application of one of the chained rewriters.</li><li><code>IfElse(cond, rw1, rw2)</code> runs the <code>cond</code> function on the input, applies <code>rw1</code> if cond  returns true, <code>rw2</code> if it returns false</li><li><code>If(cond, rw)</code> is the same as <code>IfElse(cond, rw, Empty())</code></li><li><code>Prewalk(rw; threaded=false, thread_cutoff=100)</code> returns a rewriter which does a pre-order   (<em>from top to bottom and from left to right</em>) traversal of a given expression and applies   the rewriter <code>rw</code>. <code>threaded=true</code> will use multi threading for traversal.  Note that if <code>rw</code> returns <code>nothing</code> when a match is not found, then <code>Prewalk(rw)</code> will  also return nothing unless a match is found at every level of the walk. If you are  applying multiple rules, then <code>Chain</code> already has the appropriate passthrough behavior.  If you only want to apply one rule, then consider using <code>PassThrough</code>.  <code>thread_cutoff</code>   is the minimum number of nodes in a subtree which should be walked in a threaded spawn.</li><li><code>Postwalk(rw; threaded=false, thread_cutoff=100)</code> similarly does post-order   (<em>from left to right and from bottom to top</em>) traversal.</li><li><code>Fixpoint(rw)</code> returns a rewriter which applies <code>rw</code> repeatedly until there are no changes to be made.</li><li><code>FixpointNoCycle</code> behaves like <code>Fixpoint</code> but instead it applies <code>rw</code> repeatedly only while it is returning new results.</li><li><code>PassThrough(rw)</code> returns a rewriter which if <code>rw(x)</code> returns <code>nothing</code> will instead  return <code>x</code> otherwise will return <code>rw(x)</code>.</li></ul><h3 id="Chaining-rewriters"><a class="docs-heading-anchor" href="#Chaining-rewriters">Chaining rewriters</a><a id="Chaining-rewriters-1"></a><a class="docs-heading-anchor-permalink" href="#Chaining-rewriters" title="Permalink"></a></h3><p>Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of <code>Chain</code> is that it returns the expression instead of <code>nothing</code> if it doesn&#39;t change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn&#39;t work the same as in earlier example</p><p>One way to circumvent the problem of order of applying rules in chain is to use <code>RestartedChain</code>, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use <code>Fixpoint</code> to apply the rules until there are no changes.</p></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../">« Metatheory.jl 2.0</a><a class="docs-footer-nextpage" href="../egraphs/">EGraphs and Equality Saturation »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Wednesday 31 May 2023 16:13">Wednesday 31 May 2023</span>. Using Julia version 1.8.5.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+t = comm_monoid ∪ comm_group ∪ distrib</code></pre><h2 id="Composing-rewriters"><a class="docs-heading-anchor" href="#Composing-rewriters">Composing rewriters</a><a id="Composing-rewriters-1"></a><a class="docs-heading-anchor-permalink" href="#Composing-rewriters" title="Permalink"></a></h2><p>Rules may be <em>chained together</em> into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object which takes an expression and returns an expression or <code>nothing</code>. If <code>nothing</code> is returned that means there was no changes applicable to the input expression. The Rules we created above are rewriters.</p><p>The <code>Metatheory.Rewriters</code> module contains some types which create and transform rewriters.</p><ul><li><code>Empty()</code> is a rewriter which always returns <code>nothing</code></li><li><code>Chain(itr)</code> chain an iterator of rewriters into a single rewriter which applies  each chained rewriter in the given order.  If a rewriter returns <code>nothing</code> this is treated as a no-change.</li><li><code>RestartedChain(itr)</code> like <code>Chain(itr)</code> but restarts from the first rewriter once on the  first successful application of one of the chained rewriters.</li><li><code>IfElse(cond, rw1, rw2)</code> runs the <code>cond</code> function on the input, applies <code>rw1</code> if cond  returns true, <code>rw2</code> if it returns false</li><li><code>If(cond, rw)</code> is the same as <code>IfElse(cond, rw, Empty())</code></li><li><code>Prewalk(rw; threaded=false, thread_cutoff=100)</code> returns a rewriter which does a pre-order   (<em>from top to bottom and from left to right</em>) traversal of a given expression and applies   the rewriter <code>rw</code>. <code>threaded=true</code> will use multi threading for traversal.  Note that if <code>rw</code> returns <code>nothing</code> when a match is not found, then <code>Prewalk(rw)</code> will  also return nothing unless a match is found at every level of the walk. If you are  applying multiple rules, then <code>Chain</code> already has the appropriate passthrough behavior.  If you only want to apply one rule, then consider using <code>PassThrough</code>.  <code>thread_cutoff</code>   is the minimum number of nodes in a subtree which should be walked in a threaded spawn.</li><li><code>Postwalk(rw; threaded=false, thread_cutoff=100)</code> similarly does post-order   (<em>from left to right and from bottom to top</em>) traversal.</li><li><code>Fixpoint(rw)</code> returns a rewriter which applies <code>rw</code> repeatedly until there are no changes to be made.</li><li><code>FixpointNoCycle</code> behaves like <code>Fixpoint</code> but instead it applies <code>rw</code> repeatedly only while it is returning new results.</li><li><code>PassThrough(rw)</code> returns a rewriter which if <code>rw(x)</code> returns <code>nothing</code> will instead  return <code>x</code> otherwise will return <code>rw(x)</code>.</li></ul><h3 id="Chaining-rewriters"><a class="docs-heading-anchor" href="#Chaining-rewriters">Chaining rewriters</a><a id="Chaining-rewriters-1"></a><a class="docs-heading-anchor-permalink" href="#Chaining-rewriters" title="Permalink"></a></h3><p>Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of <code>Chain</code> is that it returns the expression instead of <code>nothing</code> if it doesn&#39;t change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn&#39;t work the same as in earlier example</p><p>One way to circumvent the problem of order of applying rules in chain is to use <code>RestartedChain</code>, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use <code>Fixpoint</code> to apply the rules until there are no changes.</p></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../">« Metatheory.jl 2.0</a><a class="docs-footer-nextpage" href="../egraphs/">EGraphs and Equality Saturation »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> on <span class="colophon-date" title="Monday 7 August 2023 12:40">Monday 7 August 2023</span>. Using Julia version 1.9.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>