/// Construct formulae ergonomically.
///
/// Uppercase identifiers (starting with uppercase) are treated as variables,
/// lowercase identifiers as constants.
///
/// # Examples
///
/// ```
/// use pickaxe_rs::formula;
/// use pickaxe_rs::language::formula::{Formula, Term};
///
/// // Propositional atom (no arguments).
/// let p = formula!(rain);
///
/// // Positive predicate atom with a constant.
/// let f = formula!(flies(tweety));
///
/// // Classical negation.
/// let g = formula!(!flies(tweety));
///
/// // Multi-arity predicate with a variable (uppercase = variable).
/// let h = formula!(likes(X, bob));
/// // X is a Var, bob is a Const.
/// assert_eq!(h.variables(), vec![&"X".to_string()]);
///
/// // Implication.
/// let i = formula!(bird(tweety) -> flies(tweety));
///
/// // Conjunction and disjunction (parenthesised operands).
/// let j = formula!((bird(tweety)) & (feathered(tweety)));
/// let k = formula!((rain) | (snow));
/// ```
#[macro_export]
macro_rules! formula {
    // Implication: (a) -> (b) with parenthesised operands
    (($($lhs:tt)+) -> ($($rhs:tt)+)) => {
        $crate::language::formula::Formula::Implies(
            Box::new($crate::formula!($($lhs)+)),
            Box::new($crate::formula!($($rhs)+)),
        )
    };

    // Implication: atom -> atom (simple forms without parens)
    ($pred1:ident ( $($t1:ident),+ ) -> $pred2:ident ( $($t2:ident),+ )) => {
        $crate::language::formula::Formula::Implies(
            Box::new($crate::formula!($pred1($($t1),+))),
            Box::new($crate::formula!($pred2($($t2),+))),
        )
    };

    // Implication: prop -> prop
    ($a:ident -> $b:ident) => {
        $crate::language::formula::Formula::Implies(
            Box::new($crate::formula!($a)),
            Box::new($crate::formula!($b)),
        )
    };

    // Disjunction: (a) | (b) with parenthesised operands
    (($($a:tt)+) | ($($b:tt)+)) => {
        $crate::language::formula::Formula::Or(vec![
            $crate::formula!($($a)+),
            $crate::formula!($($b)+),
        ])
    };

    // Conjunction: (a) & (b) with parenthesised operands
    (($($a:tt)+) & ($($b:tt)+)) => {
        $crate::language::formula::Formula::And(vec![
            $crate::formula!($($a)+),
            $crate::formula!($($b)+),
        ])
    };

    // Negated atom with arguments: !pred(term1, term2, ...)
    (! $pred:ident ( $($term:ident),+ )) => {
        $crate::language::formula::Formula::Lit(
            $crate::language::formula::Literal::Neg(
                $crate::language::formula::Atom {
                    predicate: stringify!($pred).to_string(),
                    terms: vec![$($crate::formula!(@term $term)),+],
                }
            )
        )
    };

    // Negated propositional atom: !pred
    (! $pred:ident) => {
        $crate::language::formula::Formula::Lit(
            $crate::language::formula::Literal::Neg(
                $crate::language::formula::Atom {
                    predicate: stringify!($pred).to_string(),
                    terms: vec![],
                }
            )
        )
    };

    // Positive atom with arguments: pred(term1, term2, ...)
    ($pred:ident ( $($term:ident),+ )) => {
        $crate::language::formula::Formula::Lit(
            $crate::language::formula::Literal::Pos(
                $crate::language::formula::Atom {
                    predicate: stringify!($pred).to_string(),
                    terms: vec![$($crate::formula!(@term $term)),+],
                }
            )
        )
    };

    // Propositional atom (no arguments): pred
    ($pred:ident) => {
        $crate::language::formula::Formula::Lit(
            $crate::language::formula::Literal::Pos(
                $crate::language::formula::Atom {
                    predicate: stringify!($pred).to_string(),
                    terms: vec![],
                }
            )
        )
    };

    // Internal: classify a term identifier as Var (uppercase first char) or Const
    (@term $t:ident) => {{
        let name = stringify!($t);
        let first = name.chars().next().unwrap();
        if first.is_uppercase() {
            $crate::language::formula::Term::Var(name.to_string())
        } else {
            $crate::language::formula::Term::Const(name.to_string())
        }
    }};
}
