diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/coq/misc/Loops.v | 8 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 14 |
2 files changed, 6 insertions, 16 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index ec8fa39c..29f312bf 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -63,7 +63,7 @@ Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := . (** [loops::clear] *) -Definition clear_loop_fwd_back +Fixpoint clear_loop_fwd_back (n : nat) (v : vec u32) (i : usize) : result (vec u32) := match n with | O => Fail_ OutOfFuel @@ -73,16 +73,14 @@ Definition clear_loop_fwd_back then ( i1 <- usize_add i 1%usize; v0 <- vec_index_mut_back u32 v i (0%u32); - v1 <- clear_loop_fwd n0 v0 i1; - let _ := v1 in - Return v0) + clear_loop_fwd_back n0 v0 i1) else Return v end . (** [loops::clear] *) Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) := - v0 <- clear_loop_fwd n v (0%usize); let _ := v0 in Return v + clear_loop_fwd_back n v (0%usize) . (** [loops::List] *) diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index d19e9328..c0aca975 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -70,7 +70,7 @@ let sum_with_shared_borrows_fwd (max : u32) : result u32 = sum_with_shared_borrows_loop_fwd max 0 0 (** [loops::clear] *) -let clear_loop_fwd_back +let rec clear_loop_fwd_back (v : vec u32) (i : usize) : Tot (result (vec u32)) (decreases (clear_decreases v i)) = @@ -82,21 +82,13 @@ let clear_loop_fwd_back | Return i1 -> begin match vec_index_mut_back u32 v i 0 with | Fail e -> Fail e - | Return v0 -> - begin match clear_loop_fwd v0 i1 with - | Fail e -> Fail e - | Return _ -> Return v0 - end + | Return v0 -> clear_loop_fwd_back v0 i1 end end else Return v (** [loops::clear] *) -let clear_fwd_back (v : vec u32) : result (vec u32) = - begin match clear_loop_fwd v 0 with - | Fail e -> Fail e - | Return _ -> Return v - end +let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0 (** [loops::list_mem] *) let rec list_mem_loop_fwd |