diff options
Diffstat (limited to '')
-rw-r--r-- | tests/coq/array/Array.v (renamed from tests/coq/array/Array_Funs.v) | 36 | ||||
-rw-r--r-- | tests/coq/array/Array_Types.v | 14 | ||||
-rw-r--r-- | tests/coq/array/_CoqProject | 3 |
3 files changed, 16 insertions, 37 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 . diff --git a/tests/coq/array/Array_Types.v b/tests/coq/array/Array_Types.v deleted file mode 100644 index a13d64e6..00000000 --- a/tests/coq/array/Array_Types.v +++ /dev/null @@ -1,14 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [array]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module Array_Types. - -(** [array::AB] *) -Inductive AB_t := | AB_A : AB_t | AB_B : AB_t. - -End Array_Types . diff --git a/tests/coq/array/_CoqProject b/tests/coq/array/_CoqProject index f33cefe6..87d8fc3d 100644 --- a/tests/coq/array/_CoqProject +++ b/tests/coq/array/_CoqProject @@ -3,6 +3,5 @@ -arg -w -arg all -Array_Funs.v Primitives.v -Array_Types.v +Array.v |