Update benchmarks

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;

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)));

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);
 

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;

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