summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2023-08-18 12:23:03 +0200
committerSon Ho2023-08-18 12:23:03 +0200
commit8543092569616ef6a75949a72532f7b73dc696f2 (patch)
treea19129e9e291e51018f44cde6bd6471b2f35cd37 /tests
parenta9c256fe95523842a1ff025e73f6e9ce7c2db38a (diff)
Regenerate the array tests
Diffstat (limited to '')
-rw-r--r--tests/coq/array/Array_Funs.v9
-rw-r--r--tests/fstar/array/Array.Funs.fst8
-rw-r--r--tests/lean/Array/Funs.lean8
3 files changed, 25 insertions, 0 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v
index d47e4633..6ff3066a 100644
--- a/tests/coq/array/Array_Funs.v
+++ b/tests/coq/array/Array_Funs.v
@@ -451,6 +451,15 @@ Definition f3_fwd (n : nat) : result u32 :=
sum2_fwd n s s0
.
+(** [array::SZ] *)
+Definition sz_body : result usize := Return 32%usize.
+Definition sz_c : usize := sz_body%global.
+
+(** [array::f5]: forward function *)
+Definition f5_fwd (x : array u32 32%usize) : result u32 :=
+ array_index_shared u32 32%usize x 0%usize
+.
+
(** [array::ite]: forward function *)
Definition ite_fwd : result unit :=
s <-
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst
index 72163585..83256398 100644
--- a/tests/fstar/array/Array.Funs.fst
+++ b/tests/fstar/array/Array.Funs.fst
@@ -347,6 +347,14 @@ let f3_fwd : result u32 =
]) 16 18 in
sum2_fwd s s0
+(** [array::SZ] *)
+let sz_body : result usize = Return 32
+let sz_c : usize = eval_global sz_body
+
+(** [array::f5]: forward function *)
+let f5_fwd (x : array u32 32) : result u32 =
+ array_index_shared u32 32 x 0
+
(** [array::ite]: forward function *)
let ite_fwd : result unit =
let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in
diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean
index 8d10c660..a42072d1 100644
--- a/tests/lean/Array/Funs.lean
+++ b/tests/lean/Array/Funs.lean
@@ -447,6 +447,14 @@ def f3 : Result U32 :=
]) (Usize.ofInt 16) (Usize.ofInt 18)
sum2 s s0
+/- [array::SZ] -/
+def sz_body : Result Usize := Result.ret (Usize.ofInt 32)
+def sz_c : Usize := eval_global sz_body (by simp)
+
+/- [array::f5]: forward function -/
+def f5 (x : Array U32 (Usize.ofInt 32)) : Result U32 :=
+ Array.index_shared U32 (Usize.ofInt 32) x (Usize.ofInt 0)
+
/- [array::ite]: forward function -/
def ite : Result Unit :=
do