summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
authorSon Ho2023-12-23 00:41:25 +0100
committerSon Ho2023-12-23 00:41:25 +0100
commitb6ef8ee33802e75409c3bd2b82e7b5ad22f1d053 (patch)
tree8c649905852a0fe17782985c6b88300e15288450 /tests/fstar/misc
parentaa5e25785738a779ca5fd89191c85d6ab828c142 (diff)
Improve the micro passes to eliminate pattern `let f := fun x => g x`
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/Loops.Funs.fst25
1 files changed, 8 insertions, 17 deletions
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index a047c170..88389300 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -121,9 +121,7 @@ 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)
+ let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back)
(** [loops::list_nth_shared_loop]: loop 0:
Source: 'src/loops.rs', lines 91:0-101:1 *)
@@ -201,7 +199,7 @@ 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)
+ Return (ls, Return)
(** [loops::id_shared]:
Source: 'src/loops.rs', lines 139:0-139:45 *)
@@ -296,9 +294,7 @@ let list_nth_mut_loop_pair
result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))
=
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)
+ Return (p, back_'a, back_'b)
(** [loops::list_nth_shared_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 198:0-219:1 *)
@@ -362,8 +358,7 @@ let list_nth_mut_loop_pair_merge
result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))
=
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)
+ Return (p, back_'a)
(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 241:0-256:1 *)
@@ -425,8 +420,7 @@ let list_nth_mut_shared_loop_pair
result ((t & t) & (t -> result (list_t t)))
=
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)
+ Return (p, back_'a)
(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 278:0-293:1 *)
@@ -462,8 +456,7 @@ let list_nth_mut_shared_loop_pair_merge
result ((t & t) & (t -> result (list_t t)))
=
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)
+ Return (p, back_'a)
(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 297:0-312:1 *)
@@ -498,8 +491,7 @@ let list_nth_shared_mut_loop_pair
result ((t & t) & (t -> result (list_t t)))
=
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)
+ Return (p, back_'b)
(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 316:0-331:1 *)
@@ -535,6 +527,5 @@ let list_nth_shared_mut_loop_pair_merge
result ((t & t) & (t -> result (list_t t)))
=
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)
+ Return (p, back_'a)