fix: fix bug when translating empty return

CoqOfRust/blacklist.txt

@@ -47,9 +47,6 @@ 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_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
 examples/default/examples/rust_book/flow_of_control/for_and_iterators_iter_mut.v
 examples/default/examples/rust_book/flow_of_control/loop_nesting_and_labels.v
@@ -86,7 +83,6 @@ examples/default/examples/rust_book/scoping_rules/scoping_rules_ownership_and_ru
 examples/default/examples/rust_book/std_library_types/hash_map_hash_set.v
 examples/default/examples/rust_book/std_misc/file_io_read_lines_efficient_method.v
 examples/default/examples/rust_book/std_misc/foreign_function_interface.v
-examples/default/examples/rust_book/std_misc/program_arguments_parsing.v
 examples/default/examples/rust_book/traits/hash.v
 examples/default/examples/rust_book/traits/impl_trait_as_return_type.v
 examples/default/examples/rust_book/traits/iterators.v

CoqOfRust/core/error.v

@@ -68,10 +68,10 @@ Module Error.
   Class Trait (Self : Set) : Set := {
     L0 :: fmt.Debug.Trait Self;
     L1 :: fmt.Display.Trait Self;
-    source {A : Set} : ref Self -> M (option.Option.t (ref A));
+    source : ref Self -> M (option.Option.t (ref (dyn [])));
     type_id : ref Self -> private.Internal.t -> M any.TypeId.t;
     description : ref Self -> M (ref str.t);
-    cause {A : Set} : ref Self -> M (option.Option.t (ref A));
+    cause : ref Self -> M (option.Option.t (ref (dyn [])));
     provide : ref Self -> mut_ref any.Demand.t -> M unit;
   }.
 
@@ -80,10 +80,10 @@ Module Error.
     Trait Self := {
     L0 := Required.L0;
     L1 := Required.L1;
-    source {A : Set} := Provided.source (A := A);
+    source := Provided.source;
     type_id := Provided.type_id;
     description := Provided.description;
-    cause {A : Set} := Provided.cause (A := A);
+    cause := Provided.cause;
     provide := Provided.provide;
   }.
 End Error.

CoqOfRust/core/option.v

@@ -128,11 +128,11 @@ Module Impl_Option. Section Impl_Option.
   where
       F: FnOnce(T) -> U,
   *)
-  Parameter map_or : forall {U : Set}, Self -> U -> (T -> M U) -> M U.
+  Parameter map_or : forall {U F : Set}, Self -> U -> F -> M U.
 
-  Global Instance AF_map_or {U : Set} :
+  Global Instance AF_map_or {U F : Set} :
     Notations.DoubleColon Self "map_or" := {
-    Notations.double_colon := map_or (U := U);
+    Notations.double_colon := map_or (U := U) (F := F);
   }.
 
   (*
@@ -178,6 +178,17 @@ Module Impl_Option. Section Impl_Option.
     Notations.double_colon := or;
   }.
 
+  (*
+  pub fn or_else<F>(self, f: F) -> Option<T>
+  where
+      F: FnOnce() -> Option<T>,
+  *)
+  Parameter or_else : forall {F : Set}, Self -> F -> M Self.
+
+  Global Instance AF_or_else {F : Set} : Notations.DoubleColon Self "or_else" := {
+    Notations.double_colon := or_else (F := F);
+  }.
+
   Global Instance I_Default {ℋ : default.Default.Trait T} :
     default.Default.Trait (core.option.Option.t T).
   Admitted.

CoqOfRust/core/result_impl.v

@@ -55,12 +55,12 @@ Section Impl_Result.
   where
       F: FnOnce(T) -> U,
   *)
-  Parameter map : forall {U : Set},
-    Self -> (T -> M U) -> M (Result.t U E).
+  Parameter map : forall {U F : Set},
+    Self -> F -> M (Result.t U E).
 
-  Global Instance AF_map {U : Set} :
+  Global Instance AF_map {U F : Set} :
       Notations.DoubleColon Self "map" := {|
-    Notations.double_colon := map (U := U);
+    Notations.double_colon := map (U := U) (F := F);
   |}.
 
   (*

CoqOfRust/examples/axiomatized/examples/rust_book/error_handling/unpacking_options_via_question_mark.v

@@ -1,16 +1,52 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
-Module  Person.
-Section Person.
+Module  PhoneNumber.
+Section PhoneNumber.
   Record t : Set := {
-    job : core.option.Option.t unpacking_options_via_question_mark.Job.t;
+    area_code : core.option.Option.t u8.t;
+    number : u32.t;
   }.
 
-  Definition Get_job :=
-    Ref.map (fun α => Some α.(job)) (fun β α => Some (α <| job := β |>)).
-End Person.
-End Person.
+  Definition Get_area_code :=
+    Ref.map
+      (fun α => Some α.(area_code))
+      (fun β α => Some (α <| area_code := β |>)).
+  Definition Get_number :=
+    Ref.map (fun α => Some α.(number)) (fun β α => Some (α <| number := β |>)).
+End PhoneNumber.
+End PhoneNumber.
+
+Module  Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+Section Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
+
+  (*
+  Clone
+  *)
+  Parameter clone :
+      (ref Self) -> M unpacking_options_via_question_mark.PhoneNumber.t.
+
+  Global Instance AssociatedFunction_clone :
+    Notations.DoubleColon Self "clone" := {
+    Notations.double_colon := clone;
+  }.
+
+  Global Instance ℐ : core.clone.Clone.Required.Trait Self := {
+    core.clone.Clone.clone := clone;
+    core.clone.Clone.clone_from := Datatypes.None;
+  }.
+End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+
+Module  Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
+
+  Global Instance ℐ : core.marker.Copy.Trait Self := {
+  }.
+End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
 
 Module  Job.
 Section Job.
@@ -56,52 +92,16 @@ Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 
-Module  PhoneNumber.
-Section PhoneNumber.
+Module  Person.
+Section Person.
   Record t : Set := {
-    area_code : core.option.Option.t u8.t;
-    number : u32.t;
-  }.
-
-  Definition Get_area_code :=
-    Ref.map
-      (fun α => Some α.(area_code))
-      (fun β α => Some (α <| area_code := β |>)).
-  Definition Get_number :=
-    Ref.map (fun α => Some α.(number)) (fun β α => Some (α <| number := β |>)).
-End PhoneNumber.
-End PhoneNumber.
-
-Module  Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-Section Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
-
-  (*
-  Clone
-  *)
-  Parameter clone :
-      (ref Self) -> M unpacking_options_via_question_mark.PhoneNumber.t.
-
-  Global Instance AssociatedFunction_clone :
-    Notations.DoubleColon Self "clone" := {
-    Notations.double_colon := clone;
+    job : core.option.Option.t unpacking_options_via_question_mark.Job.t;
   }.
 
-  Global Instance ℐ : core.clone.Clone.Required.Trait Self := {
-    core.clone.Clone.clone := clone;
-    core.clone.Clone.clone_from := Datatypes.None;
-  }.
-End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-
-Module  Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
-
-  Global Instance ℐ : core.marker.Copy.Trait Self := {
-  }.
-End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Get_job :=
+    Ref.map (fun α => Some α.(job)) (fun β α => Some (α <| job := β |>)).
+End Person.
+End Person.
 
 Module  Impl_unpacking_options_via_question_mark_Person_t.
 Section Impl_unpacking_options_via_question_mark_Person_t.

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

@@ -1,16 +1,74 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
-Module  Person.
-Section Person.
+Module  PhoneNumber.
+Section PhoneNumber.
   Record t : Set := {
-    job : core.option.Option.t unpacking_options_via_question_mark.Job.t;
+    area_code : core.option.Option.t u8.t;
+    number : u32.t;
   }.
 
-  Definition Get_job :=
-    Ref.map (fun α => Some α.(job)) (fun β α => Some (α <| job := β |>)).
-End Person.
-End Person.
+  Definition Get_area_code :=
+    Ref.map
+      (fun α => Some α.(area_code))
+      (fun β α => Some (α <| area_code := β |>)).
+  Definition Get_number :=
+    Ref.map (fun α => Some α.(number)) (fun β α => Some (α <| number := β |>)).
+End PhoneNumber.
+End PhoneNumber.
+
+Module  Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+Section Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
+
+  (*
+  Clone
+  *)
+  Definition clone
+      (self : ref Self)
+      : M unpacking_options_via_question_mark.PhoneNumber.t :=
+    let* self := M.alloc self in
+    let* α0 : M.Val unpacking_options_via_question_mark.PhoneNumber.t :=
+      match_operator
+        (DeclaredButUndefinedVariable
+          (A := core.clone.AssertParamIsClone.t (core.option.Option.t u8.t)))
+        [
+          fun γ =>
+            (match_operator
+              (DeclaredButUndefinedVariable
+                (A := core.clone.AssertParamIsClone.t u32.t))
+              [
+                fun γ =>
+                  (let* α0 :
+                      ref unpacking_options_via_question_mark.PhoneNumber.t :=
+                    M.read self in
+                  M.pure (deref α0)) :
+                  M (M.Val unpacking_options_via_question_mark.PhoneNumber.t)
+              ]) :
+            M (M.Val unpacking_options_via_question_mark.PhoneNumber.t)
+        ] in
+    M.read α0.
+
+  Global Instance AssociatedFunction_clone :
+    Notations.DoubleColon Self "clone" := {
+    Notations.double_colon := clone;
+  }.
+
+  Global Instance ℐ : core.clone.Clone.Required.Trait Self := {
+    core.clone.Clone.clone := clone;
+    core.clone.Clone.clone_from := Datatypes.None;
+  }.
+End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
+
+Module  Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
+
+  Global Instance ℐ : core.marker.Copy.Trait Self := {
+  }.
+End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
 
 Module  Job.
 Section Job.
@@ -74,74 +132,16 @@ Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_Job_t.
 
-Module  PhoneNumber.
-Section PhoneNumber.
+Module  Person.
+Section Person.
   Record t : Set := {
-    area_code : core.option.Option.t u8.t;
-    number : u32.t;
-  }.
-
-  Definition Get_area_code :=
-    Ref.map
-      (fun α => Some α.(area_code))
-      (fun β α => Some (α <| area_code := β |>)).
-  Definition Get_number :=
-    Ref.map (fun α => Some α.(number)) (fun β α => Some (α <| number := β |>)).
-End PhoneNumber.
-End PhoneNumber.
-
-Module  Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-Section Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
-
-  (*
-  Clone
-  *)
-  Definition clone
-      (self : ref Self)
-      : M unpacking_options_via_question_mark.PhoneNumber.t :=
-    let* self := M.alloc self in
-    let* α0 : M.Val unpacking_options_via_question_mark.PhoneNumber.t :=
-      match_operator
-        (DeclaredButUndefinedVariable
-          (A := core.clone.AssertParamIsClone.t (core.option.Option.t u8.t)))
-        [
-          fun γ =>
-            (match_operator
-              (DeclaredButUndefinedVariable
-                (A := core.clone.AssertParamIsClone.t u32.t))
-              [
-                fun γ =>
-                  (let* α0 :
-                      ref unpacking_options_via_question_mark.PhoneNumber.t :=
-                    M.read self in
-                  M.pure (deref α0)) :
-                  M (M.Val unpacking_options_via_question_mark.PhoneNumber.t)
-              ]) :
-            M (M.Val unpacking_options_via_question_mark.PhoneNumber.t)
-        ] in
-    M.read α0.
-
-  Global Instance AssociatedFunction_clone :
-    Notations.DoubleColon Self "clone" := {
-    Notations.double_colon := clone;
-  }.
-
-  Global Instance ℐ : core.clone.Clone.Required.Trait Self := {
-    core.clone.Clone.clone := clone;
-    core.clone.Clone.clone_from := Datatypes.None;
+    job : core.option.Option.t unpacking_options_via_question_mark.Job.t;
   }.
-End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-End Impl_core_clone_Clone_for_unpacking_options_via_question_mark_PhoneNumber_t.
-
-Module  Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-Section Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-  Definition Self : Set := unpacking_options_via_question_mark.PhoneNumber.t.
 
-  Global Instance ℐ : core.marker.Copy.Trait Self := {
-  }.
-End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
-End Impl_core_marker_Copy_for_unpacking_options_via_question_mark_PhoneNumber_t.
+  Definition Get_job :=
+    Ref.map (fun α => Some α.(job)) (fun β α => Some (α <| job := β |>)).
+End Person.
+End Person.
 
 Module  Impl_unpacking_options_via_question_mark_Person_t.
 Section Impl_unpacking_options_via_question_mark_Person_t.

CoqOfRust/examples/default/examples/rust_book/std_misc/program_arguments_parsing.v

@@ -352,8 +352,7 @@ Definition main : M unit :=
                           let* α0 : unit :=
                             M.call program_arguments_parsing.help in
                           M.alloc α0 in
-                        let* α0 : M.Val unit := M.alloc tt in
-                        let* α0 : M.Val never.t := return_ α0 in
+                        let* α0 : M.Val never.t := return_ tt in
                         let* α1 := M.read α0 in
                         let* α2 : i32.t := never_to_any α1 in
                         M.alloc α2