diff options
Diffstat (limited to 'tests/fstar')
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 7 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.fst | 7 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 21 |
3 files changed, 15 insertions, 20 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index bc5ed046..053b7663 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -46,8 +46,7 @@ let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat = (** [loops::get_elem_shared]: decreases clause *) unfold -let get_elem_shared_loop_decreases (slots : vec (list_t usize)) (x : usize) - (ls : list_t usize) (ls0 : list_t usize) : nat = +let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat = admit () (** [loops::list_nth_mut_loop_with_id]: decreases clause *) @@ -58,8 +57,8 @@ let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) (** [loops::list_nth_shared_loop_with_id]: decreases clause *) unfold -let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (ls : list_t t) - (i : u32) (ls0 : list_t t) : nat = +let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = admit () (** [loops::list_nth_mut_loop_pair]: decreases clause *) diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst index c748da71..82f34de1 100644 --- a/tests/fstar/misc/Loops.Clauses.fst +++ b/tests/fstar/misc/Loops.Clauses.fst @@ -43,8 +43,7 @@ let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : list_t usize = (** [loops::get_elem_shared]: decreases clause *) unfold -let get_elem_shared_loop_decreases (slots : vec (list_t usize)) (x : usize) - (ls : list_t usize) (ls0 : list_t usize) : list_t usize = +let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : list_t usize = ls (** [loops::list_nth_mut_loop_with_id]: decreases clause *) @@ -55,8 +54,8 @@ let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) (ls : list_t (** [loops::list_nth_shared_loop_with_id]: decreases clause *) unfold -let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (l : list_t t) - (i : u32) (ls : list_t t) : list_t t = +let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : list_t t = ls (** [loops::list_nth_mut_loop_pair]: decreases clause *) diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index ebf30654..73539cf6 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -222,14 +222,11 @@ let get_elem_mut_back (** [loops::get_elem_shared] *) let rec get_elem_shared_loop_fwd - (slots : vec (list_t usize)) (x : usize) (ls : list_t usize) - (ls0 : list_t usize) : - Tot (result usize) - (decreases (get_elem_shared_loop_decreases slots x ls ls0)) + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) = begin match ls with - | ListCons y tl -> - if y = x then Return y else get_elem_shared_loop_fwd slots x tl ls0 + | ListCons y tl -> if y = x then Return y else get_elem_shared_loop_fwd x tl | ListNil -> Fail Failure end @@ -238,7 +235,7 @@ let get_elem_shared_fwd (slots : vec (list_t usize)) (x : usize) : result usize = begin match vec_index_fwd (list_t usize) slots 0 with | Fail e -> Fail e - | Return l -> get_elem_shared_loop_fwd slots x l l + | Return l -> get_elem_shared_loop_fwd x l end (** [loops::id_mut] *) @@ -313,18 +310,18 @@ let list_nth_mut_loop_with_id_back (** [loops::list_nth_shared_loop_with_id] *) let rec list_nth_shared_loop_with_id_loop_fwd - (t : Type0) (ls : list_t t) (i : u32) (ls0 : list_t t) : + (t : Type0) (i : u32) (ls : list_t t) : Tot (result t) - (decreases (list_nth_shared_loop_with_id_loop_decreases t ls i ls0)) + (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls)) = - begin match ls0 with + begin match ls with | ListCons x tl -> if i = 0 then Return x else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t ls i0 tl + | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t i0 tl end | ListNil -> Fail Failure end @@ -334,7 +331,7 @@ let list_nth_shared_loop_with_id_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = begin match id_shared_fwd t ls with | Fail e -> Fail e - | Return ls0 -> list_nth_shared_loop_with_id_loop_fwd t ls i ls0 + | Return ls0 -> list_nth_shared_loop_with_id_loop_fwd t i ls0 end (** [loops::list_nth_mut_loop_pair] *) |