anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Sub Expression Elimination #97

Closed mariari closed 1 year ago

mariari commented 1 year ago

This PR remvoes common sub-expressions

mariari commented 1 year ago

Further gains can be had, if one ran it on the vampir code after it's done, I intended to do this, but ended up not, it would save some computational cycles if I did however.

mariari commented 1 year ago

Further gains can be had, by instead of running the sub-expression eliminator on the poly output, and abstraction functions,

instead running it on vampir itself, first, and reduce complexity via the composition letting I did in this pr, such that we don't run out of stack space.

This would give the maximal sharing, but create only 1 function at the end.

One big issue with the sharing technique, is that we explicitly separate it with a let for composition, to make the stack depth not be reached. But we do no reference chasing for uniqueness, meaning that although the def saves us stack space, we have repeat code like

 def g467 x = {
   def c565 = x - 4;
   def c566 = mod32 x 1;
   def c567 = x - 4;
   def c568 = mod32 c567 1;
   def c569 =
     2 * ((pwless32 x 4 (x / 4) (c565 / 4)) + (pwless32 x 4 c566 (1 + c568)));
   def c570 = 1 * (c569 + 0);
   def c571 = c570;
   def c572 = c571 - 8;
   def c573 = mod32 c571 1;
   def c574 = c571 - 8;
   def c575 = mod32 c574 1;
   def c576 =
     2 * ((pwless32 c571 8 (c571 / 8) (c572 / 8)) + (pwless32 c571 8 c573 (1 + c575)));
   def c577 = c576 / 8;
   def c578 = c576 / 8;
   def c579 = 4 * ((c577 / 4) + (2 * ((mod32 c578 2) + (mod32 c576 2))));
   def c580 = c579 / 4;
   def c581 = c579 / 4;
   def c582 = 16 * ((c580 / 1) + (4 * ((mod32 c581 4) + (mod32 c579 4))));
   def c583 = 1 * ((mod32 c582 16) + (c582 / 1));
   def c584 = 1 * (c569 + 0);
   def c585 = 8 + c584;
   def c586 = c585 - 8;
   def c587 = mod32 c585 1;
   def c588 = c585 - 8;
   def c589 = mod32 c588 1;
   def c590 =
     2 * ((pwless32 c585 8 (c585 / 8) (c586 / 8)) + (pwless32 c585 8 c587 (1 + c589)));
   def c591 = c590 / 8;
   def c592 = c590 / 8;
   def c593 = 4 * ((c591 / 4) + (2 * ((mod32 c592 2) + (mod32 c590 2))));
   def c594 = c593 / 4;
   def c595 = c593 / 4;
   def c596 = 16 * ((c594 / 1) + (4 * ((mod32 c595 4) + (mod32 c593 4))));
   def c597 = 1 * ((mod32 c596 16) + (c596 / 1));
   16 * ((c583 / 16) + (c597 / 16))
 };

which has potentially has repeat logic within it. Meaning that any common code between composition at this level lives.

This can be fixed, by another pass, which collases repeat lets, and then recomputes uniqueness. we can run this until all repeat code is let out.