From ac93f4e638ec47542ed3b89461440f8ad2a18267 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Sat, 7 Oct 2023 18:02:14 +0200 Subject: [PATCH] wip --- CoqOfRust/_std/io.v | 3 +- CoqOfRust/blacklist.txt | 14 +- CoqOfRust/core/result.v | 1 + CoqOfRust/core/result_impl.v | 3 +- .../default/examples/cargo/concurrent_tests.v | 138 ++++++++++++++---- .../default/examples/traits/clone.v | 44 ++++-- 6 files changed, 160 insertions(+), 43 deletions(-) diff --git a/CoqOfRust/_std/io.v b/CoqOfRust/_std/io.v index 3282d5d4e..a2ac95eb5 100644 --- a/CoqOfRust/_std/io.v +++ b/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. diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt index 14ff42f84..62107574e 100644 --- a/CoqOfRust/blacklist.txt +++ b/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 diff --git a/CoqOfRust/core/result.v b/CoqOfRust/core/result.v index cb37f85b0..a90bfd0b6 100644 --- a/CoqOfRust/core/result.v +++ b/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. diff --git a/CoqOfRust/core/result_impl.v b/CoqOfRust/core/result_impl.v index 4b62433fa..7dd862eea 100644 --- a/CoqOfRust/core/result_impl.v +++ b/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" := {| diff --git a/coq_translation/default/examples/cargo/concurrent_tests.v b/coq_translation/default/examples/cargo/concurrent_tests.v index 1ade4dc75..bb87c21e9 100644 --- a/coq_translation/default/examples/cargo/concurrent_tests.v +++ b/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. *) diff --git a/coq_translation/default/examples/traits/clone.v b/coq_translation/default/examples/traits/clone.v index 735ee2810..9fe500b72 100644 --- a/coq_translation/default/examples/traits/clone.v +++ b/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. *)