Skip to content

Commit dcf7350

Browse files
clarusclarus
committed
feat: add polymorphic const parameters except in top_level
1 parent ec3e8cd commit dcf7350

File tree

295 files changed

+10810
-4669
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

295 files changed

+10810
-4669
lines changed

‎CoqOfRust/examples/axiomatized/examples/custom/polymorphic_associated_function.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Require Import CoqOfRust.CoqOfRust.
1010

1111
Module Impl_polymorphic_associated_function_Foo_A.
1212
Definition Self (A : Ty.t) : Ty.t :=
13-
Ty.apply (Ty.path "polymorphic_associated_function::Foo") [ A ].
13+
Ty.apply (Ty.path "polymorphic_associated_function::Foo") [ A ] [].
1414

1515
Parameter convert : forall (A : Ty.t), (list Ty.t) -> (list Value.t) -> M.
1616

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,8 @@ Module Impl_core_marker_Copy_for_basic_contract_caller_AccountId.
4242
End Impl_core_marker_Copy_for_basic_contract_caller_AccountId.
4343

4444
Axiom Hash :
45-
(Ty.path "basic_contract_caller::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8" ]).
45+
(Ty.path "basic_contract_caller::Hash") =
46+
(Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]).
4647

4748
(* Enum Error *)
4849
(* {

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,8 @@ Module Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddre
6060
Definition Self : Ty.t :=
6161
Ty.apply
6262
(Ty.path "call_runtime::MultiAddress")
63-
[ Ty.path "call_runtime::AccountId"; Ty.tuple [] ].
63+
[ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]
64+
[].
6465

6566
Parameter from : (list Ty.t) -> (list Value.t) -> M.
6667

@@ -85,7 +86,8 @@ End Impl_core_convert_From_call_runtime_AccountId_for_call_runtime_MultiAddress_
8586
("dest",
8687
Ty.apply
8788
(Ty.path "call_runtime::MultiAddress")
88-
[ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]);
89+
[ Ty.path "call_runtime::AccountId"; Ty.tuple [] ]
90+
[]);
8991
("value", Ty.path "u128")
9092
];
9193
discriminant := None;

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,10 @@ Require Import CoqOfRust.CoqOfRust.
88
fields :=
99
[
1010
("value",
11-
Ty.apply (Ty.path "alloc::vec::Vec") [ Ty.path "bool"; Ty.path "alloc::alloc::Global" ])
11+
Ty.apply
12+
(Ty.path "alloc::vec::Vec")
13+
[ Ty.path "bool"; Ty.path "alloc::alloc::Global" ]
14+
[])
1215
];
1316
} *)
1417

‎CoqOfRust/examples/axiomatized/examples/ink_contracts/dns.v‎

Lines changed: 31 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@ Require Import CoqOfRust.CoqOfRust.
77
ty_params := [ "K"; "V" ];
88
fields :=
99
[
10-
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
11-
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
10+
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
11+
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
1212
];
1313
} *)
1414

1515
Module Impl_core_default_Default_for_dns_Mapping_K_V.
16-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ].
16+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].
1717

1818
Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
1919

@@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_dns_Mapping_K_V.
2727
End Impl_core_default_Default_for_dns_Mapping_K_V.
2828

2929
Module Impl_dns_Mapping_K_V.
30-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ].
30+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].
3131

3232
Parameter contains : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
3333

@@ -136,7 +136,7 @@ Module Impl_core_cmp_PartialEq_for_dns_AccountId.
136136
(* Instance *) [ ("eq", InstanceField.Method eq) ].
137137
End Impl_core_cmp_PartialEq_for_dns_AccountId.
138138

139-
Module Impl_core_convert_From_array_u8_for_dns_AccountId.
139+
Module Impl_core_convert_From_array_u8_32_for_dns_AccountId.
140140
Definition Self : Ty.t := Ty.path "dns::AccountId".
141141

142142
Parameter from : (list Ty.t) -> (list Value.t) -> M.
@@ -145,13 +145,16 @@ Module Impl_core_convert_From_array_u8_for_dns_AccountId.
145145
M.IsTraitInstance
146146
"core::convert::From"
147147
Self
148-
(* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
148+
(* Trait polymorphic types *)
149+
[ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ] ]
149150
(* Instance *) [ ("from", InstanceField.Method from) ].
150-
End Impl_core_convert_From_array_u8_for_dns_AccountId.
151+
End Impl_core_convert_From_array_u8_32_for_dns_AccountId.
151152

152153
Axiom Balance : (Ty.path "dns::Balance") = (Ty.path "u128").
153154

154-
Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8" ]).
155+
Axiom Hash :
156+
(Ty.path "dns::Hash") =
157+
(Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]).
155158

156159
(* StructRecord
157160
{
@@ -165,7 +168,10 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
165168
name := "Register";
166169
ty_params := [];
167170
fields :=
168-
[ ("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]); ("from", Ty.path "dns::AccountId") ];
171+
[
172+
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]);
173+
("from", Ty.path "dns::AccountId")
174+
];
169175
} *)
170176

171177
(* StructRecord
@@ -174,9 +180,9 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
174180
ty_params := [];
175181
fields :=
176182
[
177-
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]);
183+
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]);
178184
("from", Ty.path "dns::AccountId");
179-
("old_address", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ]);
185+
("old_address", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ] []);
180186
("new_address", Ty.path "dns::AccountId")
181187
];
182188
} *)
@@ -187,9 +193,9 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
187193
ty_params := [];
188194
fields :=
189195
[
190-
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]);
196+
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]);
191197
("from", Ty.path "dns::AccountId");
192-
("old_owner", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ]);
198+
("old_owner", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ] []);
193199
("new_owner", Ty.path "dns::AccountId")
194200
];
195201
} *)
@@ -238,11 +244,19 @@ End Impl_dns_Env.
238244
("name_to_address",
239245
Ty.apply
240246
(Ty.path "dns::Mapping")
241-
[ Ty.apply (Ty.path "array") [ Ty.path "u8" ]; Ty.path "dns::AccountId" ]);
247+
[
248+
Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ];
249+
Ty.path "dns::AccountId"
250+
]
251+
[]);
242252
("name_to_owner",
243253
Ty.apply
244254
(Ty.path "dns::Mapping")
245-
[ Ty.apply (Ty.path "array") [ Ty.path "u8" ]; Ty.path "dns::AccountId" ]);
255+
[
256+
Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ];
257+
Ty.path "dns::AccountId"
258+
]
259+
[]);
246260
("default_address", Ty.path "dns::AccountId")
247261
];
248262
} *)
@@ -331,8 +345,8 @@ End Impl_core_cmp_Eq_for_dns_Error.
331345

332346
Axiom Result :
333347
forall (T : Ty.t),
334-
(Ty.apply (Ty.path "dns::Result") [ T ]) =
335-
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "dns::Error" ]).
348+
(Ty.apply (Ty.path "dns::Result") [ T ] []) =
349+
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "dns::Error" ] []).
336350

337351
Module Impl_dns_DomainNameService.
338352
Definition Self : Ty.t := Ty.path "dns::DomainNameService".

‎CoqOfRust/examples/axiomatized/examples/ink_contracts/erc1155.v‎

Lines changed: 17 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@ Require Import CoqOfRust.CoqOfRust.
77
ty_params := [ "K"; "V" ];
88
fields :=
99
[
10-
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
11-
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
10+
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
11+
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
1212
];
1313
} *)
1414

1515
Module Impl_core_default_Default_for_erc1155_Mapping_K_V.
16-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ].
16+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].
1717

1818
Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
1919

@@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_erc1155_Mapping_K_V.
2727
End Impl_core_default_Default_for_erc1155_Mapping_K_V.
2828

2929
Module Impl_erc1155_Mapping_K_V.
30-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ].
30+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].
3131

3232
Parameter contains : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
3333

@@ -130,7 +130,7 @@ Module Impl_core_cmp_PartialEq_for_erc1155_AccountId.
130130
(* Instance *) [ ("eq", InstanceField.Method eq) ].
131131
End Impl_core_cmp_PartialEq_for_erc1155_AccountId.
132132

133-
Module Impl_core_convert_From_array_u8_for_erc1155_AccountId.
133+
Module Impl_core_convert_From_array_u8_32_for_erc1155_AccountId.
134134
Definition Self : Ty.t := Ty.path "erc1155::AccountId".
135135

136136
Parameter from : (list Ty.t) -> (list Value.t) -> M.
@@ -139,9 +139,10 @@ Module Impl_core_convert_From_array_u8_for_erc1155_AccountId.
139139
M.IsTraitInstance
140140
"core::convert::From"
141141
Self
142-
(* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
142+
(* Trait polymorphic types *)
143+
[ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ] ]
143144
(* Instance *) [ ("from", InstanceField.Method from) ].
144-
End Impl_core_convert_From_array_u8_for_erc1155_AccountId.
145+
End Impl_core_convert_From_array_u8_32_for_erc1155_AccountId.
145146

146147
Axiom Balance : (Ty.path "erc1155::Balance") = (Ty.path "u128").
147148

@@ -249,8 +250,8 @@ End Impl_core_cmp_Eq_for_erc1155_Error.
249250

250251
Axiom Result :
251252
forall (T : Ty.t),
252-
(Ty.apply (Ty.path "erc1155::Result") [ T ]) =
253-
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc1155::Error" ]).
253+
(Ty.apply (Ty.path "erc1155::Result") [ T ] []) =
254+
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc1155::Error" ] []).
254255

255256
(* Trait *)
256257
(* Empty module 'Erc1155' *)
@@ -268,9 +269,9 @@ Axiom Operator : (Ty.path "erc1155::Operator") = (Ty.path "erc1155::AccountId").
268269
ty_params := [];
269270
fields :=
270271
[
271-
("operator", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
272-
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
273-
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
272+
("operator", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
273+
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
274+
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
274275
("token_id", Ty.path "u128");
275276
("value", Ty.path "u128")
276277
];
@@ -339,12 +340,13 @@ End Impl_erc1155_Env.
339340
("balances",
340341
Ty.apply
341342
(Ty.path "erc1155::Mapping")
342-
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ]);
343+
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ]
344+
[]);
343345
("approvals",
344346
Ty.apply
345347
(Ty.path "erc1155::Mapping")
346-
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ]; Ty.tuple []
347-
]);
348+
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ]; Ty.tuple [] ]
349+
[]);
348350
("token_id_nonce", Ty.path "u128")
349351
];
350352
} *)

‎CoqOfRust/examples/axiomatized/examples/ink_contracts/erc20.v‎

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@ Require Import CoqOfRust.CoqOfRust.
77
ty_params := [ "K"; "V" ];
88
fields :=
99
[
10-
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ]);
11-
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ])
10+
("_key", Ty.apply (Ty.path "core::marker::PhantomData") [ K ] []);
11+
("_value", Ty.apply (Ty.path "core::marker::PhantomData") [ V ] [])
1212
];
1313
} *)
1414

1515
Module Impl_core_default_Default_for_erc20_Mapping_K_V.
16-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ].
16+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].
1717

1818
Parameter default : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
1919

@@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_erc20_Mapping_K_V.
2727
End Impl_core_default_Default_for_erc20_Mapping_K_V.
2828

2929
Module Impl_erc20_Mapping_K_V.
30-
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ].
30+
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].
3131

3232
Parameter get : forall (K V : Ty.t), (list Ty.t) -> (list Value.t) -> M.
3333

@@ -99,11 +99,12 @@ Axiom Balance : (Ty.path "erc20::Balance") = (Ty.path "u128").
9999
[
100100
("total_supply", Ty.path "u128");
101101
("balances",
102-
Ty.apply (Ty.path "erc20::Mapping") [ Ty.path "erc20::AccountId"; Ty.path "u128" ]);
102+
Ty.apply (Ty.path "erc20::Mapping") [ Ty.path "erc20::AccountId"; Ty.path "u128" ] []);
103103
("allowances",
104104
Ty.apply
105105
(Ty.path "erc20::Mapping")
106-
[ Ty.tuple [ Ty.path "erc20::AccountId"; Ty.path "erc20::AccountId" ]; Ty.path "u128" ])
106+
[ Ty.tuple [ Ty.path "erc20::AccountId"; Ty.path "erc20::AccountId" ]; Ty.path "u128" ]
107+
[])
107108
];
108109
} *)
109110

@@ -126,8 +127,8 @@ End Impl_core_default_Default_for_erc20_Erc20.
126127
ty_params := [];
127128
fields :=
128129
[
129-
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ]);
130-
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ]);
130+
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ] []);
131+
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ] []);
131132
("value", Ty.path "u128")
132133
];
133134
} *)
@@ -182,8 +183,8 @@ End Impl_core_default_Default_for_erc20_Erc20.
182183

183184
Axiom Result :
184185
forall (T : Ty.t),
185-
(Ty.apply (Ty.path "erc20::Result") [ T ]) =
186-
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc20::Error" ]).
186+
(Ty.apply (Ty.path "erc20::Result") [ T ] []) =
187+
(Ty.apply (Ty.path "core::result::Result") [ T; Ty.path "erc20::Error" ] []).
187188

188189
Module Impl_erc20_Env.
189190
Definition Self : Ty.t := Ty.path "erc20::Env".

0 commit comments

Comments
 (0)