#![deny(missing_docs)]
extern crate pocket_prover;
#[macro_use]
extern crate pocket_prover_derive;
use pocket_prover::*;
#[derive(Copy, Clone, Construct)]
pub struct Set {
pub any: u64,
pub uniq: u64,
pub fin_many: u64,
pub inf_many: u64,
}
impl CoreRules for Set {
fn core_rules(&self) -> u64 {self.rules()}
}
impl ExtendRules for Set {
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &Self::Inner) -> u64 {T}
}
impl Set {
pub fn rules(&self) -> u64 {
and(
imply(or3(self.uniq, self.fin_many, self.inf_many), and(self.some(), not(self.any))),
imply(self.some(), xor4(self.uniq, self.fin_many, self.inf_many, self.any))
)
}
pub fn none(&self) -> u64 {
not(or4(self.any, self.uniq, self.fin_many, self.inf_many))
}
pub fn some(&self) -> u64 {
or4(self.any, self.uniq, self.fin_many, self.inf_many)
}
pub fn undefined(&self) -> u64 {
and4(self.any, not(self.uniq), not(self.fin_many), not(self.inf_many))
}
pub fn multiple(&self) -> u64 {
or(self.fin_many, self.inf_many)
}
pub fn count<F: Fn(Set) -> u64>(f: F) -> u32 {
count4(&mut |any, uniq, fin_many, inf_many| {
f(Set {any, uniq, fin_many, inf_many})
})
}
}
pub trait MSet {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
}
impl MSet for (Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.any, self.1.any])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.uniq, self.1.uniq])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.fin_many, self.1.fin_many])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.inf_many, self.1.inf_many])
}
}
impl MSet for (Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.any, self.1.any, self.2.any])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.uniq, self.1.uniq, self.2.uniq])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many])
}
}
impl MSet for (Set, Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.any, self.1.any, self.2.any, self.3.any])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many])
}
}
impl MSet for (Set, Set, Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.any, self.1.any, self.2.any, self.3.any, self.4.any])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq, self.4.uniq])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many, self.4.fin_many])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many, self.4.inf_many])
}
}
impl MSet for (Set, Set, Set, Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.any, self.1.any, self.2.any, self.3.any, self.4.any, self.5.any])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq, self.4.uniq, self.5.uniq])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
self.4.fin_many, self.5.fin_many])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
self.4.inf_many, self.5.inf_many])
}
}
impl MSet for (Set, Set, Set, Set, Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.any, self.1.any, self.2.any, self.3.any,
self.4.any, self.5.any, self.6.any
])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq,
self.4.uniq, self.5.uniq, self.6.uniq
])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
self.4.fin_many, self.5.fin_many, self.6.fin_many
])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
self.4.inf_many, self.5.inf_many, self.6.inf_many
])
}
}
impl MSet for (Set, Set, Set, Set, Set, Set, Set, Set) {
fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.any, self.1.any, self.2.any, self.3.any,
self.4.any, self.5.any, self.6.any, self.7.any
])
}
fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq,
self.4.uniq, self.5.uniq, self.6.uniq, self.7.uniq
])
}
fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
self.4.fin_many, self.5.fin_many, self.6.fin_many, self.7.fin_many
])
}
fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
f(&[
self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
self.4.inf_many, self.5.inf_many, self.6.inf_many, self.7.inf_many
])
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn both_none_and_some_means_uniq_is_nonsense() {
assert!(!Set::means(
|s| and(s.none(), s.some()),
|s| not(s.uniq)
));
}
#[test]
fn multiple_is_exclusive_from_undefined() {
assert!(Set::exc(
|s| s.multiple(),
|s| s.undefined()
));
}
#[test]
fn some_includes_undefined() {
assert!(!Set::exc(
|s| s.some(),
|s| s.undefined()
));
}
#[test]
fn none_is_not_some() {
assert!(Set::imply(|s| s.none(), |s| not(s.some())));
}
#[test]
fn some_is_not_none() {
assert!(Set::imply(|s| s.some(), |s| not(s.none())));
}
#[test]
fn some_is_eq_not_none() {
assert!(Set::eq(|s| s.some(), |s| not(s.none())));
}
#[test]
fn uniq_is_some() {
assert!(Set::imply(|s| s.uniq, |s| s.some()));
}
#[test]
fn uniq_is_not_fin_many() {
assert!(Set::imply(|s| s.uniq, |s| not(s.fin_many)))
}
#[test]
fn any_is_some() {
assert!(Set::imply(|s| s.any, |s| s.some()));
}
#[test]
fn fin_many_is_some() {
assert!(Set::imply(|s| s.fin_many, |s| s.some()));
}
#[test]
fn inf_many_is_some() {
assert!(Set::imply(|s| s.inf_many, |s| s.some()));
}
#[test]
fn some_does_not_mean_any() {
assert!(Set::does_not_mean(|s| s.some(), |s| s.any));
}
#[test]
fn not_uniq_and_not_none_is_either_fin_many_inf_many_or_any() {
assert!(Set::imply(
|s| and(not(s.uniq), not(s.none())),
|s| or3(s.fin_many, s.inf_many, s.any)
));
}
#[test]
fn fin_many_is_not_inf_many() {
assert!(Set::imply(|s| s.fin_many, |s| not(s.inf_many)));
}
#[test]
fn not_fin_many_does_not_mean_inf_many() {
assert!(Set::does_not_mean(|s| not(s.fin_many), |s| s.inf_many));
}
#[test]
fn none_is_equal_to_neither_uniq_fin_many_inf_many_or_any() {
assert!(Set::eq(
|s| s.none(),
|s| not(or4(s.uniq, s.fin_many, s.inf_many, s.any))
));
}
#[test]
fn undefined_is_some() {
assert!(Set::imply(
|s| s.undefined(),
|s| s.some()
));
}
}