diff options
Diffstat (limited to '')
-rw-r--r-- | tests/coq/array/Array_Funs.v | 300 |
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 . |