Merge pull request #449 from formal-land/guillaume-claret@move-rust_b…

…ook-examples-to-dedicated-folder

ci: move Rust Book examples to dedicated folder

CoqOfRust/blacklist.txt

@@ -1,100 +1,96 @@
 std/iter_type.v
 std/iter.v
 std/net.v
-examples/axiomatized
-examples/axiomatized/examples/conversion/try_from_and_try_into.v
-examples/axiomatized/examples/custom_types/enums_testcase_linked_list.v
-examples/axiomatized/examples/error_handling/boxing_errors.v
-examples/axiomatized/examples/error_handling/other_uses_of_question_mark.v
-examples/axiomatized/examples/error_handling/unpacking_options_via_question_mark.v
-examples/axiomatized/examples/error_handling/wrapping_errors.v
-examples/axiomatized/examples/expressions/const_underscore_expression.v
-examples/axiomatized/examples/functions/functions_closures_as_input_parameters.v
-examples/axiomatized/examples/functions/functions_closures_as_output_parameters.v
-examples/axiomatized/examples/functions/functions_closures_input_functions.v
-examples/axiomatized/examples/functions/functions_closures_type_anonymity_define_and_use.v
-examples/axiomatized/examples/generics/generics_associated_types_solution.v
-examples/axiomatized/examples/generics/generics_functions.v
-examples/axiomatized/examples/generics/generics_implementation.v
-examples/axiomatized/examples/generics/generics_phantom_type_test_case_unit_clarification.v
-examples/axiomatized/examples/generics/generics_phantom_type.v
-examples/axiomatized/examples/generics/generics_traits.v
-examples/axiomatized/examples/generics/generics_where_clauses.v
-examples/axiomatized/examples/modules/struct_visibility.v
-examples/axiomatized/examples/modules/super_and_self.v
-examples/axiomatized/examples/modules/the_use_as_declaration.v
-examples/axiomatized/examples/modules/visibility.v
-examples/axiomatized/examples/scoping_rules/scoping_rules_lifetimes_bounds.v
-examples/axiomatized/examples/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
-examples/axiomatized/examples/scoping_rules/scoping_rules_raii_desctructor.v
-examples/axiomatized/examples/std_library_types/hash_map_alternate_or_custom_key_types.v
-examples/axiomatized/examples/std_library_types/strings_raw_string_literals.v
-examples/axiomatized/examples/std_misc/file_io_read_lines_efficient_method.v
-examples/axiomatized/examples/std_misc/file_io_read_lines.v
-examples/axiomatized/examples/std_misc/filesystem_operations.v
-examples/axiomatized/examples/std_misc/foreign_function_interface.v
+examples/axiomatized/examples/rust_book/conversion/try_from_and_try_into.v
+examples/axiomatized/examples/rust_book/custom_types/enums_testcase_linked_list.v
+examples/axiomatized/examples/rust_book/error_handling/boxing_errors.v
+examples/axiomatized/examples/rust_book/error_handling/other_uses_of_question_mark.v
+examples/axiomatized/examples/rust_book/error_handling/unpacking_options_via_question_mark.v
+examples/axiomatized/examples/rust_book/error_handling/wrapping_errors.v
+examples/axiomatized/examples/rust_book/expressions/const_underscore_expression.v
+examples/axiomatized/examples/rust_book/functions/functions_closures_as_input_parameters.v
+examples/axiomatized/examples/rust_book/functions/functions_closures_as_output_parameters.v
+examples/axiomatized/examples/rust_book/functions/functions_closures_input_functions.v
+examples/axiomatized/examples/rust_book/functions/functions_closures_type_anonymity_define_and_use.v
+examples/axiomatized/examples/rust_book/functions/functions_closures_type_anonymity_define.v
+examples/axiomatized/examples/rust_book/generics/generics_associated_types_solution.v
+examples/axiomatized/examples/rust_book/generics/generics_functions.v
+examples/axiomatized/examples/rust_book/generics/generics_implementation.v
+examples/axiomatized/examples/rust_book/generics/generics_phantom_type_test_case_unit_clarification.v
+examples/axiomatized/examples/rust_book/generics/generics_phantom_type.v
+examples/axiomatized/examples/rust_book/generics/generics_traits.v
+examples/axiomatized/examples/rust_book/generics/generics_where_clauses.v
+examples/axiomatized/examples/rust_book/modules/struct_visibility.v
+examples/axiomatized/examples/rust_book/modules/super_and_self.v
+examples/axiomatized/examples/rust_book/modules/the_use_as_declaration.v
+examples/axiomatized/examples/rust_book/modules/visibility.v
+examples/axiomatized/examples/rust_book/scoping_rules/scoping_rules_lifetimes_bounds.v
+examples/axiomatized/examples/rust_book/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
+examples/axiomatized/examples/rust_book/scoping_rules/scoping_rules_raii_desctructor.v
+examples/axiomatized/examples/rust_book/std_library_types/hash_map_alternate_or_custom_key_types.v
+examples/axiomatized/examples/rust_book/std_library_types/strings_raw_string_literals.v
+examples/axiomatized/examples/rust_book/std_misc/file_io_read_lines_efficient_method.v
+examples/axiomatized/examples/rust_book/std_misc/file_io_read_lines.v
+examples/axiomatized/examples/rust_book/std_misc/filesystem_operations.v
+examples/axiomatized/examples/rust_book/std_misc/foreign_function_interface.v
+examples/axiomatized/examples/rust_book/traits/disambiguating_overlapping_traits.v
+examples/axiomatized/examples/rust_book/traits/hash.v
+examples/axiomatized/examples/rust_book/traits/impl_trait_as_return_type.v
+examples/axiomatized/examples/rust_book/traits/iterators.v
+examples/axiomatized/examples/rust_book/traits/operator_overloading.v
+examples/axiomatized/examples/rust_book/traits/returning_traits_with_dyn.v
+examples/axiomatized/examples/rust_book/traits/supertraits.v
+examples/axiomatized/examples/rust_book/traits/traits_parms.v
+examples/axiomatized/examples/rust_book/traits/traits.v
 examples/axiomatized/examples/subtle.v
 examples/axiomatized/examples/test0.v
-examples/axiomatized/examples/traits/disambiguating_overlapping_traits.v
-examples/axiomatized/examples/traits/hash.v
-examples/axiomatized/examples/traits/impl_trait_as_return_type.v
-examples/axiomatized/examples/traits/iterators.v
-examples/axiomatized/examples/traits/operator_overloading.v
-examples/axiomatized/examples/traits/returning_traits_with_dyn.v
-examples/axiomatized/examples/traits/supertraits.v
-examples/axiomatized/examples/traits/traits_parms.v
-examples/axiomatized/examples/traits/traits.v
-examples/default/examples/custom_types/enums_c_like.v
-examples/default/examples/custom_types/enums_testcase_linked_list.v
-examples/default/examples/error_handling/pulling_results_out_of_options_with_stop_error_processing.v
-examples/default/examples/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v
-examples/default/examples/error_handling/unpacking_options_and_defaults_via_or_else.v
-examples/default/examples/error_handling/unpacking_options_via_question_mark.v
-examples/default/examples/error_handling/wrapping_errors.v
-examples/default/examples/flow_of_control/for_and_iterators_iter_mut.v
-examples/default/examples/flow_of_control/loop_nesting_and_labels.v
-examples/default/examples/flow_of_control/loop_returning_from_loops.v
-examples/default/examples/flow_of_control/match_destructuring_arrays_slices.v
-examples/default/examples/functions/diverging_functions_example_sum_odd_numbers.v
-examples/default/examples/functions/functions_closures_as_input_parameters.v
-examples/default/examples/functions/functions_closures_as_output_parameters.v
-examples/default/examples/functions/functions_closures_capturing.v
-examples/default/examples/functions/functions_closures_example_searching_through_iterators_Iterator_find.v
-examples/default/examples/functions/functions_closures_forced_capturing_with_move.v
-examples/default/examples/functions/functions_closures_input_functions.v
-examples/default/examples/functions/functions_closures_type_anonymity_define_and_use.v
-examples/default/examples/functions/functions_closures_type_anonymity_define_and_use.v
-examples/default/examples/functions/functions_closures_type_anonymity_define.v
-examples/default/examples/functions/functions_closures.v
-examples/default/examples/generics/generics_associated_types_solution.v
-examples/default/examples/generics/generics_functions.v
-examples/default/examples/generics/generics_implementation.v
-examples/default/examples/generics/generics_phantom_type_test_case_unit_clarification.v
-examples/default/examples/generics/generics_phantom_type.v
-examples/default/examples/generics/generics.v
 examples/default/examples/ink_contracts/Proofs/erc20.v
-examples/default/examples/macro_rules/macro_rules_designators.v
-examples/default/examples/macro_rules/macro_rules_repeat.v
-examples/default/examples/modules/struct_visibility.v
-examples/default/examples/modules/super_and_self.v
-examples/default/examples/modules/the_use_as_declaration.v
-examples/default/examples/modules/visibility.v
-examples/default/examples/primitives/arrays_and_slices.v
-examples/default/examples/primitives/tuples.v
-examples/default/examples/scoping_rules/scoping_rules_lifetimes_bounds.v
-examples/default/examples/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
-examples/default/examples/std_library_types/hash_map_hash_set.v
-examples/default/examples/std_misc/file_io_read_lines_efficient_method.v
-examples/default/examples/std_misc/foreign_function_interface.v
-examples/default/examples/std_misc/program_arguments_parsing.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/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
+examples/default/examples/rust_book/flow_of_control/loop_returning_from_loops.v
+examples/default/examples/rust_book/flow_of_control/match_destructuring_arrays_slices.v
+examples/default/examples/rust_book/functions/diverging_functions_example_sum_odd_numbers.v
+examples/default/examples/rust_book/functions/functions_closures_as_input_parameters.v
+examples/default/examples/rust_book/functions/functions_closures_as_output_parameters.v
+examples/default/examples/rust_book/functions/functions_closures_capturing.v
+examples/default/examples/rust_book/functions/functions_closures_example_searching_through_iterators_Iterator_find.v
+examples/default/examples/rust_book/functions/functions_closures_forced_capturing_with_move.v
+examples/default/examples/rust_book/functions/functions_closures_input_functions.v
+examples/default/examples/rust_book/functions/functions_closures_type_anonymity_define_and_use.v
+examples/default/examples/rust_book/functions/functions_closures_type_anonymity_define_and_use.v
+examples/default/examples/rust_book/functions/functions_closures_type_anonymity_define.v
+examples/default/examples/rust_book/functions/functions_closures.v
+examples/default/examples/rust_book/functions/functions_order.v
+examples/default/examples/rust_book/generics/generics_associated_types_solution.v
+examples/default/examples/rust_book/generics/generics_functions.v
+examples/default/examples/rust_book/generics/generics_implementation.v
+examples/default/examples/rust_book/generics/generics_phantom_type_test_case_unit_clarification.v
+examples/default/examples/rust_book/generics/generics_phantom_type.v
+examples/default/examples/rust_book/generics/generics.v
+examples/default/examples/rust_book/macro_rules/macro_rules_designators.v
+examples/default/examples/rust_book/macro_rules/macro_rules_repeat.v
+examples/default/examples/rust_book/modules/struct_visibility.v
+examples/default/examples/rust_book/modules/super_and_self.v
+examples/default/examples/rust_book/modules/the_use_as_declaration.v
+examples/default/examples/rust_book/modules/visibility.v
+examples/default/examples/rust_book/primitives/arrays_and_slices.v
+examples/default/examples/rust_book/primitives/tuples.v
+examples/default/examples/rust_book/scoping_rules/scoping_rules_lifetimes_bounds.v
+examples/default/examples/rust_book/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
+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/traits/hash.v
+examples/default/examples/rust_book/traits/impl_trait_as_return_type.v
+examples/default/examples/rust_book/traits/iterators.v
+examples/default/examples/rust_book/traits/returning_traits_with_dyn.v
+examples/default/examples/rust_book/traits/supertraits.v
+examples/default/examples/rust_book/traits/traits.v
 examples/default/examples/subtle.v
 examples/default/examples/test0.v
-examples/default/examples/traits/hash.v
-examples/default/examples/traits/impl_trait_as_return_type.v
-examples/default/examples/traits/iterators.v
-examples/default/examples/traits/returning_traits_with_dyn.v
-examples/default/examples/traits/supertraits.v
-examples/default/examples/traits/traits.v
 ink/
 ink/erc20.v
 ink/ink_e2e.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/ops.v

@@ -343,16 +343,15 @@ End deref.
 
 Module function.
   Module FnOnce.
-    Class Trait (Self : Set) {Args : Set} : Type := {
+    Class Trait (Self : Set) {Args : Set} {Output : Set} : Set := {
       Output : Set;
       call_once : Self -> Args -> M Output;
     }.
   End FnOnce.
 
   Module FnMut.
-    Class Trait (Self : Set) {Args : Set} : Type := {
-      L0 :: FnOnce.Trait Self (Args := Args);
-      call_mut : mut_ref Self -> Args -> M FnOnce.Output;
+    Class Trait (Self : Set) {Args : Set} {FnOnce_Output : Set} : Set := {
+      call_mut : mut_ref Self -> Args -> M FnOnce_Output;
     }.
   End FnMut.
 End function.

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);
   }.
 
   (*
@@ -157,13 +157,38 @@ 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).
 
   Global Instance AF_or : Notations.DoubleColon Self "or" := {
     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);
   |}.
 
   (*
@@ -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/axiomatized/examples/custom_types/enums_c_like.v → CoqOfRust/examples/axiomatized/examples/rust_book/custom_types/enums_c_like.v

@@ -13,6 +13,10 @@ Module Color.
   | Red
   | Green
   | Blue.
+
+  Definition Red_discriminant : isize.t := Integer.of_Z 16711680.
+  Definition Green_discriminant : isize.t := Integer.of_Z 65280.
+  Definition Blue_discriminant : isize.t := Integer.of_Z 255.
 End Color.
 
 (*