diff --git a/Cargo.lock b/Cargo.lock index ab5db75b6..442da4539 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -128,6 +128,7 @@ dependencies = [ "serde", "serde_json", "toml", + "topological-sort", "walkdir", ] @@ -517,6 +518,12 @@ dependencies = [ "serde", ] +[[package]] +name = "topological-sort" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea68304e134ecd095ac6c3574494fc62b909f416c4fca77e440530221e549d3d" + [[package]] name = "typed-arena" version = "2.0.2" diff --git a/CoqOfRust/core/convert.v b/CoqOfRust/core/convert.v index c66a28d35..8b4a1b39c 100644 --- a/CoqOfRust/core/convert.v +++ b/CoqOfRust/core/convert.v @@ -40,7 +40,7 @@ where } *) Module AsMut. - Class Trait (Self T : Set) : Set := { + Class Trait (Self : Set) {T : Set} : Set := { as_mut : mut_ref Self -> mut_ref T; }. End AsMut. @@ -55,13 +55,13 @@ where } *) Module AsRef. - Class Trait (Self T : Set) : Set := { + Class Trait (Self : Set) {T : Set} : Set := { as_ref : ref Self -> ref T; }. End AsRef. Module Impl_AsRef_for_string. - Global Instance I : convert.AsRef.Trait string string := { + Global Instance I : convert.AsRef.Trait string (T := string) := { as_ref self := self; }. End Impl_AsRef_for_string. diff --git a/CoqOfRust/ink/ink.v b/CoqOfRust/ink/ink.v index 3b7832b12..81b769ca4 100644 --- a/CoqOfRust/ink/ink.v +++ b/CoqOfRust/ink/ink.v @@ -312,7 +312,7 @@ Module reflect. Module ContractMessageDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(parity_scale_codec.codec.Decode.Trait Type_) @@ -324,6 +324,45 @@ Module reflect. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractMessageDecoder. Module DecodeDispatch. @@ -350,7 +389,7 @@ Module reflect. Module ContractConstructorDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(ink.reflect.dispatch.DecodeDispatch.Trait Type_) @@ -362,6 +401,46 @@ Module reflect. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module ink_reflect_dispatch_DecodeDispatch. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.DecodeDispatch.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_DecodeDispatch. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractConstructorDecoder. End dispatch. @@ -663,7 +742,7 @@ Module codegen. Module TraitCallForwarder. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -675,12 +754,39 @@ Module codegen. : Notation.DoubleColonType Self "Forwarder" := { Notation.double_colon_type := Forwarder; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarder. (* Module TraitCallForwarderFor. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -728,6 +834,33 @@ Module codegen. : Notation.Dot "build_mut" := { Notation.dot := build_mut; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarderFor. *) End call_builder. @@ -1303,7 +1436,7 @@ Module trait_def. Module TraitCallForwarder. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -1315,12 +1448,39 @@ Module trait_def. : Notation.DoubleColonType Self "Forwarder" := { Notation.double_colon_type := Forwarder; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarder. (* Module TraitCallForwarderFor. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -1366,6 +1526,33 @@ Module trait_def. : Notation.Dot "build_mut" := { Notation.dot := build_mut; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarderFor. *) End call_builder. @@ -1409,7 +1596,7 @@ Module call_builder. Module TraitCallForwarder. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -1421,12 +1608,39 @@ Module call_builder. : Notation.DoubleColonType Self "Forwarder" := { Notation.double_colon_type := Forwarder; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarder. (* Module TraitCallForwarderFor. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait @@ -1472,6 +1686,33 @@ Module call_builder. : Notation.Dot "build_mut" := { Notation.dot := build_mut; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarderFor. *) End call_builder. @@ -1501,7 +1742,7 @@ End TraitCallBuilder. Module TraitCallForwarder. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait Forwarder), @@ -1512,12 +1753,39 @@ Module TraitCallForwarder. : Notation.DoubleColonType Self "Forwarder" := { Notation.double_colon_type := Forwarder; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarder. (* Module TraitCallForwarderFor. Class Trait (Self : Set) : Type := { Forwarder : Set; - _ + __the_bounds_of_Forwarder : Sigma `(ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait Forwarder), @@ -1562,6 +1830,33 @@ End TraitCallForwarder. : Notation.Dot "build_mut" := { Notation.dot := build_mut; }. + Module The_Bounds_Of_Forwarder. + Module ink_codegen_trait_def_call_builder_TraitCallBuilder. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.codegen.trait_def.call_builder.TraitCallBuilder.Trait + (Forwarder (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Forwarder0 + as + [? __the_bounds_of_Forwarder0]); + assumption. + Defined. + End ink_codegen_trait_def_call_builder_TraitCallBuilder. + End The_Bounds_Of_Forwarder. End TraitCallForwarderFor. *) Module trait_message. @@ -1868,7 +2163,7 @@ Module Wrap_dispatch_1. Module ContractMessageDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(parity_scale_codec.codec.Decode.Trait Type_) @@ -1880,6 +2175,45 @@ Module Wrap_dispatch_1. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractMessageDecoder. Module DecodeDispatch. @@ -1906,7 +2240,7 @@ Module Wrap_dispatch_1. Module ContractConstructorDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(ink.reflect.dispatch.DecodeDispatch.Trait Type_) @@ -1918,6 +2252,46 @@ Module Wrap_dispatch_1. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module ink_reflect_dispatch_DecodeDispatch. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.DecodeDispatch.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_DecodeDispatch. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractConstructorDecoder. End dispatch. End Wrap_dispatch_1. @@ -2084,7 +2458,7 @@ Definition ConstructorOutputValue := @ConstructorOutputValue.t. Module ContractMessageDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(parity_scale_codec.codec.Decode.Trait Type_) @@ -2096,12 +2470,49 @@ Module ContractMessageDecoder. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractMessageDecoder. Module ContractConstructorDecoder. Class Trait (Self : Set) : Type := { Type_ : Set; - _ + __the_bounds_of_Type_ : Sigma `(ink.reflect.dispatch.DecodeDispatch.Trait Type_) @@ -2113,6 +2524,43 @@ Module ContractConstructorDecoder. : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module ink_reflect_dispatch_DecodeDispatch. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.DecodeDispatch.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_DecodeDispatch. + Module ink_reflect_dispatch_ExecuteDispatchable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink.reflect.dispatch.ExecuteDispatchable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_reflect_dispatch_ExecuteDispatchable. + End The_Bounds_Of_Type_. End ContractConstructorDecoder. Module ExecuteDispatchable. @@ -2395,13 +2843,43 @@ Module chain_extension. Module ChainExtension. Class Trait (Self : Set) : Type := { ErrorCode : Set; - _ : Sigma `(ink_env.chain_extension.FromStatusCode.Trait ErrorCode), unit; + __the_bounds_of_ErrorCode + : + Sigma `(ink_env.chain_extension.FromStatusCode.Trait ErrorCode), + unit; }. Global Instance Method_ErrorCode `(Trait) : Notation.DoubleColonType Self "ErrorCode" := { Notation.double_colon_type := ErrorCode; }. + Module The_Bounds_Of_ErrorCode. + Module ink_env_chain_extension_FromStatusCode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.chain_extension.FromStatusCode.Trait + (ErrorCode (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_ErrorCode0 + as + [? __the_bounds_of_ErrorCode0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_ErrorCode0 + as + [? __the_bounds_of_ErrorCode0]); + assumption. + Defined. + End ink_env_chain_extension_FromStatusCode. + End The_Bounds_Of_ErrorCode. End ChainExtension. Module private. @@ -2478,13 +2956,43 @@ End ChainExtensionInstance. Module ChainExtension. Class Trait (Self : Set) : Type := { ErrorCode : Set; - _ : Sigma `(ink_env.chain_extension.FromStatusCode.Trait ErrorCode), unit; + __the_bounds_of_ErrorCode + : + Sigma `(ink_env.chain_extension.FromStatusCode.Trait ErrorCode), + unit; }. Global Instance Method_ErrorCode `(Trait) : Notation.DoubleColonType Self "ErrorCode" := { Notation.double_colon_type := ErrorCode; }. + Module The_Bounds_Of_ErrorCode. + Module ink_env_chain_extension_FromStatusCode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.chain_extension.FromStatusCode.Trait + (ErrorCode (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_ErrorCode0 + as + [? __the_bounds_of_ErrorCode0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_ErrorCode0 + as + [? __the_bounds_of_ErrorCode0]); + assumption. + Defined. + End ink_env_chain_extension_FromStatusCode. + End The_Bounds_Of_ErrorCode. End ChainExtension. (* Module IsResultType. diff --git a/CoqOfRust/ink/ink_env.v b/CoqOfRust/ink/ink_env.v index ca329c37e..f84161b3b 100644 --- a/CoqOfRust/ink/ink_env.v +++ b/CoqOfRust/ink/ink_env.v @@ -102,7 +102,7 @@ Module types. Module FromLittleEndian. Class Trait (Self : Set) : Type := { Bytes : Set; - _ + __the_bounds_of_Bytes : Sigma `(core.default.Default.Trait Bytes) @@ -120,6 +120,62 @@ Module types. : Notation.Dot "from_le_bytes" := { Notation.dot := from_le_bytes; }. + Module The_Bounds_Of_Bytes. + Module core_default_Default. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.default.Default.Trait (Bytes (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_default_Default. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (Bytes (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (Bytes (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_Bytes. End FromLittleEndian. Module AccountIdGuard. @@ -144,7 +200,7 @@ Module types. Class Trait (Self : Set) : Type := { MAX_EVENT_TOPICS `{H' : State.Trait} : usize; AccountId : Set; - _ + __the_bounds_of_AccountId : Sigma `(parity_scale_codec.codec.Codec.Trait AccountId) @@ -158,7 +214,7 @@ Module types. `(core.convert.AsMut.Trait AccountId (T := Slice u8)), unit; Balance : Set; - _ + __the_bounds_of_Balance : Sigma `(parity_scale_codec.codec.Codec.Trait Balance) @@ -172,7 +228,7 @@ Module types. `(ink_env.types.FromLittleEndian.Trait Balance), unit; Hash : Set; - _ + __the_bounds_of_Hash : Sigma `(parity_scale_codec.codec.Codec.Trait Hash) @@ -188,7 +244,7 @@ Module types. `(core.convert.AsMut.Trait Hash (T := Slice u8)), unit; Timestamp : Set; - _ + __the_bounds_of_Timestamp : Sigma `(parity_scale_codec.codec.Codec.Trait Timestamp) @@ -202,7 +258,7 @@ Module types. `(ink_env.types.FromLittleEndian.Trait Timestamp), unit; BlockNumber : Set; - _ + __the_bounds_of_BlockNumber : Sigma `(parity_scale_codec.codec.Codec.Trait BlockNumber) @@ -246,6 +302,936 @@ Module types. : Notation.DoubleColonType Self "ChainExtension" := { Notation.double_colon_type := ChainExtension; }. + Module The_Bounds_Of_AccountId. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (AccountId (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.Eq.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_Eq. + Module core_cmp_Ord. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.Ord.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_Ord. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (AccountId (Trait := _Tr)) + (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (AccountId (Trait := _Tr)) + (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_AccountId. + Module The_Bounds_Of_Balance. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Balance (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Balance0 + as + [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_Balance. + Module The_Bounds_Of_Hash. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_clone_Clone. + Module ink_primitives_types_Clear. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_primitives.types.Clear.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End ink_primitives_types_Clear. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Hash (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_Eq. + Module core_cmp_Ord. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Ord.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_Ord. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (Hash (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (Hash (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_Hash. + Module The_Bounds_Of_Timestamp. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Timestamp (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.Eq.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_Timestamp. + Module The_Bounds_Of_BlockNumber. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait + (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (BlockNumber (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.Eq.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait + (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_BlockNumber. End Environment. Module NoChainExtension. @@ -272,7 +1258,7 @@ End types. Module FromLittleEndian. Class Trait (Self : Set) : Type := { Bytes : Set; - _ + __the_bounds_of_Bytes : Sigma `(core.default.Default.Trait Bytes) @@ -290,6 +1276,59 @@ Module FromLittleEndian. : Notation.Dot "from_le_bytes" := { Notation.dot := from_le_bytes; }. + Module The_Bounds_Of_Bytes. + Module core_default_Default. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.default.Default.Trait (Bytes (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_default_Default. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (Bytes (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (Bytes (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Bytes0 as [? __the_bounds_of_Bytes0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_Bytes. End FromLittleEndian. Module AccountIdGuard. @@ -314,7 +1353,7 @@ Module Environment. Class Trait (Self : Set) : Type := { MAX_EVENT_TOPICS `{H' : State.Trait} : usize; AccountId : Set; - _ + __the_bounds_of_AccountId : Sigma `(parity_scale_codec.codec.Codec.Trait AccountId) @@ -328,7 +1367,7 @@ Module Environment. `(core.convert.AsMut.Trait AccountId (T := Slice u8)), unit; Balance : Set; - _ + __the_bounds_of_Balance : Sigma `(parity_scale_codec.codec.Codec.Trait Balance) @@ -342,7 +1381,7 @@ Module Environment. `(ink_env.types.FromLittleEndian.Trait Balance), unit; Hash : Set; - _ + __the_bounds_of_Hash : Sigma `(parity_scale_codec.codec.Codec.Trait Hash) @@ -358,7 +1397,7 @@ Module Environment. `(core.convert.AsMut.Trait Hash (T := Slice u8)), unit; Timestamp : Set; - _ + __the_bounds_of_Timestamp : Sigma `(parity_scale_codec.codec.Codec.Trait Timestamp) @@ -372,7 +1411,7 @@ Module Environment. `(ink_env.types.FromLittleEndian.Trait Timestamp), unit; BlockNumber : Set; - _ + __the_bounds_of_BlockNumber : Sigma `(parity_scale_codec.codec.Codec.Trait BlockNumber) @@ -416,6 +1455,900 @@ Module Environment. : Notation.DoubleColonType Self "ChainExtension" := { Notation.double_colon_type := ChainExtension; }. + Module The_Bounds_Of_AccountId. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (AccountId (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_Eq. + Module core_cmp_Ord. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Ord.Trait (AccountId (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_cmp_Ord. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (AccountId (Trait := _Tr)) + (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (AccountId (Trait := _Tr)) + (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_AccountId0 + as + [? __the_bounds_of_AccountId0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_AccountId. + Module The_Bounds_Of_Balance. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Balance (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait (Balance (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Balance0 as [? __the_bounds_of_Balance0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_Balance. + Module The_Bounds_Of_Hash. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.marker.Copy.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.clone.Clone.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_clone_Clone. + Module ink_primitives_types_Clear. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_primitives.types.Clear.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End ink_primitives_types_Clear. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Hash (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_Eq. + Module core_cmp_Ord. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Ord.Trait (Hash (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_cmp_Ord. + Module core_convert_AsRef. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsRef.Trait (Hash (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_convert_AsRef. + Module core_convert_AsMut. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.convert.AsMut.Trait (Hash (Trait := _Tr)) (T := Slice u8)); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Hash0 as [? __the_bounds_of_Hash0]); + assumption. + Defined. + End core_convert_AsMut. + End The_Bounds_Of_Hash. + Module The_Bounds_Of_Timestamp. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (Timestamp (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve eapply (core.cmp.Eq.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait (Timestamp (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_Timestamp0 + as + [? __the_bounds_of_Timestamp0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_Timestamp. + Module The_Bounds_Of_BlockNumber. + Module parity_scale_codec_codec_Codec. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Codec.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End parity_scale_codec_codec_Codec. + Module ink_env_types_CodecAsType. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.CodecAsType.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_types_CodecAsType. + Module core_marker_Copy. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.marker.Copy.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_marker_Copy. + Module core_clone_Clone. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.clone.Clone.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_clone_Clone. + Module core_cmp_PartialEq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.PartialEq.Trait (BlockNumber (Trait := _Tr)) + (Rhs := core.cmp.PartialEq.Default.Rhs Self)); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_cmp_PartialEq. + Module core_cmp_Eq. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.cmp.Eq.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End core_cmp_Eq. + Module ink_env_arithmetic_AtLeast32BitUnsigned. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.arithmetic.AtLeast32BitUnsigned.Trait + (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_arithmetic_AtLeast32BitUnsigned. + Module ink_env_types_FromLittleEndian. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.FromLittleEndian.Trait (BlockNumber (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_BlockNumber0 + as + [? __the_bounds_of_BlockNumber0]); + assumption. + Defined. + End ink_env_types_FromLittleEndian. + End The_Bounds_Of_BlockNumber. End Environment. Module NoChainExtension. @@ -442,13 +2375,32 @@ Module contract. Module ContractEnv. Class Trait (Self : Set) : Type := { Env : Set; - _ : Sigma `(ink_env.types.Environment.Trait Env), unit; + __the_bounds_of_Env : Sigma `(ink_env.types.Environment.Trait Env), unit; }. Global Instance Method_Env `(Trait) : Notation.DoubleColonType Self "Env" := { Notation.double_colon_type := Env; }. + Module The_Bounds_Of_Env. + Module ink_env_types_Environment. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.Environment.Trait (Env (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Env0 as [? __the_bounds_of_Env0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Env0 as [? __the_bounds_of_Env0]); + assumption. + Defined. + End ink_env_types_Environment. + End The_Bounds_Of_Env. End ContractEnv. Module ContractReference. @@ -675,7 +2627,10 @@ Module call. IS_RESULT `{H' : State.Trait} : bool; Output : Set; Error : Set; - _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit; + __the_bounds_of_Error + : + Sigma `(parity_scale_codec.codec.Decode.Trait Error), + unit; ok `{H' : State.Trait} : C -> M (H := H') Output; }. @@ -701,6 +2656,26 @@ Module call. := (axiom : M (H := H') (core.option.Option Output)); }. + Module The_Bounds_Of_Error. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Error (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + End The_Bounds_Of_Error. End ConstructorReturnType. Module CreateParams. @@ -859,6 +2834,32 @@ Module call. (Args := Args) (Salt := Salt) (RetType := RetType). + + Parameter build_create : + forall + `{H' : State.Trait} + {ContractRef : Set} + `{ink_env.contract.ContractEnv.Trait ContractRef}, + M (H := H') + (ink_env.call.create_builder.CreateBuilder + (ink_env.contract.ContractEnv.Env (Self := ContractRef)) + ContractRef + (ink_env.call.common.Unset_ + (ink_env.types.Environment.Hash + (Self := ink_env.contract.ContractEnv.Env + (Self := ContractRef)))) + (ink_env.call.common.Unset_ u64) + (ink_env.call.common.Unset_ + (ink_env.types.Environment.Balance + (Self := ink_env.contract.ContractEnv.Env + (Self := ContractRef)))) + (ink_env.call.common.Unset_ + (ink_env.call.execution_input.ExecutionInput + ink_env.call.execution_input.EmptyArgumentList)) + (ink_env.call.common.Unset_ + ink_env.call.create_builder.state.Salt) + (ink_env.call.common.Unset_ + (ink_env.call.common.ReturnType unit))). End create_builder. End call. @@ -949,13 +2950,33 @@ Module hash. Class Trait (Self : Set) `{ink_env.hash.private.Sealed.Trait Self} : Type := { Type_ : Set; - _ : Sigma `(core.default.Default.Trait Type_), unit; + __the_bounds_of_Type_ : Sigma `(core.default.Default.Trait Type_), unit; }. Global Instance Method_Type_ `(Trait) : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module core_default_Default. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.default.Default.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End core_default_Default. + End The_Bounds_Of_Type_. End HashOutput. Module CryptoHash. @@ -1105,7 +3126,10 @@ Module topics. Module Topics. Class Trait (Self : Set) : Type := { RemainingTopics : Set; - _ : Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), unit; + __the_bounds_of_RemainingTopics + : + Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), + unit; topics `{H' : State.Trait} {E B : Set} @@ -1130,6 +3154,33 @@ Module topics. := topics (E := E) (B := B) (H'0 := H'0) (H'1 := H'1); }. + Module The_Bounds_Of_RemainingTopics. + Module ink_env_topics_EventTopicsAmount. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.topics.EventTopicsAmount.Trait + (RemainingTopics (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_RemainingTopics0 + as + [? __the_bounds_of_RemainingTopics0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_RemainingTopics0 + as + [? __the_bounds_of_RemainingTopics0]); + assumption. + Defined. + End ink_env_topics_EventTopicsAmount. + End The_Bounds_Of_RemainingTopics. End Topics. Module PrefixedValue. @@ -4174,7 +6225,10 @@ Module create_builder. IS_RESULT `{H' : State.Trait} : bool; Output : Set; Error : Set; - _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit; + __the_bounds_of_Error + : + Sigma `(parity_scale_codec.codec.Decode.Trait Error), + unit; ok `{H' : State.Trait} : C -> M (H := H') Output; }. @@ -4200,6 +6254,26 @@ Module create_builder. := (axiom : M (H := H') (core.option.Option Output)); }. + Module The_Bounds_Of_Error. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Error (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + End The_Bounds_Of_Error. End ConstructorReturnType. Module CreateParams. @@ -4352,6 +6426,30 @@ Module create_builder. (Args := Args) (Salt := Salt) (RetType := RetType). + + Parameter build_create : + forall + `{H' : State.Trait} + {ContractRef : Set} + `{ink_env.contract.ContractEnv.Trait ContractRef}, + M (H := H') + (ink_env.call.create_builder.CreateBuilder + (ink_env.contract.ContractEnv.Env (Self := ContractRef)) + ContractRef + (ink_env.call.common.Unset_ + (ink_env.types.Environment.Hash + (Self := ink_env.contract.ContractEnv.Env + (Self := ContractRef)))) + (ink_env.call.common.Unset_ u64) + (ink_env.call.common.Unset_ + (ink_env.types.Environment.Balance + (Self := ink_env.contract.ContractEnv.Env + (Self := ContractRef)))) + (ink_env.call.common.Unset_ + (ink_env.call.execution_input.ExecutionInput + ink_env.call.execution_input.EmptyArgumentList)) + (ink_env.call.common.Unset_ ink_env.call.create_builder.state.Salt) + (ink_env.call.common.Unset_ (ink_env.call.common.ReturnType unit))). End create_builder. Module state. @@ -4387,7 +6485,10 @@ Module ConstructorReturnType. IS_RESULT `{H' : State.Trait} : bool; Output : Set; Error : Set; - _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit; + __the_bounds_of_Error + : + Sigma `(parity_scale_codec.codec.Decode.Trait Error), + unit; ok `{H' : State.Trait} : C -> M (H := H') Output; }. @@ -4413,6 +6514,25 @@ Module ConstructorReturnType. := (axiom : M (H := H') (core.option.Option Output)); }. + Module The_Bounds_Of_Error. + Module parity_scale_codec_codec_Decode. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (parity_scale_codec.codec.Decode.Trait (Error (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Error0 as [? __the_bounds_of_Error0]); + assumption. + Defined. + End parity_scale_codec_codec_Decode. + End The_Bounds_Of_Error. End ConstructorReturnType. Module CreateParams. @@ -5002,12 +7122,31 @@ End IsResultTypeSealed. Module ContractEnv. Class Trait (Self : Set) : Type := { Env : Set; - _ : Sigma `(ink_env.types.Environment.Trait Env), unit; + __the_bounds_of_Env : Sigma `(ink_env.types.Environment.Trait Env), unit; }. Global Instance Method_Env `(Trait) : Notation.DoubleColonType Self "Env" := { Notation.double_colon_type := Env; }. + Module The_Bounds_Of_Env. + Module ink_env_types_Environment. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.types.Environment.Trait (Env (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Env0 as [? __the_bounds_of_Env0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Env0 as [? __the_bounds_of_Env0]); + assumption. + Defined. + End ink_env_types_Environment. + End The_Bounds_Of_Env. End ContractEnv. Module ContractReference. @@ -5196,13 +7335,32 @@ Definition AccountError := AccountError.t. Module HashOutput. Class Trait (Self : Set) `{ink_env.hash.private.Sealed.Trait Self} : Type := { Type_ : Set; - _ : Sigma `(core.default.Default.Trait Type_), unit; + __the_bounds_of_Type_ : Sigma `(core.default.Default.Trait Type_), unit; }. Global Instance Method_Type_ `(Trait) : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module core_default_Default. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (core.default.Default.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End core_default_Default. + End The_Bounds_Of_Type_. End HashOutput. Module CryptoHash. @@ -5364,7 +7522,10 @@ End EventTopicsAmount. Module Topics. Class Trait (Self : Set) : Type := { RemainingTopics : Set; - _ : Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), unit; + __the_bounds_of_RemainingTopics + : + Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), + unit; topics `{H' : State.Trait} {E B : Set} @@ -5389,6 +7550,33 @@ Module Topics. := topics (E := E) (B := B) (H'0 := H'0) (H'1 := H'1); }. + Module The_Bounds_Of_RemainingTopics. + Module ink_env_topics_EventTopicsAmount. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_env.topics.EventTopicsAmount.Trait + (RemainingTopics (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_RemainingTopics0 + as + [? __the_bounds_of_RemainingTopics0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_RemainingTopics0 + as + [? __the_bounds_of_RemainingTopics0]); + assumption. + Defined. + End ink_env_topics_EventTopicsAmount. + End The_Bounds_Of_RemainingTopics. End Topics. Module PrefixedValue. diff --git a/CoqOfRust/ink/ink_storage_traits.v b/CoqOfRust/ink/ink_storage_traits.v index cf286fd71..c773ad410 100644 --- a/CoqOfRust/ink/ink_storage_traits.v +++ b/CoqOfRust/ink/ink_storage_traits.v @@ -161,9 +161,12 @@ Module storage. `{ink_storage_traits.storage.StorageKey.Trait Key} : Type := { Type_ : Set; - _ : Sigma `(ink_storage_traits.storage.Storable.Trait Type_), unit; + __the_bounds_of_Type_ + : + Sigma `(ink_storage_traits.storage.Storable.Trait Type_), + unit; PreferredKey : Set; - _ + __the_bounds_of_PreferredKey : Sigma `(ink_storage_traits.storage.StorageKey.Trait PreferredKey), unit; @@ -177,6 +180,54 @@ Module storage. : Notation.DoubleColonType Self "PreferredKey" := { Notation.double_colon_type := PreferredKey; }. + Module The_Bounds_Of_Type_. + Module ink_storage_traits_storage_Storable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.Storable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_storage_traits_storage_Storable. + End The_Bounds_Of_Type_. + Module The_Bounds_Of_PreferredKey. + Module ink_storage_traits_storage_StorageKey. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.StorageKey.Trait + (PreferredKey (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_PreferredKey0 + as + [? __the_bounds_of_PreferredKey0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_PreferredKey0 + as + [? __the_bounds_of_PreferredKey0]); + assumption. + Defined. + End ink_storage_traits_storage_StorageKey. + End The_Bounds_Of_PreferredKey. End StorableHint. Module AutoStorableHint. @@ -186,13 +237,37 @@ Module storage. `{ink_storage_traits.storage.StorageKey.Trait Key} : Type := { Type_ : Set; - _ : Sigma `(ink_storage_traits.storage.Storable.Trait Type_), unit; + __the_bounds_of_Type_ + : + Sigma `(ink_storage_traits.storage.Storable.Trait Type_), + unit; }. Global Instance Method_Type_ `(Trait) : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module ink_storage_traits_storage_Storable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.Storable.Trait + (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_storage_traits_storage_Storable. + End The_Bounds_Of_Type_. End AutoStorableHint. End storage. @@ -283,9 +358,15 @@ Module StorableHint. `{ink_storage_traits.storage.StorageKey.Trait Key} : Type := { Type_ : Set; - _ : Sigma `(ink_storage_traits.storage.Storable.Trait Type_), unit; + __the_bounds_of_Type_ + : + Sigma `(ink_storage_traits.storage.Storable.Trait Type_), + unit; PreferredKey : Set; - _ : Sigma `(ink_storage_traits.storage.StorageKey.Trait PreferredKey), unit; + __the_bounds_of_PreferredKey + : + Sigma `(ink_storage_traits.storage.StorageKey.Trait PreferredKey), + unit; }. Global Instance Method_Type_ `(Trait) @@ -296,6 +377,52 @@ Module StorableHint. : Notation.DoubleColonType Self "PreferredKey" := { Notation.double_colon_type := PreferredKey; }. + Module The_Bounds_Of_Type_. + Module ink_storage_traits_storage_Storable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.Storable.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_storage_traits_storage_Storable. + End The_Bounds_Of_Type_. + Module The_Bounds_Of_PreferredKey. + Module ink_storage_traits_storage_StorageKey. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.StorageKey.Trait + (PreferredKey (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct + __the_bounds_of_PreferredKey0 + as + [? __the_bounds_of_PreferredKey0]; + try assumption). + all: + compute; + destruct _Tr; + repeat + (destruct + __the_bounds_of_PreferredKey0 + as + [? __the_bounds_of_PreferredKey0]); + assumption. + Defined. + End ink_storage_traits_storage_StorageKey. + End The_Bounds_Of_PreferredKey. End StorableHint. Module AutoStorableHint. @@ -305,13 +432,35 @@ Module AutoStorableHint. `{ink_storage_traits.storage.StorageKey.Trait Key} : Type := { Type_ : Set; - _ : Sigma `(ink_storage_traits.storage.Storable.Trait Type_), unit; + __the_bounds_of_Type_ + : + Sigma `(ink_storage_traits.storage.Storable.Trait Type_), + unit; }. Global Instance Method_Type_ `(Trait) : Notation.DoubleColonType Self "Type_" := { Notation.double_colon_type := Type_; }. + Module The_Bounds_Of_Type_. + Module ink_storage_traits_storage_Storable. + Global Instance I `(_Tr : Trait) + : ltac:(unshelve + eapply + (ink_storage_traits.storage.Storable.Trait (Type_ (Trait := _Tr))); + compute; + destruct _Tr; + repeat + destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]; + try assumption). + all: + compute; + destruct _Tr; + repeat (destruct __the_bounds_of_Type_0 as [? __the_bounds_of_Type_0]); + assumption. + Defined. + End ink_storage_traits_storage_Storable. + End The_Bounds_Of_Type_. End AutoStorableHint. Module layout. diff --git a/CoqOfRust/ink/update_after_translation.py b/CoqOfRust/ink/update_after_translation.py index 935243fd7..d9787102a 100644 --- a/CoqOfRust/ink/update_after_translation.py +++ b/CoqOfRust/ink/update_after_translation.py @@ -63,6 +63,7 @@ def update_ink_engine(): Require CoqOfRust.ink.parity_scale_codec.""", content, ) + # the part below removes a duplicated module that caused a name conflict content = content.replace( """ Module Error. diff --git a/coq-of-rust-config.json b/coq-of-rust-config.json index 97d5fb57c..d18910307 100644 --- a/coq-of-rust-config.json +++ b/coq-of-rust-config.json @@ -95,9 +95,6 @@ "CallBuilder": { "move": "up", "before": "build_call" }, "Call": { "move": "up", "before": "build_call" } }, - "top_level::call::create_builder": { - "build_create": { "move": "up" } - }, "top_level::chain_extension": { "private": { "move": "up", "before": "IsResultType" } } diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 712c3a966..7f4e20043 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -15,6 +15,7 @@ pretty = "0.11.3" serde = { version = "1.0", features = ["derive"] } serde_json = { version = "1.0" } toml = "0.5.8" +topological-sort = "0.2.2" walkdir = "2.3.2" [package.metadata.rust-analyzer] diff --git a/lib/src/algs.rs b/lib/src/algs.rs new file mode 100644 index 000000000..f3170221d --- /dev/null +++ b/lib/src/algs.rs @@ -0,0 +1,131 @@ +use std::collections::{HashMap, HashSet, VecDeque}; +use topological_sort::TopologicalSort; + +/// a type of directed graphs +pub(crate) struct DirectedGraph(HashMap>); + +impl DirectedGraph +where + V: std::clone::Clone + std::cmp::Eq + std::hash::Hash, +{ + pub(crate) fn of_hashmap(hm: &HashMap>) -> Self { + DirectedGraph(hm.to_owned()) + } + + /// if `graph` is a directed acyclic graph, + /// creates a subgraph with all descendants of `starts` + pub(crate) fn get_subgraph_of(&self, start: &V) -> DirectedGraph { + let mut result = HashMap::new(); + let mut queue = VecDeque::new(); + queue.push_back(start); + + while let Some(vertex) = queue.pop_front() { + if let Some(succs) = self.0.get(vertex) { + result.entry(vertex.clone()).or_insert(succs.clone()); + + for succ in succs { + queue.push_back(succ) + } + } + } + + DirectedGraph(result) + } + + /// topologically sort the graph + pub(crate) fn to_topological_sort(&self) -> TopologicalSort { + self.0 + .iter() + .fold(&mut TopologicalSort::new(), |result, (prec, succs)| { + succs.iter().fold(result, |result, succ| { + result.add_dependency(succ.to_owned(), prec.to_owned()); + result + }) + }) + .clone() + } +} +/*#[inline] +/// assigns `new` to `*old` if `*old < new` +fn assign_if_greater(old: &mut A, new: A) +where + A: std::cmp::PartialOrd, +{ + if *old < new { + *old = new + } +} + +pub(crate) fn longest_paths_length<'a, V>(start: &'a V, graph: &'a DirectedGraph) -> HashMap<&'a V, u32> +where + V: core::clone::Clone + std::cmp::Eq + std::hash::Hash, +{ + let mut distances = HashMap::new(); + let mut queue = VecDeque::new(); + queue.push_back((start, 0u32)); + + while let Some((current, dist)) = queue.pop_front() { + if let Some(vertices) = graph.get(current) { + for v in vertices { + let new_dist = dist + 1; + distances + .entry(v) + .and_modify(|old_dist| assign_if_greater(old_dist, new_dist)) + .or_insert(new_dist); + + queue.push_back((v, new_dist)); + } + } + } + + distances +} + +pub(crate) fn find_last(start: V, graph: DirectedGraph) -> V +where + V: core::clone::Clone + std::cmp::Eq + std::hash::Hash, +{ + let mut current_last = &start; + let mut queue = VecDeque::new(); + + while let Some(vertices) = graph.get(current_last) { + for v in vertices { + queue.push_back(v); + } + if let Some(new_last) = queue.pop_front() { + current_last = new_last; + } else { + break; + } + } + + current_last.to_owned() +} + +/// changes the direction of edges in a given directed graph +pub(crate) fn reverse_graph(graph: DirectedGraph) -> DirectedGraph +where + V: core::clone::Clone + std::cmp::Eq + std::hash::Hash, +{ + let mut reversed = HashMap::new(); + + for (src, dests) in graph { + for dest in dests { + reversed + .entry(dest) + .or_insert(HashSet::new()) + .insert(src.clone()); + } + } + + reversed +} + +#[inline] +pub(crate) fn to_set(v: &[A]) -> HashSet +where + A: core::clone::Clone + std::cmp::Eq + std::hash::Hash, +{ + v.into_iter().map(|x| x.to_owned()).collect() +} +*/ diff --git a/lib/src/coq.rs b/lib/src/coq.rs index 6e3c09a64..4d9b90a0e 100644 --- a/lib/src/coq.rs +++ b/lib/src/coq.rs @@ -87,7 +87,7 @@ pub(crate) struct Instance<'a> { name: String, parameters: Vec>, class: Expression<'a>, - bulid_expr: Expression<'a>, + bulid_expr: Option>, proof_lines: Vec>, } @@ -365,67 +365,6 @@ impl<'a> TopLevelItem<'a> { TopLevelItem::Section(section) => section.to_doc(), } } - - /// creates a module with the translation of the given trait - pub(crate) fn trait_module( - name: &'a str, - ty_params: &[(String, Option>)], - predicates: &[ArgDecl<'a>], - bounds: &[ArgDecl<'a>], - items: &[ClassFieldDef<'a>], - instances: &[Instance<'a>], - ) -> Self { - TopLevelItem::Module(Module::new( - name, - TopLevel::concat(&[ - TopLevel::locally_unset_primitive_projections_if( - items.is_empty(), - &[TopLevelItem::Class(Class::new( - "Trait", - &[ - vec![ArgDecl::new( - &ArgDeclVar::Simple { - idents: vec!["Self".to_string()], - ty: Some(Expression::Set), - }, - ArgSpecKind::Explicit, - )], - bounds.to_vec(), - if ty_params.is_empty() { - vec![] - } else { - vec![ArgDecl::new( - &ArgDeclVar::Simple { - idents: ty_params - .iter() - .map(|(ty, default)| { - match default { - // @TODO: implement the translation of type parameters with default - Some(_default) => ["(* TODO *) ", ty].concat(), - None => ty.to_string(), - } - }) - .collect(), - ty: Some(Expression::Set), - }, - ArgSpecKind::Implicit, - )] - }, - predicates.to_vec(), - ] - .concat(), - items.to_vec(), - ))], - ), - TopLevel { - items: instances - .iter() - .map(|i| TopLevelItem::Instance(i.to_owned())) - .collect(), - }, - ]), - )) - } } impl<'a> Module<'a> { @@ -585,11 +524,11 @@ impl<'a> Context<'a> { impl<'a> Class<'a> { /// produces a new coq typeclass definition - pub(crate) fn new(name: &str, params: &[ArgDecl<'a>], items: Vec>) -> Self { + pub(crate) fn new(name: &str, params: &[ArgDecl<'a>], items: &[ClassFieldDef<'a>]) -> Self { Class { name: name.to_owned(), params: params.to_owned(), - items, + items: items.to_owned(), } } @@ -638,7 +577,7 @@ impl<'a> Instance<'a> { name: &str, parameters: &[ArgDecl<'a>], class: Expression<'a>, - bulid_expr: &Expression<'a>, + bulid_expr: &Option>, proof_lines: Vec>, ) -> Self { Instance { @@ -673,10 +612,19 @@ impl<'a> Instance<'a> { }, ]), line(), - nest([text(": "), self.class.to_doc(false), line(), text(":= ")]), + nest([ + concat([text(": "), self.class.to_doc(false)]), + if self.bulid_expr.is_some() { + concat([line(), text(":= ")]) + } else { + text(".") + }, + ]), ]), - self.bulid_expr.to_doc(false), - text("."), + match &self.bulid_expr { + Some(build_expr) => concat([build_expr.to_doc(false), text(".")]), + None => nil(), + }, if self.proof_lines.is_empty() { nil() } else { @@ -868,8 +816,12 @@ impl<'a> Expression<'a> { } pub(crate) fn just_name(name: &str) -> Self { + Expression::single_var(&Path::new(&[name])) + } + + pub(crate) fn single_var(path: &Path) -> Self { Expression::Variable { - ident: Path::new(&[name]), + ident: path.to_owned(), no_implicit: false, } } @@ -929,6 +881,16 @@ impl<'a> Expression<'a> { None => Expression::Unit, } } + + #[allow(dead_code)] + pub(crate) fn some() -> Self { + Expression::just_name("Some") + } + + #[allow(dead_code)] + pub(crate) fn none() -> Self { + Expression::just_name("None") + } } impl<'a> Field<'a> { diff --git a/lib/src/env.rs b/lib/src/env.rs index a34587f20..0c4a30a31 100644 --- a/lib/src/env.rs +++ b/lib/src/env.rs @@ -1,12 +1,13 @@ use crate::configuration::*; +use crate::path::Path; use crate::ty::*; use rustc_middle::ty::TyCtxt; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; /// The environment used for the translation steps, holding various state /// information -pub(crate) struct Env<'a> { +pub(crate) struct Env<'a, 'b> { /// We use a counter for the disambiguation of several impls for the same /// type pub(crate) impl_counter: HashMap, @@ -18,4 +19,5 @@ pub(crate) struct Env<'a> { pub(crate) reorder_map: HashMap>, /// the configuration read or default if no config file is found pub(crate) configuration: Configuration, + pub(crate) supertraits: &'b mut HashMap>, } diff --git a/lib/src/path.rs b/lib/src/path.rs index b07399fa8..4b1505d10 100644 --- a/lib/src/path.rs +++ b/lib/src/path.rs @@ -163,7 +163,7 @@ pub(crate) fn compile_qpath(env: &Env, qpath: &QPath) -> Path { #[allow(dead_code)] /// returns generics for the given path pub(crate) fn get_path_generics<'a>( - env: &Env<'a>, + env: &Env<'a, '_>, path: &rustc_hir::Path, ) -> Option<&'a rustc_middle::ty::Generics> { path.res @@ -272,4 +272,10 @@ impl Path { .collect(), } } + + pub(crate) fn push(&self, segment: S) -> Self { + let mut path = self.clone(); + path.segments.push(segment.to_string()); + path + } } diff --git a/lib/src/render.rs b/lib/src/render.rs index 953607f23..fccfd1a86 100644 --- a/lib/src/render.rs +++ b/lib/src/render.rs @@ -16,6 +16,11 @@ pub(crate) fn curly_brackets(doc: RcDoc<()>) -> RcDoc<()> { RcDoc::concat([RcDoc::text("{"), doc, RcDoc::text("}")]) } +/// encloses an expression in square brackets +pub(crate) fn square_brackets(doc: RcDoc<()>) -> RcDoc<()> { + RcDoc::concat([RcDoc::text("["), doc, RcDoc::text("]")]) +} + /// encloses an expression in regular brackets pub(crate) fn round_brackets(doc: RcDoc<()>) -> RcDoc<()> { RcDoc::concat([RcDoc::text("("), doc, RcDoc::text(")")]) diff --git a/lib/src/top_level.rs b/lib/src/top_level.rs index 4cdc79ba0..1cb6844bd 100644 --- a/lib/src/top_level.rs +++ b/lib/src/top_level.rs @@ -41,7 +41,7 @@ struct FnSigAndBody { } #[derive(Clone, Debug, Eq, Hash, PartialEq)] -enum TraitItem { +enum TraitItemData { Definition { ty_params: Vec, where_predicates: Vec, @@ -151,13 +151,7 @@ enum TopLevelItem { counter: u64, items: Vec, }, - Trait { - name: String, - ty_params: Vec<(String, Option>)>, - predicates: Vec, - bounds: Vec, - body: Vec<(String, TraitItem)>, - }, + Trait(Trait), TraitImpl { generic_tys: Vec, ty_params: Vec>, @@ -179,6 +173,21 @@ struct TypeStructStruct { is_dead_code: bool, } +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +struct TraitItem { + item_name: String, + item_data: TraitItemData, +} + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +struct Trait { + name: String, + ty_params: Vec<(String, Option>)>, + predicates: Vec, + bounds: Vec, + body: Vec, +} + #[derive(Clone, Debug, Eq, Hash, PartialEq)] pub struct TopLevel(Vec); @@ -296,7 +305,12 @@ fn deduplicate_top_level_items(items: Vec) -> Vec { /// - [rustc_middle::hir::map::Map] is intuitively the type for hir environments /// - Method [body] allows retrievient the body of an identifier [body_id] in an /// hir environment [hir] -fn compile_top_level_item(tcx: &TyCtxt, env: &mut Env, item: &Item) -> Vec { +fn compile_top_level_item( + tcx: &TyCtxt, + env: &mut Env, + item: &Item, + path: Path, +) -> Vec { let name = to_valid_coq_name(item.ident.name.to_string()); if env.axiomatize { let def_id = item.owner_id.to_def_id(); @@ -362,7 +376,8 @@ fn compile_top_level_item(tcx: &TyCtxt, env: &mut Env, item: &Item) -> Vec Vec vec![TopLevelItem::Error("Union".to_string())], ItemKind::Trait(_, _, generics, generic_bounds, items) => { - vec![TopLevelItem::Trait { + collect_supertraits(env, generic_bounds, path.push(name.clone())); + vec![TopLevelItem::Trait(Trait { name, ty_params: get_ty_params(env, generics), predicates: get_where_predicates(tcx, env, generics), @@ -463,10 +479,14 @@ fn compile_top_level_item(tcx: &TyCtxt, env: &mut Env, item: &Item) -> Vec { vec![TopLevelItem::Error("TraitAlias".to_string())] @@ -548,6 +568,25 @@ fn compile_top_level_item(tcx: &TyCtxt, env: &mut Env, item: &Item) -> Vec { + Some(compile_path(env, ptraitref.trait_ref.path)) + }, + // @TODO: should we include GenericBound::LangItemTrait ? + GenericBound::LangItemTrait { .. } + // we ignore lifetimes + | GenericBound::Outlives { .. } => None, + }) + .collect(); + env.supertraits.insert(path, supertraits); +} + /// returns a pair of function signature and its body fn get_hir_fn_sig_and_body<'a>( tcx: &'a TyCtxt, @@ -732,7 +771,7 @@ fn trait_bound_to_where_predicate(bound: TraitBound, ty: Box) -> WhereP WherePredicate { bound, ty } } -/// [compile_generic_bounds] compiles generic bounds in [compile_trait_item_body] +/// [compile_generic_bounds] compiles generic bounds fn compile_generic_bounds( tcx: &TyCtxt, env: &Env, @@ -863,15 +902,15 @@ fn compile_trait_item_body( ty_params: Vec, where_predicates: Vec, item: &rustc_hir::TraitItem, -) -> TraitItem { +) -> TraitItemData { match &item.kind { - TraitItemKind::Const(ty, _) => TraitItem::Definition { + TraitItemKind::Const(ty, _) => TraitItemData::Definition { ty_params, where_predicates, ty: compile_type(env, ty), }, TraitItemKind::Fn(fn_sig, trait_fn) => match trait_fn { - TraitFn::Required(_) => TraitItem::Definition { + TraitFn::Required(_) => TraitItemData::Definition { ty_params, where_predicates, ty: compile_fn_decl(env, fn_sig.decl), @@ -880,7 +919,7 @@ fn compile_trait_item_body( let env_tcx = env.tcx; let fn_sig_and_body = get_hir_fn_sig_and_body(&env_tcx, fn_sig, body_id); let signature_and_body = compile_fn_sig_and_body(env, &fn_sig_and_body, "arg"); - TraitItem::DefinitionWithDefault { + TraitItemData::DefinitionWithDefault { ty_params, where_predicates, signature_and_body, @@ -895,19 +934,28 @@ fn compile_trait_item_body( emit_warning_with_note(env, span, warning_msg, note_msg); } let generic_bounds = compile_generic_bounds(tcx, env, generic_bounds); - TraitItem::Type(generic_bounds) + TraitItemData::Type(generic_bounds) } } } -fn compile_top_level(tcx: &TyCtxt, opts: TopLevelOptions) -> TopLevel { +fn compile_top_level( + tcx: &TyCtxt, + opts: TopLevelOptions, + supertraits_map: &mut HashMap>, +) -> TopLevel { + let file = opts.filename; + // the path to the item being compiled + let path = Path::new(&[file.clone()]); + let mut env = Env { impl_counter: HashMap::new(), tcx: *tcx, axiomatize: opts.axiomatize, - file: opts.filename, + file, reorder_map: HashMap::new(), configuration: get_configuration(&opts.configuration_file), + supertraits: supertraits_map, }; let mut results: Vec = tcx.hir().items().collect(); @@ -918,7 +966,7 @@ fn compile_top_level(tcx: &TyCtxt, opts: TopLevelOptions) -> TopLevel { .iter() .flat_map(|item_id| { let item = tcx.hir().item(*item_id); - compile_top_level_item(tcx, &mut env, item) + compile_top_level_item(tcx, &mut env, item, path.clone()) }) .collect(), ); @@ -941,9 +989,10 @@ pub(crate) fn top_level_to_coq(tcx: &TyCtxt, opts: TopLevelOptions) -> String { axiomatize: opts.axiomatize || configuration.axiomatize, ..opts }; - let top_level = compile_top_level(tcx, opts); + let mut supertraits_map = HashMap::new(); + let top_level = compile_top_level(tcx, opts, &mut supertraits_map); let top_level = mt_top_level(top_level); - top_level.to_pretty(LINE_WIDTH) + top_level.to_pretty(LINE_WIDTH, &supertraits_map) } // additional check. can be eliminated when all possible cases will be covered @@ -1006,34 +1055,37 @@ impl FnSigAndBody { } } -fn mt_trait_item(body: TraitItem) -> TraitItem { - match body { - TraitItem::Definition { - ty_params, - where_predicates, - ty, - } => TraitItem::Definition { - ty_params, - where_predicates, - ty: mt_ty(ty), - }, - TraitItem::Type(x) => TraitItem::Type(x), // @TODO apply MT - TraitItem::DefinitionWithDefault { - ty_params, - where_predicates, - signature_and_body, - } => TraitItem::DefinitionWithDefault { - ty_params, - where_predicates, - signature_and_body: signature_and_body.mt(), - }, +impl TraitItem { + fn mt(&self) -> Self { + TraitItem { + item_name: self.item_name.to_owned(), + item_data: match self.item_data.to_owned() { + TraitItemData::Definition { + ty_params, + where_predicates, + ty, + } => TraitItemData::Definition { + ty_params, + where_predicates, + ty: mt_ty(ty), + }, + TraitItemData::Type(x) => TraitItemData::Type(x), // @TODO apply MT + TraitItemData::DefinitionWithDefault { + ty_params, + where_predicates, + signature_and_body, + } => TraitItemData::DefinitionWithDefault { + ty_params, + where_predicates, + signature_and_body: signature_and_body.mt(), + }, + }, + } } } -fn mt_trait_items(body: Vec<(String, TraitItem)>) -> Vec<(String, TraitItem)> { - body.into_iter() - .map(|(s, item)| (s, mt_trait_item(item))) - .collect() +fn mt_trait_items(body: Vec) -> Vec { + body.into_iter().map(|trait_item| trait_item.mt()).collect() } /// Monad transform for [TopLevelItem] @@ -1074,19 +1126,19 @@ fn mt_top_level_item(item: TopLevelItem) -> TopLevelItem { counter, items: mt_impl_items(items), }, - TopLevelItem::Trait { + TopLevelItem::Trait(Trait { name, ty_params, predicates, bounds, body, - } => TopLevelItem::Trait { + }) => TopLevelItem::Trait(Trait { name, ty_params, predicates, bounds, body: mt_trait_items(body), - }, + }), TopLevelItem::TraitImpl { generic_tys, ty_params, @@ -1548,7 +1600,7 @@ impl WherePredicate { impl TraitBound { /// Get the generics for the trait - fn compile(tcx: &TyCtxt, env: &Env, ptraitref: &rustc_hir::PolyTraitRef) -> TraitBound { + fn compile(tcx: &TyCtxt, env: &Env, ptraitref: &rustc_hir::PolyTraitRef) -> Self { TraitBound { name: compile_path(env, ptraitref.trait_ref.path), ty_params: get_ty_params_with_default_status( @@ -1575,21 +1627,7 @@ impl TraitBound { args: self .ty_params .iter() - .map(|ty_param| match *ty_param.to_owned() { - TraitTyParamValue::JustValue { name, ty } - | TraitTyParamValue::ValWithDef { name, ty } => { - (Some(name), ty.to_coq()) - } - TraitTyParamValue::JustDefault { name } => ( - Some(name.clone()), - coq::Expression::Code(concat([ - self.name.to_doc(), - text(".Default."), - text(name), - ])) - .apply(&coq::Expression::just_name("Self")), - ), - }) + .map(|ty_param| ty_param.to_coq_arg_value(&self.name)) .collect(), }, }, @@ -1598,6 +1636,23 @@ impl TraitBound { } } +impl TraitTyParamValue { + fn to_coq_arg_value<'a>(&self, bound_name: &Path) -> (Option, coq::Expression<'a>) { + match self { + TraitTyParamValue::JustValue { name, ty } + | TraitTyParamValue::ValWithDef { name, ty } => (Some(name.to_owned()), ty.to_coq()), + TraitTyParamValue::JustDefault { name } => ( + Some(name.clone()), + coq::Expression::single_var(&Path::concat(&[ + bound_name.to_owned(), + Path::new(&["Default", name]), + ])) + .apply(&coq::Expression::just_name("Self")), + ), + } + } +} + impl TraitTyParamValue { #[allow(dead_code)] // @TODO fn to_doc(&self) -> Doc { @@ -1611,7 +1666,6 @@ impl TraitTyParamValue { } } - #[allow(dead_code)] fn to_coq_type(&self) -> Box { match self { TraitTyParamValue::JustValue { name: _, ty } => ty.to_owned(), @@ -1621,13 +1675,14 @@ impl TraitTyParamValue { } } -struct ToDocContext<'a> { +struct ToDocContext<'a, 'b> { extra_data: Option<&'a TopLevelItem>, previous_module_names: Vec, + supertraits_map: &'b HashMap>, } impl TopLevelItem { - fn to_doc<'a>(&'a self, to_doc_context: ToDocContext<'a>) -> Doc { + fn to_doc<'a>(&'a self, to_doc_context: ToDocContext<'a, '_>) -> Doc { match self { TopLevelItem::Const { name, ty, value } => match value { None => coq::TopLevel::new(&[ @@ -1682,7 +1737,7 @@ impl TopLevelItem { vec![coq::TopLevelItem::Module(coq::Module::new_with_repeat( name, nb_previous_occurrences_of_module_name, - coq::TopLevel::new(&[coq::TopLevelItem::Code(body.to_doc())]), + coq::TopLevel::new(&[coq::TopLevelItem::Code(body.to_doc(to_doc_context.supertraits_map))]), ))], ] .concat(), @@ -1879,7 +1934,7 @@ impl TopLevelItem { no_implicit: false, } .apply(&coq::Expression::just_name(&i.to_string())), - &coq::Expression::Record { + &Some(coq::Expression::Record { fields: vec![coq::Field::new( &Path::new(&["Notation", "dot"]), &[coq::ArgDecl::new( @@ -1902,7 +1957,7 @@ impl TopLevelItem { )], &coq::Expression::just_name(&format!("x{i}")), )], - }, + }), vec![], )) }) @@ -1994,261 +2049,7 @@ impl TopLevelItem { ))]) .to_doc() } - TopLevelItem::Trait { - name, - ty_params, - predicates, - bounds, - body, - } => coq::TopLevelItem::trait_module( - name, - &ty_params - .iter() - .map(|(ty, default)| { - ( - ty.to_owned(), - default.as_ref().map(|default| default.to_coq()), - ) - }) - .collect::>(), - &predicates - .iter() - .map(|predicate| predicate.to_coq()) - .collect::>(), - &bounds - .iter() - .map(|bound| { - bound.to_coq( - coq::Expression::just_name("Self"), - coq::ArgSpecKind::Implicit, - ) - }) - .collect::>(), - &body.iter() - .map(|(name, item)| match item { - TraitItem::Definition { - ty_params, - where_predicates, - ty, - } => vec![coq::ClassFieldDef::new( - &Some(name.to_owned()), - &[ - vec![coq::ArgDecl::monadic_typeclass_parameter()], - if ty_params.is_empty() { - vec![] - } else { - vec![coq::ArgDecl::new( - &coq::ArgDeclVar::Simple { - idents: ty_params.to_owned(), - ty: Some(coq::Expression::Set), - }, - coq::ArgSpecKind::Implicit, - )] - }, - where_predicates - .iter() - .enumerate() - .map(|(i, predicate)| { - predicate.to_coq().add_var(&["H'".to_string(), i.to_string()].concat()) - }) - .collect(), - ] - .concat(), - &ty.to_coq(), - )], - TraitItem::DefinitionWithDefault { .. } => vec![], - TraitItem::Type(bounds) => [ - vec![coq::ClassFieldDef::new( - &Some(name.to_owned()), - &[], - &coq::Expression::Set, - )], - if bounds.is_empty() { - vec![] - } else { - vec![coq::ClassFieldDef::new( - &None, - &[], - &coq::Expression::SigmaType { - args: bounds - .iter() - .map(|bound| { - bound.to_coq( - coq::Expression::just_name(name), - coq::ArgSpecKind::Explicit, - ) - }) - .collect::>(), - image: Box::new(coq::Expression::Unit), - }, - )] - }, - ] - .concat(), - }) - .concat(), - &body.iter() - .map(|(name, item)| match item { - TraitItem::Definition { - ty_params, - where_predicates, - ty: _, - } => coq::Instance::new( - false, - &format!("Method_{name}"), - &[ - coq::ArgDecl::monadic_typeclass_parameter(), - coq::ArgDecl::new( - &coq::ArgDeclVar::Generalized { - idents: vec![], - ty: coq::Expression::just_name("Trait"), - }, - coq::ArgSpecKind::Explicit, - ), - ], - coq::Expression::Variable { - ident: Path::new(&["Notation", "Dot"]), - no_implicit: false, - } - .apply(&coq::Expression::String(name.to_owned())), - &coq::Expression::Record { - fields: vec![coq::Field::new( - &Path::new(&["Notation", "dot"]), - &[ - if ty_params.is_empty() { - vec![] - } else { - vec![coq::ArgDecl::of_ty_params(ty_params, coq::ArgSpecKind::Implicit)] - }, - where_predicates - .iter() - .enumerate() - .map(|(i, predicate)| { - predicate.to_coq().add_var(&["H'".to_string(), i.to_string()].concat()) - }) - .collect(), - ] - .concat(), - &coq::Expression::just_name(name) - .apply_many_args( - &ty_params - .iter() - .map(|ty_param| { - (Some(ty_param.to_owned()), coq::Expression::just_name(ty_param)) - }) - .collect::>(), - ) - .apply_many_args( - &where_predicates - .iter() - .enumerate() - .map(|(i, _)| { - let var_name = ["H'".to_string(), i.to_string()].concat(); - (Some(var_name.clone()), coq::Expression::just_name(&var_name)) - }) - .collect::>() - ), - )], - }, - vec![], - ), - TraitItem::Type { .. } => coq::Instance::new( - false, - &format!("Method_{name}"), - &[coq::ArgDecl::new( - &coq::ArgDeclVar::Generalized { - idents: vec![], - ty: coq::Expression::just_name("Trait"), - }, - coq::ArgSpecKind::Explicit, - )], - coq::Expression::Variable { - ident: Path::new(&["Notation", "DoubleColonType"]), - no_implicit: false, - } - .apply(&coq::Expression::just_name("Self")) - .apply(&coq::Expression::String(name.to_owned())), - &coq::Expression::Record { - fields: vec![coq::Field::new( - &Path::new(&["Notation", "double_colon_type"]), - &[], - &coq::Expression::just_name(name), - )], - }, - vec![], - ), - TraitItem::DefinitionWithDefault { - ty_params, - where_predicates, - signature_and_body, - } => coq::Instance::new( - false, - &format!("Method_{name}"), - &[ - coq::ArgDecl::monadic_typeclass_parameter(), - coq::ArgDecl::new( - &coq::ArgDeclVar::Generalized { - idents: vec![], - ty: coq::Expression::just_name("Trait"), - }, - coq::ArgSpecKind::Explicit, - ), - ], - coq::Expression::Variable { - ident: Path::new(&["Notation", "Dot"]), - no_implicit: false, - } - .apply(&coq::Expression::String(name.to_owned())), - &coq::Expression::Record { - fields: vec![coq::Field::new( - &Path::new(&["Notation", "dot"]), - &[ - if ty_params.is_empty() { - vec![] - } else { - vec![coq::ArgDecl::of_ty_params(ty_params, coq::ArgSpecKind::Implicit)] - }, - where_predicates - .iter() - .map(|predicate| predicate.to_coq()) - .collect(), - signature_and_body - .args - .iter() - .map(|(name, ty)| { - coq::ArgDecl::new( - &coq::ArgDeclVar::Simple { - idents: vec![name.to_owned()], - ty: Some(ty.to_coq()), - }, - coq::ArgSpecKind::Explicit, - ) - }) - .collect::>(), - ] - .concat(), - &coq::Expression::Code(group([ - text("("), - match &signature_and_body.body { - None => text("axiom"), - Some(body) => body.to_doc(false), - }, - line(), - nest([ - text(":"), - line(), - signature_and_body.ret_ty.to_doc(false), - text(")"), - ]), - ])), - )], - }, - vec![], - ), - }) - .collect::>(), - ) - .to_doc(), + TopLevelItem::Trait(tr) => tr.to_doc(to_doc_context.supertraits_map), TopLevelItem::TraitImpl { generic_tys, ty_params, @@ -2318,7 +2119,7 @@ impl TopLevelItem { }) .collect::>(), ), - &if items.is_empty() { + &Some(if items.is_empty() { coq::Expression::Variable { ident: Path::concat(&[ of_trait.to_owned(), @@ -2344,7 +2145,7 @@ impl TopLevelItem { }) .collect::>(), } - }, + }), if *has_predicates_on_assoc_ty { vec![text("eauto.")] } else { @@ -2454,7 +2255,7 @@ impl TypeStructStruct { no_implicit: false, } .apply(&coq::Expression::just_name("t")), - &coq::Expression::just_name("axiom"), + &Some(coq::Expression::just_name("axiom")), vec![], ), ) @@ -2583,7 +2384,7 @@ impl TypeStructStruct { .apply(&coq::Expression::String( name.to_owned(), )), - &coq::Expression::Record { + &Some(coq::Expression::Record { fields: vec![coq::Field::new( &Path::new(&["Notation", "dot"]), &projection_pattern, @@ -2591,7 +2392,7 @@ impl TypeStructStruct { "x{i}" )), )], - }, + }), vec![], )), coq::TopLevelItem::Instance(coq::Instance::new( @@ -2609,7 +2410,7 @@ impl TypeStructStruct { coq::Expression::just_name("t"), coq::Expression::String(name.to_owned()), ]), - &coq::Expression::Record { + &Some(coq::Expression::Record { fields: vec![coq::Field::new( &Path::new(&[ "Notation", @@ -2620,7 +2421,7 @@ impl TypeStructStruct { "x{i}" )), )], - }, + }), vec![], )), ] @@ -2674,6 +2475,486 @@ impl TypeStructStruct { } } +impl Trait { + fn to_doc(&self, _supertraits_map: &HashMap>) -> Doc { + let Trait { + name, + ty_params, + predicates, + bounds, + body, + } = self; + + let items = &body + .iter() + .map(|item| match &item.item_data { + TraitItemData::Definition { + ty_params, + where_predicates, + ty, + } => vec![coq::ClassFieldDef::new( + &Some(item.item_name.to_owned()), + &[ + vec![coq::ArgDecl::monadic_typeclass_parameter()], + if ty_params.is_empty() { + vec![] + } else { + vec![coq::ArgDecl::new( + &coq::ArgDeclVar::Simple { + idents: ty_params.to_owned(), + ty: Some(coq::Expression::Set), + }, + coq::ArgSpecKind::Implicit, + )] + }, + where_predicates + .iter() + .enumerate() + .map(|(i, predicate)| { + predicate + .to_coq() + .add_var(&["H'".to_string(), i.to_string()].concat()) + }) + .collect(), + ] + .concat(), + &ty.to_coq(), + )], + TraitItemData::DefinitionWithDefault { .. } => vec![], + TraitItemData::Type(bounds) => [ + vec![coq::ClassFieldDef::new( + &Some(item.item_name.to_owned()), + &[], + &coq::Expression::Set, + )], + if bounds.is_empty() { + vec![] + } else { + vec![coq::ClassFieldDef::new( + &Some(["__the_bounds_of_", &item.item_name].concat()), + &[], + &coq::Expression::SigmaType { + args: bounds + .iter() + .map(|bound| { + bound.to_coq( + coq::Expression::just_name(&item.item_name), + coq::ArgSpecKind::Explicit, + ) + }) + .collect::>(), + image: Box::new(coq::Expression::Unit), + }, + )] + }, + ] + .concat(), + }) + .concat(); + + coq::TopLevelItem::Module(coq::Module::new( + name, + coq::TopLevel::concat(&[ + coq::TopLevel::locally_unset_primitive_projections_if( + items.is_empty(), + &[coq::TopLevelItem::Class(coq::Class::new( + "Trait", + &[ + vec![coq::ArgDecl::new( + &coq::ArgDeclVar::Simple { + idents: vec!["Self".to_string()], + ty: Some(coq::Expression::Set), + }, + coq::ArgSpecKind::Explicit, + )], + bounds + .iter() + .map(|bound| { + bound.to_coq( + coq::Expression::just_name("Self"), + coq::ArgSpecKind::Implicit, + ) + }) + .collect(), + if ty_params.is_empty() { + vec![] + } else { + vec![coq::ArgDecl::new( + &coq::ArgDeclVar::Simple { + idents: ty_params + .iter() + .map(|(ty, default)| { + match default { + // @TODO: implement the translation of type parameters with default + Some(_default) => ["(* TODO *) ", ty].concat(), + None => ty.to_string(), + } + }) + .collect(), + ty: Some(coq::Expression::Set), + }, + coq::ArgSpecKind::Implicit, + )] + }, + predicates + .iter() + .map(|predicate| predicate.to_coq()) + .collect(), + ] + .concat(), + items, + ))], + ), + coq::TopLevel::new( + &body + .iter() + .map(|item| match &item.item_data { + TraitItemData::Definition { + ty_params, + where_predicates, + ty: _, + } => coq::Instance::new( + false, + &["Method_", &item.item_name].concat(), + &[ + coq::ArgDecl::monadic_typeclass_parameter(), + coq::ArgDecl::new( + &coq::ArgDeclVar::Generalized { + idents: vec![], + ty: coq::Expression::just_name("Trait"), + }, + coq::ArgSpecKind::Explicit, + ), + ], + coq::Expression::Variable { + ident: Path::new(&["Notation", "Dot"]), + no_implicit: false, + } + .apply(&coq::Expression::String(item.item_name.to_owned())), + &Some(coq::Expression::Record { + fields: vec![coq::Field::new( + &Path::new(&["Notation", "dot"]), + &[ + if ty_params.is_empty() { + vec![] + } else { + vec![coq::ArgDecl::of_ty_params( + ty_params, + coq::ArgSpecKind::Implicit, + )] + }, + where_predicates + .iter() + .enumerate() + .map(|(i, predicate)| { + predicate.to_coq().add_var( + &["H'".to_string(), i.to_string()].concat(), + ) + }) + .collect(), + ] + .concat(), + &coq::Expression::just_name(&item.item_name) + .apply_many_args( + &ty_params + .iter() + .map(|ty_param| { + ( + Some(ty_param.to_owned()), + coq::Expression::just_name(ty_param), + ) + }) + .collect::>(), + ) + .apply_many_args( + &where_predicates + .iter() + .enumerate() + .map(|(i, _)| { + let var_name = + ["H'".to_string(), i.to_string()] + .concat(); + ( + Some(var_name.clone()), + coq::Expression::just_name(&var_name), + ) + }) + .collect::>(), + ), + )], + }), + vec![], + ), + TraitItemData::Type { .. } => coq::Instance::new( + false, + &["Method_", &item.item_name].concat(), + &[coq::ArgDecl::new( + &coq::ArgDeclVar::Generalized { + idents: vec![], + ty: coq::Expression::just_name("Trait"), + }, + coq::ArgSpecKind::Explicit, + )], + coq::Expression::Variable { + ident: Path::new(&["Notation", "DoubleColonType"]), + no_implicit: false, + } + .apply(&coq::Expression::just_name("Self")) + .apply(&coq::Expression::String(item.item_name.to_owned())), + &Some(coq::Expression::Record { + fields: vec![coq::Field::new( + &Path::new(&["Notation", "double_colon_type"]), + &[], + &coq::Expression::just_name(&item.item_name), + )], + }), + vec![], + ), + TraitItemData::DefinitionWithDefault { + ty_params, + where_predicates, + signature_and_body, + } => coq::Instance::new( + false, + &["Method_", &item.item_name].concat(), + &[ + coq::ArgDecl::monadic_typeclass_parameter(), + coq::ArgDecl::new( + &coq::ArgDeclVar::Generalized { + idents: vec![], + ty: coq::Expression::just_name("Trait"), + }, + coq::ArgSpecKind::Explicit, + ), + ], + coq::Expression::Variable { + ident: Path::new(&["Notation", "Dot"]), + no_implicit: false, + } + .apply(&coq::Expression::String(item.item_name.to_owned())), + &Some(coq::Expression::Record { + fields: vec![coq::Field::new( + &Path::new(&["Notation", "dot"]), + &[ + if ty_params.is_empty() { + vec![] + } else { + vec![coq::ArgDecl::of_ty_params( + ty_params, + coq::ArgSpecKind::Implicit, + )] + }, + where_predicates + .iter() + .map(|predicate| predicate.to_coq()) + .collect(), + signature_and_body + .args + .iter() + .map(|(name, ty)| { + coq::ArgDecl::new( + &coq::ArgDeclVar::Simple { + idents: vec![name.to_owned()], + ty: Some(ty.to_coq()), + }, + coq::ArgSpecKind::Explicit, + ) + }) + .collect::>(), + ] + .concat(), + &coq::Expression::Code(group([ + text("("), + match &signature_and_body.body { + None => text("axiom"), + Some(body) => body.to_doc(false), + }, + line(), + nest([ + text(":"), + line(), + signature_and_body.ret_ty.to_doc(false), + text(")"), + ]), + ])), + )], + }), + vec![], + ), + }) + .map(|i| coq::TopLevelItem::Instance(i.to_owned())) + .collect_vec(), + ), + // extraction of the trait instances + coq::TopLevel::new( + &body + .iter() + .filter_map(|item| match &item.item_data { + TraitItemData::Definition { .. } + | TraitItemData::DefinitionWithDefault { .. } => None, + TraitItemData::Type(bounds) => { + if bounds.is_empty() { + None + } else { + let proj_name = [ + "__the_bounds_of_", + &item.item_name, + "0", + ] + .concat(); + Some(coq::TopLevelItem::Module(coq::Module::new( + &[ + "The_Bounds_Of_", + &item.item_name, + ] + .concat(), + coq::TopLevel::new( + &bounds + .iter() + .map(|bound| { + let local_trait_name = "_Tr"; + let item_for_the_trait = coq::Expression::just_name( + &item.item_name + ) + .apply_arg( + &Some("Trait".to_string()), + &coq::Expression::just_name(local_trait_name), + ); + coq::TopLevelItem::Module(coq::Module::new( + &bound.name.to_name(), + coq::TopLevel::new(&[ + coq::TopLevelItem::Instance(coq::Instance::new( + false, + "I", + &[coq::ArgDecl::new( + &coq::ArgDeclVar::Generalized { + idents: vec!["_Tr".to_string()], + ty: coq::Expression::just_name("Trait"), + }, + coq::ArgSpecKind::Explicit, + )], + coq::Expression::Code(nest([ + text("ltac:"), + round_brackets(group([ + group([ + text("unshelve"), + line(), + text("eapply"), + line(), + coq::Expression::Variable { + ident: Path::concat(&[ + bound.name.to_owned(), + Path::new(&["Trait"]), + ]), + no_implicit: false, + } + .apply( + &item_for_the_trait, + ) + .apply_many_args( + &bound.ty_params + .iter() + .map(|ty_param| { + ty_param.to_coq_arg_value(&bound.name) + }) + .collect_vec(), + ) + .to_doc(true), + text(";"), + ]), + line(), + text("compute;"), + line(), + group([ + text("destruct"), + line(), + text("_Tr"), + text(";"), + ]), + line(), + nest([ + text("repeat"), + line(), + group([ + group([ + text("destruct"), + line(), + text(proj_name.clone()), + line(), + text("as"), + line(), + square_brackets(nest([ + text("?"), + line(), + text(proj_name.clone()), + ])), + text(";"), + ]), + line(), + group([ + text("try"), + line(), + text("assumption"), + ]), + ]), + ]), + ])), + ])), + &None, + { + vec![nest([ + text("all:"), + line(), + group([ + text("compute;"), + line(), + text("destruct _Tr;"), + line(), + nest([ + text("repeat"), + line(), + round_brackets(group([ + text("destruct"), + line(), + text(proj_name.clone()), + line(), + text("as"), + line(), + square_brackets(nest([ + text("?"), + line(), + text(proj_name.clone()), + ])), + ])), + ]), + text(";"), + line(), + text("assumption"), + ]), + text("."), + ])] + }, + )), + ]), + )) + }) + .collect_vec(), + ), + ))) + } + }, + }) + .collect_vec(), + ), + ]), + )) + .to_doc() + } +} + +// @TODO +//fn collect_supertraits_in_order + impl TopLevel { // function returns TopLevelItem::TypeStructStruct (comparing name) fn find_tli_by_name(&self, self_ty: &CoqType) -> Option<&TopLevelItem> { @@ -2692,7 +2973,7 @@ impl TopLevel { }) } - fn to_doc(&self) -> Doc { + fn to_doc(&self, supertraits_map: &HashMap>) -> Doc { // check if there is a Debug Trait implementation in the code (#[derive(Debug)]) // for a TopLevelItem::TypeStructStruct (@TODO extend to cover more cases) // if "yes" - get both TopLevelItems (Struct itself and TraitImpl for it) @@ -2739,6 +3020,7 @@ impl TopLevel { let to_doc_context = ToDocContext { extra_data, previous_module_names: previous_module_names.clone(), + supertraits_map, }; let doc = item.to_doc(to_doc_context); if let TopLevelItem::Module { name, .. } = item { @@ -2750,9 +3032,13 @@ impl TopLevel { ) } - pub fn to_pretty(&self, width: usize) -> String { + pub fn to_pretty( + &self, + width: usize, + supertraits_map: &HashMap>, + ) -> String { let mut w = Vec::new(); - self.to_doc().render(width, &mut w).unwrap(); + self.to_doc(supertraits_map).render(width, &mut w).unwrap(); format!("{}{}\n", HEADER, String::from_utf8(w).unwrap()) } } diff --git a/tmp/experiment.v b/tmp/experiment.v new file mode 100644 index 000000000..5c8c34cdf --- /dev/null +++ b/tmp/experiment.v @@ -0,0 +1,175 @@ +Notation "'Sigma' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) + (at level 200, x binder, right associativity, + format "'[' 'Sigma' '/ ' x .. y , '/ ' p ']'") + : type_scope. + + +Class supersuperclass (Self : Set) : Type := {}. +Class superclass (Self : Set) `{supersuperclass Self} : Type := { + some_other_ty : Set; + some_other_field : some_other_ty; +}. +Class class (Self : Set) `{superclass Self} : Type := { + some_ty : Set; + some_field : some_ty; +}. + +Class assoc_ty_class (Self : Set) : Type := { + ty : Set; + __ty_bound : Sigma `(class ty), unit; +}. +Compute ty. + +Definition Ty'' `(assoc_ty_class) : Type. + unshelve eapply class; try exact (ty (assoc_ty_class := H)); compute; destruct H as [ty __ty_bound']; +repeat (destruct __ty_bound' as [? __ty_bound']; try assumption). +Defined. +Print Ty''. + +Definition I'' `{H : assoc_ty_class} : Ty'' H. +compute in *. + destruct H as [ty __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + exact x1. +Defined. +Parameter IC' : forall Self `(superclass Self), class Self. +Global Existing Instance IC'. + +Section Sec. + Parameter Self : Set. + Parameter I''' : forall `{superclass Self}, class Self. + Global Instance I'''' `(superclass Self) : class Self := I'''. +End Sec. + +Parameter function : forall (T : Set) `{C : class T}, Set. + +Global Instance I''''' Self `(H : class Self) : class Self := H. + +Module Sec'. +Section Sec'. +Context (Self : Set). +Context `(H : class Self). +Global Instance I'''''' : class Self := H. +End Sec'. +End Sec'. + +Ltac t n := exact n. +Check ltac:(t tt). + +Print Instances class. +Global Hint Resolve I'' : typeclass_instances. + +Ltac t' H := unshelve eapply class; try exact (ty (assoc_ty_class := H)); compute; destruct H as [ty __ty_bound']; +repeat (destruct __ty_bound' as [? __ty_bound']; try assumption). + +Check fun `(H : assoc_ty_class) => ltac:(t' H). +Global Instance II `(H : assoc_ty_class) : ltac:(t' H) := I''. +Global Hint Resolve II : typeclass_instances. +Print II. +Check II ?[H] : class ty. +Print function. + +Print Instances class. + +Section s. +Context `(H : assoc_ty_class). + +Definition T : Set := ty. +Global Instance GI : ltac:(unshelve eapply class; try exact (ty (assoc_ty_class := H)); compute; destruct H; +repeat (destruct __ty_bound0 as [? __ty_bound0]; try assumption)). +compute. destruct H. +repeat (destruct __ty_bound0 as [? __ty_bound0]). assumption. +Defined. +Print GI. + +Parameter f : forall x `{class x}, Set. +(* Parameter x : f T. *) + +Print Instances superclass. +End s. + +(* Definition T : Set := ty. *) + +(* I'm trying to make this work v *) +(* ____________________| *) +(* vvv *) +Parameter obj : forall `{H : assoc_ty_class}, function (ty (assoc_ty_class := H)). + +Section X. +Context `(H : assoc_ty_class). +Definition S : Type. + destruct H as [ty __ty_bound]. + repeat + (destruct __ty_bound as [? __ty_bound]; + try apply (class ty)). +Defined. +Compute S. + +Definition S' : Sigma T : Type, T. + destruct H as [ty __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + destruct __ty_bound' as [? __ty_bound']. + eapply existT. + exact x1. +Defined. + +(* Global Instance I : S. + *) +Compute S'. +Compute projT2 S'. +Compute projT1 S'. +End X. +Compute fun `(H : assoc_ty_class) => (fun '({| ty := x; __ty_bound := y |}) => projT1 (S' {| ty := x; __ty_bound := y |})) H. +Compute fun '({| ty := x; __ty_bound := y |}) => projT1 (S' {| ty := x; __ty_bound := y |}). +Compute fun `(H : assoc_ty_class) => projT1 (S' H). + +Check fun '({| ty := x; __ty_bound := y |}) => {| ty := x; __ty_bound := y |}. +Compute (fun `(H : assoc_ty_class) => let '{| ty := x; __ty_bound := y |} := H in + (projT2 (S' {| ty := x; __ty_bound := y |}) : projT1 (S' {| ty := x; __ty_bound := y |}))) + : forall `(H : assoc_ty_class), let '{| ty := x; __ty_bound := y |} := H in projT1 (S' {| ty := x; __ty_bound := y |}). +Compute fun `(H : assoc_ty_class) => projT2 (S' H). + +Definition Ty `(H : assoc_ty_class) : Type. + unshelve eapply function. + - exact ty. + - destruct H. now compute. + - destruct H. now compute. + - destruct H. now compute. +Defined. +Compute Ty. + +Definition Ty' `(H : assoc_ty_class) : Type. + unshelve eapply (another_class ty). + - exact Self. + - easy. + - easy. + - easy. + - easy. +Defined. +Print Ty'. + +(* apply (fun `(H : assoc_ty_class) (x : forall (T : Set) `(H : assoc_ty_class), Type) => forall (T : Set) `(H : assoc_ty_class), x T H) with Self. +Defined. *) + +Parameter object' : forall (T : Set) `(H : assoc_ty_class), Ty H. +Compute object'. + +Definition I' `(H : assoc_ty_class) : Ty' H. + easy. +Defined. + +Parameter object : forall (T : Set) `(H : assoc_ty_class), + let '{| ty := x; __ty_bound := y |} := H in function ty (C := projT2 (S' {| ty := x; __ty_bound := y |})). + +(* Goal forall `(H : assoc_ty_class), let '{| ty := x; __ty_bound := y |} := H in projT1 (S' H) = class x. *) +(* intros. compute. destruct H. destruct __ty_bound0. destruct s. destruct s. *) +Parameter object : forall '({| ty := x; __ty_bound := y |}), function x (C := projT2 (S' {| ty := x; __ty_bound := y |})). + +Check fun '({| ty := x; __ty_bound := y |}) => {| ty := x; __ty_bound := y |}. +Compute fun '({| ty := x; __ty_bound := y |}) => (projT2 (S' {| ty := x; __ty_bound := y |}) : projT1 (S' {| ty := x; __ty_bound := y |})). +Compute fun `(H : assoc_ty_class) => projT2 (S' H). + +Parameter object : forall (T : Set) '({| ty := x; __ty_bound := y |}), function ty (C := projT1 (projT2 (S' {| ty := x; __ty_bound := y |}))).