Skip to content

Conversation

@StarGazerM
Copy link

  • 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)));
}

add test

fix include macro call argument for arg more than 1
@s-arash
Copy link
Owner

s-arash commented Sep 23, 2025

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.

@StarGazerM
Copy link
Author

StarGazerM commented Sep 23, 2025

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants