From f8b7206e0d92aa33812047c521a3c2278fdb6327 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sat, 7 Jan 2023 16:47:33 +0100 Subject: Improve the heuristic to find pretty names for the variables in the loops --- tests/fstar/misc/Loops.Funs.fst | 159 ++++++++++++++++++++-------------------- 1 file changed, 81 insertions(+), 78 deletions(-) (limited to 'tests/fstar/misc/Loops.Funs.fst') diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index b7dcd045..ca918e35 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -92,11 +92,11 @@ 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 - (i : u32) (ls : list_t u32) : - Tot (result bool) (decreases (list_mem_decreases i ls)) + (x : u32) (ls : list_t u32) : + Tot (result bool) (decreases (list_mem_decreases x ls)) = begin match ls with - | ListCons y tl -> if y = i then Return true else list_mem_loop_fwd i tl + | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl | ListNil -> Return false end @@ -222,12 +222,13 @@ let get_elem_mut_back (** [loops::get_elem_shared] *) let rec get_elem_shared_loop_fwd - (x : usize) (v : vec (list_t usize)) (l : list_t usize) (ls : list_t usize) : - Tot (result usize) (decreases (get_elem_shared_decreases x v l ls)) + (x : usize) (slots : vec (list_t usize)) (ls : list_t usize) + (ls0 : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0)) = - begin match ls with + begin match ls0 with | ListCons y tl -> - if y = x then Return y else get_elem_shared_loop_fwd x v l tl + if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl | ListNil -> Fail Failure end @@ -311,17 +312,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) (l : list_t t) (i : u32) (ls : list_t t) : - Tot (result t) (decreases (list_nth_shared_loop_with_id_decreases t l i ls)) + (t : Type0) (ls : list_t t) (i : u32) (ls0 : list_t t) : + Tot (result t) + (decreases (list_nth_shared_loop_with_id_decreases t ls i ls0)) = - begin match ls with + begin match ls0 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 l i0 tl + | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t ls i0 tl end | ListNil -> Fail Failure end @@ -336,12 +338,13 @@ let list_nth_shared_loop_with_id_fwd (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : - Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -362,13 +365,13 @@ let list_nth_mut_loop_pair_fwd (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_back'a - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -378,7 +381,7 @@ let rec list_nth_mut_loop_pair_loop_back'a | Return i0 -> begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -395,13 +398,13 @@ let list_nth_mut_loop_pair_back'a (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_back'b - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -411,7 +414,7 @@ let rec list_nth_mut_loop_pair_loop_back'b | Return i0 -> begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure @@ -428,13 +431,13 @@ let list_nth_mut_loop_pair_back'b (** [loops::list_nth_shared_loop_pair] *) let rec list_nth_shared_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -455,13 +458,13 @@ let list_nth_shared_loop_pair_fwd (** [loops::list_nth_mut_loop_pair_merge] *) let rec list_nth_mut_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -482,13 +485,13 @@ let list_nth_mut_loop_pair_merge_fwd (** [loops::list_nth_mut_loop_pair_merge] *) let rec list_nth_mut_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : (t & t)) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : Tot (result ((list_t t) & (list_t t))) - (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1) @@ -499,7 +502,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return (l1, l2) -> Return (ListCons x0 l1, ListCons x1 l2) + | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0) end end | ListNil -> Fail Failure @@ -516,13 +519,13 @@ let list_nth_mut_loop_pair_merge_back (** [loops::list_nth_shared_loop_pair_merge] *) let rec list_nth_shared_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -543,13 +546,13 @@ let list_nth_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair] *) let rec list_nth_mut_shared_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -570,13 +573,13 @@ let list_nth_mut_shared_loop_pair_fwd (** [loops::list_nth_mut_shared_loop_pair] *) let rec list_nth_mut_shared_loop_pair_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -587,7 +590,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -604,13 +607,13 @@ let list_nth_mut_shared_loop_pair_back (** [loops::list_nth_mut_shared_loop_pair_merge] *) let rec list_nth_mut_shared_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -632,13 +635,13 @@ let list_nth_mut_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair_merge] *) let rec list_nth_mut_shared_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -649,7 +652,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back begin match list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -666,13 +669,13 @@ let list_nth_mut_shared_loop_pair_merge_back (** [loops::list_nth_shared_mut_loop_pair] *) let rec list_nth_shared_mut_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -693,13 +696,13 @@ let list_nth_shared_mut_loop_pair_fwd (** [loops::list_nth_shared_mut_loop_pair] *) let rec list_nth_shared_mut_loop_pair_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -710,7 +713,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure @@ -727,13 +730,13 @@ let list_nth_shared_mut_loop_pair_back (** [loops::list_nth_shared_mut_loop_pair_merge] *) let rec list_nth_shared_mut_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -755,13 +758,13 @@ let list_nth_shared_mut_loop_pair_merge_fwd (** [loops::list_nth_shared_mut_loop_pair_merge] *) let rec list_nth_shared_mut_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -772,7 +775,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back begin match list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure -- cgit v1.2.3