1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
//! Helper utilities for extracting data from proofs.
//!
//! ```rust
//! use pocket_prover::*;
//!
//! fn main() {
//! println!("(a ∧ c) (b ∧ c) (∃)");
//! println_extract!(
//! &mut |a, b, c| and(eq(a, b), c);
//! x0 => and(a, c),
//! x1 => and(b, c)
//! );
//!
//! println!("");
//! println!("By looking at the table above one can see that `a ∧ c` and `b ∧ c` are equal.");
//! println!("Therefore, one can prove:");
//! println!("");
//! println!(" (a = b) ∧ c");
//! println!("-----------------");
//! println!("(a ∧ c) = (b ∧ c)");
//! println!("");
//! println!("Result: {}", prove!(&mut |a, b, c| {
//! imply(
//! and(eq(a, b), c),
//! eq(and(a, c), and(b, c))
//! )
//! }))
//! }
//! ```
use crate::{id, not};
/// Converts a boolean to a bit.
pub fn bit(b: bool) -> u64 {if b {1} else {0}}
/// Converts a bit to a boolean.
pub fn bitv(b: u64) -> bool {b != 0}
/// If the bit argument is `0`, returns `not`, else `id`.
pub fn bitf(b: u64) -> fn(u64) -> u64 {if b == 0 {not} else {id}}
/// Generates a "{}{}{}..." format for bits.
#[macro_export]
macro_rules! bits_format(
($x:ident) => {"{}"};
($x:ident , $($y:ident),*) => {concat!("{}", bits_format!($($y),*))};
);
/// Evaluates an expression for all bit configurations.
#[macro_export]
macro_rules! bits(
(|$($x:ident),* $(,)?| $e:expr) => {
let _n = tup_count!($($x),*);
for _x in 0_u64..(1 << _n) {
let mut _i = 0;
$(let $x = (_x >> (_n - _i - 1)) & 1; _i += 1;)*
$e
}
}
);
/// Prints a truth table with result of a boolean expression.
#[macro_export]
macro_rules! println_bits(
(|$($x:ident),* $(,)?| $e:expr) => {
bits!(|$($x),*| {
println!(concat!(bits_format!($($x),*), " {}"), $($x),*, $crate::extract::bit($e));
});
}
);
/// Prints a truth table extracted from a theory,
/// assigning each case a bit and automatically flip expression properly.
#[macro_export]
macro_rules! println_extract(
(&mut |$($t:ident),* $(,)?| $th:expr ; $($x:ident => $ch:expr),* $(,)?) => {
println_bits!(|$($x),*| {
!prove!(&mut |$($t),*| {
imply(
$th,
not(and!($($crate::extract::bitf($x)($ch)),*))
)
})
});
};
(&mut |($($t1:ident),+ $(,)?), ($($t0:ident),+ $(,)?)| $th:expr ; $($x:ident => $ch:expr),* $(,)?) => {
println_bits!(|$($x),*| {
!prove!(&mut |($($t1),+), ($($t0),+)| {
imply(
$th,
not(and!($($crate::extract::bitf($x)($ch)),*))
)
})
});
};
);