Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Draft: experiments on traits #229

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

Draft: experiments on traits #229

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

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 48 additions & 5 deletions CoqOfRust/ink/ink_env.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,22 @@ Module types.
End CodecAsType.

Module Environment.
Print parity_scale_codec.codec.Codec.Trait.

Class Boxed_Codec (Self : Set) : Type := {
Encode :: parity_scale_codec.codec.Encode.Trait Self;
Decode :: parity_scale_codec.codec.Decode.Trait Self;
Main :: parity_scale_codec.codec.Codec.Trait Self;
}.

Global Instance Boxed_Codec_from_Codec (Self : Set)
`{parity_scale_codec.codec.Codec.Trait Self} :
Boxed_Codec Self := {
Encode := _;
Decode := _;
Main := _;
}.

Class Trait (Self : Set) : Type := {
MAX_EVENT_TOPICS `{H' : State.Trait} : usize;
AccountId : Set;
Expand All @@ -156,6 +172,7 @@ Module types.
`(core.convert.AsRef.Trait AccountId (T := Slice u8))
`(core.convert.AsMut.Trait AccountId (T := Slice u8)),
unit;
AccountId_is_Codec :: Boxed_Codec AccountId;
Balance : Set;
_
:
Expand Down Expand Up @@ -216,15 +233,27 @@ Module types.
unit;
ChainExtension : Set;
}.

Definition fn_requiring_encode (T : Set)
`{parity_scale_codec.codec.Encode.Trait T} :
unit :=
tt.

Global Instance Method_AccountId `(Trait)
: Notation.DoubleColonType Self "AccountId" := {
Notation.double_colon_type := AccountId;
}.

Definition calling_fn (Env : Set) `{Trait Env} : unit :=
fn_requiring_encode (Env::type["AccountId"]).

Set Printing All.
Print calling_fn.

Global Instance Method_MAX_EVENT_TOPICS `{H' : State.Trait} `(Trait)
: Notation.Dot "MAX_EVENT_TOPICS" := {
Notation.dot := MAX_EVENT_TOPICS;
}.
Global Instance Method_AccountId `(Trait)
: Notation.DoubleColonType Self "AccountId" := {
Notation.double_colon_type := AccountId;
}.
Global Instance Method_Balance `(Trait)
: Notation.DoubleColonType Self "Balance" := {
Notation.double_colon_type := Balance;
Expand Down Expand Up @@ -449,7 +478,21 @@ Module contract.
Notation.double_colon_type := Env;
}.
End ContractEnv.


Print ContractEnv.Trait.

Module ContractEnvBis.
Class Trait (Self : Set) : Type := {
Env : Set;
Environment_for_Env :: ink_env.types.Environment.Trait Env;
}.

Global Instance Method_Env `(Trait)
: Notation.DoubleColonType Self "Env" := {
Notation.double_colon_type := Env;
}.
End ContractEnvBis.

Module ContractReference.
Class Trait (Self : Set) : Type := {
Type_ : Set;
Expand Down
Loading