ascent icon indicating copy to clipboard operation
ascent copied to clipboard

Add argument to ascent_source and avoid hygenie

Open StarGazerM opened this issue 4 months ago • 2 comments

  • 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_source because, binding need use $ for macro variable binding in body of ascent_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)));
}

StarGazerM avatar Sep 11 '25 04:09 StarGazerM

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.

s-arash avatar Sep 23 '25 01:09 s-arash

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!

StarGazerM avatar Sep 23 '25 01:09 StarGazerM