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
use crate::{id, not};
pub fn bit(b: bool) -> u64 {if b {1} else {0}}
pub fn bitv(b: u64) -> bool {b != 0}
pub fn bitf(b: u64) -> fn(u64) -> u64 {if b == 0 {not} else {id}}
#[macro_export]
macro_rules! bits_format(
($x:ident) => {"{}"};
($x:ident , $($y:ident),*) => {concat!("{}", bits_format!($($y),*))};
);
#[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
}
}
);
#[macro_export]
macro_rules! println_bits(
(|$($x:ident),* $(,)?| $e:expr) => {
bits!(|$($x),*| {
println!(concat!(bits_format!($($x),*), " {}"), $($x),*, $crate::extract::bit($e));
});
}
);
#[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)),*))
)
})
});
};
);