-
Notifications
You must be signed in to change notification settings - Fork 42
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
Preserve clause ordering of requires
and ensures
when internalisig rules in booster
#4037
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One detail:
I suggest to remove all old code related to aliases for rule LHSs (and probably all code about aliases in general)- in a follow-up PR. #3775 states that aliases were only used for rule LHSs, and they were removed from the front-end a while back
, ensures = rhs.constraints | ||
{ lhs | ||
, rhs | ||
, requires = mempty |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we are somehow losing the requires
clause on the track here ... but this whole function should be dead code anyway so we'd rather remove the alias
business altogether than fix this.
// rule `<generatedTop>`(`<T>`(`<k>`(inj{Pgm,KItem}(`int_;__IMP-SYNTAX_Pgm_Ids_Stmt`(`_,__IMP-SYNTAX_Ids_Id_Ids`(X,Xs),_Gen0))),`<state>`(`_Map_`(Rho,`.Map`(.KList)))),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{Pgm,KItem}(`int_;__IMP-SYNTAX_Pgm_Ids_Stmt`(Xs,_Gen0))),`<state>`(`_Map_`(Rho,`_|->_`(inj{Id,KItem}(X),inj{Int,KItem}(#token("0","Int")))))),_DotVar0) requires `notBool_`(`Set:in`(inj{Id,KItem}(X),`keys(_)_MAP_Set_Map`(Rho))) ensures #token("true","Bool") [UNIQUE_ID(8a8d39fed34974de05d217d0c7014950a846aae159a11794bd36c81db4b3ede1), org.kframework.attributes.Location(Location(206,8,207,38)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/playground/imp/imp.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] | ||
alias rule66LHS{}(SortMap{},SortId{},SortIds{},SortGeneratedCounterCell{},SortStmt{}) : SortGeneratedTopCell{} | ||
where rule66LHS{}(VarRho:SortMap{},VarX:SortId{},VarXs:SortIds{},Var'Unds'DotVar0:SortGeneratedCounterCell{},Var'Unds'Gen0:SortStmt{}) := | ||
\and{SortGeneratedTopCell{}} ( | ||
\equals{SortBool{},SortGeneratedTopCell{}}( | ||
LblnotBool'Unds'{}(LblSet'Coln'in{}(inj{SortId{}, SortKItem{}}(VarX:SortId{}),Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(VarRho:SortMap{}))), | ||
\dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblint'UndsSClnUndsUnds'IMP-SYNTAX'Unds'Pgm'Unds'Ids'Unds'Stmt{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}(VarX:SortId{},VarXs:SortIds{}),Var'Unds'Gen0:SortStmt{})),dotk{}())),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(VarRho:SortMap{},Lbl'Stop'Map{}()))),Var'Unds'DotVar0:SortGeneratedCounterCell{})) [] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(Example of a rule-LHS alias with a predicate)
Fixes #4028