summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r--tests/fstar/misc/Bitwise.fst10
-rw-r--r--tests/fstar/misc/Constants.fst18
-rw-r--r--tests/fstar/misc/External.Funs.fst76
-rw-r--r--tests/fstar/misc/External.FunsExternal.fsti18
-rw-r--r--tests/fstar/misc/Loops.Funs.fst602
-rw-r--r--tests/fstar/misc/Paper.fst87
-rw-r--r--tests/fstar/misc/PoloniusList.fst30
-rw-r--r--tests/fstar/misc/Primitives.fst23
8 files changed, 322 insertions, 542 deletions
diff --git a/tests/fstar/misc/Bitwise.fst b/tests/fstar/misc/Bitwise.fst
index d7ba2c57..7330f07a 100644
--- a/tests/fstar/misc/Bitwise.fst
+++ b/tests/fstar/misc/Bitwise.fst
@@ -5,27 +5,27 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [bitwise::shift_u32]: forward function
+(** [bitwise::shift_u32]:
Source: 'src/bitwise.rs', lines 3:0-3:31 *)
let shift_u32 (a : u32) : result u32 =
let* t = u32_shr #Usize a 16 in u32_shl #Usize t 16
-(** [bitwise::shift_i32]: forward function
+(** [bitwise::shift_i32]:
Source: 'src/bitwise.rs', lines 10:0-10:31 *)
let shift_i32 (a : i32) : result i32 =
let* t = i32_shr #Isize a 16 in i32_shl #Isize t 16
-(** [bitwise::xor_u32]: forward function
+(** [bitwise::xor_u32]:
Source: 'src/bitwise.rs', lines 17:0-17:37 *)
let xor_u32 (a : u32) (b : u32) : result u32 =
Return (u32_xor a b)
-(** [bitwise::or_u32]: forward function
+(** [bitwise::or_u32]:
Source: 'src/bitwise.rs', lines 21:0-21:36 *)
let or_u32 (a : u32) (b : u32) : result u32 =
Return (u32_or a b)
-(** [bitwise::and_u32]: forward function
+(** [bitwise::and_u32]:
Source: 'src/bitwise.rs', lines 25:0-25:37 *)
let and_u32 (a : u32) (b : u32) : result u32 =
Return (u32_and a b)
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index daeefbb0..7bf42b46 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -20,7 +20,7 @@ let x1_c : u32 = eval_global x1_body
let x2_body : result u32 = Return 3
let x2_c : u32 = eval_global x2_body
-(** [constants::incr]: forward function
+(** [constants::incr]:
Source: 'src/constants.rs', lines 17:0-17:32 *)
let incr (n : u32) : result u32 =
u32_add n 1
@@ -30,7 +30,7 @@ let incr (n : u32) : result u32 =
let x3_body : result u32 = incr 32
let x3_c : u32 = eval_global x3_body
-(** [constants::mk_pair0]: forward function
+(** [constants::mk_pair0]:
Source: 'src/constants.rs', lines 23:0-23:51 *)
let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) =
Return (x, y)
@@ -39,7 +39,7 @@ let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) =
Source: 'src/constants.rs', lines 36:0-36:23 *)
type pair_t (t1 t2 : Type0) = { x : t1; y : t2; }
-(** [constants::mk_pair1]: forward function
+(** [constants::mk_pair1]:
Source: 'src/constants.rs', lines 27:0-27:55 *)
let mk_pair1 (x : u32) (y : u32) : result (pair_t u32 u32) =
Return { x = x; y = y }
@@ -68,7 +68,7 @@ let p3_c : pair_t u32 u32 = eval_global p3_body
Source: 'src/constants.rs', lines 49:0-49:18 *)
type wrap_t (t : Type0) = { value : t; }
-(** [constants::{constants::Wrap<T>}::new]: forward function
+(** [constants::{constants::Wrap<T>}::new]:
Source: 'src/constants.rs', lines 54:4-54:41 *)
let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
Return { value = value }
@@ -78,7 +78,7 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
let y_body : result (wrap_t i32) = wrap_new i32 2
let y_c : wrap_t i32 = eval_global y_body
-(** [constants::unwrap_y]: forward function
+(** [constants::unwrap_y]:
Source: 'src/constants.rs', lines 43:0-43:30 *)
let unwrap_y : result i32 =
Return y_c.value
@@ -93,12 +93,12 @@ let yval_c : i32 = eval_global yval_body
let get_z1_z1_body : result i32 = Return 3
let get_z1_z1_c : i32 = eval_global get_z1_z1_body
-(** [constants::get_z1]: forward function
+(** [constants::get_z1]:
Source: 'src/constants.rs', lines 61:0-61:28 *)
let get_z1 : result i32 =
Return get_z1_z1_c
-(** [constants::add]: forward function
+(** [constants::add]:
Source: 'src/constants.rs', lines 66:0-66:39 *)
let add (a : i32) (b : i32) : result i32 =
i32_add a b
@@ -118,10 +118,10 @@ let q2_c : i32 = eval_global q2_body
let q3_body : result i32 = add q2_c 3
let q3_c : i32 = eval_global q3_body
-(** [constants::get_z2]: forward function
+(** [constants::get_z2]:
Source: 'src/constants.rs', lines 70:0-70:28 *)
let get_z2 : result i32 =
- let* i = get_z1 in let* i0 = add i q3_c in add q1_c i0
+ let* i = get_z1 in let* i1 = add i q3_c in add q1_c i1
(** [constants::S1]
Source: 'src/constants.rs', lines 80:0-80:18 *)
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 00995634..bb1b9a64 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -7,33 +7,19 @@ include External.FunsExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [external::swap]: forward function
+(** [external::swap]:
Source: 'src/external.rs', lines 6:0-6:46 *)
-let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
- let* (st0, _) = core_mem_swap t x y st in
- let* (st1, _) = core_mem_swap_back0 t x y st st0 in
- let* (st2, _) = core_mem_swap_back1 t x y st st1 in
- Return (st2, ())
+let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & t)) =
+ core_mem_swap t x y st
-(** [external::swap]: backward function 0
- Source: 'src/external.rs', lines 6:0-6:46 *)
-let swap_back
- (t : Type0) (x : t) (y : t) (st : state) (st0 : state) :
- result (state & (t & t))
- =
- let* (st1, _) = core_mem_swap t x y st in
- let* (st2, x0) = core_mem_swap_back0 t x y st st1 in
- let* (_, y0) = core_mem_swap_back1 t x y st st2 in
- Return (st0, (x0, y0))
-
-(** [external::test_new_non_zero_u32]: forward function
+(** [external::test_new_non_zero_u32]:
Source: 'src/external.rs', lines 11:0-11:60 *)
let test_new_non_zero_u32
(x : u32) (st : state) : result (state & core_num_nonzero_NonZeroU32_t) =
- let* (st0, o) = core_num_nonzero_NonZeroU32_new x st in
- core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st0
+ let* (st1, o) = core_num_nonzero_NonZeroU32_new x st in
+ core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-(** [external::test_vec]: forward function
+(** [external::test_vec]:
Source: 'src/external.rs', lines 17:0-17:17 *)
let test_vec : result unit =
let v = alloc_vec_Vec_new u32 in
@@ -43,42 +29,28 @@ let test_vec : result unit =
(** Unit test for [external::test_vec] *)
let _ = assert_norm (test_vec = Return ())
-(** [external::custom_swap]: forward function
- Source: 'src/external.rs', lines 24:0-24:66 *)
-let custom_swap (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
- let* (st0, _) = core_mem_swap t x y st in
- let* (st1, x0) = core_mem_swap_back0 t x y st st0 in
- let* (st2, _) = core_mem_swap_back1 t x y st st1 in
- Return (st2, x0)
-
-(** [external::custom_swap]: backward function 0
+(** [external::custom_swap]:
Source: 'src/external.rs', lines 24:0-24:66 *)
-let custom_swap_back
- (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) :
- result (state & (t & t))
+let custom_swap
+ (t : Type0) (x : t) (y : t) (st : state) :
+ result (state & (t & (t -> state -> result (state & (t & t)))))
=
- let* (st1, _) = core_mem_swap t x y st in
- let* (st2, _) = core_mem_swap_back0 t x y st st1 in
- let* (_, y0) = core_mem_swap_back1 t x y st st2 in
- Return (st0, (ret, y0))
-
-(** [external::test_custom_swap]: forward function
- Source: 'src/external.rs', lines 29:0-29:59 *)
-let test_custom_swap (x : u32) (y : u32) (st : state) : result (state & unit) =
- let* (st0, _) = custom_swap u32 x y st in Return (st0, ())
+ let* (st1, (x1, x2)) = core_mem_swap t x y st in
+ let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in
+ Return (st1, (x1, back_'a))
-(** [external::test_custom_swap]: backward function 0
+(** [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 *)
-let test_custom_swap_back
- (x : u32) (y : u32) (st : state) (st0 : state) :
- result (state & (u32 & u32))
- =
- custom_swap_back u32 x y st 1 st0
+let test_custom_swap
+ (x : u32) (y : u32) (st : state) : result (state & (u32 & u32)) =
+ let* (st1, (_, custom_swap_back)) = custom_swap u32 x y st in
+ let* (_, (x1, y1)) = custom_swap_back 1 st1 in
+ Return (st1, (x1, y1))
-(** [external::test_swap_non_zero]: forward function
+(** [external::test_swap_non_zero]:
Source: 'src/external.rs', lines 35:0-35:44 *)
let test_swap_non_zero (x : u32) (st : state) : result (state & u32) =
- let* (st0, _) = swap u32 x 0 st in
- let* (st1, (x0, _)) = swap_back u32 x 0 st st0 in
- if x0 = 0 then Fail Failure else Return (st1, x0)
+ let* (st1, p) = swap u32 x 0 st in
+ let (x1, _) = p in
+ if x1 = 0 then Fail Failure else Return (st1, x1)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index 923a1101..a412aea9 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -6,26 +6,16 @@ include External.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [core::mem::swap]: forward function
+(** [core::mem::swap]:
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit)
+val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
-(** [core::mem::swap]: backward function 0
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back0
- (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::mem::swap]: backward function 1
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back1
- (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
val core_num_nonzero_NonZeroU32_new
: u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+(** [core::option::{core::option::Option<T>}::unwrap]:
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
val core_option_Option_unwrap
(t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index d2ac5561..a047c170 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -7,22 +7,22 @@ include Loops.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [loops::sum]: loop 0: forward function
+(** [loops::sum]: loop 0:
Source: 'src/loops.rs', lines 4:0-14:1 *)
let rec sum_loop
(max : u32) (i : u32) (s : u32) :
Tot (result u32) (decreases (sum_loop_decreases max i s))
=
if i < max
- then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0
+ then let* s1 = u32_add s i in let* i1 = u32_add i 1 in sum_loop max i1 s1
else u32_mul s 2
-(** [loops::sum]: forward function
+(** [loops::sum]:
Source: 'src/loops.rs', lines 4:0-4:27 *)
let sum (max : u32) : result u32 =
sum_loop max 0 0
-(** [loops::sum_with_mut_borrows]: loop 0: forward function
+(** [loops::sum_with_mut_borrows]: loop 0:
Source: 'src/loops.rs', lines 19:0-31:1 *)
let rec sum_with_mut_borrows_loop
(max : u32) (mi : u32) (ms : u32) :
@@ -30,17 +30,17 @@ let rec sum_with_mut_borrows_loop
=
if mi < max
then
- let* ms0 = u32_add ms mi in
- let* mi0 = u32_add mi 1 in
- sum_with_mut_borrows_loop max mi0 ms0
+ let* ms1 = u32_add ms mi in
+ let* mi1 = u32_add mi 1 in
+ sum_with_mut_borrows_loop max mi1 ms1
else u32_mul ms 2
-(** [loops::sum_with_mut_borrows]: forward function
+(** [loops::sum_with_mut_borrows]:
Source: 'src/loops.rs', lines 19:0-19:44 *)
let sum_with_mut_borrows (max : u32) : result u32 =
sum_with_mut_borrows_loop max 0 0
-(** [loops::sum_with_shared_borrows]: loop 0: forward function
+(** [loops::sum_with_shared_borrows]: loop 0:
Source: 'src/loops.rs', lines 34:0-48:1 *)
let rec sum_with_shared_borrows_loop
(max : u32) (i : u32) (s : u32) :
@@ -48,40 +48,39 @@ let rec sum_with_shared_borrows_loop
=
if i < max
then
- let* i0 = u32_add i 1 in
- let* s0 = u32_add s i0 in
- sum_with_shared_borrows_loop max i0 s0
+ let* i1 = u32_add i 1 in
+ let* s1 = u32_add s i1 in
+ sum_with_shared_borrows_loop max i1 s1
else u32_mul s 2
-(** [loops::sum_with_shared_borrows]: forward function
+(** [loops::sum_with_shared_borrows]:
Source: 'src/loops.rs', lines 34:0-34:47 *)
let sum_with_shared_borrows (max : u32) : result u32 =
sum_with_shared_borrows_loop max 0 0
-(** [loops::clear]: loop 0: merged forward/backward function
- (there is a single backward function, and the forward function returns ())
+(** [loops::clear]: loop 0:
Source: 'src/loops.rs', lines 52:0-58:1 *)
let rec clear_loop
(v : alloc_vec_Vec u32) (i : usize) :
Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i))
=
- let i0 = alloc_vec_Vec_len u32 v in
- if i < i0
+ let i1 = alloc_vec_Vec_len u32 v in
+ if i < i1
then
- let* i1 = usize_add i 1 in
- let* v0 =
- alloc_vec_Vec_index_mut_back u32 usize
- (core_slice_index_SliceIndexUsizeSliceTInst u32) v i 0 in
- clear_loop v0 i1
+ let* (_, index_mut_back) =
+ alloc_vec_Vec_index_mut u32 usize
+ (core_slice_index_SliceIndexUsizeSliceTInst u32) v i in
+ let* i2 = usize_add i 1 in
+ let* v1 = index_mut_back 0 in
+ clear_loop v1 i2
else Return v
-(** [loops::clear]: merged forward/backward function
- (there is a single backward function, and the forward function returns ())
+(** [loops::clear]:
Source: 'src/loops.rs', lines 52:0-52:30 *)
let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) =
clear_loop v 0
-(** [loops::list_mem]: loop 0: forward function
+(** [loops::list_mem]: loop 0:
Source: 'src/loops.rs', lines 66:0-75:1 *)
let rec list_mem_loop
(x : u32) (ls : list_t u32) :
@@ -92,54 +91,41 @@ let rec list_mem_loop
| List_Nil -> Return false
end
-(** [loops::list_mem]: forward function
+(** [loops::list_mem]:
Source: 'src/loops.rs', lines 66:0-66:52 *)
let list_mem (x : u32) (ls : list_t u32) : result bool =
list_mem_loop x ls
-(** [loops::list_nth_mut_loop]: loop 0: forward function
+(** [loops::list_nth_mut_loop]: loop 0:
Source: 'src/loops.rs', lines 78:0-88:1 *)
let rec list_nth_mut_loop_loop
(t : Type0) (ls : list_t t) (i : u32) :
- Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i))
+ Tot (result (t & (t -> result (list_t t))))
+ (decreases (list_nth_mut_loop_loop_decreases t ls i))
=
begin match ls with
| List_Cons x tl ->
if i = 0
- then Return x
- else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop t tl i0
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_loop]: forward function
- Source: 'src/loops.rs', lines 78:0-78:71 *)
-let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
- list_nth_mut_loop_loop t ls i
-
-(** [loops::list_nth_mut_loop]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 78:0-88:1 *)
-let rec list_nth_mut_loop_loop_back
- (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
- Tot (result (list_t t)) (decreases (list_nth_mut_loop_loop_decreases t ls i))
- =
- begin match ls with
- | List_Cons x tl ->
- if i = 0
- then Return (List_Cons ret tl)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
- let* i0 = u32_sub i 1 in
- let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in
- Return (List_Cons x tl0)
+ let* i1 = u32_sub i 1 in
+ let* (x1, back) = list_nth_mut_loop_loop t tl i1 in
+ let back1 = fun ret -> let* tl1 = back ret in Return (List_Cons x tl1) in
+ Return (x1, back1)
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_loop]: backward function 0
+(** [loops::list_nth_mut_loop]:
Source: 'src/loops.rs', lines 78:0-78:71 *)
-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
+let list_nth_mut_loop
+ (t : Type0) (ls : list_t t) (i : u32) :
+ result (t & (t -> result (list_t t)))
+ =
+ let* (x, back) = list_nth_mut_loop_loop t ls i in
+ let back1 = fun ret -> back ret in
+ Return (x, back1)
-(** [loops::list_nth_shared_loop]: loop 0: forward function
+(** [loops::list_nth_shared_loop]: loop 0:
Source: 'src/loops.rs', lines 91:0-101:1 *)
let rec list_nth_shared_loop_loop
(t : Type0) (ls : list_t t) (i : u32) :
@@ -149,63 +135,47 @@ let rec list_nth_shared_loop_loop
| List_Cons x tl ->
if i = 0
then Return x
- else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop t tl i0
+ else let* i1 = u32_sub i 1 in list_nth_shared_loop_loop t tl i1
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_loop]: forward function
+(** [loops::list_nth_shared_loop]:
Source: 'src/loops.rs', lines 91:0-91:66 *)
let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
list_nth_shared_loop_loop t ls i
-(** [loops::get_elem_mut]: loop 0: forward function
+(** [loops::get_elem_mut]: loop 0:
Source: 'src/loops.rs', lines 103:0-117:1 *)
let rec get_elem_mut_loop
(x : usize) (ls : list_t usize) :
- Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls))
- =
- begin match ls with
- | List_Cons y tl -> if y = x then Return y else get_elem_mut_loop x tl
- | List_Nil -> Fail Failure
- end
-
-(** [loops::get_elem_mut]: forward function
- Source: 'src/loops.rs', lines 103:0-103:73 *)
-let get_elem_mut
- (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
- let* l =
- alloc_vec_Vec_index_mut (list_t usize) usize
- (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in
- get_elem_mut_loop x l
-
-(** [loops::get_elem_mut]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 103:0-117:1 *)
-let rec get_elem_mut_loop_back
- (x : usize) (ls : list_t usize) (ret : usize) :
- Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls))
+ Tot (result (usize & (usize -> result (list_t usize))))
+ (decreases (get_elem_mut_loop_decreases x ls))
=
begin match ls with
| List_Cons y tl ->
if y = x
- then Return (List_Cons ret tl)
- else let* tl0 = get_elem_mut_loop_back x tl ret in Return (List_Cons y tl0)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (y, back)
+ else
+ let* (i, back) = get_elem_mut_loop x tl in
+ let back1 = fun ret -> let* tl1 = back ret in Return (List_Cons y tl1) in
+ Return (i, back1)
| List_Nil -> Fail Failure
end
-(** [loops::get_elem_mut]: backward function 0
+(** [loops::get_elem_mut]:
Source: 'src/loops.rs', lines 103:0-103:73 *)
-let get_elem_mut_back
- (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) :
- result (alloc_vec_Vec (list_t usize))
+let get_elem_mut
+ (slots : alloc_vec_Vec (list_t usize)) (x : usize) :
+ result (usize & (usize -> result (alloc_vec_Vec (list_t usize))))
=
- let* l =
+ let* (l, index_mut_back) =
alloc_vec_Vec_index_mut (list_t usize) usize
(core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in
- let* l0 = get_elem_mut_loop_back x l ret in
- alloc_vec_Vec_index_mut_back (list_t usize) usize
- (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 l0
+ let* (i, back) = get_elem_mut_loop x l in
+ let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in
+ Return (i, back1)
-(** [loops::get_elem_shared]: loop 0: forward function
+(** [loops::get_elem_shared]: loop 0:
Source: 'src/loops.rs', lines 119:0-133:1 *)
let rec get_elem_shared_loop
(x : usize) (ls : list_t usize) :
@@ -216,7 +186,7 @@ let rec get_elem_shared_loop
| List_Nil -> Fail Failure
end
-(** [loops::get_elem_shared]: forward function
+(** [loops::get_elem_shared]:
Source: 'src/loops.rs', lines 119:0-119:68 *)
let get_elem_shared
(slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
@@ -225,69 +195,50 @@ let get_elem_shared
(core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in
get_elem_shared_loop x l
-(** [loops::id_mut]: forward function
- Source: 'src/loops.rs', lines 135:0-135:50 *)
-let id_mut (t : Type0) (ls : list_t t) : result (list_t t) =
- Return ls
-
-(** [loops::id_mut]: backward function 0
+(** [loops::id_mut]:
Source: 'src/loops.rs', lines 135:0-135:50 *)
-let id_mut_back
- (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) =
- Return ret
+let id_mut
+ (t : Type0) (ls : list_t t) :
+ result ((list_t t) & (list_t t -> result (list_t t)))
+ =
+ let back = fun ret -> Return ret in Return (ls, back)
-(** [loops::id_shared]: forward function
+(** [loops::id_shared]:
Source: 'src/loops.rs', lines 139:0-139:45 *)
let id_shared (t : Type0) (ls : list_t t) : result (list_t t) =
Return ls
-(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function
+(** [loops::list_nth_mut_loop_with_id]: loop 0:
Source: 'src/loops.rs', lines 144:0-155:1 *)
let rec list_nth_mut_loop_with_id_loop
(t : Type0) (i : u32) (ls : list_t t) :
- Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
- =
- begin match ls with
- | List_Cons x tl ->
- if i = 0
- then Return x
- else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop t i0 tl
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_loop_with_id]: forward function
- Source: 'src/loops.rs', lines 144:0-144:75 *)
-let list_nth_mut_loop_with_id
- (t : Type0) (ls : list_t t) (i : u32) : result t =
- let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0
-
-(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 144:0-155:1 *)
-let rec list_nth_mut_loop_with_id_loop_back
- (t : Type0) (i : u32) (ls : list_t t) (ret : t) :
- Tot (result (list_t t))
+ Tot (result (t & (t -> result (list_t t))))
(decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
=
begin match ls with
| List_Cons x tl ->
if i = 0
- then Return (List_Cons ret tl)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
- let* i0 = u32_sub i 1 in
- let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in
- Return (List_Cons x tl0)
+ let* i1 = u32_sub i 1 in
+ let* (x1, back) = list_nth_mut_loop_with_id_loop t i1 tl in
+ let back1 = fun ret -> let* tl1 = back ret in Return (List_Cons x tl1) in
+ Return (x1, back1)
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_loop_with_id]: backward function 0
+(** [loops::list_nth_mut_loop_with_id]:
Source: 'src/loops.rs', lines 144:0-144:75 *)
-let list_nth_mut_loop_with_id_back
- (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
- let* ls0 = id_mut t ls in
- let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in
- id_mut_back t ls l
+let list_nth_mut_loop_with_id
+ (t : Type0) (ls : list_t t) (i : u32) :
+ result (t & (t -> result (list_t t)))
+ =
+ let* (ls1, id_mut_back) = id_mut t ls in
+ let* (x, back) = list_nth_mut_loop_with_id_loop t i ls1 in
+ let back1 = fun ret -> let* l = back ret in id_mut_back l in
+ Return (x, back1)
-(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function
+(** [loops::list_nth_shared_loop_with_id]: loop 0:
Source: 'src/loops.rs', lines 158:0-169:1 *)
let rec list_nth_shared_loop_with_id_loop
(t : Type0) (i : u32) (ls : list_t t) :
@@ -298,46 +249,21 @@ let rec list_nth_shared_loop_with_id_loop
| List_Cons x tl ->
if i = 0
then Return x
- else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i0 tl
+ else let* i1 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i1 tl
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_loop_with_id]: forward function
+(** [loops::list_nth_shared_loop_with_id]:
Source: 'src/loops.rs', lines 158:0-158:70 *)
let list_nth_shared_loop_with_id
(t : Type0) (ls : list_t t) (i : u32) : result t =
- let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0
+ let* ls1 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls1
-(** [loops::list_nth_mut_loop_pair]: loop 0: forward function
+(** [loops::list_nth_mut_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 174:0-195:1 *)
let rec list_nth_mut_loop_pair_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
- (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (x0, x1)
- else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop t tl0 tl1 i0
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_loop_pair]: forward function
- Source: 'src/loops.rs', lines 174:0-178:27 *)
-let list_nth_mut_loop_pair
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_mut_loop_pair_loop t ls0 ls1 i
-
-(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 174:0-195:1 *)
-let rec list_nth_mut_loop_pair_loop_back'a
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
- Tot (result (list_t t))
+ Tot (result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))))
(decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -345,55 +271,36 @@ let rec list_nth_mut_loop_pair_loop_back'a
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (List_Cons ret tl0)
+ then
+ let back_'a = fun ret -> Return (List_Cons ret tl0) in
+ let back_'b = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back_'a, back_'b)
else
- let* i0 = u32_sub i 1 in
- let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in
- Return (List_Cons x0 tl00)
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
+ in
+ let back_'a1 =
+ fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
+ let back_'b1 =
+ fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
+ Return (p, back_'a1, back_'b1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_loop_pair]: backward function 0
+(** [loops::list_nth_mut_loop_pair]:
Source: 'src/loops.rs', lines 174:0-178:27 *)
-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]: loop 0: backward function 1
- Source: 'src/loops.rs', lines 174:0-195:1 *)
-let rec list_nth_mut_loop_pair_loop_back'b
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (List_Cons ret tl1)
- else
- let* i0 = u32_sub i 1 in
- let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in
- Return (List_Cons x1 tl10)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_loop_pair]: backward function 1
- Source: 'src/loops.rs', lines 174:0-178:27 *)
-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)
+let list_nth_mut_loop_pair
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))
=
- list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+ let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in
+ let back_'a1 = fun ret -> back_'a ret in
+ let back_'b1 = fun ret -> back_'b ret in
+ Return (p, back_'a1, back_'b1)
-(** [loops::list_nth_shared_loop_pair]: loop 0: forward function
+(** [loops::list_nth_shared_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 198:0-219:1 *)
let rec list_nth_shared_loop_pair_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
@@ -406,23 +313,23 @@ let rec list_nth_shared_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then Return (x0, x1)
- else let* i0 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i0
+ else let* i1 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i1
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_loop_pair]: forward function
+(** [loops::list_nth_shared_loop_pair]:
Source: 'src/loops.rs', lines 198:0-202:19 *)
let list_nth_shared_loop_pair
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
list_nth_shared_loop_pair_loop t ls0 ls1 i
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_mut_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 223:0-238:1 *)
let rec list_nth_mut_loop_pair_merge_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
+ Tot (result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))))
(decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -430,52 +337,35 @@ let rec list_nth_mut_loop_pair_merge_loop
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (x0, x1)
+ then
+ let back_'a =
+ fun ret ->
+ let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
+ Return ((x0, x1), back_'a)
else
- let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_merge_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+ let back_'a1 =
+ fun ret ->
+ let* (tl01, tl11) = back_'a ret in
+ Return (List_Cons x0 tl01, List_Cons x1 tl11) in
+ Return (p, back_'a1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_loop_pair_merge]: forward function
+(** [loops::list_nth_mut_loop_pair_merge]:
Source: 'src/loops.rs', lines 223:0-227:27 *)
let list_nth_mut_loop_pair_merge
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_mut_loop_pair_merge_loop t ls0 ls1 i
-
-(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 223:0-238:1 *)
-let rec list_nth_mut_loop_pair_merge_loop_back
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1)
- else
- let* i0 = u32_sub i 1 in
- let* (tl00, tl10) =
- list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
- Return (List_Cons x0 tl00, List_Cons x1 tl10)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_loop_pair_merge]: backward function 0
- Source: 'src/loops.rs', lines 223:0-227:27 *)
-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))
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))
=
- list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+ let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in
+ let back_'a1 = fun ret -> back_'a ret in
+ Return (p, back_'a1)
-(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 241:0-256:1 *)
let rec list_nth_shared_loop_pair_merge_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
@@ -489,24 +379,24 @@ let rec list_nth_shared_loop_pair_merge_loop
if i = 0
then Return (x0, x1)
else
- let* i0 = u32_sub i 1 in
- list_nth_shared_loop_pair_merge_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ list_nth_shared_loop_pair_merge_loop t tl0 tl1 i1
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_loop_pair_merge]: forward function
+(** [loops::list_nth_shared_loop_pair_merge]:
Source: 'src/loops.rs', lines 241:0-245:19 *)
let list_nth_shared_loop_pair_merge
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
list_nth_shared_loop_pair_merge_loop t ls0 ls1 i
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function
+(** [loops::list_nth_mut_shared_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 259:0-274:1 *)
let rec list_nth_mut_shared_loop_pair_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
+ Tot (result ((t & t) & (t -> result (list_t t))))
(decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -514,56 +404,35 @@ let rec list_nth_mut_shared_loop_pair_loop
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (x0, x1)
+ then
+ let back_'a = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back_'a)
else
- let* i0 = u32_sub i 1 in
- list_nth_mut_shared_loop_pair_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+ let back_'a1 =
+ fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
+ Return (p, back_'a1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_shared_loop_pair]: forward function
+(** [loops::list_nth_mut_shared_loop_pair]:
Source: 'src/loops.rs', lines 259:0-263:23 *)
let list_nth_mut_shared_loop_pair
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_mut_shared_loop_pair_loop t ls0 ls1 i
-
-(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 259:0-274:1 *)
-let rec list_nth_mut_shared_loop_pair_loop_back
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (List_Cons ret tl0)
- else
- let* i0 = u32_sub i 1 in
- let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in
- Return (List_Cons x0 tl00)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_shared_loop_pair]: backward function 0
- Source: 'src/loops.rs', lines 259:0-263:23 *)
-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)
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & (t -> result (list_t t)))
=
- list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret
+ let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in
+ let back_'a1 = fun ret -> back_'a ret in
+ Return (p, back_'a1)
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 278:0-293:1 *)
let rec list_nth_mut_shared_loop_pair_merge_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
+ Tot (result ((t & t) & (t -> result (list_t t))))
(decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -571,57 +440,36 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (x0, x1)
+ then
+ let back_'a = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back_'a)
else
- let* i0 = u32_sub i 1 in
- list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'a) =
+ list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
+ let back_'a1 =
+ fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
+ Return (p, back_'a1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function
+(** [loops::list_nth_mut_shared_loop_pair_merge]:
Source: 'src/loops.rs', lines 278:0-282:23 *)
let list_nth_mut_shared_loop_pair_merge
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i
-
-(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 278:0-293:1 *)
-let rec list_nth_mut_shared_loop_pair_merge_loop_back
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (List_Cons ret tl0)
- else
- let* i0 = u32_sub i 1 in
- let* tl00 =
- list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
- Return (List_Cons x0 tl00)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0
- Source: 'src/loops.rs', lines 278:0-282:23 *)
-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)
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & (t -> result (list_t t)))
=
- list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret
+ let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in
+ let back_'a1 = fun ret -> back_'a ret in
+ Return (p, back_'a1)
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function
+(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 297:0-312:1 *)
let rec list_nth_shared_mut_loop_pair_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
+ Tot (result ((t & t) & (t -> result (list_t t))))
(decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -629,56 +477,35 @@ let rec list_nth_shared_mut_loop_pair_loop
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (x0, x1)
+ then
+ let back_'b = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back_'b)
else
- let* i0 = u32_sub i 1 in
- list_nth_shared_mut_loop_pair_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+ let back_'b1 =
+ fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
+ Return (p, back_'b1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_mut_loop_pair]: forward function
+(** [loops::list_nth_shared_mut_loop_pair]:
Source: 'src/loops.rs', lines 297:0-301:23 *)
let list_nth_shared_mut_loop_pair
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_shared_mut_loop_pair_loop t ls0 ls1 i
-
-(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1
- Source: 'src/loops.rs', lines 297:0-312:1 *)
-let rec list_nth_shared_mut_loop_pair_loop_back
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (List_Cons ret tl1)
- else
- let* i0 = u32_sub i 1 in
- let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in
- Return (List_Cons x1 tl10)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_shared_mut_loop_pair]: backward function 1
- Source: 'src/loops.rs', lines 297:0-301:23 *)
-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)
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & (t -> result (list_t t)))
=
- list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret
+ let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in
+ let back_'b1 = fun ret -> back_'b ret in
+ Return (p, back_'b1)
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function
+(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 316:0-331:1 *)
let rec list_nth_shared_mut_loop_pair_merge_loop
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
- Tot (result (t & t))
+ Tot (result ((t & t) & (t -> result (list_t t))))
(decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
=
begin match ls0 with
@@ -686,49 +513,28 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
begin match ls1 with
| List_Cons x1 tl1 ->
if i = 0
- then Return (x0, x1)
+ then
+ let back_'a = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back_'a)
else
- let* i0 = u32_sub i 1 in
- list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i0
+ let* i1 = u32_sub i 1 in
+ let* (p, back_'a) =
+ list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+ let back_'a1 =
+ fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
+ Return (p, back_'a1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
end
-(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function
+(** [loops::list_nth_shared_mut_loop_pair_merge]:
Source: 'src/loops.rs', lines 316:0-320:23 *)
let list_nth_shared_mut_loop_pair_merge
- (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
- list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i
-
-(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0
- Source: 'src/loops.rs', lines 316:0-331:1 *)
-let rec list_nth_shared_mut_loop_pair_merge_loop_back
- (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_loop_decreases t ls0 ls1 i))
- =
- begin match ls0 with
- | List_Cons x0 tl0 ->
- begin match ls1 with
- | List_Cons x1 tl1 ->
- if i = 0
- then Return (List_Cons ret tl1)
- else
- let* i0 = u32_sub i 1 in
- let* tl10 =
- list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
- Return (List_Cons x1 tl10)
- | List_Nil -> Fail Failure
- end
- | List_Nil -> Fail Failure
- end
-
-(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0
- Source: 'src/loops.rs', lines 316:0-320:23 *)
-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)
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+ result ((t & t) & (t -> result (list_t t)))
=
- list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+ let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in
+ let back_'a1 = fun ret -> back_'a ret in
+ Return (p, back_'a1)
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 14bc59e8..c6082929 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -5,40 +5,36 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [paper::ref_incr]: merged forward/backward function
- (there is a single backward function, and the forward function returns ())
+(** [paper::ref_incr]:
Source: 'src/paper.rs', lines 4:0-4:28 *)
let ref_incr (x : i32) : result i32 =
i32_add x 1
-(** [paper::test_incr]: forward function
+(** [paper::test_incr]:
Source: 'src/paper.rs', lines 8:0-8:18 *)
let test_incr : result unit =
- let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return ()
+ let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return ()
(** Unit test for [paper::test_incr] *)
let _ = assert_norm (test_incr = Return ())
-(** [paper::choose]: forward function
+(** [paper::choose]:
Source: 'src/paper.rs', lines 15:0-15:70 *)
-let choose (t : Type0) (b : bool) (x : t) (y : t) : result t =
- if b then Return x else Return y
+let choose
+ (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
+ if b
+ then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
+ else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
-(** [paper::choose]: backward function 0
- Source: 'src/paper.rs', lines 15:0-15:70 *)
-let choose_back
- (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
- if b then Return (ret, y) else Return (x, ret)
-
-(** [paper::test_choose]: forward function
+(** [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 *)
let test_choose : result unit =
- let* z = choose i32 true 0 0 in
- let* z0 = i32_add z 1 in
- if not (z0 = 1)
+ let* (z, choose_back) = choose i32 true 0 0 in
+ let* z1 = i32_add z 1 in
+ if not (z1 = 1)
then Fail Failure
else
- let* (x, y) = choose_back i32 true 0 0 z0 in
+ let* (x, y) = choose_back z1 in
if not (x = 1)
then Fail Failure
else if not (y = 0) then Fail Failure else Return ()
@@ -52,31 +48,28 @@ type list_t (t : Type0) =
| List_Cons : t -> list_t t -> list_t t
| List_Nil : list_t t
-(** [paper::list_nth_mut]: forward function
- Source: 'src/paper.rs', lines 42:0-42:67 *)
-let rec list_nth_mut (t : Type0) (l : list_t t) (i : u32) : result t =
- begin match l with
- | List_Cons x tl ->
- if i = 0 then Return x else let* i0 = u32_sub i 1 in list_nth_mut t tl i0
- | List_Nil -> Fail Failure
- end
-
-(** [paper::list_nth_mut]: backward function 0
+(** [paper::list_nth_mut]:
Source: 'src/paper.rs', lines 42:0-42:67 *)
-let rec list_nth_mut_back
- (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
+let rec list_nth_mut
+ (t : Type0) (l : list_t t) (i : u32) :
+ result (t & (t -> result (list_t t)))
+ =
begin match l with
| List_Cons x tl ->
if i = 0
- then Return (List_Cons ret tl)
+ then
+ let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
else
- let* i0 = u32_sub i 1 in
- let* tl0 = list_nth_mut_back t tl i0 ret in
- Return (List_Cons x tl0)
+ let* i1 = u32_sub i 1 in
+ let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
+ let back_'a =
+ fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
+ in
+ Return (x1, back_'a)
| List_Nil -> Fail Failure
end
-(** [paper::sum]: forward function
+(** [paper::sum]:
Source: 'src/paper.rs', lines 57:0-57:32 *)
let rec sum (l : list_t i32) : result i32 =
begin match l with
@@ -84,27 +77,27 @@ let rec sum (l : list_t i32) : result i32 =
| List_Nil -> Return 0
end
-(** [paper::test_nth]: forward function
+(** [paper::test_nth]:
Source: 'src/paper.rs', lines 68:0-68:17 *)
let test_nth : result unit =
let l = List_Nil in
- let l0 = List_Cons 3 l in
- let l1 = List_Cons 2 l0 in
- let* x = list_nth_mut i32 (List_Cons 1 l1) 2 in
- let* x0 = i32_add x 1 in
- let* l2 = list_nth_mut_back i32 (List_Cons 1 l1) 2 x0 in
- let* i = sum l2 in
+ let l1 = List_Cons 3 l in
+ let l2 = List_Cons 2 l1 in
+ let* (x, list_nth_mut_back) = list_nth_mut i32 (List_Cons 1 l2) 2 in
+ let* x1 = i32_add x 1 in
+ let* l3 = list_nth_mut_back x1 in
+ let* i = sum l3 in
if not (i = 7) then Fail Failure else Return ()
(** Unit test for [paper::test_nth] *)
let _ = assert_norm (test_nth = Return ())
-(** [paper::call_choose]: forward function
+(** [paper::call_choose]:
Source: 'src/paper.rs', lines 76:0-76:44 *)
let call_choose (p : (u32 & u32)) : result u32 =
let (px, py) = p in
- let* pz = choose u32 true px py in
- let* pz0 = u32_add pz 1 in
- let* (px0, _) = choose_back u32 true px py pz0 in
- Return px0
+ let* (pz, choose_back) = choose u32 true px py in
+ let* pz1 = u32_add pz 1 in
+ let* (px1, _) = choose_back pz1 in
+ Return px1
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 188b22d8..cbe7d6b8 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -11,24 +11,24 @@ type list_t (t : Type0) =
| List_Cons : t -> list_t t -> list_t t
| List_Nil : list_t t
-(** [polonius_list::get_list_at_x]: forward function
+(** [polonius_list::get_list_at_x]:
Source: 'src/polonius_list.rs', lines 13:0-13:76 *)
-let rec get_list_at_x (ls : list_t u32) (x : u32) : result (list_t u32) =
- begin match ls with
- | List_Cons hd tl ->
- if hd = x then Return (List_Cons hd tl) else get_list_at_x tl x
- | List_Nil -> Return List_Nil
- end
-
-(** [polonius_list::get_list_at_x]: backward function 0
- Source: 'src/polonius_list.rs', lines 13:0-13:76 *)
-let rec get_list_at_x_back
- (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
+let rec get_list_at_x
+ (ls : list_t u32) (x : u32) :
+ result ((list_t u32) & (list_t u32 -> result (list_t u32)))
+ =
begin match ls with
| List_Cons hd tl ->
if hd = x
- then Return ret
- else let* tl0 = get_list_at_x_back tl x ret in Return (List_Cons hd tl0)
- | List_Nil -> Return ret
+ then
+ let back_'a = fun ret -> Return ret in Return (List_Cons hd tl, back_'a)
+ else
+ let* (l, get_list_at_x_back) = get_list_at_x tl x in
+ let back_'a =
+ fun ret ->
+ let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
+ Return (l, back_'a)
+ | List_Nil ->
+ let back_'a = fun ret -> Return ret in Return (List_Nil, back_'a)
end
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 6b8dbeb7..fca80829 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -55,7 +55,7 @@ type string = string
let is_zero (n: nat) : bool = n = 0
let decrease (n: nat{n > 0}) : nat = n - 1
-let core_mem_replace (a : Type0) (x : a) (y : a) : a & (a -> a) = (x, (fun x -> x))
+let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x)
// We don't really use raw pointers for now
type mut_raw_ptr (t : Type0) = { v : t }
@@ -531,10 +531,18 @@ let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : resu
if i < length x then Return (index x i)
else Fail Failure
-let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) :
+ result (array a n) =
if i < length x then Return (list_update x i nx)
else Fail Failure
+let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) :
+ result (a & (a -> result (array a n))) =
+ match array_index_usize a n x i with
+ | Fail e -> Fail e
+ | Return v ->
+ Return (v, array_update_usize a n x i)
+
(*** Slice *)
type slice (a : Type0) = s:list a{length s <= usize_max}
@@ -548,6 +556,13 @@ let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (
if i < length x then Return (list_update x i nx)
else Fail Failure
+let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) :
+ result (a & (a -> result (slice a))) =
+ match slice_index_usize a s i with
+ | Fail e -> Fail e
+ | Return x ->
+ Return (x, slice_update_usize a s i)
+
(*** Subslices *)
let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
@@ -555,6 +570,10 @@ let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : res
if length s = n then Return s
else Fail Failure
+let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) :
+ result (slice a & (slice a -> result (array a n))) =
+ Return (x, array_from_slice a n x)
+
// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
admit()
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:26:46 +0000