search

rise-lang / shine

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

[BUG] HarrisCornerDetection Tuning Nat vs. Int #215

Closed johanneslenfers closed 3 years ago

johanneslenfers commented 3 years ago

Describe the bug Tried to setup autotuning for HarrisCornerDetection. As TuningParameters are specified as Nat, I changed this function to take Nat instead of Int. Now, I get an inference exception:

   // def harrisTileShiftInwardsPar(tileX: Int, tileY: Int, mapPar: Int => ToBeTyped[Expr],
   def harrisTileShiftInwardsPar(tileX: Nat, tileY: Nat, mapPar: Nat => ToBeTyped[Expr],

To Reproduce Execute Test harris tuning in branch harris_tuning

Output

[...]
rise.core.types.InferenceException was thrown.
inference exception: could not solve constraints List(((dt1574 -> dt1575) -> (n1573.dt1574 -> n1573.dt1575))  ~  (nat -> ((n2293.(n1423+n1424).dt2295 -> n1579.n1423.dt1580) -> ((1+(((-1+n1372)) / (tuned_tileY))).(4+tuned_tileY).n1373.3.f32 -> (1+(((-1+n1372)) / (tuned_tileY))).tuned_tileY.(-4+n1373).f32))), ((dt1658 -> dt1659) -> (n1657.dt1658 -> n1657.dt1659))  ~  (nat -> (((4+tuned_tileX).(4+tuned_tileY).3.f32 -> tuned_tileX.tuned_tileY.f32) -> ((1+(((-1+n1423)) / (tuned_tileX))).(n1424+tuned_tileX).n2293.dt2295 -> (1+(((-1+n1423)) / (tuned_tileX))).tuned_tileX.n1579.dt1580))))
Bastacyclop commented 3 years ago

If you dissect the inference exception, the problem is in solving:

((dt1574 -> dt1575) -> ...)  ~  (nat -> ...)
((dt1658 -> dt1659) -> ...)  ~  (nat -> ...)

So, it looks like a nat is given as argument to a non-nat-dependent function, or in the opposite direction a nat is not given to a nat-dependent function.

Bastacyclop commented 3 years ago

Here is a fix: https://github.com/rise-lang/shine/commit/241410c6980fc52fbff2470bb04892599ba75b2a mapGlobal is not a nat-dependent function, it is a collection of primitives indexed by an Int dimension.