More tests for the VampIR compilation pipeline (#2197)

test/VampIR/Compilation/Positive.hs

@@ -164,5 +164,17 @@ tests =
       "Test020: boolean target"
       $(mkRelDir ".")
       $(mkRelFile "test020.juvix")
-      $(mkRelFile "data/test020.json")
+      $(mkRelFile "data/test020.json"),
+    posTest
+      11
+      "Test021: fast exponentiation (exponential unrolling)"
+      $(mkRelDir ".")
+      $(mkRelFile "test021.juvix")
+      $(mkRelFile "data/test021.json"),
+    posTest
+      10
+      "Test022: fast exponentiation"
+      $(mkRelDir ".")
+      $(mkRelFile "test022.juvix")
+      $(mkRelFile "data/test022.json")
   ]

tests/VampIR/positive/Compilation/data/test021.json

@@ -0,0 +1,5 @@
+{
+    "in1": "5",
+    "in2": "3",
+    "out": "125"
+}

tests/VampIR/positive/Compilation/data/test022.json

@@ -0,0 +1,5 @@
+{
+    "in1": "5",
+    "in2": "11",
+    "out": "48828125"
+}

tests/VampIR/positive/Compilation/test021.juvix

@@ -0,0 +1,23 @@
+-- fast exponentiation (exponential unrolling blow-up)
+module test021;
+
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
+
+{-# unroll: 4 #-}
+terminating
+power' : Nat → Nat → Nat → Nat;
+power' acc a b :=
+  if
+    (b == 0)
+    acc
+    (if
+      (mod b 2 == 0)
+      (power' acc (a * a) (div b 2))
+      (power' (acc * a) (a * a) (div b 2)));
+
+power : Nat → Nat → Nat;
+power := power' 1;
+
+main : Nat -> Nat -> Nat;
+main := power;

tests/VampIR/positive/Compilation/test022.juvix

@@ -0,0 +1,19 @@
+-- fast exponentiation
+module test022;
+
+import Stdlib.Prelude open;
+import Stdlib.Data.Nat.Ord open;
+
+{-# unroll: 10 #-}
+terminating
+power' : Nat → Nat → Nat → Nat;
+power' acc a b :=
+  let
+    acc' : Nat := if (mod b 2 == 0) acc (acc * a);
+  in if (b == 0) acc (power' acc' (a * a) (div b 2));
+
+power : Nat → Nat → Nat;
+power := power' 1;
+
+main : Nat -> Nat -> Nat;
+main := power;