AllFunctions store BoolFnExt + Connective

examples/truth_table.rs

@@ -1,27 +1,46 @@
 //! Print truth tables for all the binary functions.
 #![allow(clippy::wildcard_imports)]
 
-use prop_logic::connective::*;
+use prop_logic::{connective::*, two_powers, CheckedArray};
+
+fn print_stat<const ARITY: usize>(f: &dyn StoredBoolFn<ARITY>)
+where
+    TruthTable<ARITY>: std::fmt::Display,
+    two_powers::D: CheckedArray<ARITY>,
+{
+    print!("{}", f.notation());
+    let alternate: Vec<_> = f
+        .alternate_notations()
+        .into_iter()
+        .flatten()
+        .map(|n| n.to_string())
+        .collect();
+    if alternate.is_empty() {
+        println!();
+    } else {
+        println!(" (aka {alternate:?})");
+    }
+
+    let table = f.get_truth_table();
+    println!("{table}");
+}
 
 fn main() {
     println!("=== NULLARY ===");
     for f in NULLARY_FUNCTIONS.iter() {
-        let table = f.get_truth_table();
-        println!("{table}");
+        print_stat(f);
         println!();
     }
 
     println!("=== UNARY ===");
     for f in UNARY_FUNCTIONS.iter() {
-        let table = f.get_truth_table();
-        println!("{table}");
+        print_stat(f);
         println!();
     }
 
     println!("=== BINARY ===");
     for f in BINARY_FUNCTIONS.iter() {
-        let table = f.get_truth_table();
-        println!("{table}");
+        print_stat(f);
         println!();
     }
 }

src/connective/mod.rs

@@ -22,7 +22,7 @@ pub use self::{
     ops::{Associativity, Commutativity, Converse, Negate},
     priority::{Prioritized, Priority},
     properties::{is_basis, is_complete, BoolFnExt},
-    storage::{AllFunctions, BINARY_FUNCTIONS, NULLARY_FUNCTIONS, UNARY_FUNCTIONS},
+    storage::{AllFunctions, StoredBoolFn, BINARY_FUNCTIONS, NULLARY_FUNCTIONS, UNARY_FUNCTIONS},
     traits::{BoolFn, Connective, FormulaComposer, Reducible, TruthFn},
     truth_table::TruthTable,
 };

src/connective/properties.rs

@@ -757,8 +757,9 @@ mod tests_completeness {
         let truly_sheffer_ids = SHEFFER_FNS.map(|f| (*f).type_id());
 
         let mut found_sheffers = 0;
-        for f in BINARY_FUNCTIONS.iter() {
-            if truly_sheffer_ids.contains(&(**f).type_id()) {
+        for &f in BINARY_FUNCTIONS.iter() {
+            let f: &dyn BoolFnExt<2> = f.up();
+            if truly_sheffer_ids.contains(&(*f).type_id()) {
                 assert!(f.is_sheffer());
                 assert!(is_basis(&[f]));
                 found_sheffers += 1;
@@ -830,10 +831,10 @@ mod tests_completeness {
         let all_ids: Vec<_> = BINARY_FUNCTIONS.iter().map(|f| (**f).type_id()).collect();
         dbg!(all_ids);
 
-        let all_pairs: Vec<_> = BINARY_FUNCTIONS
+        let all_pairs: Vec<[&dyn BoolFnExt<2>; 2]> = BINARY_FUNCTIONS
             .iter()
             .cartesian_product(BINARY_FUNCTIONS.iter())
-            .map(|(f1, f2)| [*f1, *f2])
+            .map(|(&f1, &f2)| [f1.up(), f2.up()])
             .collect();
         assert_eq!(all_pairs.len(), 256);
 
@@ -926,8 +927,8 @@ mod tests_completeness {
             .iter()
             .combinations(3)
             .map(|x| {
-                let x: Vec<_> = x.into_iter().copied().collect();
-                <[_; 3]>::try_from(x)
+                let x: Vec<_> = x.into_iter().copied().map(Upcast::up).collect();
+                <[&dyn BoolFnExt<2>; 3]>::try_from(x)
                     .unwrap_or_else(|_| unreachable!("combinations produce Vec-s of size 3"))
             })
             .collect();
@@ -1013,8 +1014,8 @@ mod tests_completeness {
             .iter()
             .combinations(4)
             .map(|x| {
-                let x: Vec<_> = x.into_iter().copied().collect();
-                <[_; 4]>::try_from(x)
+                let x: Vec<_> = x.into_iter().copied().map(Upcast::up).collect();
+                <[&dyn BoolFnExt<2>; 4]>::try_from(x)
                     .unwrap_or_else(|_| unreachable!("combinations produce Vec-s of size 3"))
             })
             .collect();

src/connective/storage.rs

@@ -1,12 +1,29 @@
-use super::{functions, BoolFnExt};
+use super::{functions, BoolFnExt, Connective};
 
-use crate::{arity::two_powers_of_two_powers::D, utils::dependent_array::CheckedStorage};
+use crate::{
+    arity::two_powers_of_two_powers::D,
+    utils::{dependent_array::CheckedStorage, upcast::Upcast},
+};
+
+/// Combination of [`BoolFnExt`] and [`Connective`] to allow to use in dyn context.
+///
+/// Implemented automatically for all `F: BoolFnExt + Connective`.
+pub trait StoredBoolFn<const ARITY: usize>:
+    BoolFnExt<ARITY> + Connective<ARITY> + Upcast<dyn BoolFnExt<ARITY>>
+{
+}
+
+impl<const ARITY: usize, F> StoredBoolFn<ARITY> for F where
+    F: BoolFnExt<ARITY> + Connective<ARITY> + Upcast<dyn BoolFnExt<ARITY>>
+{
+}
 
 /// This type stores all `BoolFnExt`-s for a given `ARITY`.
 ///
 /// Also, it allows to compare the given generic function
 /// (identified by their truth tables, TO BE DONE) with the [concrete ones][BoolFnExt].
-pub type AllFunctions<const ARITY: usize> = CheckedStorage<ARITY, D, &'static dyn BoolFnExt<ARITY>>;
+pub type AllFunctions<const ARITY: usize> =
+    CheckedStorage<ARITY, D, &'static dyn StoredBoolFn<ARITY>>;
 
 const _ASSERT_0: () = <AllFunctions<0>>::ASSERT_SIZE;
 const _ASSERT_1: () = <AllFunctions<1>>::ASSERT_SIZE;
@@ -15,14 +32,14 @@ const _ASSERT_2: () = <AllFunctions<2>>::ASSERT_SIZE;
 #[allow(trivial_casts)] // need to define at least one cast to prevent compile-error
 /// The array of 0-arity functions.
 pub const NULLARY_FUNCTIONS: AllFunctions<0> = CheckedStorage::new([
-    &functions::Falsity as &'static dyn BoolFnExt<0>,
+    &functions::Falsity as &'static dyn StoredBoolFn<0>,
     &functions::Truth,
 ]);
 
 #[allow(trivial_casts)] // need to define at least one cast to prevent compile-error
 /// The array of unary functions.
 pub const UNARY_FUNCTIONS: AllFunctions<1> = CheckedStorage::new([
-    &functions::Falsity as &'static dyn BoolFnExt<1>,
+    &functions::Falsity as &'static dyn StoredBoolFn<1>,
     &functions::LogicalIdentity,
     &functions::Negation,
     &functions::Truth,
@@ -34,22 +51,22 @@ type NProj1 = functions::ProjectAndUnary<1, functions::Negation>;
 #[allow(trivial_casts)] // need to define at least one cast to prevent compile-error
 /// The array of unary functions.
 pub const BINARY_FUNCTIONS: AllFunctions<2> = CheckedStorage::new([
-    &functions::Falsity as &'static dyn BoolFnExt<2>, // 0 0 0 0
-    &functions::Conjunction,                          // 0 0 0 1
-    &functions::MaterialNonImplication,               // 0 0 1 0
-    &functions::Projection::<0>,                      // 0 0 1 1
-    &functions::ConverseNonImplication,               // 0 1 0 0
-    &functions::Projection::<1>,                      // 0 1 0 1
-    &functions::ExclusiveDisjunction,                 // 0 1 1 0
-    &functions::Disjunction,                          // 0 1 1 1
-    &functions::NonDisjunction,                       // 1 0 0 0
-    &functions::LogicalBiconditional,                 // 1 0 0 1
-    &NProj1::new(),                                   // 1 0 1 0
-    &functions::ConverseImplication,                  // 1 0 1 1
-    &NProj0::new(),                                   // 1 1 0 0
-    &functions::MaterialImplication,                  // 1 1 0 1
-    &functions::NonConjunction,                       // 1 1 1 0
-    &functions::Truth,                                // 1 1 1 1
+    &functions::Falsity as &'static dyn StoredBoolFn<2>, // 0 0 0 0
+    &functions::Conjunction,                             // 0 0 0 1
+    &functions::MaterialNonImplication,                  // 0 0 1 0
+    &functions::Projection::<0>,                         // 0 0 1 1
+    &functions::ConverseNonImplication,                  // 0 1 0 0
+    &functions::Projection::<1>,                         // 0 1 0 1
+    &functions::ExclusiveDisjunction,                    // 0 1 1 0
+    &functions::Disjunction,                             // 0 1 1 1
+    &functions::NonDisjunction,                          // 1 0 0 0
+    &functions::LogicalBiconditional,                    // 1 0 0 1
+    &NProj1::new(),                                      // 1 0 1 0
+    &functions::ConverseImplication,                     // 1 0 1 1
+    &NProj0::new(),                                      // 1 1 0 0
+    &functions::MaterialImplication,                     // 1 1 0 1
+    &functions::NonConjunction,                          // 1 1 1 0
+    &functions::Truth,                                   // 1 1 1 1
 ]);
 
 #[cfg(test)]