Draft: experimental branch for more type-classes inference

CoqOfRust/_std/io.v

@@ -40,7 +40,8 @@ Module Error.
 End Error.
 Definition Error := Error.t.
 
-Definition Result (T : Set) := core.result_types.Result T Error.t.
+Definition Result (T : Set) : Set :=
+  core.result_types.Result T Error.t.
 
 (* pub struct BorrowedBuf<'data> { /* private fields */ } *)
 Module BorrowedBuf.

CoqOfRust/blacklist.txt

@@ -1,9 +1,9 @@
-examples/cargo/concurrent_tests.v
-examples/custom_types/enums_c_like.v
-examples/custom_types/enums_testcase_linked_list.v
-examples/custom_types/enums_type_aliases_v1.v
-examples/custom_types/enums_type_aliases_v2.v
-examples/custom_types/structures.v
+# examples/cargo/concurrent_tests.v
+# examples/custom_types/enums_c_like.v
+# examples/custom_types/enums_testcase_linked_list.v
+# examples/custom_types/enums_type_aliases_v1.v
+# examples/custom_types/enums_type_aliases_v2.v
+# examples/custom_types/structures.v
 examples/error_handling/aliases_for_result.v
 examples/error_handling/boxing_errors.v
 examples/error_handling/combinators_and_then.v
@@ -110,7 +110,7 @@ examples/std_misc/threads_test_case_map_reduce.v
 examples/std_misc/threads.v
 examples/subtle.v
 examples/testing/documentation_testing.v
-examples/traits/clone.v
+# examples/traits/clone.v
 examples/traits/derive.v
 examples/traits/hash.v
 examples/traits/impl_trait_as_return_type.v

CoqOfRust/core/result.v

@@ -10,6 +10,7 @@ Module Iter := Iter.
 Module IterMut := IterMut.
 Module Result := Result.
 Module Impl_PartialEq_for_Result := Impl_PartialEq_for_Result.
+Module Impl_Result := Impl_Result.
 
 Definition IntoIter := IntoIter.t.
 Definition Iter := Iter.t.

CoqOfRust/core/result_impl.v

@@ -31,10 +31,11 @@ Section Impl_Result.
   Context {T E : Set}.
 
   Definition Self : Set := Result T E.
+  Arguments Self /.
 
   Parameter expect :
     forall `{H : State.Trait},
-    Self -> string -> M (H := H) T.
+    Self -> ref str -> M (H := H) T.
 
   Global Instance Method_expect `{State.Trait} :
     Notation.Dot "expect" := {|

coq_translation/default/examples/cargo/concurrent_tests.v

@@ -1,5 +1,6 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
+Require Import smpl.Smpl.
 
 Definition foo
     `{H' : State.Trait}
@@ -21,35 +22,122 @@ Definition foo
     Pure tt
   end.
 
+Smpl Create expect.
+
+(* Check result.Impl_Result.expect. *)
+
+Ltac apply_expect x1 x2 :=
+  eapply result.Impl_Result.expect;
+    try exact x1;
+    try exact x2.
+
+Smpl Add apply_expect : expect.
+
+Set Printing All.
+(* Check result.Impl_Result.expect. *)
+
+Module Method_expect.
+  Class Class `{H' : State.Trait} {Self Argument Result : Set} : Set := {
+    method : Self -> Argument -> M (H := H') Result;
+  }.
+
+  (* Check result.Impl_Result.expect. *)
+
+  Global Instance I `{H' : State.Trait} (T E : Set) : Class := {
+    method := result.Impl_Result.expect (T := T) (E := E);
+  }.
+
+  Global Instance Method_expect `{State.Trait} (T E : Set) :
+    Notation.Dot "expect" := {|
+    Notation.dot := result.Impl_Result.expect (T := T) (E := E);
+  |}.
+End Method_expect.
+
+Module Merged_method_expect.
+  Class Class {Self A : Set} : Set := {
+    merged_method : Self -> A;
+  }.
+
+  (* Check result.Impl_Result.expect. *)
+
+  Global Instance I `{H' : State.Trait} (T E : Set) : Class := {
+    merged_method := result.Impl_Result.expect (T := T) (E := E);
+  }.
+End Merged_method_expect.
+
+Module Explicit_string_method.
+  Class Class `{H' : State.Trait}
+      (name : str) {Self Argument Result : Set} : Set := {
+    method : Self -> Argument -> M (H := H') Result;
+  }.
+
+  Global Instance I `{H' : State.Trait} (T E : Set) : Class "expect" := {
+    method := result.Impl_Result.expect (T := T) (E := E);
+  }.
+End Explicit_string_method.
+
 Module tests.
-  Definition test_file `{H' : State.Trait} : M (H := H') unit :=
+  Definition foo `{H' : State.Trait} : M (H := H') unit :=
     let* file :=
       let* α0 := std.fs.OpenOptions::["new"] in
       let* α1 := α0.["append"] true in
       let* α2 := α1.["create"] true in
       let* α3 := α2.["open"] "ferris.txt" in
-      α3.["expect"] "Failed to open ferris.txt" in
-    let* α0 :=
-      {| std.ops.Range.start := 0; std.ops.Range._end := 5; |}.["into_iter"] in
-    match α0 with
-    | iter =>
-      loop
-        (let* _ :=
-          let* α0 := (addr_of iter).["next"] in
-          match α0 with
-          | core.option.Option.None  => Break
-          | core.option.Option.Some _ =>
-            let* _ :=
-              let* α0 := "Ferris
-".["as_bytes"] in
-              let* α1 := file.["write_all"] α0 in
-              α1.["expect"] "Could not write to ferris.txt" in
-            Pure tt
-          end in
-        Pure tt)
-    end.
+      (* α3.["expect"] "Failed to open ferris.txt" in *)
+      Method_expect.method α3 "Failed to open ferris.txt" in
+    Pure tt.
+
+  Definition foo2 `{H' : State.Trait} : M (H := H') unit :=
+    let* file :=
+      let* α0 := std.fs.OpenOptions::["new"] in
+      let* α1 := α0.["append"] true in
+      let* α2 := α1.["create"] true in
+      let* α3 := α2.["open"] "ferris.txt" in
+      (* α3.["expect"] "Failed to open ferris.txt" in *)
+      (* Merged_method_expect.merged_method α3 "Failed to open ferris.txt" in *)
+      Explicit_string_method.method (name := "expect") α3 "Failed to open ferris.txt" in
+    Pure tt.
+
+  Definition test_file `{H' : State.Trait} :
+      M (H := H') (result.Result std.fs.File _) :=
+    let* file :=
+      let* α0 := std.fs.OpenOptions::["new"] in
+      let* α1 := α0.["append"] true in
+      let* α2 := α1.["create"] true in
+      α2.["open"] "ferris.txt" in
+    Pure file.
+
+  (* Print CoqOfRust.Notation.Dot.
+  Print CoqOfRust.Notation.dot. *)
+
+  Definition test_file2 `{H' : State.Trait} : M (H := H') std.fs.File :=
+    Monad.bind
+      test_file
+      (fun file =>
+        Method_expect.method
+          file
+          "Failed to open ferris.txt"
+      ).
+
+  (* Definition test_file2' `{H' : State.Trait} : M (H := H') std.fs.File :=
+    Monad.bind
+      test_file
+      (fun file =>
+        ltac:(apply result.Impl_Result.expect;
+          try exact file;
+          try exact "Failed to open ferris.txt"
+        )
+      ).
+
+  Definition test_file3 `{H' : State.Trait}
+    (file : result.Result std.fs.File io.Error.t) :
+    M (H := H') std.fs.File :=
+    file.["expect"] "Failed to open ferris.txt". *)
+
+  (* Set Printing All.
+  Print test_file. *)
 
-  Definition test_file_also `{H' : State.Trait} : M (H := H') unit :=
+  (* Definition test_file_also `{H' : State.Trait} : M (H := H') unit :=
     let* file :=
       let* α0 := std.fs.OpenOptions::["new"] in
       let* α1 := α0.["append"] true in
@@ -74,10 +162,10 @@ Module tests.
             Pure tt
           end in
         Pure tt)
-    end.
+    end. *)
 End tests.
 
-Definition test_file `{H' : State.Trait} : M (H := H') unit :=
+(* Definition test_file `{H' : State.Trait} : M (H := H') unit :=
   let* file :=
     let* α0 := std.fs.OpenOptions::["new"] in
     let* α1 := α0.["append"] true in
@@ -129,4 +217,4 @@ Definition test_file_also `{H' : State.Trait} : M (H := H') unit :=
           Pure tt
         end in
       Pure tt)
-  end.
+  end. *)

coq_translation/default/examples/traits/clone.v

@@ -70,7 +70,7 @@ Module Pair.
 End Pair.
 Definition Pair := @Pair.t.
 
-Module Impl_core_clone_Clone_for_clone_Pair.
+(* Module Impl_core_clone_Clone_for_clone_Pair.
   Definition Self := clone.Pair.
 
   Definition clone
@@ -89,7 +89,30 @@ Module Impl_core_clone_Clone_for_clone_Pair.
     core.clone.Clone.clone `{H' : State.Trait} := clone;
   }.
   Global Hint Resolve I : core.
-End Impl_core_clone_Clone_for_clone_Pair.
+End Impl_core_clone_Clone_for_clone_Pair. *)
+
+Parameter debug_tuple_field2_finish :
+  forall `{State.Trait} {T1 T2 : Set}
+    `{core.fmt.Debug.Trait T1} `{core.fmt.Debug.Trait T2},
+  mut_ref core.fmt.Formatter * ref str * T1 * T2 ->
+  M core.fmt.Result.
+
+Module New_static.
+  Class Class `{State.Trait} (Base : Set) (name : string)
+      {Argument Result : Set} : Set := {
+    field : Argument -> M Result;
+  }.
+  Check field.
+
+  Global Instance I `{State.Trait} (T1 T2 : Set)
+      `{core.fmt.Debug.Trait T1} `{core.fmt.Debug.Trait T2} :
+      Class core.fmt.Formatter "debug_tuple_field2_finish" := {
+    field := debug_tuple_field2_finish (T1 := T2) (T2 := T2);
+  }.
+End New_static.
+
+Module Old_static.
+End Old_static.
 
 Module Impl_core_fmt_Debug_for_clone_Pair.
   Definition Self := clone.Pair.
@@ -99,11 +122,14 @@ Module Impl_core_fmt_Debug_for_clone_Pair.
       (self : ref Self)
       (f : mut_ref core.fmt.Formatter)
       : M (H := H') core.fmt.Result :=
-    core.fmt.Formatter::["debug_tuple_field2_finish"]
-      f
-      "Pair"
-      (addr_of (self.[0]))
-      (addr_of (addr_of (self.[1]))).
+    (* core.fmt.Formatter::["debug_tuple_field2_finish"] *)
+    New_static.field
+        (Base := core.fmt.Formatter) (name := "debug_tuple_field2_finish") (
+      f,
+      "Pair",
+      (addr_of (self.[0])),
+      (addr_of (addr_of (self.[1])))
+    ).
 
   Global Instance Method_fmt `{H' : State.Trait} : Notation.Dot "fmt" := {
     Notation.dot := fmt;
@@ -115,7 +141,7 @@ Module Impl_core_fmt_Debug_for_clone_Pair.
   Global Hint Resolve I : core.
 End Impl_core_fmt_Debug_for_clone_Pair.
 
-(* #[allow(dead_code)] - function was ignored by the compiler *)
+(* #[allow(dead_code)] - function was ignored by the compiler
 Definition main `{H' : State.Trait} : M (H := H') unit :=
   let unit := clone.Unit.Build in
   let copied_unit := unit in
@@ -176,4 +202,4 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
           (addr_of [ α0 ]) in
       std.io.stdio._print α1 in
     Pure tt in
-  Pure tt.
+  Pure tt. *)