diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/array/Array.v (renamed from tests/coq/array/Array_Funs.v) | 36 |
1 files changed, 15 insertions, 21 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array.v index 9980a6e8..825f73e0 100644 --- a/tests/coq/array/Array_Funs.v +++ b/tests/coq/array/Array.v @@ -1,14 +1,15 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [array]: function definitions *) +(** [array] *) 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. +Module Array. + +(** [array::AB] *) +Inductive AB_t := | AB_A : AB_t | AB_B : AB_t. (** [array::incr]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) @@ -98,7 +99,7 @@ Definition index_mut_slice_back (** [array::slice_subslice_shared_]: forward function *) Definition slice_subslice_shared_ - (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := core_slice_index_Slice_index u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32) x {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} @@ -106,7 +107,7 @@ Definition slice_subslice_shared_ (** [array::slice_subslice_mut_]: forward function *) Definition slice_subslice_mut_ - (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32) x {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} @@ -114,7 +115,7 @@ Definition slice_subslice_mut_ (** [array::slice_subslice_mut_]: backward function 0 *) Definition slice_subslice_mut__back - (n : nat) (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : + (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : result (slice u32) := core_slice_index_Slice_index_mut_back u32 (core_ops_range_Range usize) @@ -141,9 +142,7 @@ Definition array_to_slice_mut__back (** [array::array_subslice_shared_]: forward function *) Definition array_subslice_shared_ - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -152,9 +151,7 @@ Definition array_subslice_shared_ (** [array::array_subslice_mut_]: forward function *) Definition array_subslice_mut_ - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index_mut u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexMutInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -163,8 +160,7 @@ Definition array_subslice_mut_ (** [array::array_subslice_mut_]: backward function 0 *) Definition array_subslice_mut__back - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) - : + (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) : result (array u32 32%usize) := core_array_Array_index_mut_back u32 (core_ops_range_Range usize) 32%usize @@ -310,7 +306,7 @@ Definition update_all : result unit := . (** [array::range_all]: forward function *) -Definition range_all (n : nat) : result unit := +Definition range_all : result unit := s <- core_array_Array_index_mut u32 (core_ops_range_Range usize) 4%usize (core_slice_index_Slice_coreopsindexIndexMutInst u32 @@ -432,9 +428,7 @@ Definition f2 (i : u32) : result unit := (** [array::f4]: forward function *) Definition f4 - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -449,7 +443,7 @@ Definition f3 (n : nat) : result u32 := _ <- f2 i; let b := array_repeat u32 32%usize 0%u32 in s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); - s0 <- f4 n b 16%usize 18%usize; + s0 <- f4 b 16%usize 18%usize; sum2 n s s0 . @@ -473,4 +467,4 @@ Definition ite : result unit := Return tt . -End Array_Funs . +End Array . |