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.

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

Struct objects #150

Merged
merged 12 commits into from
Oct 9, 2024
Merged

Struct objects #150

merged 12 commits into from
Oct 9, 2024

Conversation

ACassimiro
Copy link
Collaborator

Introducing struct creation and usage. Structs can be created with or without its inner variable assignments. For example:

struct Pair{i: u32, j: u32 }
[...]
//Within a function
let _pair = ::structs::Pair {
     i: 1_u32,
     j: 2_u32
};
// or
let _pair = ::structs::Pair {
     1_u32,
     2_u32
};

@@ -540,7 +545,12 @@ https://doc.rust-lang.org/reference/items/extern-crates.html

```k

syntax StructExpression ::= "TODO: not needed yet, not implementing"
syntax StructExpression ::= TypePath "{" StructFieldsExpression "}"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This does not follow the Rust reference (see the link at line 544). We should not follow it precisely when it helps us, but could you document the changes (a TODO would probably be enough)? Also, whenever possible, could you try to preserve the sort names in the Rust reference?

Some more precise questions:

  1. Why did you use a TypePath instead of a PathInExpression here? If a TypePath is easier to implement, it's probably fine, since we don't plan to use generics in this way.
  2. Does the LiteralExpressionList thing below actually work in Rust? By looking at this page, I'm not sure how: https://doc.rust-lang.org/reference/expressions/struct-expr.html . If it does not work in Rust, do we need it?
  3. Does it help if you use LiteralExpression in StructExprField / StructFieldAssignment instead of Expression? The same question for LiteralExpressionList - you may be able to use TupleElementsNoEndComma here, which can be transformed to ExpressionList. I'm asking this because, if you use Expression/ExpressionList instead, you may have easier ways to evaluate expressions.

Copy link
Collaborator Author

@ACassimiro ACassimiro Oct 8, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. For the TypePath, I'm having issues converting a PathExpression into a TypePath, so I decided to use it directly in the construction. If you think the effort is valid, I can take some time to continue digging into it.
  2. and 3. In the first implementation, I focused on implementing a syntax that would work for the specific case I was trying to handle on our tests. I ended up not correcting the syntax once the test was correctly executed, so I reimplemented the syntax to become closer to the reference implementation. Please notice that, even in this updated syntax, a few of the approaches that we use to initialize structs are not yet supported, and we're using a TypePath where a PathInExpression should be.

rust-semantics/expression/struct.md Show resolved Hide resolved
<struct multiplicity="*" type="Map">
<struct-path> my_identifier:TypePath </struct-path>
<variable-list> .List </variable-list> // List of Identifier
<variables>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s/variable/field/, perhaps?

</variable>
...
</variables>
</struct> [owise]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this an owise rule?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Testing it without the [owise] always caused tests to reach a stuck state. My understanding is that there is a certain degree of ambiguity between this rule and the rule right below it, and when the second one should be applied to finish the parsing of the struct declaration, it would apply the first, leading the K cell to a state where it could not be rewritten further.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, now I understand what happens... I was misreading the rule below. You may try to replace it with

rule structParser(_Name:TypePath, .StructFields) => .K

and then you will probably not need an owise rule here.

@@ -195,7 +195,12 @@ https://doc.rust-lang.org/reference/items/extern-crates.html

```k

syntax Struct ::= "TODO: not needed yet, not implementing"
syntax Structs ::= List{Struct, ""}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you need the "Structs" sort?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've just noticed it is not necessary. Will remove it.

syntax Structs ::= List{Struct, ""}
syntax Struct ::= StructStruct | TupleStruct
syntax TupleStruct ::= "TODO: not needed yet, not implementing"
syntax StructStruct ::= "struct" Identifier MaybeGenericParams "{" StructFields "}"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you either match the reference, or add some TODOs where the implementation is different? Here you're missing WhereClause?, which is fine since we don't need it. Something similar applies to "StructField" below.

</variable>
...
</variables>
</struct> [owise]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, now I understand what happens... I was misreading the rule below. You may try to replace it with

rule structParser(_Name:TypePath, .StructFields) => .K

and then you will probably not need an owise rule here.

rule <k> struct(P, Fields) => ptrValue(null, struct(P, Fields)) ... </k>

// KItems for breaking down struct expressions into the adequate format struct(P, F)
syntax KItem ::= fromStructExpressionWithLiteralsBuildFieldsMap(TypePath, StructBases, List, Map)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably it's a good idea to not implement this, since we are short on time, but, for the future, probably the better way of implementing this is something like this:

syntax KItem ::= fromStructExpressionWithLiteralsBuildFieldsMap(TypePath, StructBases, List)  [strict(2), result(ValueWithPtr)]

rule isValueWithPtr(.StructBases) => true
rule isValueWithPtr(E:Expression Es:StructBases) => isValueWithPtr(E) andBool isValueWithPtr(Es)

rule E:Expression Es:StructBases => E ~> E Es  [heat, result(ValueWithPtr)]
rule E:Expression ~> _:Expression Es:StructBases => E Es  [cool, result(ValueWithPtr)]

rule E:Expression Es:StructBases => Es ~> E Es requires isValueWithPtr(E)  [heat, result(ValueWithPtr)]
rule Es:StructBases ~> E:Expression _:StructBases => E Es requires isValueWithPtr(E)  [cool, result(ValueWithPtr)]

rule fromStructExpressionWithLiteralsBuildFieldsMap(I, RL, FieldNameList) => almostAStruct(I, pairFieldsWithValues(RL, FieldNameList, .Map))
rule almostAStruct(I, M:Map) => struct(I, M)

syntax MapOrError ::= pairFieldsWithValues(StructBases, List, .Map)  [function, total]
rule pairFieldsWithValues(.StructBases, .List, M:Map) => M
rule pairFieldsWithValues(???) => ???
...

Something similar applies to fromStructExpressionWithAssignmentsBuildFieldsMap.

syntax StructExprStruct ::= TypePath "{" MaybeStructExprFieldsOrStructBase "}" //TODO: Not implemented properly
//Should use PathInExpression instead of
//TypePath.
syntax MaybeStructExprFieldsOrStructBase ::= "" | StructExprFields | StructBases
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that there is at most one StructBase here. It's fine to keep it as-is, but add a "//TODO: Not implemented properly". I think that you can also have StructExprFields , StructBase and StructExprFields , here. Again, we don't need them, but you should add the TODO. Also, StructBase below is actually ".. Expression". You should probably not change it, but you should add a TODO.

@ACassimiro ACassimiro merged commit 3e4b57e into main Oct 9, 2024
3 checks passed
@ACassimiro ACassimiro deleted the struct-objects branch October 9, 2024 15:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants