From abe0c6ff94713807bd4a30675eb29ba290c6a012 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 29 Sep 2023 13:16:44 +0200
Subject: [PATCH 1/3] update mapfun benchmark

---
 tests/benchmark/mapfun/juvix/mapfun.juvix | 25 ++++++++++++-----------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/tests/benchmark/mapfun/juvix/mapfun.juvix b/tests/benchmark/mapfun/juvix/mapfun.juvix
index 7b35aae2bc..b09c92acc9 100644
--- a/tests/benchmark/mapfun/juvix/mapfun.juvix
+++ b/tests/benchmark/mapfun/juvix/mapfun.juvix
@@ -1,35 +1,36 @@
 -- successively map K functions to a list of N integers
 module mapfun;
 
-import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
+import Stdlib.Prelude open hiding {+};
+import Stdlib.Data.Int open;
+import Stdlib.Data.Int.Ord open;
 
 mapfun : {A : Type} → List (A → A) → List A → List A
   | nil xs := xs
   | (f :: fs) xs := mapfun fs (map f xs);
 
-genfs : Nat → List (Nat → Nat)
+genfs : Nat → List (Int → Int)
   | zero := nil
-  | (suc n) := sub (suc n) :: genfs n;
+  | n@(suc n') := (-) (ofNat n) :: genfs n';
 
-step : Nat → (Nat → Nat) → Nat → Nat
-  | n f x := f (x + n);
+step : Nat → (Int → Int) → Int → Int
+  | n f x := f (x + ofNat n);
 
-genffs : Nat → List ((Nat → Nat) → Nat → Nat)
+genffs : Nat → List ((Int → Int) → Int → Int)
   | zero := nil
   | (suc n) := step (suc n) :: genffs n;
 
-sum_go : Nat → List Nat → Nat
+sum_go : Int → List Int → Int
   | acc nil := acc
   | acc (h :: t) := sum_go (acc + h) t;
 
-sum : List Nat → Nat := sum_go 0;
+sum : List Int → Int := sum_go 0;
 
 terminating
-gen : Nat → Nat → List Nat
-  | k n := if (k == n) (k :: nil) (k :: gen (suc k) n);
+gen : Int → Int → List Int
+  | k n := if (k == n) (k :: nil) (k :: gen (k + 1) n);
 
 main : IO :=
-  printNatLn
+  printIntLn
     (sum
       (mapfun (mapfun (genffs 100) (genfs 100)) (gen 1 10000)));

From 93d33f5867e6e57cb1920fbbe4d698c1bfd802f6 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 29 Sep 2023 14:08:25 +0200
Subject: [PATCH 2/3] format

---
 tests/benchmark/maybe/juvix/maybe.juvix         | 4 +---
 tests/benchmark/mergesort/juvix/mergesort.juvix | 1 -
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/tests/benchmark/maybe/juvix/maybe.juvix b/tests/benchmark/maybe/juvix/maybe.juvix
index 01b64a072f..c7670662d2 100644
--- a/tests/benchmark/maybe/juvix/maybe.juvix
+++ b/tests/benchmark/maybe/juvix/maybe.juvix
@@ -17,7 +17,6 @@ gen : Nat → Tree
 
 terminating
 sum : Nat → Tree → Maybe Nat
-  
   | x leaf := just 0
   | x (node y l r) :=
     if (x == y) nothing (step1 x y (sum x l) r);
@@ -35,12 +34,11 @@ maybeStepRun : Nat → Nat → Maybe Nat
   | x y := just (sub y x);
 
 run : Nat → Tree → Maybe Nat
-  
   | zero t := sum 0 t
   | (suc n) t := stepRun (suc n) t (run n t);
 
 stepRun : Nat → Tree → Maybe Nat → Maybe Nat
-  
+
   | n t nothing := sum n t
   | n t (just x) := maybe nothing (maybeStepRun x) (sum n t);
 
diff --git a/tests/benchmark/mergesort/juvix/mergesort.juvix b/tests/benchmark/mergesort/juvix/mergesort.juvix
index 8006ec93de..7acc9bae2b 100644
--- a/tests/benchmark/mergesort/juvix/mergesort.juvix
+++ b/tests/benchmark/mergesort/juvix/mergesort.juvix
@@ -27,7 +27,6 @@ merget : List Nat → List Nat → List Nat → List Nat
 
 terminating
 sort' : List Nat × List Nat → List Nat
-  
   | (l1, l2) := merget (sort l1) (sort l2) nil;
 
 terminating

From 17dd89009a437d22e0a3e1387bd7275d3b032d02 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 29 Sep 2023 14:14:09 +0200
Subject: [PATCH 3/3] update benchmarks

---
 tests/benchmark/combinations/runtime/combinations.c | 2 +-
 tests/benchmark/maybe/runtime/maybe.c               | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/benchmark/combinations/runtime/combinations.c b/tests/benchmark/combinations/runtime/combinations.c
index af664f7550..4b33a2da49 100644
--- a/tests/benchmark/combinations/runtime/combinations.c
+++ b/tests/benchmark/combinations/runtime/combinations.c
@@ -12,7 +12,7 @@ static constr_info_t juvix_constr_info_array[CONSTRS_NUM] = {BUILTIN_UIDS_INFO};
 
 int main() {
     JUVIX_DECL_ARGS;
-    JUVIX_PROLOGUE(2);
+    JUVIX_PROLOGUE(3);
 
     juvix_constrs_num = CONSTRS_NUM;
     juvix_constr_info = juvix_constr_info_array;
diff --git a/tests/benchmark/maybe/runtime/maybe.c b/tests/benchmark/maybe/runtime/maybe.c
index c822155781..7b3d88d638 100644
--- a/tests/benchmark/maybe/runtime/maybe.c
+++ b/tests/benchmark/maybe/runtime/maybe.c
@@ -25,7 +25,7 @@ static constr_info_t juvix_constr_info_array[CONSTRS_NUM] = {
 
 int main() {
     JUVIX_DECL_ARGS;
-    JUVIX_PROLOGUE(2);
+    JUVIX_PROLOGUE(3);
 
     juvix_constrs_num = CONSTRS_NUM;
     juvix_constr_info = juvix_constr_info_array;