#[macro_export]
macro_rules! assume {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
}
};
}
#[macro_export]
macro_rules! checked_assume {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
} else {
assert!($condition);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition);
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_assume_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right)
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right);
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_assume_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right)
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right);
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
} else {
debug_assert!($condition);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition);
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right)
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right);
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right)
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right);
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! precondition {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
}
};
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
}
};
($condition:expr, $($arg:tt)*) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
}
};
}
#[macro_export]
macro_rules! checked_precondition {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
} else {
assert!($condition);
}
);
($condition:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
} else {
assert!($condition, $message);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_precondition_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
} else {
assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_precondition_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
} else {
assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
} else {
debug_assert!($condition);
}
);
($condition:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
} else {
debug_assert!($condition, $message);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
} else {
debug_assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
} else {
debug_assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! verify {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
}
};
}
#[macro_export]
macro_rules! checked_verify {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
} else {
assert!($condition);
}
);
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("false verification condition: ", $message))
} else {
assert!($condition, $message);
}
};
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", stringify!($($arg)*)));
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_verify_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
} else {
assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_verify_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
} else {
assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
} else {
debug_assert!($condition);
}
);
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition($condition, concat!("false verification condition: ", $message))
} else {
debug_assert!($condition, $message);
}
};
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", stringify!($($arg)*)));
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
} else {
debug_assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
} else {
debug_assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! get_model_field {
($target:expr, $field_name:ident, $default_value:expr) => {
mirai_annotations::mirai_get_model_field($target, stringify!($field_name), $default_value)
};
}
#[macro_export]
macro_rules! result {
() => {
if cfg!(mirai) {
mirai_annotations::mirai_result()
} else {
unimplemented!()
}
};
}
#[macro_export]
macro_rules! set_model_field {
($target:expr, $field_name:ident, $value:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_set_model_field($target, stringify!($field_name), $value);
}
};
}
#[doc(hidden)]
pub fn mirai_assume(_condition: bool) {}
#[doc(hidden)]
pub fn mirai_precondition(_condition: bool, _message: &str) {}
#[doc(hidden)]
pub fn mirai_verify(_condition: bool, _message: &str) {}
#[doc(hidden)]
pub fn mirai_get_model_field<T, V>(_target: T, _field_name: &str, default_value: V) -> V {
default_value
}
#[doc(hidden)]
pub fn mirai_result<T>() -> T {
unreachable!()
}
#[doc(hidden)]
pub fn mirai_set_model_field<T, V>(_target: T, _field_name: &str, _value: V) {}