Conversation
|
|
||
| rule Instrs_ok/instr: | ||
| C |- instr : t_1* -> t_2* | ||
| -- Instr_ok: C |- instr : t_1* -> t_2* |
There was a problem hiding this comment.
Oh, I am amazed that this can be correctly parsed by the backends, as at first glance it really looks like a self-referential rule; but actually it says instr_ok C instr : t1* -> ts2* constructs instrs_ok C [instr].
There was a problem hiding this comment.
Well, the frontend does the resolution. There is nothing specific to do in the after elaboration.
There was a problem hiding this comment.
Then I'll praise the frontend to have handled this cleanly!
| C |- instr_1 instr_2* : t_1* -> t_3* | ||
| -- Instr_ok: C |- instr_1 : t_1* -> t_2* | ||
| C |- instr_1* instr_2* : t_1* -> t_3* | ||
| -- Instrs_ok: C |- instr_1* : t_1* -> t_2* |
There was a problem hiding this comment.
Hmm, this formulation will allow derivations of arbitrary lengths now, since either instruction list can be empty. I thought it would be better to preserve the original cons form of the rule and leave the general list append as a lemma (not too difficult to prove). Or did I overlook anything here?
Same for the 2.0/3.0 changes below.
|
Just a quick check regarding |
rossberg
left a comment
rossberg
left a comment
There was a problem hiding this comment.
Yes, it's deliberate. It's more symmetric and a better separation of concerns this way. In particular, I prefer if there is only one rule that injects from Instr_ok into Instrs_ok.
Arbitrarily long derivations are already possible without this change, since you can always throw in another redundant application of the subsumption (with it = it') or frame (with t* = eps) rule. Likewise, there generally are multiple choices where you can invoke these rules when they're necessary, so a unique shortest derivation also already doesn't exist. So I don't think this formulation loses anything relevant.
|
|
||
| rule Instrs_ok/instr: | ||
| C |- instr : t_1* -> t_2* | ||
| -- Instr_ok: C |- instr : t_1* -> t_2* |
There was a problem hiding this comment.
Well, the frontend does the resolution. There is nothing specific to do in the after elaboration.
|
Thanks for the clarification! Upd: actually, it's probably about equal, because forward composition is free but inversion is slightly harder (and actually a bit more than slightly harder for 3.0 due to instruction types carrying the additional local flags). |
2 participants
Fixes #2194.
@raoxiaojia, PTAL.