From b6ef8ee33802e75409c3bd2b82e7b5ad22f1d053 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 00:41:25 +0100
Subject: Improve the micro passes to eliminate pattern `let f := fun x => g x`

---
 tests/coq/misc/Loops.v          | 26 ++++++++------------------
 tests/fstar/misc/Loops.Funs.fst | 25 ++++++++-----------------
 tests/lean/Loops.lean           | 25 ++++++++-----------------
 3 files changed, 24 insertions(+), 52 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 313c2cfd..cc76f359 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -160,10 +160,7 @@ Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_loop_loop T n ls i;
-  let (t, back) := p in
-  let back1 := fun (ret : T) => back ret in
-  Return (t, back1)
+  p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
@@ -265,7 +262,7 @@ Definition id_mut
   (T : Type) (ls : List_t T) :
   result ((List_t T) * (List_t T -> result (List_t T)))
   :=
-  let back := fun (ret : List_t T) => Return ret in Return (ls, back)
+  Return (ls, Return)
 .
 
 (** [loops::id_shared]:
@@ -382,9 +379,7 @@ Definition list_nth_mut_loop_pair
   :=
   t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
   let (p, back_'a, back_'b) := t in
-  let back_'a1 := fun (ret : T) => back_'a ret in
-  let back_'b1 := fun (ret : T) => back_'b ret in
-  Return (p, back_'a1, back_'b1)
+  Return (p, back_'a, back_'b)
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -465,8 +460,7 @@ Definition list_nth_mut_loop_pair_merge
   :=
   p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
   let (p1, back_'a) := p in
-  let back_'a1 := fun (ret : (T * T)) => back_'a ret in
-  Return (p1, back_'a1)
+  Return (p1, back_'a)
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -542,8 +536,7 @@ Definition list_nth_mut_shared_loop_pair
   :=
   p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
   let (p1, back_'a) := p in
-  let back_'a1 := fun (ret : T) => back_'a ret in
-  Return (p1, back_'a1)
+  Return (p1, back_'a)
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -585,8 +578,7 @@ Definition list_nth_mut_shared_loop_pair_merge
   :=
   p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
   let (p1, back_'a) := p in
-  let back_'a1 := fun (ret : T) => back_'a ret in
-  Return (p1, back_'a1)
+  Return (p1, back_'a)
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -628,8 +620,7 @@ Definition list_nth_shared_mut_loop_pair
   :=
   p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
   let (p1, back_'b) := p in
-  let back_'b1 := fun (ret : T) => back_'b ret in
-  Return (p1, back_'b1)
+  Return (p1, back_'b)
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -671,8 +662,7 @@ Definition list_nth_shared_mut_loop_pair_merge
   :=
   p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
   let (p1, back_'a) := p in
-  let back_'a1 := fun (ret : T) => back_'a ret in
-  Return (p1, back_'a1)
+  Return (p1, back_'a)
 .
 
 End Loops.
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)
 
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 805ecabc..fbb4616f 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -122,8 +122,7 @@ def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   do
   let (t, back) ← list_nth_mut_loop_loop T ls i
-  let back1 := fun ret => back ret
-  Result.ret (t, back1)
+  Result.ret (t, back)
 
 /- [loops::list_nth_shared_loop]: loop 0:
    Source: 'src/loops.rs', lines 91:0-101:1 -/
@@ -207,8 +206,7 @@ def id_mut
   (T : Type) (ls : List T) :
   Result ((List T) × (List T → Result (List T)))
   :=
-  let back := fun ret => Result.ret ret
-  Result.ret (ls, back)
+  Result.ret (ls, Result.ret)
 
 /- [loops::id_shared]:
    Source: 'src/loops.rs', lines 139:0-139:45 -/
@@ -308,9 +306,7 @@ def list_nth_mut_loop_pair
   :=
   do
   let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i
-  let back_'a1 := fun ret => back_'a ret
-  let back_'b1 := fun ret => back_'b ret
-  Result.ret (p, back_'a1, back_'b1)
+  Result.ret (p, back_'a, back_'b)
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 198:0-219:1 -/
@@ -372,8 +368,7 @@ def list_nth_mut_loop_pair_merge
   :=
   do
   let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
-  let back_'a1 := fun ret => back_'a ret
-  Result.ret (p, back_'a1)
+  Result.ret (p, back_'a)
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 241:0-256:1 -/
@@ -432,8 +427,7 @@ def list_nth_mut_shared_loop_pair
   :=
   do
   let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
-  let back_'a1 := fun ret => back_'a ret
-  Result.ret (p, back_'a1)
+  Result.ret (p, back_'a)
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 278:0-293:1 -/
@@ -470,8 +464,7 @@ def list_nth_mut_shared_loop_pair_merge
   :=
   do
   let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
-  let back_'a1 := fun ret => back_'a ret
-  Result.ret (p, back_'a1)
+  Result.ret (p, back_'a)
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 297:0-312:1 -/
@@ -507,8 +500,7 @@ def list_nth_shared_mut_loop_pair
   :=
   do
   let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
-  let back_'b1 := fun ret => back_'b ret
-  Result.ret (p, back_'b1)
+  Result.ret (p, back_'b)
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 316:0-331:1 -/
@@ -545,7 +537,6 @@ def list_nth_shared_mut_loop_pair_merge
   :=
   do
   let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
-  let back_'a1 := fun ret => back_'a ret
-  Result.ret (p, back_'a1)
+  Result.ret (p, back_'a)
 
 end loops
-- 
cgit v1.2.3