addv example

float-safe-optimizer/Optimize.scala

@@ -10,19 +10,32 @@ object Optimize {
     val rules = {
       import rise.eqsat.rules._
       Seq(
-        mapFusion,
+        // implementation choices:
         reduceSeq,
         mapSeq,
+        // satisfying read/write annotations:
         mapSeqArray,
+        // simplifications:
+        mapFusion,
+        reduceSeqMapFusion,
         removeTransposePair,
         fstReduction,
         sndReduction,
       /* maybe:
         omp.mapPar --> need heuristic vs mapSeq
-        toMemAfterMapSeq
+        toMemAfterMapSeq / storeToMem
         storeToMem
         reduceSeqMapFusion
-        reduceSeqUnroll --> need heuristic
+        mapSeqUnroll/reduceSeqUnroll --> need heuristic
+        eliminateMapIdentity
+
+        is it worth the cost?:
+        betaExtract
+        betaNatExtract
+        eta
+
+        not generic enough, use Elevate passes or custom applier?:
+        idxReduction_i_n
       */
       )
     }

float-safe-optimizer/examples/addv.rise

@@ -0,0 +1,4 @@
+depFun((n: Nat) => depFun((m: Nat) => depFun((o: Nat) =>
+  fun(((n+o)`.`i32) ->: ((m+o)`.`i32) ->: (o`.`i32))((a, b) =>
+  zip(take(o)(a))(take(o)(b)) |> map(fun(x => fst(x) + snd(x)))
+))))