From f3eb7aed4082e8f014d03c3c6045852687989a5b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Jan 2023 21:17:30 +0100 Subject: Implement support for nested borrows in loops, and add loop tests --- tests/coq/misc/Loops.v | 380 +++++++++++++++++++++++++++- tests/fstar/misc/Loops.Clauses.Template.fst | 51 +++- tests/fstar/misc/Loops.Clauses.fst | 51 +++- tests/fstar/misc/Loops.Funs.fst | 356 +++++++++++++++++++++++++- 4 files changed, 820 insertions(+), 18 deletions(-) (limited to 'tests') diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 67ee0880..4fc68e1c 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -22,8 +22,8 @@ Definition sum_fwd (n : nat) (max : u32) : result u32 := sum_loop_fwd n max (0%u32) (0%u32) . -(** [loops::sum_with_borrows] *) -Fixpoint sum_with_borrows_loop_fwd +(** [loops::sum_with_mut_borrows] *) +Fixpoint sum_with_mut_borrows_loop_fwd (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := match n with | O => Fail_ OutOfFuel @@ -32,14 +32,34 @@ Fixpoint sum_with_borrows_loop_fwd then ( ms0 <- u32_add ms mi; mi0 <- u32_add mi 1%u32; - sum_with_borrows_loop_fwd n0 max mi0 ms0) + sum_with_mut_borrows_loop_fwd n0 max mi0 ms0) else u32_mul ms 2%u32 end . -(** [loops::sum_with_borrows] *) -Definition sum_with_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_borrows_loop_fwd n max (0%u32) (0%u32) +(** [loops::sum_with_mut_borrows] *) +Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 := + sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32) +. + +(** [loops::sum_with_shared_borrows] *) +Fixpoint sum_with_shared_borrows_loop_fwd + (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + if i s< max + then ( + i0 <- u32_add i 1%u32; + s0 <- u32_add s i0; + sum_with_shared_borrows_loop_fwd n0 max i0 s0) + else u32_mul s 2%u32 + end +. + +(** [loops::sum_with_shared_borrows] *) +Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := + sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32) . (** [loops::List] *) @@ -102,6 +122,28 @@ Definition list_nth_mut_loop_back list_nth_mut_loop_loop_back T n ls i ret . +(** [loops::list_nth_shared_loop] *) +Fixpoint list_nth_shared_loop_loop_fwd + (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match ls with + | ListCons x tl => + if i s= 0%u32 + then Return x + else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop_fwd T n0 tl i0) + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_loop] *) +Definition list_nth_shared_loop_fwd + (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := + list_nth_shared_loop_loop_fwd T n ls i +. + (** [loops::list_nth_mut_loop_pair] *) Fixpoint list_nth_mut_loop_pair_loop_fwd (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : @@ -200,6 +242,38 @@ Definition list_nth_mut_loop_pair_back'b list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret . +(** [loops::list_nth_shared_loop_pair] *) +Fixpoint list_nth_shared_loop_pair_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_loop_pair] *) +Definition list_nth_shared_loop_pair_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i +. + (** [loops::list_nth_mut_loop_pair_merge] *) Fixpoint list_nth_mut_loop_pair_merge_loop_fwd (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : @@ -268,4 +342,298 @@ Definition list_nth_mut_loop_pair_merge_back list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret . +(** [loops::list_nth_shared_loop_pair_merge] *) +Fixpoint list_nth_shared_loop_pair_merge_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_loop_pair_merge] *) +Definition list_nth_shared_loop_pair_merge_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i +. + +(** [loops::list_nth_mut_shared_loop_pair] *) +Fixpoint list_nth_mut_shared_loop_pair_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_mut_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_shared_loop_pair] *) +Definition list_nth_mut_shared_loop_pair_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i +. + +(** [loops::list_nth_mut_shared_loop_pair] *) +Fixpoint list_nth_mut_shared_loop_pair_loop_back + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl0) + else ( + i0 <- u32_sub i 1%u32; + l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x0 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_shared_loop_pair] *) +Definition list_nth_mut_shared_loop_pair_back + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret +. + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_mut_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +Definition list_nth_mut_shared_loop_pair_merge_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i +. + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl0) + else ( + i0 <- u32_sub i 1%u32; + l1 <- + list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x0 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +Definition list_nth_mut_shared_loop_pair_merge_back + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret +. + +(** [loops::list_nth_shared_mut_loop_pair] *) +Fixpoint list_nth_shared_mut_loop_pair_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_mut_loop_pair] *) +Definition list_nth_shared_mut_loop_pair_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i +. + +(** [loops::list_nth_shared_mut_loop_pair] *) +Fixpoint list_nth_shared_mut_loop_pair_loop_back + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl1) + else ( + i0 <- u32_sub i 1%u32; + l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x1 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_mut_loop_pair] *) +Definition list_nth_shared_mut_loop_pair_back + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret +. + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + result (T * T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (x0, x1) + else ( + i0 <- u32_sub i 1%u32; + list_nth_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +Definition list_nth_shared_mut_loop_pair_merge_fwd + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : + result (T * T) + := + list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i +. + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back + (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match l with + | ListCons x0 tl0 => + match l0 with + | ListCons x1 tl1 => + if i s= 0%u32 + then Return (ListCons ret tl1) + else ( + i0 <- u32_sub i 1%u32; + l1 <- + list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x1 l1)) + | ListNil => Fail_ Failure + end + | ListNil => Fail_ Failure + end + end +. + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +Definition list_nth_shared_mut_loop_pair_merge_back + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : + result (List_t T) + := + list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret +. + End Loops . diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index 3e44ef4f..cd29ca13 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -9,9 +9,14 @@ open Loops.Types (** [loops::sum]: decreases clause *) unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit () -(** [loops::sum_with_borrows]: decreases clause *) +(** [loops::sum_with_mut_borrows]: decreases clause *) unfold -let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat = +let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat = + admit () + +(** [loops::sum_with_shared_borrows]: decreases clause *) +unfold +let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::list_nth_mut_loop]: decreases clause *) @@ -19,15 +24,57 @@ unfold let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat = admit () +(** [loops::list_nth_shared_loop]: decreases clause *) +unfold +let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat + = + admit () + (** [loops::list_nth_mut_loop_pair]: decreases clause *) unfold let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : nat = admit () +(** [loops::list_nth_shared_loop_pair]: decreases clause *) +unfold +let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *) unfold let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : nat = admit () +(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : nat = + admit () + diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst index d315a4f0..9cf5db1f 100644 --- a/tests/fstar/misc/Loops.Clauses.fst +++ b/tests/fstar/misc/Loops.Clauses.fst @@ -9,25 +9,70 @@ open Loops.Types unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = if i <= max then max - i else 0 +(** [loops::sum_with_mut_borrows]: decreases clause *) +unfold +let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat = + if max >= mi then max - mi else 0 -(** [loops::sum_with_borrows]: decreases clause *) +(** [loops::sum_with_shared_borrows]: decreases clause *) unfold -let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat = - if mi <= max then max - mi else 0 +let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat = + if max >= i then max - i else 0 (** [loops::list_nth_mut_loop]: decreases clause *) unfold let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat = i +(** [loops::list_nth_shared_loop]: decreases clause *) +unfold +let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t = + ls + (** [loops::list_nth_mut_loop_pair]: decreases clause *) unfold let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : nat = i +(** [loops::list_nth_shared_loop_pair]: decreases clause *) +unfold +let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l + (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *) unfold let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : nat = i + +(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l + +(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l + +(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l + +(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l + +(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) + (l0 : list_t t) (i : u32) : list_t t = + l diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 05d1f70f..ee8e95d2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -27,10 +27,10 @@ let rec sum_loop_fwd (** [loops::sum] *) let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0 -(** [loops::sum_with_borrows] *) -let rec sum_with_borrows_loop_fwd +(** [loops::sum_with_mut_borrows] *) +let rec sum_with_mut_borrows_loop_fwd (max : u32) (mi : u32) (ms : u32) : - Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms)) + Tot (result u32) (decreases (sum_with_mut_borrows_decreases max mi ms)) = if mi < max then @@ -39,14 +39,35 @@ let rec sum_with_borrows_loop_fwd | Return ms0 -> begin match u32_add mi 1 with | Fail e -> Fail e - | Return mi0 -> sum_with_borrows_loop_fwd max mi0 ms0 + | Return mi0 -> sum_with_mut_borrows_loop_fwd max mi0 ms0 end end else u32_mul ms 2 -(** [loops::sum_with_borrows] *) -let sum_with_borrows_fwd (max : u32) : result u32 = - sum_with_borrows_loop_fwd max 0 0 +(** [loops::sum_with_mut_borrows] *) +let sum_with_mut_borrows_fwd (max : u32) : result u32 = + sum_with_mut_borrows_loop_fwd max 0 0 + +(** [loops::sum_with_shared_borrows] *) +let rec sum_with_shared_borrows_loop_fwd + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_shared_borrows_decreases max i s)) + = + if i < max + then + begin match u32_add i 1 with + | Fail e -> Fail e + | Return i0 -> + begin match u32_add s i0 with + | Fail e -> Fail e + | Return s0 -> sum_with_shared_borrows_loop_fwd max i0 s0 + end + end + else u32_mul s 2 + +(** [loops::sum_with_shared_borrows] *) +let sum_with_shared_borrows_fwd (max : u32) : result u32 = + sum_with_shared_borrows_loop_fwd max 0 0 (** [loops::list_nth_mut_loop] *) let rec list_nth_mut_loop_loop_fwd @@ -95,6 +116,27 @@ let list_nth_mut_loop_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_loop_loop_back t ls i ret +(** [loops::list_nth_shared_loop] *) +let rec list_nth_shared_loop_loop_fwd + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_shared_loop_decreases t ls i)) + = + 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_loop_fwd t tl i0 + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_loop] *) +let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_shared_loop_loop_fwd t ls i + (** [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) : @@ -187,6 +229,33 @@ let list_nth_mut_loop_pair_back'b = list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair] *) +let list_nth_shared_loop_pair_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_loop_fwd t ls0 ls1 i + (** [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) : @@ -248,3 +317,276 @@ let list_nth_mut_loop_pair_merge_back = list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair_merge] *) +let list_nth_shared_loop_pair_merge_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_merge_loop_fwd t ls0 ls1 i + +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair] *) +let list_nth_mut_shared_loop_pair_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_loop_fwd t ls0 ls1 i + +(** [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) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (ListCons ret tl0) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + 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) + end + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair] *) +let list_nth_mut_shared_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret + +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +let list_nth_mut_shared_loop_pair_merge_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_merge_loop_fwd t ls0 ls1 i + +(** [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) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (ListCons ret tl0) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + 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) + end + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge] *) +let list_nth_mut_shared_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret + +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair] *) +let list_nth_shared_mut_loop_pair_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_loop_fwd t ls0 ls1 i + +(** [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) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (ListCons ret tl1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + 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) + end + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair] *) +let list_nth_shared_mut_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret + +(** [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) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +let list_nth_shared_mut_loop_pair_merge_fwd + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_merge_loop_fwd t ls0 ls1 i + +(** [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) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + = + begin match l with + | ListCons x0 tl0 -> + begin match l0 with + | ListCons x1 tl1 -> + if i = 0 + then Return (ListCons ret tl1) + else + begin match u32_sub i 1 with + | Fail e -> Fail e + | Return i0 -> + 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) + end + end + | ListNil -> Fail Failure + end + | ListNil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge] *) +let list_nth_shared_mut_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret + -- cgit v1.2.3