feat: add polymorphic const parameters except in top_level

formal-land · Apr 1, 2024 · e476d93 · e476d93
1 parent 88290f5
commit e476d93
Show file tree

Hide file tree

Showing 295 changed files with 11,041 additions and 3,878 deletions.
diff --git a/CoqOfRust/examples/axiomatized/examples/custom/polymorphic_associated_function.v b/CoqOfRust/examples/axiomatized/examples/custom/polymorphic_associated_function.v
@@ -10,7 +10,7 @@ Require Import CoqOfRust.CoqOfRust.
 
 Module Impl_polymorphic_associated_function_Foo_A.
   Definition Self (A : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "polymorphic_associated_function::Foo") [ A ].
+    Ty.apply (Ty.path "polymorphic_associated_function::Foo") [ A ] [].
 
   Parameter convert : forall (A : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/basic_contract_caller.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/basic_contract_caller.v
@@ -47,7 +47,10 @@ 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.apply
+      (Ty.path "array")
+      [ Ty.path "u8" ]
+      [ Value.Integer Integer.Usize 32 ]).
 
 (* Enum Error *)
 (* {

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/call_runtime.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/call_runtime.v
@@ -64,7 +64,8 @@ Module Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddre
   Definition Self : Ty.t :=
     Ty.apply
       (Ty.path "call_runtime::MultiAddress")
-      [ Ty.path "call_runtime::AccountId"; Ty.tuple [] ].
+      [ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]
+      [].
 
   Parameter from : (list Ty.t) -> (list Value.t) -> M.
 
@@ -90,7 +91,8 @@ End Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddress_
               ("dest",
                 Ty.apply
                   (Ty.path "call_runtime::MultiAddress")
-                  [ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]);
+                  [ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]
+                  []);
               ("value", Ty.path "u128")
             ];
         discriminant := None;

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/custom_allocator.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/custom_allocator.v
@@ -10,7 +10,8 @@ Require Import CoqOfRust.CoqOfRust.
         ("value",
           Ty.apply
             (Ty.path "alloc::vec::Vec")
-            [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ])
+            [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ]
+            [])
       ];
   } *)
 

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/dns.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/dns.v
@@ -7,14 +7,14 @@ Require Import CoqOfRust.CoqOfRust.
     ty_params := [ "K"; "V" ];
     fields :=
       [
-        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
-        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
+        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
+        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
       ];
   } *)
 
 Module Impl_core_default_Default_for_dns_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "dns::Mapping") [ K; V ].
+    Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].
 
   Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -29,7 +29,7 @@ End Impl_core_default_Default_for_dns_Mapping_K_V.
 
 Module Impl_dns_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "dns::Mapping") [ K; V ].
+    Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].
 
   Parameter contains : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -142,7 +142,7 @@ Module Impl_core_cmp_PartialEq_for_dns_AccountId.
       (* Instance *) [ ("eq", InstanceField.Method eq) ].
 End Impl_core_cmp_PartialEq_for_dns_AccountId.
 
-Module Impl_core_convert_From_array_u8_for_dns_AccountId.
+Module Impl_core_convert_From_array_u8_32_for_dns_AccountId.
   Definition Self : Ty.t := Ty.path "dns::AccountId".
 
   Parameter from : (list Ty.t) -> (list Value.t) -> M.
@@ -152,14 +152,24 @@ Module Impl_core_convert_From_array_u8_for_dns_AccountId.
       "core::convert::From"
       Self
       (* Trait polymorphic types *)
-        [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
+        [
+          (* T *)
+            Ty.apply
+              (Ty.path "array")
+              [ Ty.path "u8" ]
+              [ Value.Integer Integer.Usize 32 ]
+        ]
       (* Instance *) [ ("from", InstanceField.Method from) ].
-End Impl_core_convert_From_array_u8_for_dns_AccountId.
+End Impl_core_convert_From_array_u8_32_for_dns_AccountId.
 
 Axiom Balance : (Ty.path "dns::Balance") = (Ty.path "u128").
 
 Axiom Hash :
-  (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8" ]).
+  (Ty.path "dns::Hash") =
+    (Ty.apply
+      (Ty.path "array")
+      [ Ty.path "u8" ]
+      [ Value.Integer Integer.Usize 32 ]).
 
 (* StructRecord
   {
@@ -174,7 +184,11 @@ Axiom Hash :
     ty_params := [];
     fields :=
       [
-        ("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]);
+        ("name",
+          Ty.apply
+            (Ty.path "array")
+            [ Ty.path "u8" ]
+            [ Value.Integer Integer.Usize 32 ]);
         ("from", Ty.path "dns::AccountId")
       ];
   } *)
@@ -185,12 +199,17 @@ Axiom Hash :
     ty_params := [];
     fields :=
       [
-        ("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]);
+        ("name",
+          Ty.apply
+            (Ty.path "array")
+            [ Ty.path "u8" ]
+            [ Value.Integer Integer.Usize 32 ]);
         ("from", Ty.path "dns::AccountId");
         ("old_address",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "dns::AccountId" ]);
+            [ Ty.path "dns::AccountId" ]
+            []);
         ("new_address", Ty.path "dns::AccountId")
       ];
   } *)
@@ -201,12 +220,17 @@ Axiom Hash :
     ty_params := [];
     fields :=
       [
-        ("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]);
+        ("name",
+          Ty.apply
+            (Ty.path "array")
+            [ Ty.path "u8" ]
+            [ Value.Integer Integer.Usize 32 ]);
         ("from", Ty.path "dns::AccountId");
         ("old_owner",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "dns::AccountId" ]);
+            [ Ty.path "dns::AccountId" ]
+            []);
         ("new_owner", Ty.path "dns::AccountId")
       ];
   } *)
@@ -257,16 +281,24 @@ End Impl_dns_Env.
           Ty.apply
             (Ty.path "dns::Mapping")
             [
-              Ty.apply (Ty.path "array") [ Ty.path "u8" ];
+              Ty.apply
+                (Ty.path "array")
+                [ Ty.path "u8" ]
+                [ Value.Integer Integer.Usize 32 ];
               Ty.path "dns::AccountId"
-            ]);
+            ]
+            []);
         ("name_to_owner",
           Ty.apply
             (Ty.path "dns::Mapping")
             [
-              Ty.apply (Ty.path "array") [ Ty.path "u8" ];
+              Ty.apply
+                (Ty.path "array")
+                [ Ty.path "u8" ]
+                [ Value.Integer Integer.Usize 32 ];
               Ty.path "dns::AccountId"
-            ]);
+            ]
+            []);
         ("default_address", Ty.path "dns::AccountId")
       ];
   } *)
@@ -358,8 +390,8 @@ End Impl_core_cmp_Eq_for_dns_Error.
 
 Axiom Result :
   forall (T : Ty.t),
-  (Ty.apply (Ty.path "dns::Result") [ T ]) =
-    (Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "dns::Error" ]).
+  (Ty.apply (Ty.path "dns::Result") [ T ] []) =
+    (Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "dns::Error" ] []).
 
 Module Impl_dns_DomainNameService.
   Definition Self : Ty.t := Ty.path "dns::DomainNameService".

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/erc1155.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/erc1155.v
@@ -7,14 +7,14 @@ Require Import CoqOfRust.CoqOfRust.
     ty_params := [ "K"; "V" ];
     fields :=
       [
-        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
-        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
+        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
+        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
       ];
   } *)
 
 Module Impl_core_default_Default_for_erc1155_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "erc1155::Mapping") [ K; V ].
+    Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].
 
   Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -29,7 +29,7 @@ End Impl_core_default_Default_for_erc1155_Mapping_K_V.
 
 Module Impl_erc1155_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "erc1155::Mapping") [ K; V ].
+    Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].
 
   Parameter contains : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -136,7 +136,7 @@ Module Impl_core_cmp_PartialEq_for_erc1155_AccountId.
       (* Instance *) [ ("eq", InstanceField.Method eq) ].
 End Impl_core_cmp_PartialEq_for_erc1155_AccountId.
 
-Module Impl_core_convert_From_array_u8_for_erc1155_AccountId.
+Module Impl_core_convert_From_array_u8_32_for_erc1155_AccountId.
   Definition Self : Ty.t := Ty.path "erc1155::AccountId".
 
   Parameter from : (list Ty.t) -> (list Value.t) -> M.
@@ -146,9 +146,15 @@ Module Impl_core_convert_From_array_u8_for_erc1155_AccountId.
       "core::convert::From"
       Self
       (* Trait polymorphic types *)
-        [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
+        [
+          (* T *)
+            Ty.apply
+              (Ty.path "array")
+              [ Ty.path "u8" ]
+              [ Value.Integer Integer.Usize 32 ]
+        ]
       (* Instance *) [ ("from", InstanceField.Method from) ].
-End Impl_core_convert_From_array_u8_for_erc1155_AccountId.
+End Impl_core_convert_From_array_u8_32_for_erc1155_AccountId.
 
 Axiom Balance : (Ty.path "erc1155::Balance") = (Ty.path "u128").
 
@@ -259,8 +265,11 @@ End Impl_core_cmp_Eq_for_erc1155_Error.
 
 Axiom Result :
   forall (T : Ty.t),
-  (Ty.apply (Ty.path "erc1155::Result") [ T ]) =
-    (Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc1155::Error" ]).
+  (Ty.apply (Ty.path "erc1155::Result") [ T ] []) =
+    (Ty.apply
+      (Ty.path "core::result::Result")
+      [ T; Ty.path "erc1155::Error" ]
+      []).
 
 (* Trait *)
 (* Empty module 'Erc1155' *)
@@ -281,15 +290,18 @@ Axiom Operator : (Ty.path "erc1155::Operator") = (Ty.path "erc1155::AccountId").
         ("operator",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "erc1155::AccountId" ]);
+            [ Ty.path "erc1155::AccountId" ]
+            []);
         ("from",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "erc1155::AccountId" ]);
+            [ Ty.path "erc1155::AccountId" ]
+            []);
         ("to",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "erc1155::AccountId" ]);
+            [ Ty.path "erc1155::AccountId" ]
+            []);
         ("token_id", Ty.path "u128");
         ("value", Ty.path "u128")
       ];
@@ -364,15 +376,17 @@ End Impl_erc1155_Env.
             [
               Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ];
               Ty.path "u128"
-            ]);
+            ]
+            []);
         ("approvals",
           Ty.apply
             (Ty.path "erc1155::Mapping")
             [
               Ty.tuple
                 [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ];
               Ty.tuple []
-            ]);
+            ]
+            []);
         ("token_id_nonce", Ty.path "u128")
       ];
   } *)

diff --git a/CoqOfRust/examples/axiomatized/examples/ink_contracts/erc20.v b/CoqOfRust/examples/axiomatized/examples/ink_contracts/erc20.v
@@ -7,14 +7,14 @@ Require Import CoqOfRust.CoqOfRust.
     ty_params := [ "K"; "V" ];
     fields :=
       [
-        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
-        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
+        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
+        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
       ];
   } *)
 
 Module Impl_core_default_Default_for_erc20_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "erc20::Mapping") [ K; V ].
+    Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].
 
   Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -29,7 +29,7 @@ End Impl_core_default_Default_for_erc20_Mapping_K_V.
 
 Module Impl_erc20_Mapping_K_V.
   Definition Self (K V : Ty.t) : Ty.t :=
-    Ty.apply (Ty.path "erc20::Mapping") [ K; V ].
+    Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].
 
   Parameter get : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
 
@@ -107,15 +107,17 @@ Axiom Balance : (Ty.path "erc20::Balance") = (Ty.path "u128").
         ("balances",
           Ty.apply
             (Ty.path "erc20::Mapping")
-            [ Ty.path "erc20::AccountId"; Ty.path "u128" ]);
+            [ Ty.path "erc20::AccountId"; Ty.path "u128" ]
+            []);
         ("allowances",
           Ty.apply
             (Ty.path "erc20::Mapping")
             [
               Ty.tuple
                 [ Ty.path "erc20::AccountId"; Ty.path "erc20::AccountId" ];
               Ty.path "u128"
-            ])
+            ]
+            [])
       ];
   } *)
 
@@ -141,11 +143,13 @@ End Impl_core_default_Default_for_erc20_Erc20.
         ("from",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "erc20::AccountId" ]);
+            [ Ty.path "erc20::AccountId" ]
+            []);
         ("to",
           Ty.apply
             (Ty.path "core::option::Option")
-            [ Ty.path "erc20::AccountId" ]);
+            [ Ty.path "erc20::AccountId" ]
+            []);
         ("value", Ty.path "u128")
       ];
   } *)
@@ -200,8 +204,11 @@ End Impl_core_default_Default_for_erc20_Erc20.
 
 Axiom Result :
   forall (T : Ty.t),
-  (Ty.apply (Ty.path "erc20::Result") [ T ]) =
-    (Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc20::Error" ]).
+  (Ty.apply (Ty.path "erc20::Result") [ T ] []) =
+    (Ty.apply
+      (Ty.path "core::result::Result")
+      [ T; Ty.path "erc20::Error" ]
+      []).
 
 Module Impl_erc20_Env.
   Definition Self : Ty.t := Ty.path "erc20::Env".