Merge pull request #501 from formal-land/gy@UniformizeWarnings

Uniformize Warnings & 100 Character Line Width

Author: InfiniteEchoes

CoqOfRust/examples/axiomatized/examples/custom/provided_method.v

@@ -6,10 +6,7 @@ Module ProvidedAndRequired.
   Parameter provided : (list Ty.t) -> (list Value.t) -> M.
 
   Axiom ProvidedMethod_provided :
-    M.IsProvidedMethod
-      "provided_method::ProvidedAndRequired"
-      "provided"
-      provided.
+    M.IsProvidedMethod "provided_method::ProvidedAndRequired" "provided" provided.
 End ProvidedAndRequired.
 
 Module Impl_provided_method_ProvidedAndRequired_for_i32.
@@ -38,9 +35,7 @@ Module Impl_provided_method_ProvidedAndRequired_for_u32.
       Self
       (* Trait polymorphic types *) []
       (* Instance *)
-        [
-          ("required", InstanceField.Method required);
-          ("provided", InstanceField.Method provided)
+        [ ("required", InstanceField.Method required); ("provided", InstanceField.Method provided)
         ].
 End Impl_provided_method_ProvidedAndRequired_for_u32.
 

CoqOfRust/examples/axiomatized/examples/ink_contracts/basic_contract_caller.v

@@ -38,16 +38,11 @@ Module Impl_core_marker_Copy_for_basic_contract_caller_AccountId.
   Definition Self : Ty.t := Ty.path "basic_contract_caller::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_basic_contract_caller_AccountId.
 
 Axiom Hash :
-  (Ty.path "basic_contract_caller::Hash") =
-    (Ty.apply (Ty.path "array") [ Ty.path "u8" ]).
+  (Ty.path "basic_contract_caller::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8" ]).
 
 (* Enum Error *)
 (* {
@@ -82,20 +77,17 @@ End Impl_basic_contract_caller_OtherContract.
   {
     name := "BasicContractCaller";
     ty_params := [];
-    fields :=
-      [ ("other_contract", Ty.path "basic_contract_caller::OtherContract") ];
+    fields := [ ("other_contract", Ty.path "basic_contract_caller::OtherContract") ];
   } *)
 
 Module Impl_basic_contract_caller_BasicContractCaller.
-  Definition Self : Ty.t :=
-    Ty.path "basic_contract_caller::BasicContractCaller".
+  Definition Self : Ty.t := Ty.path "basic_contract_caller::BasicContractCaller".
 
   Parameter new : (list Ty.t) -> (list Value.t) -> M.
 
   Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
 
   Parameter flip_and_get : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_flip_and_get :
-    M.IsAssociatedFunction Self "flip_and_get" flip_and_get.
+  Axiom AssociatedFunction_flip_and_get : M.IsAssociatedFunction Self "flip_and_get" flip_and_get.
 End Impl_basic_contract_caller_BasicContractCaller.

CoqOfRust/examples/axiomatized/examples/ink_contracts/call_runtime.v

@@ -38,11 +38,7 @@ Module Impl_core_marker_Copy_for_call_runtime_AccountId.
   Definition Self : Ty.t := Ty.path "call_runtime::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_call_runtime_AccountId.
 
 Axiom Balance : (Ty.path "call_runtime::Balance") = (Ty.path "u128").
@@ -72,8 +68,7 @@ Module Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddre
     M.IsTraitInstance
       "core::convert::From"
       Self
-      (* Trait polymorphic types *)
-        [ (* T *) Ty.path "call_runtime::AccountId" ]
+      (* Trait polymorphic types *) [ (* T *) Ty.path "call_runtime::AccountId" ]
       (* Instance *) [ ("from", InstanceField.Method from) ].
 End Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddress_call_runtime_AccountId_Tuple_.
 
@@ -202,10 +197,7 @@ Module Impl_core_cmp_Eq_for_call_runtime_RuntimeError.
       Self
       (* Trait polymorphic types *) []
       (* Instance *)
-        [
-          ("assert_receiver_is_total_eq",
-            InstanceField.Method assert_receiver_is_total_eq)
-        ].
+        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
 End Impl_core_cmp_Eq_for_call_runtime_RuntimeError.
 
 (* Enum EnvError *)
@@ -244,17 +236,15 @@ Module Impl_call_runtime_Env.
 
   Parameter call_runtime : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_call_runtime :
-    M.IsAssociatedFunction Self "call_runtime" call_runtime.
+  Axiom AssociatedFunction_call_runtime : M.IsAssociatedFunction Self "call_runtime" call_runtime.
 End Impl_call_runtime_Env.
 
 Module Impl_call_runtime_RuntimeCaller.
   Definition Self : Ty.t := Ty.path "call_runtime::RuntimeCaller".
 
   Parameter init_env : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_init_env :
-    M.IsAssociatedFunction Self "init_env" init_env.
+  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
 
   Parameter env : (list Ty.t) -> (list Value.t) -> M.
 
@@ -267,16 +257,10 @@ Module Impl_call_runtime_RuntimeCaller.
   Parameter transfer_through_runtime : (list Ty.t) -> (list Value.t) -> M.
 
   Axiom AssociatedFunction_transfer_through_runtime :
-    M.IsAssociatedFunction
-      Self
-      "transfer_through_runtime"
-      transfer_through_runtime.
+    M.IsAssociatedFunction Self "transfer_through_runtime" transfer_through_runtime.
 
   Parameter call_nonexistent_extrinsic : (list Ty.t) -> (list Value.t) -> M.
 
   Axiom AssociatedFunction_call_nonexistent_extrinsic :
-    M.IsAssociatedFunction
-      Self
-      "call_nonexistent_extrinsic"
-      call_nonexistent_extrinsic.
+    M.IsAssociatedFunction Self "call_nonexistent_extrinsic" call_nonexistent_extrinsic.
 End Impl_call_runtime_RuntimeCaller.

CoqOfRust/examples/axiomatized/examples/ink_contracts/conditional_compilation.v

@@ -38,17 +38,12 @@ Module Impl_core_marker_Copy_for_conditional_compilation_AccountId.
   Definition Self : Ty.t := Ty.path "conditional_compilation::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_conditional_compilation_AccountId.
 
 Axiom Balance : (Ty.path "conditional_compilation::Balance") = (Ty.path "u128").
 
-Axiom BlockNumber :
-  (Ty.path "conditional_compilation::BlockNumber") = (Ty.path "u32").
+Axiom BlockNumber : (Ty.path "conditional_compilation::BlockNumber") = (Ty.path "u32").
 
 (* StructRecord
   {
@@ -65,10 +60,7 @@ Axiom BlockNumber :
     name := "Changes";
     ty_params := [];
     fields :=
-      [
-        ("new_value", Ty.path "bool");
-        ("by_", Ty.path "conditional_compilation::AccountId")
-      ];
+      [ ("new_value", Ty.path "bool"); ("by_", Ty.path "conditional_compilation::AccountId") ];
   } *)
 
 (* StructRecord
@@ -110,13 +102,11 @@ Module Impl_conditional_compilation_Env.
 
   Parameter emit_event : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_emit_event :
-    M.IsAssociatedFunction Self "emit_event" emit_event.
+  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
 
   Parameter block_number : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_block_number :
-    M.IsAssociatedFunction Self "block_number" block_number.
+  Axiom AssociatedFunction_block_number : M.IsAssociatedFunction Self "block_number" block_number.
 End Impl_conditional_compilation_Env.
 
 (* StructRecord
@@ -127,13 +117,11 @@ End Impl_conditional_compilation_Env.
   } *)
 
 Module Impl_conditional_compilation_ConditionalCompilation.
-  Definition Self : Ty.t :=
-    Ty.path "conditional_compilation::ConditionalCompilation".
+  Definition Self : Ty.t := Ty.path "conditional_compilation::ConditionalCompilation".
 
   Parameter init_env : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_init_env :
-    M.IsAssociatedFunction Self "init_env" init_env.
+  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
 
   Parameter env : (list Ty.t) -> (list Value.t) -> M.
 
@@ -145,18 +133,15 @@ Module Impl_conditional_compilation_ConditionalCompilation.
 
   Parameter new_foo : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_new_foo :
-    M.IsAssociatedFunction Self "new_foo" new_foo.
+  Axiom AssociatedFunction_new_foo : M.IsAssociatedFunction Self "new_foo" new_foo.
 
   Parameter new_bar : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_new_bar :
-    M.IsAssociatedFunction Self "new_bar" new_bar.
+  Axiom AssociatedFunction_new_bar : M.IsAssociatedFunction Self "new_bar" new_bar.
 
   Parameter new_foo_bar : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_new_foo_bar :
-    M.IsAssociatedFunction Self "new_foo_bar" new_foo_bar.
+  Axiom AssociatedFunction_new_foo_bar : M.IsAssociatedFunction Self "new_foo_bar" new_foo_bar.
 
   Parameter inherent_flip_foo : (list Ty.t) -> (list Value.t) -> M.
 
@@ -170,8 +155,7 @@ Module Impl_conditional_compilation_ConditionalCompilation.
 End Impl_conditional_compilation_ConditionalCompilation.
 
 Module Impl_conditional_compilation_Flip_for_conditional_compilation_ConditionalCompilation.
-  Definition Self : Ty.t :=
-    Ty.path "conditional_compilation::ConditionalCompilation".
+  Definition Self : Ty.t := Ty.path "conditional_compilation::ConditionalCompilation".
 
   Parameter flip : (list Ty.t) -> (list Value.t) -> M.
 

CoqOfRust/examples/axiomatized/examples/ink_contracts/contract_terminate.v

@@ -38,11 +38,7 @@ Module Impl_core_marker_Copy_for_contract_terminate_AccountId.
   Definition Self : Ty.t := Ty.path "contract_terminate::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_contract_terminate_AccountId.
 
 (* StructRecord
@@ -76,8 +72,7 @@ Module Impl_contract_terminate_JustTerminate.
 
   Parameter init_env : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_init_env :
-    M.IsAssociatedFunction Self "init_env" init_env.
+  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
 
   Parameter env : (list Ty.t) -> (list Value.t) -> M.
 
@@ -89,6 +84,5 @@ Module Impl_contract_terminate_JustTerminate.
 
   Parameter terminate_me : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_terminate_me :
-    M.IsAssociatedFunction Self "terminate_me" terminate_me.
+  Axiom AssociatedFunction_terminate_me : M.IsAssociatedFunction Self "terminate_me" terminate_me.
 End Impl_contract_terminate_JustTerminate.

CoqOfRust/examples/axiomatized/examples/ink_contracts/contract_transfer.v

@@ -38,11 +38,7 @@ Module Impl_core_marker_Copy_for_contract_transfer_AccountId.
   Definition Self : Ty.t := Ty.path "contract_transfer::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_contract_transfer_AccountId.
 
 Axiom Balance : (Ty.path "contract_transfer::Balance") = (Ty.path "u128").
@@ -63,13 +59,11 @@ Module Impl_contract_transfer_Env.
 
   Parameter balance : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_balance :
-    M.IsAssociatedFunction Self "balance" balance.
+  Axiom AssociatedFunction_balance : M.IsAssociatedFunction Self "balance" balance.
 
   Parameter transfer : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_transfer :
-    M.IsAssociatedFunction Self "transfer" transfer.
+  Axiom AssociatedFunction_transfer : M.IsAssociatedFunction Self "transfer" transfer.
 
   Parameter transferred_value : (list Ty.t) -> (list Value.t) -> M.
 
@@ -88,8 +82,7 @@ Module Impl_contract_transfer_GiveMe.
 
   Parameter init_env : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_init_env :
-    M.IsAssociatedFunction Self "init_env" init_env.
+  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
 
   Parameter env : (list Ty.t) -> (list Value.t) -> M.
 
@@ -101,11 +94,9 @@ Module Impl_contract_transfer_GiveMe.
 
   Parameter give_me : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_give_me :
-    M.IsAssociatedFunction Self "give_me" give_me.
+  Axiom AssociatedFunction_give_me : M.IsAssociatedFunction Self "give_me" give_me.
 
   Parameter was_it_ten : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_was_it_ten :
-    M.IsAssociatedFunction Self "was_it_ten" was_it_ten.
+  Axiom AssociatedFunction_was_it_ten : M.IsAssociatedFunction Self "was_it_ten" was_it_ten.
 End Impl_contract_transfer_GiveMe.

CoqOfRust/examples/axiomatized/examples/ink_contracts/custom_allocator.v

@@ -8,9 +8,7 @@ Require Import CoqOfRust.CoqOfRust.
     fields :=
       [
         ("value",
-          Ty.apply
-            (Ty.path "alloc::vec::Vec")
-            [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ])
+          Ty.apply (Ty.path "alloc::vec::Vec") [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ])
       ];
   } *)
 
@@ -23,8 +21,7 @@ Module Impl_custom_allocator_CustomAllocator.
 
   Parameter default : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_default :
-    M.IsAssociatedFunction Self "default" default.
+  Axiom AssociatedFunction_default : M.IsAssociatedFunction Self "default" default.
 
   Parameter flip : (list Ty.t) -> (list Value.t) -> M.
 

CoqOfRust/examples/axiomatized/examples/ink_contracts/custom_environment.v

@@ -38,11 +38,7 @@ Module Impl_core_marker_Copy_for_custom_environment_AccountId.
   Definition Self : Ty.t := Ty.path "custom_environment::AccountId".
 
   Axiom Implements :
-    M.IsTraitInstance
-      "core::marker::Copy"
-      Self
-      (* Trait polymorphic types *) []
-      (* Instance *) [].
+    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
 End Impl_core_marker_Copy_for_custom_environment_AccountId.
 
 Axiom Balance : (Ty.path "custom_environment::Balance") = (Ty.path "u128").
@@ -122,17 +118,15 @@ Module Impl_custom_environment_Env.
 
   Parameter emit_event : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_emit_event :
-    M.IsAssociatedFunction Self "emit_event" emit_event.
+  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
 End Impl_custom_environment_Env.
 
 Module Impl_custom_environment_Topics.
   Definition Self : Ty.t := Ty.path "custom_environment::Topics".
 
   Parameter init_env : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_init_env :
-    M.IsAssociatedFunction Self "init_env" init_env.
+  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
 
   Parameter env : (list Ty.t) -> (list Value.t) -> M.
 
@@ -144,6 +138,5 @@ Module Impl_custom_environment_Topics.
 
   Parameter trigger : (list Ty.t) -> (list Value.t) -> M.
 
-  Axiom AssociatedFunction_trigger :
-    M.IsAssociatedFunction Self "trigger" trigger.
+  Axiom AssociatedFunction_trigger : M.IsAssociatedFunction Self "trigger" trigger.
 End Impl_custom_environment_Topics.