quantor/macros/
quantify.rs

1/// Evaluates logical quantifiers using mathematical-style syntax over iterables.
2///
3/// This macro acts as a declarative frontend to the basic quantifier functions in `quantor`,
4/// allowing expressive, readable logic similar to mathematics.
5///
6/// ## Supported Quantifiers
7/// - `forall x in &a => predicate`
8/// - `exists x in &a => predicate`
9/// - `none x in &a => predicate`
10/// - `exactly_one x in &a => predicate`
11/// - `all_equal x in &a => predicate`
12/// - `pairwise x in &a => predicate`
13/// - `forallexists x in &a, y in &b => predicate`
14/// - `existsforall x in &a, y in &b => predicate`
15///
16/// See the quantifier functions (e.g. [`forall`](crate::quantifiers::basic::forall)) for behavior.
17///
18/// ## Examples
19/// ```rust
20/// use quantor::quantify;
21///
22/// let xs = vec!(2, 4, 6);
23/// assert!(quantify!(forall x in &xs => x % 2 == 0));
24///
25/// let ys = vec!(1, 3, 5);
26/// assert!(quantify!(exists x in &ys => *x == 3));
27/// 
28/// let numbers = vec!(1, 1, 1);
29/// assert!(quantify!(all_equal x in &numbers));
30///
31/// let a = vec!(1, 2);
32/// let b = vec!(3, 4);
33/// assert!(quantify!(forallexists x in &a, y in &b => x < y));
34/// ```
35#[macro_export]
36macro_rules! quantify {
37    // Basic
38    (forall $x:ident in $xs:expr => $cond:expr) => {
39        $crate::quantifiers::basic::forall($xs, |$x| $cond)
40    };
41
42    (exists $x:ident in $xs:expr => $cond:expr) => {
43        $crate::quantifiers::basic::exists($xs, |$x| $cond)
44    };
45
46    (none $x:ident in $xs:expr => $cond:expr) => {
47        $crate::quantifiers::basic::none($xs, |$x| $cond)
48    };
49
50    (exactly_one $x:ident in $xs:expr => $cond:expr) => {
51        $crate::quantifiers::basic::exactly_one($xs, |$x| $cond)
52    };
53
54    (all_equal $x:ident in $xs:expr) => {
55        $crate::quantifiers::basic::all_equal($xs)
56    };
57
58    (pairwise $x:ident in $xs:expr => $cond:expr) => {
59        $crate::quantifiers::basic::pairwise($xs, |$x, x_next| $cond)
60    };
61
62    // Nested
63    (existsforall $a:ident in $as:expr, $b:ident in $bs:expr => $cond:expr) => {
64        $crate::quantifiers::nested::existsforall($as, $bs, |$a, $b| $cond)
65    };
66
67    (forallexists $a:ident in $as:expr, $b:ident in $bs:expr => $cond:expr) => {
68        $crate::quantifiers::nested::forallexists($as, $bs, |$a, $b| $cond)
69    };
70
71    ($($t:tt)*) => {
72        compile_error!("Invalid syntax in quantify! macro.");
73    };
74}