Make-reference-arguments also applies to #swap #818
Conversation
| let sig := [:: sig; sig ] in | ||
| Let: (prologue, es) := make_prologue ii X 0 sig es in | ||
| Let: (xs, epilogue) := make_epilogue ii X sig xs in | ||
| ok (prologue ++ MkI ii (Copn xs tg (Opseudo_op (pseudo_operator.Oswap ty)) es) :: epilogue) |
There was a problem hiding this comment.
Can we add a code like this
let tg := if Nat.eqb (size prologue) 2 &&
Nat.eqb (size epilogue) 2 then AT_none else tg in
(* I don't know why but I have a syntax error if I use == instead of Nat.eqb *)
There was a problem hiding this comment.
The idea is that it is clearly a case where we compute address to swap them, but where the swap instruction will be never used.
There was a problem hiding this comment.
Did you understand the syntax error ?
There was a problem hiding this comment.
No. Coq notations dark magic.
There was a problem hiding this comment.
We do not include all_ssreflect so you need to import eqType and probably ssrnat to be able to use == here.
|
Just rebased to address merge conflicts in the changelog. |
Fixes #815