wip: add impl as axiom instead of notation

formal-land · Jan 16, 2024 · 0722bc4 · 0722bc4
1 parent 5b57510
commit 0722bc4
Show file tree

Hide file tree

Showing 313 changed files with 4,234 additions and 7,142 deletions.
diff --git a/CoqOfRust/_std/ops.v b/CoqOfRust/_std/ops.v
@@ -239,12 +239,16 @@ pub trait Generator<R = ()> {
 }
 *)
 Module Generator.
-  Class Trait (Self : Set) (R : option Set) (Yield Return : Set) : Set := {
-    R := defaultType R unit;
+  Class Trait (Self : Set) {R Yield Return : Set} : Set := {
+    R := R;
     Yield := Yield;
     Return := Return;
     resume : Pin (mut_ref Self) -> R -> GeneratorState Yield Return;
   }.
+
+  Module Default.
+    Definition R : Set := unit.
+  End Default.
 End Generator.
 
 (* 

diff --git a/CoqOfRust/alloc/collections/btree/map.v b/CoqOfRust/alloc/collections/btree/map.v
@@ -33,7 +33,6 @@ where
 Module Cursor.
   Parameter t : Set -> Set -> Set.
 End Cursor.
-Definition Cursor := Cursor.t.
 
 (* 
 pub struct CursorMut<'a, K, V, A = Global>
@@ -45,8 +44,6 @@ where
 Module CursorMut.
   Parameter t : Set -> Set -> Set -> Set.
 End CursorMut.
-Definition CursorMut (K V : Set) (A : option Set) := 
-  CursorMut.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct DrainFilter<'a, K, V, F, A = Global>
@@ -61,11 +58,6 @@ Module DrainFilter.
     `{core.clone.Clone.Trait A},
     Set.
 End DrainFilter.
-Definition DrainFilter (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  DrainFilter.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct OccupiedEntry<'a, K, V, A = Global>
@@ -79,11 +71,6 @@ Module OccupiedEntry.
     `{core.clone.Clone.Trait A},
     Set.
 End OccupiedEntry.
-Definition OccupiedEntry (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  OccupiedEntry.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct OccupiedError<'a, K, V, A = Global>
@@ -101,15 +88,10 @@ Module OccupiedError.
     `{alloc.Allocator.Trait A}
     `{core.clone.Clone.Trait A}
   : Set := { 
-    entry : OccupiedEntry K V (Some A);
+    entry : OccupiedEntry.t K V A;
     value : V;
   }.
 End OccupiedError.
-Definition OccupiedError (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  OccupiedError.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct BTreeMap<K, V, A = Global>
@@ -127,11 +109,6 @@ Module BTreeMap.
     Definition A : Set := alloc.Global.t.
   End Default.
 End BTreeMap.
-Definition BTreeMap (K V A : Set)
-  {H0 : alloc.Allocator.Trait A}
-  {H1 : core.clone.Clone.Trait A} :
-  Set :=
-  M.Val (BTreeMap.t K V A).
 
 (* 
 pub struct IntoIter<K, V, A = Global>
@@ -145,11 +122,6 @@ Module IntoIter.
     `{core.clone.Clone.Trait A},
     Set.
 End IntoIter.
-Definition IntoIter (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  IntoIter.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct IntoKeys<K, V, A = Global>
@@ -163,11 +135,6 @@ Module IntoKeys.
     `{core.clone.Clone.Trait A},
     Set.
 End IntoKeys.
-Definition IntoKeys (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  IntoKeys.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct IntoValues<K, V, A = Global>
@@ -181,11 +148,6 @@ Module IntoValues.
     `{core.clone.Clone.Trait A},
     Set.
 End IntoValues.
-Definition IntoValues (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  IntoValues.t K V (defaultType A alloc.Global.t).
 
 (* 
 pub struct Iter<'a, K, V>
@@ -197,7 +159,6 @@ where
 Module Iter.
   Parameter t : Set -> Set -> Set.
 End Iter.
-Definition Iter := Iter.t.
 
 (* 
 pub struct IterMut<'a, K, V>
@@ -209,13 +170,11 @@ where
 Module IterMut.
   Parameter t : Set -> Set -> Set.
 End IterMut.
-Definition IterMut := IterMut.t.
 
 (* pub struct Keys<'a, K, V> { /* private fields */ } *)
 Module Keys.
   Parameter t : Set -> Set -> Set.
 End Keys.
-Definition Keys := Keys.t.
 
 (* 
 pub struct Range<'a, K, V>
@@ -227,7 +186,6 @@ where
 Module Range.
   Parameter t : Set -> Set -> Set.
 End Range.
-Definition Range := Range.t.
 
 (* 
 pub struct RangeMut<'a, K, V>
@@ -239,7 +197,6 @@ where
 Module RangeMut.
   Parameter t : Set -> Set -> Set.
 End RangeMut.
-Definition RangeMut := RangeMut.t.
 
 (* 
 pub struct VacantEntry<'a, K, V, A = Global>
@@ -253,23 +210,16 @@ Module VacantEntry.
     `{core.clone.Clone.Trait A},
     Set.
 End VacantEntry.
-Definition VacantEntry (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  VacantEntry.t K V (defaultType A alloc.Global.t).
 
 (* pub struct Values<'a, K, V> { /* private fields */ } *)
 Module Values.
   Parameter t : Set -> Set -> Set.
 End Values.
-Definition Values := Values.t.
 
 (* pub struct ValuesMut<'a, K, V> { /* private fields */ } *)
 Module ValuesMut.
   Parameter t : Set -> Set -> Set.
 End ValuesMut.
-Definition ValuesMut := ValuesMut.t.
 
 (* ********ENUMS******** *)
 (* 
@@ -297,8 +247,3 @@ Module Entry.
   | Occupied
   .
 End Entry.
-Definition Entry (K V : Set) (A : option Set)
-  `{alloc.Allocator.Trait (defaultType A alloc.Global.t)}
-  `{core.clone.Clone.Trait (defaultType A alloc.Global.t)}
-  : Set :=
-  Entry.t K V (defaultType A alloc.Global.t).
diff --git a/CoqOfRust/alloc/vec.v b/CoqOfRust/alloc/vec.v
@@ -27,11 +27,6 @@ where
 Module DrainFilter.
   Parameter t : forall (T F A : Set), Set.
 End DrainFilter.
-Definition DrainFilter (T F : Set) (A : option Set)
-  `{Allocator.Trait (defaultType A alloc.Global.t)} 
-  `{FnMut.Trait F (mut_ref T -> bool)}
-  : Set :=
-  DrainFilter.t T F (defaultType A alloc.Global.t).
   (* 
   let A_type := (defaultType A Global) in
   let traits 
@@ -50,8 +45,6 @@ where
 Module Drain.
   Parameter t : forall (T A : Set), Set.
 End Drain.
-Definition Drain (T : Set) (A : option Set) : Set :=
-  Drain.t T (defaultType A alloc.Global.t).
   (* 
   let A_type := (defaultType A Global) in
   let traits 
@@ -71,8 +64,6 @@ Module into_iter.
   Module IntoIter.
     Parameter t : forall (T A : Set), Set.
   End IntoIter.
-  Definition IntoIter (T : Set) (A : option Set) :=
-    IntoIter.t T (defaultType A alloc.Global.t).
     (* 
     let A_type := (defaultType A Global) in
     let traits 
@@ -94,8 +85,6 @@ where
 Module Splice.
   Parameter t : forall (I A : Set), Set.
 End Splice.
-Definition Splice (I : Set) (A : option Set) :=
-  Splice.t I (defaultType A alloc.Global.t).
 
 (* BUGGED: same as above *)
 (* 

diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt
@@ -44,17 +44,11 @@ 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/conversion/parsing_a_string.v
 examples/default/examples/conversion/try_from_and_try_into.v
 examples/default/examples/custom_types/enums_c_like.v
 examples/default/examples/custom_types/enums_testcase_linked_list.v
 examples/default/examples/custom_types/structures.v
-examples/default/examples/error_handling/aliases_for_result.v
 examples/default/examples/error_handling/boxing_errors.v
-examples/default/examples/error_handling/defining_an_error_type.v
-examples/default/examples/error_handling/early_returns.v
-examples/default/examples/error_handling/introducing_question_mark_is_an_replacement_for_deprecated_try.v
-examples/default/examples/error_handling/introducing_question_mark.v
 examples/default/examples/error_handling/iterating_over_results_collect_valid_values_and_failures_via_partition_unwrapped.v
 examples/default/examples/error_handling/iterating_over_results_collect_valid_values_and_failures_via_partition.v
 examples/default/examples/error_handling/iterating_over_results_collect_via_map_err_and_filter_map.v
@@ -63,14 +57,10 @@ examples/default/examples/error_handling/iterating_over_results_failed.v
 examples/default/examples/error_handling/iterating_over_results_handle_via_filter_map.v
 examples/default/examples/error_handling/map_in_result_via_combinators.v
 examples/default/examples/error_handling/map_in_result_via_match.v
-examples/default/examples/error_handling/multiple_error_types.v
 examples/default/examples/error_handling/other_uses_of_question_mark.v
 examples/default/examples/error_handling/pulling_results_out_of_options_with_stop_error_processing.v
-examples/default/examples/error_handling/pulling_results_out_of_options.v
-examples/default/examples/error_handling/result_use_in_main.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_and_defaults_via_or.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
@@ -102,47 +92,38 @@ examples/default/examples/generics/generics_phantom_type_test_case_unit_clarific
 examples/default/examples/generics/generics_phantom_type.v
 examples/default/examples/generics/generics.v
 examples/default/examples/guessing_game/guessing_game.v
-examples/default/examples/hello_world/formatted_print.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/literals_operators.v
 examples/default/examples/primitives/tuples.v
 examples/default/examples/scoping_rules/scoping_rules_borrowing.v
 examples/default/examples/scoping_rules/scoping_rules_lifetimes_bounds.v
 examples/default/examples/scoping_rules/scoping_rules_lifetimes_structs.v
-examples/default/examples/scoping_rules/scoping_rules_lifetimes_traits.v
 examples/default/examples/scoping_rules/scoping_rules_ownership_and_rules_mutablity.v
 examples/default/examples/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
 examples/default/examples/std_library_types/arc.v
 examples/default/examples/std_library_types/box_stack_heap.v
 examples/default/examples/std_library_types/hash_map_alternate_or_custom_key_types.v
 examples/default/examples/std_library_types/hash_map_hash_set.v
 examples/default/examples/std_library_types/hash_map.v
-examples/default/examples/std_library_types/option.v
 examples/default/examples/std_library_types/rc.v
 examples/default/examples/std_library_types/result_chaining_with_question_mark.v
 examples/default/examples/std_library_types/result.v
-examples/default/examples/std_library_types/strings_byte_strings_as_non_utf8.v
 examples/default/examples/std_library_types/strings_literals_and_escapes.v
 examples/default/examples/std_library_types/strings_raw_string_literals.v
 examples/default/examples/std_library_types/strings.v
 examples/default/examples/std_library_types/vectors.v
 examples/default/examples/std_misc/channels.v
 examples/default/examples/std_misc/child_processes_pipes.v
-examples/default/examples/std_misc/child_processes_wait.v
 examples/default/examples/std_misc/child_processes.v
-examples/default/examples/std_misc/file_io_create.v
-examples/default/examples/std_misc/file_io_open.v
 examples/default/examples/std_misc/file_io_read_lines_efficient_method.v
 examples/default/examples/std_misc/file_io_read_lines.v
 examples/default/examples/std_misc/filesystem_operations.v
 examples/default/examples/std_misc/foreign_function_interface.v
-examples/default/examples/std_misc/path.v
 examples/default/examples/std_misc/program_arguments_parsing.v
 examples/default/examples/std_misc/program_arguments.v
 examples/default/examples/std_misc/threads_test_case_map_reduce.v

diff --git a/CoqOfRust/examples/axiomatized/examples/conversion/converting_to_string.v b/CoqOfRust/examples/axiomatized/examples/conversion/converting_to_string.v
@@ -24,9 +24,7 @@ Section Impl_core_fmt_Display_for_converting_to_string_Circle_t.
   Parameter fmt :
       (ref Self) -> (mut_ref core.fmt.Formatter.t) -> M ltac:(core.fmt.Result).
 
-  Global Instance AssociatedFunction_fmt : Notations.DoubleColon Self "fmt" := {
-    Notations.double_colon := fmt;
-  }.
+  Axiom fmt_is_impl : impl Self "fmt" = fmt.
 
   Global Instance ℐ : core.fmt.Display.Trait Self := {
     core.fmt.Display.fmt := fmt;

diff --git a/CoqOfRust/examples/axiomatized/examples/conversion/from.v b/CoqOfRust/examples/axiomatized/examples/conversion/from.v
@@ -23,10 +23,7 @@ Section Impl_core_convert_From_i32_t_for_from_Number_t.
   *)
   Parameter from : i32.t -> M Self.
 
-  Global Instance AssociatedFunction_from :
-    Notations.DoubleColon Self "from" := {
-    Notations.double_colon := from;
-  }.
+  Axiom from_is_impl : impl Self "from" = from.
 
   Global Instance ℐ : core.convert.From.Trait Self (T := i32.t) := {
     core.convert.From.from := from;

diff --git a/CoqOfRust/examples/axiomatized/examples/conversion/into.v b/CoqOfRust/examples/axiomatized/examples/conversion/into.v
@@ -23,10 +23,7 @@ Section Impl_core_convert_From_i32_t_for_into_Number_t.
   *)
   Parameter from : i32.t -> M Self.
 
-  Global Instance AssociatedFunction_from :
-    Notations.DoubleColon Self "from" := {
-    Notations.double_colon := from;
-  }.
+  Axiom from_is_impl : impl Self "from" = from.
 
   Global Instance ℐ : core.convert.From.Trait Self (T := i32.t) := {
     core.convert.From.from := from;

diff --git a/CoqOfRust/examples/axiomatized/examples/conversion/try_from_and_try_into.v b/CoqOfRust/examples/axiomatized/examples/conversion/try_from_and_try_into.v
@@ -22,9 +22,7 @@ Section Impl_core_fmt_Debug_for_try_from_and_try_into_EvenNumber_t.
   Parameter fmt :
       (ref Self) -> (mut_ref core.fmt.Formatter.t) -> M ltac:(core.fmt.Result).
 
-  Global Instance AssociatedFunction_fmt : Notations.DoubleColon Self "fmt" := {
-    Notations.double_colon := fmt;
-  }.
+  Axiom fmt_is_impl : impl Self "fmt" = fmt.
 
   Global Instance ℐ : core.fmt.Debug.Trait Self := {
     core.fmt.Debug.fmt := fmt;
@@ -51,9 +49,7 @@ Section Impl_core_cmp_PartialEq_for_try_from_and_try_into_EvenNumber_t.
   Parameter eq :
       (ref Self) -> (ref try_from_and_try_into.EvenNumber.t) -> M bool.t.
 
-  Global Instance AssociatedFunction_eq : Notations.DoubleColon Self "eq" := {
-    Notations.double_colon := eq;
-  }.
+  Axiom eq_is_impl : impl Self "eq" = eq.
 
   Global Instance ℐ :
     core.cmp.PartialEq.Required.Trait Self
@@ -84,10 +80,7 @@ Section Impl_core_convert_TryFrom_i32_t_for_try_from_and_try_into_EvenNumber_t.
   *)
   Parameter try_from : i32.t -> M (core.result.Result.t Self Error.t).
 
-  Global Instance AssociatedFunction_try_from :
-    Notations.DoubleColon Self "try_from" := {
-    Notations.double_colon := try_from;
-  }.
+  Axiom try_from_is_impl : impl Self "try_from" = try_from.
 
   Global Instance ℐ : core.convert.TryFrom.Trait Self (T := i32.t) := {
     core.convert.TryFrom.Error := Error;