feat: add an empty parameter for lambdas without parameters

CoqOfRust/blacklist.txt

@@ -47,7 +47,7 @@ examples/axiomatized/examples/test0.v
 examples/default/examples/ink_contracts/Proofs/erc20.v
 examples/default/examples/rust_book/custom_types/enums_testcase_linked_list.v
 examples/default/examples/rust_book/error_handling/pulling_results_out_of_options_with_stop_error_processing.v
-examples/default/examples/rust_book/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v
+#examples/default/examples/rust_book/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v
 examples/default/examples/rust_book/error_handling/unpacking_options_and_defaults_via_or_else.v
 examples/default/examples/rust_book/error_handling/unpacking_options_via_question_mark.v
 examples/default/examples/rust_book/error_handling/wrapping_errors.v

CoqOfRust/core/option.v

@@ -157,6 +157,20 @@ Module Impl_Option. Section Impl_Option.
     Notations.double_colon := get_or_insert;
   }.
 
+  (*
+  pub fn get_or_insert_with<F>(&mut self, f: F) -> &mut T
+  where
+      F: FnOnce() -> T,
+  *)
+  Parameter get_or_insert_with :
+    forall {F : Set},
+    mut_ref Self -> F -> M (mut_ref T).
+
+  Global Instance AF_get_or_insert_with {F : Set} :
+      Notations.DoubleColon Self "get_or_insert_with" := {
+    Notations.double_colon := get_or_insert_with (F := F);
+  }.
+
   (* pub fn or(self, optb: Option<T>) -> Option<T> *)
   Parameter or : Self -> option.Option.t T -> M (option.Option.t T).
 

CoqOfRust/core/result_impl.v

@@ -153,11 +153,11 @@ Section Impl_Option.
   where
       F: FnOnce() -> E,
   *)
-  Parameter ok_or_else : forall {E : Set}, Self -> M E -> M (Result.t T E).
+  Parameter ok_or_else : forall {E F : Set}, Self -> F -> M (Result.t T E).
 
-  Global Instance AF_ok_or_else {E : Set} :
+  Global Instance AF_ok_or_else {E F : Set} :
       Notations.DoubleColon Self "ok_or_else" := {
-    Notations.double_colon := ok_or_else (E := E);
+    Notations.double_colon := ok_or_else (E := E) (F := F);
   }.
 End Impl_Option.
 End Impl_Option.

CoqOfRust/examples/default/examples/rust_book/error_handling/boxing_errors.v

@@ -146,25 +146,36 @@ Definition double_first
     M.call
       ((core.option.Option.t (ref (ref str.t)))::["ok_or_else"]
         α2
-        ((let* α0 :
-            boxing_errors.EmptyVec.t ->
-              M
-                (alloc.boxed.Box.t
-                  (dyn [core.error.Error.Trait])
-                  alloc.alloc.Global.t) :=
-          ltac:(M.get_method (fun ℐ =>
-            core.convert.Into.into
-              (Self := boxing_errors.EmptyVec.t)
-              (T :=
-                alloc.boxed.Box.t
-                  (dyn [core.error.Error.Trait])
-                  alloc.alloc.Global.t)
-              (Trait := ℐ))) in
-        M.call (α0 boxing_errors.EmptyVec.Build)) :
-        M
-          (alloc.boxed.Box.t
-            (dyn [core.error.Error.Trait])
-            alloc.alloc.Global.t))) in
+        (fun (α0 : unit) =>
+          (let* α0 := M.alloc α0 in
+          match_operator
+            α0
+            [
+              fun γ =>
+                (let* α0 :
+                    boxing_errors.EmptyVec.t ->
+                      M
+                        (alloc.boxed.Box.t
+                          (dyn [core.error.Error.Trait])
+                          alloc.alloc.Global.t) :=
+                  ltac:(M.get_method (fun ℐ =>
+                    core.convert.Into.into
+                      (Self := boxing_errors.EmptyVec.t)
+                      (T :=
+                        alloc.boxed.Box.t
+                          (dyn [core.error.Error.Trait])
+                          alloc.alloc.Global.t)
+                      (Trait := ℐ))) in
+                M.call (α0 boxing_errors.EmptyVec.Build)) :
+                M
+                  (alloc.boxed.Box.t
+                    (dyn [core.error.Error.Trait])
+                    alloc.alloc.Global.t)
+            ]) :
+          M
+            (alloc.boxed.Box.t
+              (dyn [core.error.Error.Trait])
+              alloc.alloc.Global.t))) in
   M.call
     ((core.result.Result.t
           (ref (ref str.t))

CoqOfRust/examples/default/examples/rust_book/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v

@@ -149,25 +149,34 @@ Definition main : M unit :=
         (unit ->
           M unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t) :=
     M.alloc
-      ((let* _ : M.Val unit :=
-        let* _ : M.Val unit :=
-          let* α0 : ref str.t :=
-            M.read (mk_str "Providing lemon as fallback
+      (fun (α0 : unit) =>
+        (let* α0 := M.alloc α0 in
+        match_operator
+          α0
+          [
+            fun γ =>
+              (let* _ : M.Val unit :=
+                let* _ : M.Val unit :=
+                  let* α0 : ref str.t :=
+                    M.read (mk_str "Providing lemon as fallback
 ") in
-          let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
-          let* α2 : core.fmt.Arguments.t :=
-            M.call
-              (core.fmt.Arguments.t::["new_const"]
-                (pointer_coercion "Unsize" (borrow α1))) in
-          let* α3 : unit := M.call (std.io.stdio._print α2) in
-          M.alloc α3 in
-        M.alloc tt in
-      let* α0 :
-          M.Val unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t :=
-        M.alloc
-          unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon in
-      M.read α0) :
-      M unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t) in
+                  let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
+                  let* α2 : core.fmt.Arguments.t :=
+                    M.call
+                      (core.fmt.Arguments.t::["new_const"]
+                        (pointer_coercion "Unsize" (borrow α1))) in
+                  let* α3 : unit := M.call (std.io.stdio._print α2) in
+                  M.alloc α3 in
+                M.alloc tt in
+              let* α0 :
+                  M.Val
+                    unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t :=
+                M.alloc
+                  unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon in
+              M.read α0) :
+              M unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t
+          ]) :
+        M unpacking_options_and_defaults_via_get_or_insert_with.Fruit.t) in
   let* first_available_fruit :
       M.Val
         (mut_ref

CoqOfRust/examples/default/examples/rust_book/error_handling/unpacking_options_and_defaults_via_or_else.v

@@ -144,61 +144,81 @@ Definition main : M unit :=
             (core.option.Option.t
               unpacking_options_and_defaults_via_or_else.Fruit.t)) :=
     M.alloc
-      ((let* _ : M.Val unit :=
-        let* _ : M.Val unit :=
-          let* α0 : ref str.t :=
-            M.read (mk_str "Providing kiwi as fallback
+      (fun (α0 : unit) =>
+        (let* α0 := M.alloc α0 in
+        match_operator
+          α0
+          [
+            fun γ =>
+              (let* _ : M.Val unit :=
+                let* _ : M.Val unit :=
+                  let* α0 : ref str.t :=
+                    M.read (mk_str "Providing kiwi as fallback
 ") in
-          let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
-          let* α2 : core.fmt.Arguments.t :=
-            M.call
-              (core.fmt.Arguments.t::["new_const"]
-                (pointer_coercion "Unsize" (borrow α1))) in
-          let* α3 : unit := M.call (std.io.stdio._print α2) in
-          M.alloc α3 in
-        M.alloc tt in
-      let* α0 :
-          M.Val
-            (core.option.Option.t
-              unpacking_options_and_defaults_via_or_else.Fruit.t) :=
-        M.alloc
-          (core.option.Option.Some
-            unpacking_options_and_defaults_via_or_else.Fruit.Kiwi) in
-      M.read α0) :
-      M
-        (core.option.Option.t
-          unpacking_options_and_defaults_via_or_else.Fruit.t)) in
+                  let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
+                  let* α2 : core.fmt.Arguments.t :=
+                    M.call
+                      (core.fmt.Arguments.t::["new_const"]
+                        (pointer_coercion "Unsize" (borrow α1))) in
+                  let* α3 : unit := M.call (std.io.stdio._print α2) in
+                  M.alloc α3 in
+                M.alloc tt in
+              let* α0 :
+                  M.Val
+                    (core.option.Option.t
+                      unpacking_options_and_defaults_via_or_else.Fruit.t) :=
+                M.alloc
+                  (core.option.Option.Some
+                    unpacking_options_and_defaults_via_or_else.Fruit.Kiwi) in
+              M.read α0) :
+              M
+                (core.option.Option.t
+                  unpacking_options_and_defaults_via_or_else.Fruit.t)
+          ]) :
+        M
+          (core.option.Option.t
+            unpacking_options_and_defaults_via_or_else.Fruit.t)) in
   let* get_lemon_as_fallback :
       M.Val
         (unit ->
           M
             (core.option.Option.t
               unpacking_options_and_defaults_via_or_else.Fruit.t)) :=
     M.alloc
-      ((let* _ : M.Val unit :=
-        let* _ : M.Val unit :=
-          let* α0 : ref str.t :=
-            M.read (mk_str "Providing lemon as fallback
+      (fun (α0 : unit) =>
+        (let* α0 := M.alloc α0 in
+        match_operator
+          α0
+          [
+            fun γ =>
+              (let* _ : M.Val unit :=
+                let* _ : M.Val unit :=
+                  let* α0 : ref str.t :=
+                    M.read (mk_str "Providing lemon as fallback
 ") in
-          let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
-          let* α2 : core.fmt.Arguments.t :=
-            M.call
-              (core.fmt.Arguments.t::["new_const"]
-                (pointer_coercion "Unsize" (borrow α1))) in
-          let* α3 : unit := M.call (std.io.stdio._print α2) in
-          M.alloc α3 in
-        M.alloc tt in
-      let* α0 :
-          M.Val
-            (core.option.Option.t
-              unpacking_options_and_defaults_via_or_else.Fruit.t) :=
-        M.alloc
-          (core.option.Option.Some
-            unpacking_options_and_defaults_via_or_else.Fruit.Lemon) in
-      M.read α0) :
-      M
-        (core.option.Option.t
-          unpacking_options_and_defaults_via_or_else.Fruit.t)) in
+                  let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in
+                  let* α2 : core.fmt.Arguments.t :=
+                    M.call
+                      (core.fmt.Arguments.t::["new_const"]
+                        (pointer_coercion "Unsize" (borrow α1))) in
+                  let* α3 : unit := M.call (std.io.stdio._print α2) in
+                  M.alloc α3 in
+                M.alloc tt in
+              let* α0 :
+                  M.Val
+                    (core.option.Option.t
+                      unpacking_options_and_defaults_via_or_else.Fruit.t) :=
+                M.alloc
+                  (core.option.Option.Some
+                    unpacking_options_and_defaults_via_or_else.Fruit.Lemon) in
+              M.read α0) :
+              M
+                (core.option.Option.t
+                  unpacking_options_and_defaults_via_or_else.Fruit.t)
+          ]) :
+        M
+          (core.option.Option.t
+            unpacking_options_and_defaults_via_or_else.Fruit.t)) in
   let* first_available_fruit :
       M.Val
         (core.option.Option.t

CoqOfRust/examples/default/examples/rust_book/functions/functions_closures.v

@@ -116,7 +116,13 @@ Definition main : M unit :=
       M.alloc α9 in
     M.alloc tt in
   let* one : M.Val (unit -> M i32.t) :=
-    M.alloc ((M.pure ((Integer.of_Z 1) : i32.t)) : M i32.t) in
+    M.alloc
+      (fun (α0 : unit) =>
+        (let* α0 := M.alloc α0 in
+        match_operator
+          α0
+          [ fun γ => (M.pure ((Integer.of_Z 1) : i32.t)) : M i32.t ]) :
+        M i32.t) in
   let* _ : M.Val unit :=
     let* _ : M.Val unit :=
       let* α0 : ref str.t := M.read (mk_str "closure returning one: ") in