diff options
Diffstat (limited to 'tests/coq/array/Array_Funs.v')
| -rw-r--r-- | tests/coq/array/Array_Funs.v | 467 |
1 files changed, 0 insertions, 467 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v deleted file mode 100644 index 6d791873..00000000 --- a/tests/coq/array/Array_Funs.v +++ /dev/null @@ -1,467 +0,0 @@ -(** 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::take_array]: forward function *) -Definition take_array_fwd (a : array u32 2%usize) : result unit := - Return tt. - -(** [array::take_array_borrow]: forward function *) -Definition take_array_borrow_fwd (a : array u32 2%usize) : result unit := - Return tt -. - -(** [array::take_slice]: forward function *) -Definition take_slice_fwd (s : slice u32) : result unit := - Return tt. - -(** [array::take_mut_slice]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) -Definition take_mut_slice_fwd_back (s : slice u32) : result (slice u32) := - Return s -. - -(** [array::take_all]: forward function *) -Definition take_all_fwd : result unit := - _ <- take_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- take_array_borrow_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s <- - array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - _ <- take_slice_fwd s; - s0 <- - array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s1 <- take_mut_slice_fwd_back s0; - _ <- - array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) - s1; - Return tt -. - -(** [array::index_array]: forward function *) -Definition index_array_fwd (x : array u32 2%usize) : result u32 := - array_index_shared u32 2%usize x 0%usize -. - -(** [array::index_array_borrow]: forward function *) -Definition index_array_borrow_fwd (x : array u32 2%usize) : result u32 := - array_index_shared u32 2%usize x 0%usize -. - -(** [array::index_slice_u32_0]: forward function *) -Definition index_slice_u32_0_fwd (x : slice u32) : result u32 := - slice_index_shared u32 x 0%usize -. - -(** [array::index_mut_slice_u32_0]: forward function *) -Definition index_mut_slice_u32_0_fwd (x : slice u32) : result u32 := - slice_index_shared u32 x 0%usize -. - -(** [array::index_mut_slice_u32_0]: backward function 0 *) -Definition index_mut_slice_u32_0_back (x : slice u32) : result (slice u32) := - _ <- slice_index_shared u32 x 0%usize; Return x -. - -(** [array::index_all]: forward function *) -Definition index_all_fwd : result u32 := - i <- index_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i0 <- index_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i1 <- u32_add i i0; - i2 <- index_array_borrow_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i3 <- u32_add i1 i2; - s <- - array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i4 <- index_slice_u32_0_fwd s; - i5 <- u32_add i3 i4; - s0 <- - array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - i6 <- index_mut_slice_u32_0_fwd s0; - i7 <- u32_add i5 i6; - s1 <- index_mut_slice_u32_0_back s0; - _ <- - array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) - s1; - Return i7 -. - -(** [array::update_array]: forward function *) -Definition update_array_fwd (x : array u32 2%usize) : result unit := - _ <- array_index_mut_back u32 2%usize x 0%usize 1%u32; Return tt -. - -(** [array::update_array_mut_borrow]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) -Definition update_array_mut_borrow_fwd_back - (x : array u32 2%usize) : result (array u32 2%usize) := - array_index_mut_back u32 2%usize x 0%usize 1%u32 -. - -(** [array::update_mut_slice]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) -Definition update_mut_slice_fwd_back (x : slice u32) : result (slice u32) := - slice_index_mut_back u32 x 0%usize 1%u32 -. - -(** [array::update_all]: forward function *) -Definition update_all_fwd : result unit := - _ <- update_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - x <- - update_array_mut_borrow_fwd_back (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s <- array_to_slice_mut_fwd u32 2%usize x; - s0 <- update_mut_slice_fwd_back s; - _ <- array_to_slice_mut_back u32 2%usize x s0; - Return tt -. - -(** [array::range_all]: forward function *) -Definition range_all_fwd : result unit := - s <- - array_subslice_mut_fwd u32 4%usize - (mk_array u32 4%usize [ 0%u32; 0%u32; 0%u32; 0%u32 ]) (mk_range 1%usize - 3%usize); - s0 <- update_mut_slice_fwd_back s; - _ <- - array_subslice_mut_back u32 4%usize - (mk_array u32 4%usize [ 0%u32; 0%u32; 0%u32; 0%u32 ]) (mk_range 1%usize - 3%usize) s0; - Return tt -. - -(** [array::deref_array_borrow]: forward function *) -Definition deref_array_borrow_fwd (x : array u32 2%usize) : result u32 := - array_index_shared u32 2%usize x 0%usize -. - -(** [array::deref_array_mut_borrow]: forward function *) -Definition deref_array_mut_borrow_fwd (x : array u32 2%usize) : result u32 := - array_index_shared u32 2%usize x 0%usize -. - -(** [array::deref_array_mut_borrow]: backward function 0 *) -Definition deref_array_mut_borrow_back - (x : array u32 2%usize) : result (array u32 2%usize) := - _ <- array_index_shared u32 2%usize x 0%usize; Return x -. - -(** [array::take_array_t]: forward function *) -Definition take_array_t_fwd (a : array T_t 2%usize) : result unit := - Return tt. - -(** [array::non_copyable_array]: forward function *) -Definition non_copyable_array_fwd : result unit := - _ <- take_array_t_fwd (mk_array T_t 2%usize [ TA; TB ]); 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::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::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 -. - -(** [array::ite]: forward function *) -Definition ite_fwd : result unit := - s <- - array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s0 <- - array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - s1 <- index_mut_slice_u32_0_back s0; - _ <- - array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) - s1; - s2 <- index_mut_slice_u32_0_back s; - _ <- - array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) - s2; - Return tt -. - -End Array_Funs . |