Skip to content

Draft: add polymorphic const parameters #498

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Draft: add polymorphic const parameters #498

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CoqOfRust/examples/axiomatized/examples/custom/polymorphic_associated_function.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
3 changes: 2 additions & 1 deletion CoqOfRust/examples/axiomatized/examples/ink_contracts/basic_contract_caller.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ Module Impl_core_marker_Copy_for_basic_contract_caller_AccountId.
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" ] [ Value.Integer Integer.Usize 32 ]).

(* Enum Error *)
(* {
Expand Down
6 changes: 4 additions & 2 deletions CoqOfRust/examples/axiomatized/examples/ink_contracts/call_runtime.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,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.

Expand All @@ -85,7 +86,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;
Expand Down
5 changes: 4 additions & 1 deletion CoqOfRust/examples/axiomatized/examples/ink_contracts/custom_allocator.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ 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" ]
[])
];
} *)

Expand Down
48 changes: 31 additions & 17 deletions CoqOfRust/examples/axiomatized/examples/ink_contracts/dns.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ 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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].

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

Expand All @@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_dns_Mapping_K_V.
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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::Mapping") [ K; V ] [].

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

Expand Down Expand Up @@ -136,7 +136,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.
Expand All @@ -145,13 +145,16 @@ Module Impl_core_convert_From_array_u8_for_dns_AccountId.
M.IsTraitInstance
"core::convert::From"
Self
(* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
(* Trait polymorphic types *)
[ (* 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" ]).
Axiom Hash :
(Ty.path "dns::Hash") =
(Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]).

(* StructRecord
{
Expand All @@ -165,7 +168,10 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
name := "Register";
ty_params := [];
fields :=
[ ("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ]); ("from", Ty.path "dns::AccountId") ];
[
("name", Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ]);
("from", Ty.path "dns::AccountId")
];
} *)

(* StructRecord
Expand All @@ -174,9 +180,9 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
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" ]);
("old_address", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ] []);
("new_address", Ty.path "dns::AccountId")
];
} *)
Expand All @@ -187,9 +193,9 @@ Axiom Hash : (Ty.path "dns::Hash") = (Ty.apply (Ty.path "array") [ Ty.path "u8"
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" ]);
("old_owner", Ty.apply (Ty.path "core::option::Option") [ Ty.path "dns::AccountId" ] []);
("new_owner", Ty.path "dns::AccountId")
];
} *)
Expand Down Expand Up @@ -238,11 +244,19 @@ End Impl_dns_Env.
("name_to_address",
Ty.apply
(Ty.path "dns::Mapping")
[ Ty.apply (Ty.path "array") [ Ty.path "u8" ]; Ty.path "dns::AccountId" ]);
[
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.path "dns::AccountId" ]);
[
Ty.apply (Ty.path "array") [ Ty.path "u8" ] [ Value.Integer Integer.Usize 32 ];
Ty.path "dns::AccountId"
]
[]);
("default_address", Ty.path "dns::AccountId")
];
} *)
Expand Down Expand Up @@ -331,8 +345,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".
Expand Down
32 changes: 17 additions & 15 deletions CoqOfRust/examples/axiomatized/examples/ink_contracts/erc1155.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ 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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].

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

Expand All @@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_erc1155_Mapping_K_V.
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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [ K; V ] [].

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

Expand Down Expand Up @@ -130,7 +130,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.
Expand All @@ -139,9 +139,10 @@ Module Impl_core_convert_From_array_u8_for_erc1155_AccountId.
M.IsTraitInstance
"core::convert::From"
Self
(* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "array") [ Ty.path "u8" ] ]
(* Trait polymorphic types *)
[ (* 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").

Expand Down Expand Up @@ -249,8 +250,8 @@ 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' *)
Expand All @@ -268,9 +269,9 @@ Axiom Operator : (Ty.path "erc1155::Operator") = (Ty.path "erc1155::AccountId").
ty_params := [];
fields :=
[
("operator", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ]);
("operator", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc1155::AccountId" ] []);
("token_id", Ty.path "u128");
("value", Ty.path "u128")
];
Expand Down Expand Up @@ -339,12 +340,13 @@ End Impl_erc1155_Env.
("balances",
Ty.apply
(Ty.path "erc1155::Mapping")
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ]);
[ 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 []
]);
[ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ]; Ty.tuple [] ]
[]);
("token_id_nonce", Ty.path "u128")
];
} *)
Expand Down
21 changes: 11 additions & 10 deletions CoqOfRust/examples/axiomatized/examples/ink_contracts/erc20.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ 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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].

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

Expand All @@ -27,7 +27,7 @@ Module Impl_core_default_Default_for_erc20_Mapping_K_V.
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 ].
Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc20::Mapping") [ K; V ] [].

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

Expand Down Expand Up @@ -99,11 +99,12 @@ Axiom Balance : (Ty.path "erc20::Balance") = (Ty.path "u128").
[
("total_supply", Ty.path "u128");
("balances",
Ty.apply (Ty.path "erc20::Mapping") [ Ty.path "erc20::AccountId"; Ty.path "u128" ]);
Ty.apply (Ty.path "erc20::Mapping") [ 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" ])
[ Ty.tuple [ Ty.path "erc20::AccountId"; Ty.path "erc20::AccountId" ]; Ty.path "u128" ]
[])
];
} *)

Expand All @@ -126,8 +127,8 @@ End Impl_core_default_Default_for_erc20_Erc20.
ty_params := [];
fields :=
[
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ]);
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ]);
("from", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ] []);
("to", Ty.apply (Ty.path "core::option::Option") [ Ty.path "erc20::AccountId" ] []);
("value", Ty.path "u128")
];
} *)
Expand Down Expand Up @@ -182,8 +183,8 @@ 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".
Expand Down
Loading