Inlining of a macro call comming from another macro expansion

[W95Psp]

Consider the following macro public_bytes from the Hacspec lib:

macro_rules! public_bytes {
    ($name:ident, $l:expr) => {
        array!($name, $l, u8);
    };
}

This macro is really just a helper macro that wraps a call to the more "primitive" macro array, that Hax handles in a special way.

We don't want to handle public_bytes in a special way --clients might actually define such wrappers themselves, and so we'd need to expand public_bytes once and stop there. Our approach to inlining macro calls cannot handle that at all.

I think this issue adds a motivation against having macros that encode some kinds of DSLs. (like hacspec lib does)

[W95Psp]

Waiting on #145

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[franziskuskiefer]

We will remove all legacy hacspec lib code.