//! Macros for defining predicates.

/// Defines a predicate (boolean expression) over a context type.
///
/// This macro creates a new type implementing [`CvlrFormula`] for the specified context.
/// The predicate body consists of one or more expressions that are evaluated, asserted,
/// or assumed together.
///
/// # Syntax
///
/// ```ignore
/// cvlr_def_predicate! {
///     pred <name> ( <context_var> : <context_type> ) {
///         <expression1>;
///         <expression2>;
///         ...
///     }
/// }
/// ```
///
/// # Parameters
///
/// * `name` - The name of the predicate type to create
/// * `context_var` - The variable name to use for the context in the predicate body
/// * `context_type` - The type of the context
/// * `expressions` - One or more expressions that form the predicate body
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::cvlr_def_predicate;
///
/// struct MyContext {
///     x: i32,
///     y: i32,
/// }
///
/// cvlr_def_predicate! {
///     pred IsPositive ( c : MyContext ) {
///         c.x > 0;
///         c.y > 0;
///     }
/// }
///
/// let ctx = MyContext { x: 5, y: 10 };
/// let pred = IsPositive;
/// assert!(pred.eval(&ctx));
/// ```
#[macro_export]
macro_rules! cvlr_def_predicate {
    (pred $name: ident ( $c:ident : $ctx: ident ) {  $( $e: expr );* $(;)? }) => {
        struct $name;
        impl $crate::CvlrFormula for $name {
            type Context = $ctx;
            fn eval(&self, ctx: &Self::Context) -> bool {
                let $c = ctx;
                $crate::__macro_support::cvlr_eval_all!(
                    $($e),*
                )
            }
            fn assert(&self, ctx: &Self::Context) {
                let $c = ctx;
                $crate::__macro_support::cvlr_assert_all!(
                    $($e),*
                );
            }

            fn assume(&self, ctx: &Self::Context) {
                let $c = ctx;
                $crate::__macro_support::cvlr_assume_all!(
                    $($e),*
                );
            }
        }
        impl $crate::CvlrPredicate for $name { }
    };
}

/// Defines a predicate that evaluates over two states.
///
/// This macro creates a new type implementing [`CvlrFormula`] with `Context = Ctx`.
/// The predicate uses [`eval_with_states`](crate::CvlrFormula::eval_with_states) to evaluate
/// over both the current/post-state (`c`) and the old/pre-state (`o`),
/// allowing you to express postconditions that compare pre-state and post-state.
///
/// # Syntax
///
/// ```ignore
/// cvlr_def_states_predicate! {
///     pred <name> ( [ <current_var>, <old_var> ] : <context_type> ) {
///         <expression1>;
///         <expression2>;
///         ...
///     }
/// }
/// ```
///
/// # Parameters
///
/// * `name` - The name of the predicate type to create
/// * `current_var` - The variable name for the current/post-state context
/// * `old_var` - The variable name for the old/pre-state context
/// * `context_type` - The type of the context
/// * `expressions` - One or more expressions that form the predicate body
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::cvlr_def_states_predicate;
///
/// struct Counter {
///     value: i32,
/// }
///
/// cvlr_def_states_predicate! {
///     pred CounterIncreases ( [ c, o ] : Counter ) {
///         c.value > o.value;
///     }
/// }
///
/// // Use the predicate with eval_with_states
/// let pre = Counter { value: 5 };
/// let post = Counter { value: 10 };
/// let pred = CounterIncreases;
/// assert!(pred.eval_with_states(&post, &pre));
/// ```
#[macro_export]
macro_rules! cvlr_def_states_predicate {
    (pred $name: ident ( [ $c:ident, $o: ident ] : $ctx: ident ) {  $( $e: expr );* $(;)? }) => {
        struct $name;
        impl $crate::CvlrFormula for $name {
            type Context = $ctx;
            fn eval_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) -> bool {
                let $c = ctx0;
                let $o = ctx1;
                $crate::__macro_support::cvlr_eval_all!(
                    $($e),*
                )
            }
            fn assert_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
                let $c = ctx0;
                let $o = ctx1;
                $crate::__macro_support::cvlr_assert_all!(
                    $($e),*
                );
            }
            fn assume_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
                let $c = ctx0;
                let $o = ctx1;
                $crate::__macro_support::cvlr_assume_all!(
                    $($e),*
                );
            }

            fn eval(&self, ctx: &Self::Context) -> bool {
                $crate::__macro_support::cvlr_assert!(false);
                panic!("eval should never be called for a state pair predicate; use eval_with_states instead");
            }
            fn assert(&self, ctx: &Self::Context) {
                $crate::__macro_support::cvlr_assert!(false);
                panic!("assert should never be called for a state pair predicate; use assert_with_states instead");
            }
            fn assume(&self, ctx: &Self::Context) {
                $crate::__macro_support::cvlr_assert!(false);
                panic!("assume should never be called for a state pair predicate; use assume_with_states instead");
            }
        }
        impl $crate::CvlrPredicate for $name { }
    };
}

/// Defines multiple predicates in a single macro invocation.
///
/// This is a convenience macro that allows you to define multiple predicates
/// at once using the same syntax as [`cvlr_def_predicate!`].
///
/// # Syntax
///
/// ```ignore
/// cvlr_def_predicates! {
///     pred <name1> ( <c1> : <ctx> ) { ... }
///     pred <name2> ( <c2> : <ctx> ) { ... }
///     ...
/// }
/// ```
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::cvlr_def_predicates;
///
/// struct MyContext {
///     x: i32,
/// }
///
/// cvlr_def_predicates! {
///     pred IsPositive ( c : MyContext ) {
///         c.x > 0;
///     }
///     pred IsEven ( c : MyContext ) {
///         c.x % 2 == 0;
///     }
/// }
/// ```
#[macro_export]
macro_rules! cvlr_def_predicates {
    ($(pred $name: ident ( $c:ident : $ctx: ident ) {  $( $e: expr );* $(;)? })*) => {
        $(
            $crate::cvlr_def_predicate! {
                pred $name ( $c : $ctx ) { $( $e );* }
            }
        )*
    };
}

/// Defines multiple state predicates in a single macro invocation.
///
/// This is a convenience macro that allows you to define multiple predicates
/// that evaluate over two states at once using the same syntax as [`cvlr_def_states_predicate!`].
///
/// # Syntax
///
/// ```ignore
/// cvlr_def_states_predicates! {
///     pred <name1> ( [ <c1>, <o1> ] : <ctx> ) { ... }
///     pred <name2> ( [ <c2>, <o2> ] : <ctx> ) { ... }
///     ...
/// }
/// ```
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::cvlr_def_states_predicates;
///
/// struct Counter {
///     value: i32,
/// }
///
/// cvlr_def_states_predicates! {
///     pred Increases ( [ c, o ] : Counter ) {
///         c.value > o.value;
///     }
///     pred NonDecreasing ( [ c, o ] : Counter ) {
///         c.value >= o.value;
///     }
/// }
/// ```
#[macro_export]
macro_rules! cvlr_def_states_predicates {
    ($(pred $name: ident ( [ $c:ident, $o: ident ] : $ctx: ident ) {  $( $e: expr );* $(;)? })*) => {
        $(
            $crate::cvlr_def_states_predicate! {
                pred $name ( [ $c, $o ] : $ctx ) { $( $e );* }
            }
        )*
    };
}

/// Creates an anonymous predicate (boolean expression) over a context type.
///
/// This macro creates an anonymous predicate that implements [`CvlrFormula`](crate::CvlrFormula) for the
/// specified context type. Unlike [`cvlr_def_predicate!`], this macro creates an
/// unnamed predicate that can be used inline without defining a separate type.
///
/// # Syntax
///
/// ```ignore
/// cvlr_predicate! {
///     | <context_var> : <context_type> | -> {
///         <expression1>;
///         <expression2>;
///         ...
///     }
/// }
/// ```
///
/// # Parameters
///
/// * `context_var` - The variable name to use for the context in the predicate body
/// * `context_type` - The type of the context
/// * `expressions` - One or more expressions that form the predicate body
///
/// # Returns
///
/// Returns a value implementing [`CvlrFormula`](crate::CvlrFormula) with `Context = Ctx` that can be evaluated,
/// asserted, or assumed.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::cvlr_predicate;
///
/// struct Counter {
///     value: i32,
/// }
///
/// let ctx = Counter { value: 5 };
///
/// // Create an anonymous predicate
/// let pred = cvlr_predicate! { | c : Counter | -> {
///     c.value > 0;
///     c.value < 100
/// } };
///
/// assert!(pred.eval(&ctx));
/// ```
///
/// Note: This example is marked `ignore` because it doesn't require special setup.
/// In actual usage, predicates are often used within lemmas or other verification contexts.
///
/// This macro is often used internally by [`cvlr_lemma!`] to create the requires
/// and ensures predicates.
#[macro_export]
macro_rules! cvlr_predicate {
    (| $c:ident : $ctx: ident | -> { $($body:tt)* } ) => {
        {
            #[$crate::__macro_support::cvlr_predicate]
            fn __anonymous_predicate($c: &$ctx) {
                $($body)*
            }
            $crate::__macro_support::cvlr_pif!(__anonymous_predicate)
        }
    };
}

/// Defines a lemma with preconditions (requires) and postconditions (ensures).
///
/// This macro creates a new type implementing [`CvlrLemma`](spec::CvlrLemma) for the specified context.
/// A lemma is a logical statement: if the preconditions hold, then the postconditions
/// must also hold. Lemmas can be verified using the [`verify`](spec::CvlrLemma::verify) or
/// [`verify_with_context`](spec::CvlrLemma::verify_with_context) methods.
///
/// # Syntax
///
/// The macro supports two syntax forms:
///
/// **Form 1: Block syntax with inline expressions**
/// ```ignore
/// cvlr_lemma! {
///     <name> ( <context_var> : <context_type> ) {
///         requires -> {
///             <requires_expr1>;
///             <requires_expr2>;
///             ...
///         }
///         ensures -> {
///             <ensures_expr1>;
///             <ensures_expr2>;
///             ...
///         }
///     }
/// }
/// ```
///
/// **Form 2: Expression syntax with pre-built predicates**
/// ```ignore
/// cvlr_lemma! {
///     <name> for <context_type> {
///         requires: <requires_expr>,
///         ensures: <ensures_expr>,
///     }
/// }
/// ```
///
/// # Parameters
///
/// **Form 1 parameters:**
/// * `name` - The name of the lemma type to create
/// * `context_var` - The variable name to use for the context in the requires/ensures clauses
/// * `context_type` - The type of the context (must implement [`Nondet`](cvlr_nondet::Nondet) and [`CvlrLog`](cvlr_log::CvlrLog))
/// * `requires` - One or more expressions that form the preconditions
/// * `ensures` - One or more expressions that form the postconditions
///
/// **Form 2 parameters:**
/// * `name` - The name of the lemma type to create
/// * `context_type` - The type of the context (must implement [`Nondet`](cvlr_nondet::Nondet) and [`CvlrLog`](cvlr_log::CvlrLog))
/// * `requires` - A single expression (predicate, identifier, or composed expression) that forms the preconditions
/// * `ensures` - A single expression (predicate, identifier, or composed expression) that forms the postconditions
///
/// # Returns
///
/// Creates a struct with the given name that implements [`CvlrLemma`](spec::CvlrLemma) with `Context = Ctx`.
///
/// # Examples
///
/// ```ignore
/// extern crate cvlr;
/// use cvlr_spec::cvlr_lemma;
///
/// // Counter must implement Nondet and CvlrLog for lemma verification
/// #[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
/// struct Counter {
///     value: i32,
/// }
///
/// // Define a lemma: if value > 0, then value > 0 (trivial but demonstrates syntax)
/// cvlr_lemma! {
///     CounterPositiveLemma(c: Counter) {
///         requires -> {
///             c.value > 0
///         }
///         ensures -> {
///             c.value > 0
///         }
///     }
/// }
///
/// // Use the lemma
/// let lemma = CounterPositiveLemma;
/// lemma.verify(); // Verifies the lemma holds for all contexts
/// ```
///
/// More complex example:
///
/// ```ignore
/// extern crate cvlr;
/// use cvlr_spec::cvlr_lemma;
///
/// #[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
/// struct Counter {
///     value: i32,
/// }
///
/// cvlr_lemma! {
///     CounterDoublesLemma(c: Counter) {
///         requires -> {
///             c.value > 0;
///             c.value < 100
///         }
///         ensures -> {
///             c.value > 0;
///             c.value * 2 > c.value
///         }
///     }
/// }
/// ```
///
/// **Form 2: Using pre-built predicates or expressions**
///
/// This form is useful when you already have predicates defined or want to use composed expressions:
///
/// ```ignore
/// extern crate cvlr;
/// use cvlr_spec::{cvlr_lemma, cvlr_predicate, cvlr_and};
///
/// #[derive(cvlr::derive::Nondet, cvlr::derive::CvlrLog)]
/// struct Counter {
///     value: i32,
/// }
///
/// // Define predicates separately
/// let positive_pred = cvlr_predicate! { | c : Counter | -> { c.value > 0 } };
/// let bounded_pred = cvlr_predicate! { | c : Counter | -> { c.value < 100 } };
///
/// // Use them in a lemma with the expression syntax
/// cvlr_lemma! {
///     CounterBoundedLemma for Counter {
///         requires: cvlr_and!(positive_pred, bounded_pred),
///         ensures: positive_pred,
///     }
/// }
///
/// // Or use identifier predicates
/// cvlr_def_predicate! {
///     pred IsPositive(c: Counter) {
///         c.value > 0
///     }
/// }
///
/// cvlr_lemma! {
///     CounterPositiveLemma for Counter {
///         requires: IsPositive,
///         ensures: IsPositive,
///     }
/// }
/// ```
///
/// # Verification
///
/// When verifying a lemma:
/// 1. The preconditions (requires) are assumed to hold
/// 2. The postconditions (ensures) are asserted to hold
///
/// If the postconditions don't hold when the preconditions are assumed,
/// the verification will fail.
#[macro_export]
macro_rules! cvlr_lemma {
    ($name: ident ( $c:ident : $ctx: ident ) {
        requires -> { $($requires:tt)* }
        ensures -> { $($ensures:tt)* } }) => {
            pub struct $name;
            impl $crate::spec::CvlrLemma for $name {
                type Context = $ctx;
                fn requires(&self) -> impl $crate::CvlrFormula<Context = Self::Context> {
                    $crate::cvlr_predicate! { | $c : $ctx | -> { $($requires)* } }
                }
                fn ensures(&self) -> impl $crate::CvlrFormula<Context = Self::Context> {
                    $crate::cvlr_predicate! { | $c : $ctx | -> { $($ensures)* } }
                }
            }
        };

    ($name:ident for $ctx:ident { requires: $r:expr , ensures: $e:expr $(,)? }) => {
        pub struct $name;
        impl $crate::spec::CvlrLemma for $name {
            type Context = $ctx;
            fn requires(&self) -> impl $crate::CvlrFormula<Context = Self::Context> {
                $r
            }
            fn ensures(&self) -> impl $crate::CvlrFormula<Context = Self::Context> {
                $e
            }
        }
    };
}

/// Defines multiple rules for a specification across multiple base functions.
///
/// This macro is a convenience macro that generates multiple rule definitions
/// by calling [`cvlr_rule_for_spec!`](crate::__macro_support::cvlr_rule_for_spec) for each
/// base function in the list. Each rule will have the same name and specification,
/// but will be applied to different base functions.
///
/// # Syntax
///
/// ```ignore
/// cvlr_rules! {
///     name: "rule_name",
///     spec: spec_expression,
///     bases: [
///         base_function1,
///         base_function2,
///         base_function3,
///     ]
/// }
/// ```
///
/// # Parameters
///
/// * `name` - A string literal that will be converted to snake_case and combined with each base function name
/// * `spec` - An expression representing the specification (must implement [`CvlrSpec`](crate::spec::CvlrSpec))
/// * `bases` - A list of function identifiers (if they start with `base_`, that prefix is stripped)
///
/// # Expansion
///
/// This macro expands to multiple calls to `cvlr_rule_for_spec!`, one for each base function:
///
/// ```text
/// // Input:
/// cvlr_rules! {
///     name: "solvency",
///     spec: my_spec,
///     bases: [base_function1, base_function2]
/// }
///
/// // Expands to:
/// cvlr_rule_for_spec!{name: "solvency", spec: my_spec, base: base_function1}
/// cvlr_rule_for_spec!{name: "solvency", spec: my_spec, base: base_function2}
/// ```
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_rules, cvlr_spec, cvlr_predicate};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Create a spec
/// let my_spec = cvlr_spec! {
///     requires: cvlr_predicate! { | c : Counter | -> { c.value > 0 } },
///     ensures: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } }
/// };
///
/// // Define rules for multiple functions
/// cvlr_rules! {
///     name: "solvency",
///     spec: my_spec,
///     bases: [
///         base_update_counter,
///         base_reset_counter,
///         base_increment_counter,
///     ]
/// }
/// ```
///
/// This will create three rules:
/// - `solvency_update_counter`
/// - `solvency_reset_counter`
/// - `solvency_increment_counter`
#[macro_export]
macro_rules! cvlr_rules {
    (name: $name:literal, spec: $spec:expr, bases: [ $( $base:ident ),* $(,)? ] ) => {
        $(
            $crate::__macro_support::cvlr_rule_for_spec!{name: $name, spec: $spec, base: $base}
        )*
    };
}

/// Creates a specification from preconditions (requires) and postconditions (ensures).
///
/// This macro is a convenience wrapper around [`cvlr_spec`](crate::spec::cvlr_spec) that
/// provides a more readable syntax for creating specifications.
///
/// # Syntax
///
/// ```ignore
/// cvlr_spec! {
///     requires: requires_expression,
///     ensures: ensures_expression,
/// }
///
/// // Or omit `requires` to use [`cvlr_true`](crate::cvlr_true) as the precondition:
/// cvlr_spec! {
///     ensures: ensures_expression,
/// }
/// ```
///
/// # Parameters
///
/// * `requires` (optional) - A boolean expression over the context type representing the precondition.
///   If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `ensures`.
/// * `ensures` - A boolean expression over the context type that uses [`eval_with_states`](crate::CvlrFormula::eval_with_states)
///   to evaluate over both pre-state and post-state
///
/// # Returns
///
/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the `ensures` expression.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_spec, cvlr_predicate, cvlr_def_states_predicate};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Define a predicate for the ensures clause that compares pre and post states
/// cvlr_def_states_predicate! {
///     pred CounterIncreases ( [ c, o ] : Counter ) {
///         c.value > o.value;
///     }
/// }
///
/// // Create a spec using the macro
/// let spec = cvlr_spec! {
///     requires: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } },
///     ensures: CounterIncreases,
/// };
///
/// // Use the spec
/// let pre = Counter { value: 5 };
/// let post = Counter { value: 10 };
/// spec.assume_requires(&pre);
/// spec.check_ensures(&post, &pre);
/// ```
#[macro_export]
macro_rules! cvlr_spec {
    (requires: $r:expr, ensures: $e:expr $(,)?) => {
        $crate::cvlr_spec($r, $e)
    };
    (ensures: $e:expr $(,)?) => {
        $crate::cvlr_spec($crate::cvlr_true::<_>(), $e)
    };
}

/// Creates an invariant specification from an assumption and an invariant.
///
/// This macro is a convenience wrapper around [`cvlr_invar_spec`](crate::spec::cvlr_invar_spec) that
/// provides a more readable syntax for creating invariant specifications.
///
/// An invariant specification represents a contract where:
/// - An assumption (additional precondition) is assumed before the operation
/// - An invariant must hold both before and after the operation
///
/// # Syntax
///
/// ```ignore
/// cvlr_invar_spec! {
///     assumption: assumption_expression,
///     invariant: invariant_expression,
/// }
///
/// // Or omit `assumption` to use [`cvlr_true`](crate::cvlr_true) as the extra precondition:
/// cvlr_invar_spec! {
///     invariant: invariant_expression,
/// }
/// ```
///
/// # Parameters
///
/// * `assumption` (optional) - A boolean expression representing an additional precondition.
///   If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `invariant`.
/// * `invariant` - A boolean expression representing an invariant that must hold before and after
///
/// # Returns
///
/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the `invariant` expression.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_invar_spec, cvlr_predicate};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Create an invariant spec
/// let spec = cvlr_invar_spec! {
///     assumption: cvlr_predicate! { | c : Counter | -> { c.value % 2 == 0 } },
///     invariant: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } },
/// };
///
/// // Use the spec
/// let ctx = Counter { value: 4 };
/// spec.assume_requires(&ctx);  // Assumes both assumption and invariant
/// spec.check_ensures(&ctx, &ctx);  // Asserts invariant holds
/// ```
#[macro_export]
macro_rules! cvlr_invar_spec {
    (assumption: $a:expr, invariant: $i:expr $(,)?) => {
        $crate::cvlr_invar_spec($a, $i)
    };
    (invariant: $i:expr $(,)?) => {
        $crate::cvlr_invar_spec($crate::cvlr_true::<_>(), $i)
    };
}

/// Defines multiple rules for an invariant specification across multiple base functions.
///
/// This macro is a convenience macro that combines [`cvlr_invar_spec!`] and [`cvlr_rules!`]
/// to create multiple rules with an invariant specification. It generates multiple rule definitions
/// by creating an invariant spec from the assumption and invariant, then applying it to each
/// base function in the list.
///
/// # Syntax
///
/// ```ignore
/// cvlr_invariant_rules! {
///     name: "rule_name",
///     assumption: assumption_expression,
///     invariant: invariant_expression,
///     bases: [
///         base_function1,
///         base_function2,
///         base_function3,
///     ]
/// }
///
/// // `assumption` may be omitted (uses [`cvlr_true`](crate::cvlr_true)):
/// cvlr_invariant_rules! {
///     name: "rule_name",
///     invariant: invariant_expression,
///     bases: [ base_function1 ]
/// }
/// ```
///
/// # Parameters
///
/// * `name` - A string literal that will be converted to snake_case and combined with each base function name
/// * `assumption` (optional) - A boolean expression representing an additional precondition.
///   If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `invariant`.
/// * `invariant` - A boolean expression representing an invariant that must hold before and after
/// * `bases` - A list of function identifiers (if they start with `base_`, that prefix is stripped)
///
/// # Expansion
///
/// This macro expands to multiple calls to `cvlr_rule_for_spec!`, one for each base function,
/// with an invariant spec created from the assumption and invariant:
///
/// ```text
/// // Input:
/// cvlr_invariant_rules! {
///     name: "non_negative",
///     assumption: assumption_expr,
///     invariant: invariant_expr,
///     bases: [base_function1, base_function2]
/// }
///
/// // Expands to:
/// cvlr_rule_for_spec!{name: "non_negative", spec: cvlr_invar_spec(assumption_expr, invariant_expr), base: base_function1}
/// cvlr_rule_for_spec!{name: "non_negative", spec: cvlr_invar_spec(assumption_expr, invariant_expr), base: base_function2}
/// ```
///
/// If `assumption` is omitted, `cvlr_invar_spec(cvlr_true::<_>(), invariant_expr)` is used instead.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_invariant_rules, cvlr_predicate};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Define invariant rules for multiple functions
/// cvlr_invariant_rules! {
///     name: "non_negative",
///     assumption: cvlr_predicate! { | c : Counter | -> { c.value % 2 == 0 } },
///     invariant: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } },
///     bases: [
///         base_update_counter,
///         base_reset_counter,
///         base_increment_counter,
///     ]
/// }
/// ```
///
/// This will create three rules:
/// - `non_negative_update_counter`
/// - `non_negative_reset_counter`
/// - `non_negative_increment_counter`
///
/// Each rule uses an invariant specification that:
/// - Assumes both the assumption and invariant in the pre-state
/// - Asserts the invariant in the post-state
#[macro_export]
macro_rules! cvlr_invariant_rules {
    (name: $name:literal, assumption: $a:expr, invariant: $i:expr, bases: [ $( $base:ident ),* $(,)? ] ) => {
        $(
            $crate::__macro_support::cvlr_rule_for_spec!{
                name: $name,
                spec: $crate::spec::cvlr_invar_spec($a, $i),
                base: $base
            }
        )*
    };
    (name: $name:literal, invariant: $i:expr, bases: [ $( $base:ident ),* $(,)? ] ) => {
        $(
            $crate::__macro_support::cvlr_rule_for_spec!{
                name: $name,
                spec: $crate::spec::cvlr_invar_spec($crate::cvlr_true::<_>(), $i),
                base: $base
            }
        )*
    };
}

/// Creates a boolean expression representing the logical AND of two or more expressions.
///
/// This macro is a convenience wrapper around [`cvlr_and`](crate::cvlr_and) that
/// provides flexible syntax for combining boolean expressions. It supports both identifiers
/// and expressions as arguments, and can combine 2 to 6 expressions.
///
/// # Syntax
///
/// ```ignore
/// cvlr_and!(a, b)                    // Two arguments
/// cvlr_and!(a, b, c)                 // Three arguments
/// cvlr_and!(a, b, c, d)              // Four arguments
/// cvlr_and!(a, b, c, d, e)           // Five arguments
/// cvlr_and!(a, b, c, d, e, f)        // Six arguments
/// ```
///
/// # Arguments
///
/// The macro accepts identifiers or expressions that implement [`CvlrFormula`](crate::CvlrFormula)
/// with the same context type. Arguments can be:
/// - Identifiers (e.g., `XPositive`)
/// - Expressions (e.g., `cvlr_predicate! { | c : Ctx | -> { c.x > 0 } }`)
/// - Mixed (e.g., `cvlr_and!(XPositive, cvlr_predicate! { | c : Ctx | -> { c.y > 0 } })`)
///
/// # Returns
///
/// Returns a value implementing [`CvlrFormula`](crate::CvlrFormula) that evaluates to `true`
/// only when all input expressions evaluate to `true`.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_and, cvlr_predicate, CvlrFormula};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Using identifiers
/// cvlr_def_predicate! {
///     pred IsPositive(c: Counter) {
///         c.value > 0
///     }
/// }
///
/// cvlr_def_predicate! {
///     pred IsEven(c: Counter) {
///         c.value % 2 == 0
///     }
/// }
///
/// let ctx = Counter { value: 6 };
/// let expr = cvlr_and!(IsPositive, IsEven);
/// assert!(expr.eval(&ctx));
///
/// // Using expressions
/// let expr2 = cvlr_and!(
///     cvlr_predicate! { | c : Counter | -> { c.value > 0 } },
///     cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
/// );
/// assert!(expr2.eval(&ctx));
///
/// // Using multiple arguments
/// let expr3 = cvlr_and!(
///     IsPositive,
///     IsEven,
///     cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
/// );
/// assert!(expr3.eval(&ctx));
/// ```
#[macro_export]
macro_rules! cvlr_and {
    ($a:expr, $b:expr) => {
        $crate::cvlr_and($a, $b)
    };

    ($a:expr, $b:expr, $c:expr) => {
        $crate::cvlr_and($a, $crate::cvlr_and($b, $c))
    };
    ($a:expr, $b:expr, $c:expr, $d:expr) => {
        $crate::cvlr_and($a, $crate::cvlr_and($b, $crate::cvlr_and($c, $d)))
    };
    ($a:expr, $b:expr, $c:expr, $d:expr, $e:expr) => {
        $crate::cvlr_and(
            $a,
            $crate::cvlr_and($b, $crate::cvlr_and($c, $crate::cvlr_and($d, $e))),
        )
    };
    ($a:expr, $b:expr, $c:expr, $d:expr, $e:expr, $f:expr) => {
        $crate::cvlr_and(
            $a,
            $crate::cvlr_and(
                $b,
                $crate::cvlr_and($c, $crate::cvlr_and($d, $crate::cvlr_and($e, $f))),
            ),
        )
    };
}

/// Creates a boolean expression representing the logical AND of two or more predicate functions.
///
/// This macro is similar to [`cvlr_and!`], but it automatically converts predicate function names
/// (snake_case) to their corresponding struct names (PascalCase) using [`cvlr_pif!`](crate::__macro_support::cvlr_pif)
/// before combining them. This is useful when working with predicates defined using the
/// [`#[cvlr::predicate]`](crate::__macro_support::cvlr_predicate) attribute macro.
///
/// # Syntax
///
/// ```ignore
/// cvlr_pif_and!(predicate_func1, predicate_func2)                    // Two arguments
/// cvlr_pif_and!(predicate_func1, predicate_func2, predicate_func3)   // Three arguments
/// cvlr_pif_and!(predicate_func1, predicate_func2, predicate_func3, predicate_func4)  // Four arguments
/// cvlr_pif_and!(predicate_func1, predicate_func2, predicate_func3, predicate_func4, predicate_func5)  // Five arguments
/// cvlr_pif_and!(predicate_func1, predicate_func2, predicate_func3, predicate_func4, predicate_func5, predicate_func6)  // Six arguments
/// ```
///
/// # Arguments
///
/// The macro accepts identifiers (function names) that correspond to predicates defined with
/// the [`#[cvlr::predicate]`](crate::__macro_support::cvlr_predicate) attribute. Each identifier
/// is converted from snake_case to PascalCase:
///
/// - `my_predicate` → `MyPredicate`
/// - `is_positive` → `IsPositive`
/// - `x_gt_zero` → `XGtZero`
///
/// All predicates must implement [`CvlrFormula`](crate::CvlrFormula) with the same context type.
///
/// # Returns
///
/// Returns a value implementing [`CvlrFormula`](crate::CvlrFormula) that evaluates to `true`
/// only when all input predicates evaluate to `true`.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_pif_and, CvlrFormula};
/// use cvlr::predicate;
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Define predicates using the attribute macro
/// #[predicate]
/// fn is_positive(c: &Counter) {
///     c.value > 0
/// }
///
/// #[predicate]
/// fn is_even(c: &Counter) {
///     c.value % 2 == 0
/// }
///
/// #[predicate]
/// fn is_bounded(c: &Counter) {
///     c.value < 100
/// }
///
/// // Combine predicates using cvlr_pif_and
/// let ctx = Counter { value: 6 };
/// let expr = cvlr_pif_and!(is_positive, is_even);
/// assert!(expr.eval(&ctx)); // Both predicates are true
///
/// // Combine multiple predicates
/// let expr2 = cvlr_pif_and!(is_positive, is_even, is_bounded);
/// assert!(expr2.eval(&ctx)); // All three predicates are true
///
/// let ctx2 = Counter { value: 5 };
/// assert!(!expr.eval(&ctx2)); // is_even is false, so the AND is false
/// ```
///
/// # Comparison with `cvlr_and!`
///
/// - **`cvlr_and!`**: Works with struct names (PascalCase) or expressions directly
///   - Example: `cvlr_and!(IsPositive, IsEven)` or `cvlr_and!(pred1, pred2)` where `pred1` is already a struct
/// - **`cvlr_pif_and!`**: Works with function names (snake_case) and converts them automatically
///   - Example: `cvlr_pif_and!(is_positive, is_even)` where `is_positive` is a function name
///
/// Use `cvlr_pif_and!` when you have predicates defined with `#[cvlr::predicate]` and want
/// to reference them by their function names. Use `cvlr_and!` when you already have struct
/// names or expressions.
#[macro_export]
macro_rules! cvlr_pif_and {
    ($a:expr, $b:expr) => {
        $crate::cvlr_and(
            $crate::__macro_support::cvlr_pif!($a),
            $crate::__macro_support::cvlr_pif!($b),
        )
    };

    ($a:expr, $b:expr, $c:expr) => {
        $crate::cvlr_and(
            $crate::__macro_support::cvlr_pif!($a),
            $crate::cvlr_and(
                $crate::__macro_support::cvlr_pif!($b),
                $crate::__macro_support::cvlr_pif!($c),
            ),
        )
    };
    ($a:expr, $b:expr, $c:expr, $d:expr) => {
        $crate::cvlr_and(
            $crate::__macro_support::cvlr_pif!($a),
            $crate::cvlr_and(
                $crate::__macro_support::cvlr_pif!($b),
                $crate::cvlr_and(
                    $crate::__macro_support::cvlr_pif!($c),
                    $crate::__macro_support::cvlr_pif!($d),
                ),
            ),
        )
    };
    ($a:expr, $b:expr, $c:expr, $d:expr, $e:expr) => {
        $crate::cvlr_and(
            $crate::__macro_support::cvlr_pif!($a),
            $crate::cvlr_and(
                $crate::__macro_support::cvlr_pif!($b),
                $crate::cvlr_and(
                    $crate::__macro_support::cvlr_pif!($c),
                    $crate::cvlr_and(
                        $crate::__macro_support::cvlr_pif!($d),
                        $crate::__macro_support::cvlr_pif!($e),
                    ),
                ),
            ),
        )
    };
    ($a:expr, $b:expr, $c:expr, $d:expr, $e:expr, $f:expr) => {
        $crate::cvlr_and(
            $crate::__macro_support::cvlr_pif!($a),
            $crate::cvlr_and(
                $crate::__macro_support::cvlr_pif!($b),
                $crate::cvlr_and(
                    $crate::__macro_support::cvlr_pif!($c),
                    $crate::cvlr_and(
                        $crate::__macro_support::cvlr_pif!($d),
                        $crate::cvlr_and(
                            $crate::__macro_support::cvlr_pif!($e),
                            $crate::__macro_support::cvlr_pif!($f),
                        ),
                    ),
                ),
            ),
        )
    };
}

/// Creates a boolean expression representing logical implication (A → B).
///
/// This macro is a convenience wrapper around [`cvlr_implies`](crate::cvlr_implies) that
/// provides flexible syntax for creating implications. It supports both identifiers and expressions
/// as arguments.
///
/// An implication `A → B` evaluates to `true` when either:
/// - The antecedent `A` is `false`, or
/// - Both `A` and `B` are `true`
///
/// # Syntax
///
/// ```ignore
/// cvlr_implies!(antecedent, consequent)
/// ```
///
/// # Arguments
///
/// * `antecedent` - The left-hand side (A) of the implication, can be an identifier or expression
/// * `consequent` - The right-hand side (B) of the implication, can be an identifier or expression
///
/// Both arguments must implement [`CvlrFormula`](crate::CvlrFormula) with the same context type.
///
/// # Returns
///
/// Returns a value implementing [`CvlrFormula`](crate::CvlrFormula) that represents the logical
/// implication `antecedent → consequent`.
///
/// # Examples
///
/// ```ignore
/// use cvlr_spec::{cvlr_implies, cvlr_predicate, CvlrFormula};
///
/// struct Counter {
///     value: i32,
/// }
///
/// // Using identifiers
/// cvlr_def_predicate! {
///     pred IsPositive(c: Counter) {
///         c.value > 0
///     }
/// }
///
/// cvlr_def_predicate! {
///     pred IsEven(c: Counter) {
///         c.value % 2 == 0
///     }
/// }
///
/// let ctx1 = Counter { value: 6 };
/// let expr = cvlr_implies!(IsPositive, IsEven);
/// assert!(expr.eval(&ctx1)); // 6 > 0 → 6 % 2 == 0 (both true, so true)
///
/// let ctx2 = Counter { value: 5 };
/// assert!(!expr.eval(&ctx2)); // 5 > 0 → 5 % 2 == 0 (antecedent true, consequent false, so false)
///
/// let ctx3 = Counter { value: -2 };
/// assert!(expr.eval(&ctx3)); // -2 > 0 → ... (antecedent false, so true)
///
/// // Using expressions
/// let expr2 = cvlr_implies!(
///     cvlr_predicate! { | c : Counter | -> { c.value > 0 } },
///     cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
/// );
/// assert!(expr2.eval(&ctx1));
///
/// // Mixed identifiers and expressions
/// let expr3 = cvlr_implies!(
///     IsPositive,
///     cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
/// );
/// assert!(expr3.eval(&ctx1));
/// ```
#[macro_export]
macro_rules! cvlr_implies {
    ($a:expr, $b:expr) => {
        $crate::cvlr_implies($a, $b)
    };
}
