Skip to content

Check parameters on attributes#3579

Merged
rv-jenkins merged 10 commits intodevelopfrom
checkAttParams
Aug 17, 2023
Merged

Check parameters on attributes#3579
rv-jenkins merged 10 commits intodevelopfrom
checkAttParams

Conversation

@gtrepta
Copy link
Copy Markdown
Contributor

@gtrepta gtrepta commented Aug 15, 2023

Makes progress on #3481

@gtrepta gtrepta marked this pull request as ready for review August 15, 2023 23:04
Copy link
Copy Markdown
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

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

One minor comment.
You can automerge once you fix that.

Comment thread kore/src/main/scala/org/kframework/attributes/Att.scala Outdated
Copy link
Copy Markdown
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

Looks good but I see a couple things that look like they might be copy paste errors and I just want to clarify.

Comment thread kore/src/main/scala/org/kframework/attributes/Att.scala
Comment thread kore/src/main/scala/org/kframework/attributes/Att.scala Outdated
final val KORE = Key("kore", KeyType.BuiltIn, KeyParameter.Forbidden)
final val LABEL = Key("label", KeyType.BuiltIn, KeyParameter.Required)
final val LATEX = Key("latex", KeyType.BuiltIn, KeyParameter.Required)
final val LEFT = Key("left", KeyType.BuiltIn, KeyParameter.Optional)
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

This one is forbidden, right?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Thank you for bringing these up, I forgot about them. I set some of these to Optional because they were being generated by the compiler in a way that deviates from our discussions. For the left/right attributes, ModuleToKORE is making them with values:

att = att.add(Att.LEFT(), KList.class, getAssoc(module.leftAssoc(), prod.klabel().get()));
att = att.add(Att.RIGHT(), KList.class, getAssoc(module.rightAssoc(), prod.klabel().get()));

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

These were introduced by #1287.

Comment thread kore/src/main/scala/org/kframework/attributes/Att.scala Outdated
final val PUBLIC = Key("public", KeyType.BuiltIn, KeyParameter.Forbidden)
final val RESULT = Key("result", KeyType.BuiltIn, KeyParameter.Required)
final val RETURNS_UNIT = Key("returnsUnit", KeyType.BuiltIn, KeyParameter.Forbidden)
final val RIGHT = Key("right", KeyType.BuiltIn, KeyParameter.Optional)
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Same here?

@gtrepta
Copy link
Copy Markdown
Contributor Author

gtrepta commented Aug 16, 2023

@dwightguth If I can determine that the compiler is not using the values in the compiler generated attributes that forbid parameters, I can just remove the parameters and change the restrictions in Att appropriately. Does this sound good?

Addressing these will probably require separate issues for them.

@gtrepta gtrepta requested a review from dwightguth August 16, 2023 17:12
@rv-jenkins rv-jenkins merged commit 43f8e3a into develop Aug 17, 2023
@rv-jenkins rv-jenkins deleted the checkAttParams branch August 17, 2023 12:29
@Baltoli Baltoli mentioned this pull request Dec 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants