Add argument to ascent_source and avoid hygenie
- Adding extra arguments to allow binding unbound term in
ascent_source! - Adding extra arguments to
include_source!syntax inside ascent. - commented the unused nesting in
ascent_sourcebecause, binding need use$for macro variable binding in body ofascent_source
Example :
#[test]
fn test_macro_with_binding() {
let z = 1;
mod foom {
use super::*;
ascent_source! {
foo_gen (z):
foo(x, y) <-- foo(y, x), if y == &$z;
}
}
let prog = ascent_run! {
// struct MacroTest;
relation foo(usize, usize);
foo(1, 2);
include_source!(foom::foo_gen, z);
};
assert!(prog.foo.contains(&(2, 1)));
}
Thanks for the PR @StarGazerM!
You could argue that it would be useful to try and make ascent_source parameterized. Is this what this PR is doing? Otherwise I don't quite see the motivation to circumvent hygiene.
The hygiene issue happens in macro expanded from original ascent_source! macro, if it contain any ungrounded identifier, for example:
ascent_source! {
foo_gen:
foo(x, y) <-- foo(y, x), if y == &z;
}
Although by itself, this source code is a valid ascent code, as long as variable z has been defined in upper scope; Here z is ungrounded in rust macro expanded from ascent_source! and will cause rust compiler says it undefined, even if z has already been defined in the scope. This PR is trying to solve this issue by add optional variable in macro expanded from ascent_source!