summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tests/coq/misc/Loops.v186
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst17
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst17
-rw-r--r--tests/fstar/misc/Loops.Funs.fst174
4 files changed, 394 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8d552b5b..67ee0880 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -22,6 +22,26 @@ 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
+ (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if mi s< max
+ then (
+ ms0 <- u32_add ms mi;
+ mi0 <- u32_add mi 1%u32;
+ sum_with_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::List] *)
Inductive List_t (T : Type) :=
| ListCons : T -> List_t T -> List_t T
@@ -82,4 +102,170 @@ Definition list_nth_mut_loop_back
list_nth_mut_loop_loop_back T n ls i ret
.
+(** [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) :
+ 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_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop_pair] *)
+Definition list_nth_mut_loop_pair_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_mut_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_loop_pair] *)
+Fixpoint list_nth_mut_loop_pair_loop_back'a
+ (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_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop_pair] *)
+Definition list_nth_mut_loop_pair_back'a
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_loop_pair_loop_back'a T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_mut_loop_pair] *)
+Fixpoint list_nth_mut_loop_pair_loop_back'b
+ (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_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 l1))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop_pair] *)
+Definition list_nth_mut_loop_pair_back'b
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+ result (List_t T)
+ :=
+ list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
+.
+
+(** [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) :
+ 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_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+Definition list_nth_mut_loop_pair_merge_fwd
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+ result (T * T)
+ :=
+ list_nth_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+Fixpoint list_nth_mut_loop_pair_merge_loop_back
+ (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : (T * T))
+ :
+ result ((List_t T) * (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 let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1)
+ else (
+ i0 <- u32_sub i 1%u32;
+ p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+ let (l1, l2) := p in
+ Return (ListCons x0 l1, ListCons x1 l2))
+ | ListNil => Fail_ Failure
+ end
+ | ListNil => Fail_ Failure
+ end
+ end
+.
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+Definition list_nth_mut_loop_pair_merge_back
+ (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
+ (ret : (T * T)) :
+ result ((List_t T) * (List_t T))
+ :=
+ list_nth_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 79a9dc4e..3e44ef4f 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -9,8 +9,25 @@ 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 *)
+unfold
+let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ admit ()
+
(** [loops::list_nth_mut_loop]: decreases clause *)
unfold
let list_nth_mut_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_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 ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 2087f2e7..d315a4f0 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,8 +9,25 @@ 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_borrows]: decreases clause *)
+unfold
+let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ if mi <= max then max - mi 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_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_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
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index cf05b7f2..05d1f70f 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -27,6 +27,27 @@ 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
+ (max : u32) (mi : u32) (ms : u32) :
+ Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms))
+ =
+ if mi < max
+ then
+ begin match u32_add ms mi with
+ | Fail e -> Fail e
+ | Return ms0 ->
+ begin match u32_add mi 1 with
+ | Fail e -> Fail e
+ | Return mi0 -> sum_with_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::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop_fwd
(t : Type0) (ls : list_t t) (i : u32) :
@@ -74,3 +95,156 @@ 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_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))
+ =
+ 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_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_loop_pair] *)
+let list_nth_mut_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [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) :
+ Tot (result (list_t t))
+ (decreases (list_nth_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 tl0)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | 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)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_loop_pair] *)
+let list_nth_mut_loop_pair_back'a
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret
+
+(** [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) :
+ Tot (result (list_t t))
+ (decreases (list_nth_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_mut_loop_pair_loop_back'b 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_mut_loop_pair] *)
+let list_nth_mut_loop_pair_back'b
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+
+(** [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) :
+ Tot (result (t & t))
+ (decreases (list_nth_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_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let list_nth_mut_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [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)) :
+ Tot (result ((list_t t) & (list_t t)))
+ (decreases (list_nth_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 let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ 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)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let list_nth_mut_loop_pair_merge_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
+ result ((list_t t) & (list_t t))
+ =
+ list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 15:46:23 +0000