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}