search

rise-lang / shine

The Shine compiler for the RISE language
https://rise-lang.org
MIT License
73 stars 8 forks source link

[BUG] rule annotation breaks rewriting #219

Closed johanneslenfers closed 2 years ago

johanneslenfers commented 2 years ago

Describe the bug splitJoin rule cannot be applied two times, if definition is annotated with @rule

To Reproduce Execute main here

Expected behavior Rewriting is successful for the non annotated strategy, but fails for the annotaed version with this error:

could not pivot 1 = 1
could not pivot 1 = 1
could not solve constraints List((n6*tuned_tp301*(1/^((tuned_tp277*tuned_tp301))))  ~  (n6*(1/^(tuned_tp277))))
could not solve constraints List((n6*tuned_tp301*(1/^((tuned_tp277*tuned_tp301)))).tuned_tp277.f32  ~  (n6*(1/^(tuned_tp277))).tuned_tp277.f32)
Bastacyclop commented 2 years ago

  1. It is not so much about the @rule, but more about the def versus val. I think in one case you create two tuning parameters, and in the other case only one. To check this, change the val into def topDownSplitJoin, and it will also fail to be applied twice.

  2. I think that the type inference should accept 1 = 1 as being a solution without any required subsitution. Currently it is probably expected that a subsitution is required, because == was checked before running the pivot mechanism. Here, I believe that we observe that the pivot mechanism is better at deciding == than the default == of ArithExpr.

Bastacyclop commented 2 years ago

Here is a fix: https://github.com/rise-lang/shine/commit/fdc0dc7d320413ab26f00454af6674e54a8edad8

johanneslenfers commented 2 years ago

I see, that makes sense! Didn't observe that only one tuning parameter was created. Thank you for the fix.