Generate the array test files for Coq and F*

1 files changed, 300 insertions, 0 deletions

diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v
new file mode 100644
index 00000000..4a862d1b
--- /dev/null
+++ b/tests/coq/array/Array_Funs.v
@@ -0,0 +1,300 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [array]: function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export Array_Types.
+Import Array_Types.
+Module Array_Funs.
+
+(** [array::array_to_shared_slice_]: forward function *)
+Definition array_to_shared_slice__fwd
+  (T : Type) (s : array T 32%usize) : result (slice T) :=
+  array_to_slice_shared T 32%usize s
+.
+
+(** [array::array_to_mut_slice_]: forward function *)
+Definition array_to_mut_slice__fwd
+  (T : Type) (s : array T 32%usize) : result (slice T) :=
+  array_to_slice_mut_fwd T 32%usize s
+.
+
+(** [array::array_to_mut_slice_]: backward function 0 *)
+Definition array_to_mut_slice__back
+  (T : Type) (s : array T 32%usize) (ret : slice T) :
+  result (array T 32%usize)
+  :=
+  array_to_slice_mut_back T 32%usize s ret
+.
+
+(** [array::array_len]: forward function *)
+Definition array_len_fwd (T : Type) (s : array T 32%usize) : result usize :=
+  s0 <- array_to_slice_shared T 32%usize s; let i := slice_len T s0 in Return i
+.
+
+(** [array::shared_array_len]: forward function *)
+Definition shared_array_len_fwd
+  (T : Type) (s : array T 32%usize) : result usize :=
+  s0 <- array_to_slice_shared T 32%usize s; let i := slice_len T s0 in Return i
+.
+
+(** [array::shared_slice_len]: forward function *)
+Definition shared_slice_len_fwd (T : Type) (s : slice T) : result usize :=
+  let i := slice_len T s in Return i
+.
+
+(** [array::index_array_shared]: forward function *)
+Definition index_array_shared_fwd
+  (T : Type) (s : array T 32%usize) (i : usize) : result T :=
+  array_index_shared T 32%usize s i
+.
+
+(** [array::index_array_u32]: forward function *)
+Definition index_array_u32_fwd
+  (s : array u32 32%usize) (i : usize) : result u32 :=
+  array_index_shared u32 32%usize s i
+.
+
+(** [array::index_array_generic]: forward function *)
+Definition index_array_generic_fwd
+  (N : usize) (s : array u32 N) (i : usize) : result u32 :=
+  array_index_shared u32 N s i
+.
+
+(** [array::index_array_generic_call]: forward function *)
+Definition index_array_generic_call_fwd
+  (N : usize) (s : array u32 N) (i : usize) : result u32 :=
+  index_array_generic_fwd N s i
+.
+
+(** [array::index_array_copy]: forward function *)
+Definition index_array_copy_fwd (x : array u32 32%usize) : result u32 :=
+  array_index_shared u32 32%usize x 0%usize
+.
+
+(** [array::index_mut_array]: forward function *)
+Definition index_mut_array_fwd
+  (T : Type) (s : array T 32%usize) (i : usize) : result T :=
+  array_index_mut_fwd T 32%usize s i
+.
+
+(** [array::index_mut_array]: backward function 0 *)
+Definition index_mut_array_back
+  (T : Type) (s : array T 32%usize) (i : usize) (ret : T) :
+  result (array T 32%usize)
+  :=
+  array_index_mut_back T 32%usize s i ret
+.
+
+(** [array::index_slice]: forward function *)
+Definition index_slice_fwd (T : Type) (s : slice T) (i : usize) : result T :=
+  slice_index_shared T s i
+.
+
+(** [array::index_mut_slice]: forward function *)
+Definition index_mut_slice_fwd
+  (T : Type) (s : slice T) (i : usize) : result T :=
+  slice_index_mut_fwd T s i
+.
+
+(** [array::index_mut_slice]: backward function 0 *)
+Definition index_mut_slice_back
+  (T : Type) (s : slice T) (i : usize) (ret : T) : result (slice T) :=
+  slice_index_mut_back T s i ret
+.
+
+(** [array::slice_subslice_shared_]: forward function *)
+Definition slice_subslice_shared__fwd
+  (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
+  slice_subslice_shared u32 x (mk_range y z)
+.
+
+(** [array::slice_subslice_mut_]: forward function *)
+Definition slice_subslice_mut__fwd
+  (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
+  slice_subslice_mut_fwd u32 x (mk_range y z)
+.
+
+(** [array::slice_subslice_mut_]: backward function 0 *)
+Definition slice_subslice_mut__back
+  (x : slice u32) (y : usize) (z : usize) (ret : slice u32) :
+  result (slice u32)
+  :=
+  slice_subslice_mut_back u32 x (mk_range y z) ret
+.
+
+(** [array::array_to_slice_shared_]: forward function *)
+Definition array_to_slice_shared__fwd
+  (x : array u32 32%usize) : result (slice u32) :=
+  array_to_slice_shared u32 32%usize x
+.
+
+(** [array::array_to_slice_mut_]: forward function *)
+Definition array_to_slice_mut__fwd
+  (x : array u32 32%usize) : result (slice u32) :=
+  array_to_slice_mut_fwd u32 32%usize x
+.
+
+(** [array::array_to_slice_mut_]: backward function 0 *)
+Definition array_to_slice_mut__back
+  (x : array u32 32%usize) (ret : slice u32) : result (array u32 32%usize) :=
+  array_to_slice_mut_back u32 32%usize x ret
+.
+
+(** [array::array_subslice_shared_]: forward function *)
+Definition array_subslice_shared__fwd
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
+  array_subslice_shared u32 32%usize x (mk_range y z)
+.
+
+(** [array::array_subslice_mut_]: forward function *)
+Definition array_subslice_mut__fwd
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
+  array_subslice_mut_fwd u32 32%usize x (mk_range y z)
+.
+
+(** [array::array_subslice_mut_]: backward function 0 *)
+Definition array_subslice_mut__back
+  (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) :
+  result (array u32 32%usize)
+  :=
+  array_subslice_mut_back u32 32%usize x (mk_range y z) ret
+.
+
+(** [array::index_slice_0]: forward function *)
+Definition index_slice_0_fwd (T : Type) (s : slice T) : result T :=
+  slice_index_shared T s 0%usize
+.
+
+(** [array::index_array_0]: forward function *)
+Definition index_array_0_fwd (T : Type) (s : array T 32%usize) : result T :=
+  array_index_shared T 32%usize s 0%usize
+.
+
+(** [array::index_index_array]: forward function *)
+Definition index_index_array_fwd
+  (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) :
+  result u32
+  :=
+  a <- array_index_shared (array u32 32%usize) 32%usize s i;
+  array_index_shared u32 32%usize a j
+.
+
+(** [array::update_update_array]: forward function *)
+Definition update_update_array_fwd
+  (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) :
+  result unit
+  :=
+  a <- array_index_mut_fwd (array u32 32%usize) 32%usize s i;
+  a0 <- array_index_mut_back u32 32%usize a j 0%u32;
+  _ <- array_index_mut_back (array u32 32%usize) 32%usize s i a0;
+  Return tt
+.
+
+(** [array::array_local_deep_copy]: forward function *)
+Definition array_local_deep_copy_fwd (x : array u32 32%usize) : result unit :=
+  Return tt
+.
+
+(** [array::f0]: forward function *)
+Definition f0_fwd : result unit :=
+  s <-
+    array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]);
+  s0 <- slice_index_mut_back u32 s 0%usize 1%u32;
+  _ <-
+    array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ])
+      s0;
+  Return tt
+.
+
+(** [array::f1]: forward function *)
+Definition f1_fwd : result unit :=
+  _ <-
+    array_index_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ])
+      0%usize 1%u32;
+  Return tt
+.
+
+(** [array::sum]: loop 0: forward function *)
+Fixpoint sum_loop_fwd
+  (n : nat) (s : slice u32) (sum : u32) (i : usize) : result u32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := slice_len u32 s in
+    if i s< i0
+    then (
+      i1 <- slice_index_shared u32 s i;
+      sum0 <- u32_add sum i1;
+      i2 <- usize_add i 1%usize;
+      sum_loop_fwd n0 s sum0 i2)
+    else Return sum
+  end
+.
+
+(** [array::sum]: forward function *)
+Definition sum_fwd (n : nat) (s : slice u32) : result u32 :=
+  sum_loop_fwd n s 0%u32 0%usize
+.
+
+(** [array::sum2]: loop 0: forward function *)
+Fixpoint sum2_loop_fwd
+  (n : nat) (s : slice u32) (s2 : slice u32) (sum : u32) (i : usize) :
+  result u32
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := slice_len u32 s in
+    if i s< i0
+    then (
+      i1 <- slice_index_shared u32 s i;
+      i2 <- slice_index_shared u32 s2 i;
+      i3 <- u32_add i1 i2;
+      sum0 <- u32_add sum i3;
+      i4 <- usize_add i 1%usize;
+      sum2_loop_fwd n0 s s2 sum0 i4)
+    else Return sum
+  end
+.
+
+(** [array::sum2]: forward function *)
+Definition sum2_fwd (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
+  let i := slice_len u32 s in
+  let i0 := slice_len u32 s2 in
+  if negb (i s= i0) then Fail_ Failure else sum2_loop_fwd n s s2 0%u32 0%usize
+.
+
+(** [array::f2]: forward function *)
+Definition f2_fwd (i : u32) : result unit :=
+  Return tt.
+
+(** [array::f4]: forward function *)
+Definition f4_fwd
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
+  array_subslice_shared u32 32%usize x (mk_range y z)
+.
+
+(** [array::f3]: forward function *)
+Definition f3_fwd (n : nat) : result u32 :=
+  i <-
+    array_index_shared u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ])
+      0%usize;
+  _ <- f2_fwd i;
+  s <-
+    array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]);
+  s0 <-
+    f4_fwd
+      (mk_array u32 32%usize [
+        0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32;
+        0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32;
+        0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32;
+        0%u32; 0%u32
+        ]) 16%usize 18%usize;
+  sum2_fwd n s s0
+.
+
+End Array_Funs .