diff --git a/Cargo.lock b/Cargo.lock index 3fa18ef1..bf05fd3f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -294,9 +294,9 @@ checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" [[package]] name = "cpufeatures" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ca741a962e1b0bff6d724a1a0958b686406e853bb14061f218562e1896f95e6" +checksum = "16b80225097f2e5ae4e7179dd2266824648f3e2f49d9134d584b76389d31c4c3" dependencies = [ "libc", ] @@ -335,7 +335,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13b588ba4ac1a99f7f2964d24b3d896ddc6bf847ee3855dbd4366f058cfcd331" dependencies = [ "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] @@ -359,7 +359,7 @@ dependencies = [ "proc-macro2", "quote", "rustc_version", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] @@ -515,7 +515,7 @@ checksum = "162ee34ebcb7c64a8abebc059ce0fee27c2262618d7b60ed8faf72fef13c3650" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] @@ -778,9 +778,9 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hashbrown" -version = "0.15.1" +version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" +checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" [[package]] name = "heck" @@ -825,7 +825,7 @@ checksum = "601cbb57e577e2f5ef5be8e7b83f0f63994f25aa94d673e54a92d5c516d101f1" dependencies = [ "bytes", "fnv", - "itoa 1.0.11", + "itoa 1.0.14", ] [[package]] @@ -854,7 +854,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" dependencies = [ "equivalent", - "hashbrown 0.15.1", + "hashbrown 0.15.2", ] [[package]] @@ -874,9 +874,9 @@ checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4" [[package]] name = "itoa" -version = "1.0.11" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" +checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674" [[package]] name = "jni" @@ -921,9 +921,9 @@ checksum = "884e2677b40cc8c339eaefcb701c32ef1fd2493d71118dc0ca4b6a736c93bd67" [[package]] name = "libc" -version = "0.2.162" +version = "0.2.166" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" +checksum = "c2ccc108bbc0b1331bd061864e7cd823c0cab660bbe6970e66e2c0614decde36" [[package]] name = "linux-raw-sys" @@ -1239,7 +1239,7 @@ checksum = "3c0f5fad0874fc7abcd4d750e76917eaebbecaa2c20bde22e1dbeeba8beb758c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] @@ -1322,9 +1322,9 @@ checksum = "dc375e1527247fe1a97d8b7156678dfe7c1af2fc075c9a4db3690ecd2a148068" [[package]] name = "proc-macro2" -version = "1.0.89" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" +checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0" dependencies = [ "unicode-ident", ] @@ -1497,9 +1497,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.40" +version = "0.38.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99e4ea3e1cdc4b559b8e5650f9c8e5998e3e5c1343b4eaf034565f32318d63c0" +checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6" dependencies = [ "bitflags 2.6.0", "errno", @@ -1605,16 +1605,16 @@ checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] name = "serde_json" -version = "1.0.132" +version = "1.0.133" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d726bfaff4b320266d395898905d0eba0345aae23b54aee3a737e260fd46db03" +checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377" dependencies = [ - "itoa 1.0.11", + "itoa 1.0.14", "memchr", "ryu", "serde", @@ -1627,7 +1627,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" dependencies = [ "form_urlencoded", - "itoa 1.0.11", + "itoa 1.0.14", "ryu", "serde", ] @@ -1744,9 +1744,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.87" +version = "2.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" +checksum = "44d46482f1c1c87acd84dea20c1bf5ebff4c757009ed6bf19cfd36fb10e92c4e" dependencies = [ "proc-macro2", "quote", @@ -1827,7 +1827,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] @@ -1862,9 +1862,9 @@ dependencies = [ [[package]] name = "tracing" -version = "0.1.40" +version = "0.1.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef" +checksum = "784e0ac535deb450455cbfa28a6f0df145ea1bb7ae51b821cf5e7927fdcfbdd0" dependencies = [ "pin-project-lite", "tracing-attributes", @@ -1873,20 +1873,20 @@ dependencies = [ [[package]] name = "tracing-attributes" -version = "0.1.27" +version = "0.1.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" +checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] [[package]] name = "tracing-core" -version = "0.1.32" +version = "0.1.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54" +checksum = "e672c95779cf947c5311f83787af4fa8fffd12fb27e4993211a84bdfd9610f9c" dependencies = [ "once_cell", ] @@ -1899,9 +1899,9 @@ checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" [[package]] name = "unicode-ident" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" +checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83" [[package]] name = "unicode-width" @@ -2075,7 +2075,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", "wasm-bindgen-shared", ] @@ -2109,7 +2109,7 @@ checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -2320,5 +2320,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.87", + "syn 2.0.89", ] diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 808cfdd8..21f57a99 100644 --- a/aris/src/expr.rs +++ b/aris/src/expr.rs @@ -28,9 +28,8 @@ assert_eq!(&handle_user_input("bad(missing, paren"), "unsuccessful parse"); use std::collections::BTreeSet; use std::collections::{HashMap, HashSet}; -use std::fmt; -use std::mem; use std::ops::Not; +use std::{fmt, mem}; use itertools::Itertools; use maplit::hashset; @@ -897,7 +896,7 @@ impl Expr { Expr::collect_unique_exprs_idempotence(&normalized_expr, op, &mut unique_exprs); } - // If there's only one unique expression, return it; otherwise, reassemble the expression + // If there's only one unique expression, return it. Otherwise, reassemble the expression let unique_exprs: Vec = unique_exprs.into_iter().collect(); if unique_exprs.len() == 1 { @@ -951,13 +950,51 @@ impl Expr { } } + fn collect_reduction_exprs(expr: &Expr, op: Op, reduced_exprs: &mut BTreeSet) { + match expr { + Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { + exprs.iter().for_each(|sub_expr| Self::collect_reduction_exprs(sub_expr, op, reduced_exprs)); + } + Expr::Assoc { op: inner_op, exprs } if (op, *inner_op) == (Op::And, Op::Or) || (op, *inner_op) == (Op::Or, Op::And) => { + let (mut other_terms, mut negated_match) = (vec![], None); + + for sub_expr in exprs { + match sub_expr { + Expr::Not { operand } => { + if Self::is_subset_of_assoc(operand, reduced_exprs, Op::And) { + negated_match = Some(sub_expr.clone()); + } else { + other_terms.push(sub_expr.clone()); + } + } + _ if reduced_exprs.contains(&Expr::Not { operand: Box::new(sub_expr.clone()) }) => { + negated_match = Some(sub_expr.clone()); + } + _ => other_terms.push(sub_expr.clone()), + } + } + + if negated_match.is_some() { + reduced_exprs.extend(other_terms); + } else { + reduced_exprs.insert(expr.clone()); + } + } + Expr::Quant { kind, name, body } => { + reduced_exprs.insert(Expr::Quant { kind: *kind, name: name.clone(), body: Box::new(body.clone().normalize_reduction()) }); + } + _ => { + reduced_exprs.insert(expr.clone()); + } + } + } + pub fn normalize_reduction(self) -> Expr { match self { - // Handle Associative operations (AND/OR) Expr::Assoc { op, exprs } => { let mut reduced_exprs = BTreeSet::new(); - // Recurse through the expressions inside the Assoc operation + // Recurse through the expressions for expr in exprs { let normalized_expr = expr.normalize_reduction(); Self::collect_reduction_exprs(&normalized_expr, op, &mut reduced_exprs); @@ -968,75 +1005,127 @@ impl Expr { let first = expr_iter.next().unwrap(); let second = expr_iter.next().unwrap(); - // Check if the second expression is a quantifier if let Expr::Quant { kind, name, body } = second { return Expr::Assoc { op: Op::Or, exprs: vec![first, Expr::Quant { kind, name, body }] }; } } + Expr::Assoc { op, exprs: reduced_exprs.into_iter().collect() } } - // Recursively normalize quantifier body + + // If the expression is a quantifier, recursively normalize its body Expr::Quant { kind, name, body } => { let normalized_body = body.normalize_reduction(); Expr::Quant { kind, name, body: Box::new(normalized_body) } } + // If the expression is a negation, attempt to simplify the negated quantifier - Expr::Not { operand } => { - match *operand { - // If the operand is a quantifier, recursively normalize its body - Expr::Quant { kind, name, body } => { - let normalized_body = body.normalize_reduction(); - Expr::Quant { kind, name, body: Box::new(normalized_body) } - } - _ => Expr::Not { operand: Box::new(operand.normalize_reduction()) }, + Expr::Not { operand } => match *operand { + Expr::Quant { kind, name, body } => { + let normalized_body = body.normalize_reduction(); + Expr::Quant { kind, name, body: Box::new(normalized_body) } } - } + _ => Expr::Not { operand: Box::new(operand.normalize_reduction()) }, + }, + _ => self, } } - fn collect_reduction_exprs(expr: &Expr, op: Op, reduced_exprs: &mut BTreeSet) { + fn is_subset_of_assoc(expr: &Expr, set: &BTreeSet, op: Op) -> bool { match expr { - // If the expression is an associative operation with the same operator, recurse into its subexpressions - Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { - for sub_expr in exprs { - Self::collect_reduction_exprs(sub_expr, op, reduced_exprs); + Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().all(|sub_expr| set.contains(sub_expr)), + single_expr => set.contains(single_expr), + } + } + + pub fn normalize_adjacency(self) -> Expr { + match self { + Expr::Assoc { op, exprs } => { + let unique_exprs = exprs.into_iter().flat_map(|e| e.normalize_adjacency().extract_associative(op)).collect::>(); + + match Self::simplify_general(unique_exprs.clone(), op) { + Some(simplified) => simplified, + None => match unique_exprs.len() { + 1 => unique_exprs.into_iter().next().unwrap(), + _ => Expr::Assoc { op, exprs: unique_exprs }, + }, } } - // If the expression involves an AND/OR between a quantifier and another expression, handle simplifications - Expr::Assoc { op: inner_op, exprs } => match (op, inner_op) { - (Op::And, Op::Or) | (Op::Or, Op::And) => { - let mut other_terms = vec![]; - let mut negated_match = None; - for sub_expr in exprs { - match sub_expr { - // If the subexpression involves a negated quantifier, simplify it - Expr::Not { operand } if reduced_exprs.contains(operand) => { - negated_match = Some(operand.as_ref().clone()); - } - _ => other_terms.push(sub_expr.clone()), - } - } - if negated_match.is_some() { - reduced_exprs.extend(other_terms); - } else { - reduced_exprs.insert(expr.clone()); - } - } - _ => { - reduced_exprs.insert(expr.clone()); - } - }, - // Simplify quantifier body Expr::Quant { kind, name, body } => { - let normalized_body = body.clone().normalize_reduction(); - let simplified_expr = Expr::Quant { kind: *kind, name: name.clone(), body: Box::new(normalized_body) }; - reduced_exprs.insert(simplified_expr); + // Normalize the body of the quantifier + let normalized_body = body.normalize_adjacency(); + Expr::Quant { kind, name, body: Box::new(normalized_body) } } - _ => { - reduced_exprs.insert(expr.clone()); + _ => self, + } + } + + fn extract_associative(self, op: Op) -> Vec { + match self { + Expr::Assoc { op: expr_op, exprs } if expr_op == op => exprs, + _ => vec![self], + } + } + + fn simplify_general(mut exprs: Vec, op: Op) -> Option { + for i in 0..exprs.len() { + for j in (i + 1..exprs.len()).rev() { + if let Some(simplified) = Self::try_simplify_pair(&exprs[i], &exprs[j], op) { + exprs.swap_remove(j); + exprs[i] = simplified; + return Self::simplify_general(exprs, op); // Restart with updated list + } } } + exprs.sort(); + exprs.dedup(); + match exprs.len() { + 0 => None, + 1 => Some(exprs.into_iter().next().unwrap()), + _ => Some(Expr::Assoc { op, exprs }), + } + } + + fn try_simplify_pair(e1: &Expr, e2: &Expr, op: Op) -> Option { + match op { + Op::Or | Op::And => Self::simplify_logic(e1, e2), + _ => None, + } + } + + fn simplify_logic(e1: &Expr, e2: &Expr) -> Option { + match (e1, e2) { + (Expr::Assoc { op: sub_op1, exprs: exprs1 }, Expr::Assoc { op: sub_op2, exprs: exprs2 }) if *sub_op1 == *sub_op2 => { + let common: Vec<_> = exprs1.iter().filter(|e| exprs2.contains(e)).cloned().collect(); + if common.is_empty() { + return None; + } + let rest1: Vec<_> = exprs1.iter().filter(|e| !common.contains(*e)).collect(); + let rest2: Vec<_> = exprs2.iter().filter(|e| !common.contains(*e)).collect(); + if Self::is_complementary(&rest1, &rest2) { + return Some(Self::assoc_or_single(common, *sub_op1)); + } + } + _ => {} + } + None + } + + fn assoc_or_single(mut exprs: Vec, op: Op) -> Expr { + exprs.sort(); + exprs.dedup(); + match exprs.len() { + 1 => exprs.pop().unwrap(), + _ => Expr::Assoc { op, exprs }, + } + } + + fn is_complementary(others1: &[&Expr], others2: &[&Expr]) -> bool { + matches!( + (others1, others2), + ([Expr::Not { operand: o1 }], [e2]) | ([e2], [Expr::Not { operand: o1 }]) if **o1 == **e2 + ) } /// Helper function for complement quantified expressions @@ -1399,46 +1488,67 @@ impl Expr { }) } - /// Distribute forall/exists into and/or - pub fn quantifier_distribution(self) -> Expr { - let push_quantifier_inside = |kind: QuantKind, qname: String, exprs: &mut Vec| { - for iter in exprs.iter_mut() { - match kind { - QuantKind::Exists => { - let tmp = mem::replace(iter, Expr::Contra); - *iter = Expr::exists(qname.as_str(), tmp); + pub fn quantifier_inference(self) -> Expr { + let distribute_quantifiers = |expr: &Expr| -> Option { + match expr { + // (∃ x (P(x) ∧ Q(x))) => ((∃ x P(x)) ∧ (∃ x Q(x))) + Expr::Quant { kind: QuantKind::Exists, name, body } if matches!(body.as_ref(), Expr::Assoc { op: Op::And, .. }) => { + if let Expr::Assoc { op: Op::And, exprs } = body.as_ref() { + let distributed = exprs.iter().map(|inner| Expr::exists(name, inner.clone())).collect::>(); + return Some(Expr::assoc(Op::And, &distributed)); } - - QuantKind::Forall => { - let tmp = mem::replace(iter, Expr::Contra); - *iter = Expr::forall(qname.as_str(), tmp); + } + // ((∀ x P(x)) ∨ (∀ x Q(x))) => (∀ x (P(x) ∨ Q(x))) + Expr::Assoc { op: Op::Or, exprs } if exprs.iter().all(|e| matches!(e, Expr::Quant { kind: QuantKind::Forall, .. })) => { + let names_and_bodies: Vec<(&str, &Expr)> = exprs + .iter() + .filter_map(|e| match e { + Expr::Quant { kind: QuantKind::Forall, name, body } => Some((name.as_str(), body.as_ref())), + _ => None, + }) + .collect(); + + let first_name = names_and_bodies[0].0; + if names_and_bodies.iter().all(|(name, _)| name == &first_name) { + let combined_body = Expr::assoc(Op::Or, &names_and_bodies.iter().map(|(_, body)| (*body).clone()).collect::>()); + return Some(Expr::forall(first_name, combined_body)); } } + _ => {} } + None }; - self.transform(&|expr| { - let orig_expr = expr.clone(); + self.transform(&|expr| distribute_quantifiers(&expr).map_or((expr.clone(), false), |transformed| (transformed, true))) + } - match expr { - Expr::Quant { kind, name, body } => { - match *body { - Expr::Assoc { op, mut exprs } => { - // continue only if op is And or Or - match op { - Op::And | Op::Or => {} - _ => return (orig_expr, false), - }; - - // inline push_quantifier_inside here - push_quantifier_inside(kind, name, &mut exprs); - (Expr::assoc(op, &exprs), true) - } - _ => (orig_expr, false), + pub fn quantifier_distribution(self) -> Expr { + let push_quantifier_inside = |kind: QuantKind, qname: String, exprs: &mut Vec| { + exprs.iter_mut().for_each(|iter| { + let tmp = mem::replace(iter, Expr::Contra); + *iter = match kind { + QuantKind::Exists => Expr::exists(qname.as_str(), tmp), + QuantKind::Forall => Expr::forall(qname.as_str(), tmp), + }; + }); + }; + + self.transform(&|expr| match expr.clone() { + Expr::Quant { kind, name, body } => match *body { + Expr::Assoc { op, mut exprs } => match op { + Op::And if kind == QuantKind::Forall => { + push_quantifier_inside(kind, name, &mut exprs); + (Expr::assoc(Op::And, &exprs), true) } - } - _ => (expr, false), - } + Op::Or if kind == QuantKind::Exists => { + push_quantifier_inside(kind, name, &mut exprs); + (Expr::assoc(Op::Or, &exprs), true) + } + _ => (expr.clone(), false), + }, + _ => (expr.clone(), false), + }, + _ => (expr, false), }) } diff --git a/aris/src/parser.rs b/aris/src/parser.rs index 4c35df14..4e32f92b 100644 --- a/aris/src/parser.rs +++ b/aris/src/parser.rs @@ -102,7 +102,22 @@ fn conditional_space(input: &str) -> IResult<&str, ()> { } fn binder(input: &str) -> IResult<&str, Expr> { - map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(conditional_space, expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input) + map( + tuple(( + preceded(space, quantifier), + preceded(space, variable), + preceded( + conditional_space, + alt(( + // Parse multiple terms enclosed in parentheses + delimited(tuple((space, tag("("), space)), expr, tuple((space, tag(")"), space))), + // Parse a single term without parentheses + paren_expr, + )), + ), + )), + |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) }, + )(input) } fn impl_term(input: &str) -> IResult<&str, Expr> { @@ -180,10 +195,10 @@ fn test_parser() { println!("{:?}", predicate("s(s(s(s(s(z)))))")); println!("{:?}", expr("a & b & c(x,y)\n")); println!("{:?}", expr("forall a (b & c)\n")); - let e = expr("exists x (Tet(x) & SameCol(x, b)) -> ~forall x (Tet(x) -> LeftOf(x, b))\n").unwrap(); + let e = expr("exists x ((Tet(x) & SameCol(x, b)) -> ~forall x (Tet(x) -> LeftOf(x, b)))\n").unwrap(); let fv = free_vars(&e.1); println!("{e:?} {fv:?}"); - let e = expr("forall a forall b ((forall x in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap(); + let e = expr("forall a (forall b (((forall x (in(x,a) <-> in(x,b)) -> eq(a,b)))))\n").unwrap(); let fv = free_vars(&e.1); assert_eq!(fv, ["eq", "in"].iter().map(|x| String::from(*x)).collect()); println!("{e:?} {fv:?}"); diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index bb9f13fa..959d6f68 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -489,8 +489,8 @@ where (r5, r6, r7) }) .unwrap(); - let r8 = prf.add_step(Justification(p("forall y p(y) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); - let r9 = prf.add_step(Justification(p("forall y p(a) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); + let r8 = prf.add_step(Justification(p("forall y (p(y) & q(y))"), RuleM::ForallIntro, vec![], vec![r4.clone()])); + let r9 = prf.add_step(Justification(p("forall y (p(a) & q(y))"), RuleM::ForallIntro, vec![], vec![r4.clone()])); let r10 = prf.add_subproof(); let r11 = prf .with_mut_subproof(&r10, |sub| { @@ -514,7 +514,7 @@ where (r17, r18) }) .unwrap(); - let r19 = sub1.add_step(Justification(p("forall x forall y s(x, y)"), RuleM::ForallIntro, vec![], vec![r14])); + let r19 = sub1.add_step(Justification(p("forall x (forall y s(x, y))"), RuleM::ForallIntro, vec![], vec![r14])); (r17, r18, r19) }) .unwrap(); @@ -546,13 +546,13 @@ where let r3 = prf.add_step(Justification(p("exists x p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); let r4 = prf.add_step(Justification(p("exists x p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); let r5 = prf.add_step(Justification(p("exists x p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![])); - let r6 = prf.add_step(Justification(p("exists x p(x) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r7 = prf.add_step(Justification(p("exists x p(b) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r8 = prf.add_step(Justification(p("exists x p(x) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r9 = prf.add_step(Justification(p("exists x p(b) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r10 = prf.add_step(Justification(p("exists x p(y) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r11 = prf.add_step(Justification(p("exists x p(a) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r12 = prf.add_step(Justification(p("exists x p(y) & p(x)"), RuleM::ExistsIntro, vec![i(r2)], vec![])); + let r6 = prf.add_step(Justification(p("exists x (p(x) & p(x))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("exists x (p(b) & p(x))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("exists x (p(x) & p(b))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r9 = prf.add_step(Justification(p("exists x (p(b) & p(b))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r10 = prf.add_step(Justification(p("exists x (p(y) & p(b))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r11 = prf.add_step(Justification(p("exists x (p(a) & p(b))"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r12 = prf.add_step(Justification(p("exists x (p(y) & p(x))"), RuleM::ExistsIntro, vec![i(r2)], vec![])); (prf, vec![i(r3), i(r4), i(r6), i(r7), i(r8), i(r9)], vec![i(r5), i(r10), i(r11), i(r12)]) } @@ -584,7 +584,7 @@ where let r12 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); let r13 = prf.add_step(Justification(p("r(a)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); - let s1 = prf.add_premise(p("forall y man(y) → mortal(y)")); + let s1 = prf.add_premise(p("forall y (man(y) → mortal(y))")); let s2 = prf.add_premise(p("exists x man(x)")); let s3 = prf.add_subproof(); let (s5, s6, s7) = prf @@ -592,7 +592,7 @@ where let s4 = sub.add_premise(p("man(socrates)")); let s5 = sub.add_step(Justification(p("man(socrates) → mortal(socrates)"), RuleM::ForallElim, vec![i(s1.clone())], vec![])); let s6 = sub.add_step(Justification(p("mortal(socrates)"), RuleM::ImpElim, vec![i(s4), i(s5.clone())], vec![])); - let s7 = sub.add_step(Justification(p("exists foo mortal(foo)"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![])); + let s7 = sub.add_step(Justification(p("exists foo (mortal(foo))"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![])); (s5, s6, s7) }) .unwrap(); @@ -611,11 +611,11 @@ where let t6 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![t2.clone()])); let u1 = prf.add_subproof(); - let u2 = prf.add_premise(p("forall c forall d p(c) -> s(d)")); + let u2 = prf.add_premise(p("forall c (forall d (p(c) -> s(d)))")); let (u4, u5, u6) = prf .with_mut_subproof(&u1, |sub| { let u3 = sub.add_premise(p("p(a)")); - let u4 = sub.add_step(Justification(p("forall d p(a) -> s(d)"), RuleM::ForallElim, vec![i(u2.clone())], vec![])); + let u4 = sub.add_step(Justification(p("forall d (p(a) -> s(d))"), RuleM::ForallElim, vec![i(u2.clone())], vec![])); let u5 = sub.add_step(Justification(p("p(a) -> s(foo)"), RuleM::ForallElim, vec![i(u4.clone())], vec![])); // TODO: generalized forall? let u6 = sub.add_step(Justification(p("s(foo)"), RuleM::ImpElim, vec![i(u3), i(u5.clone())], vec![])); (u4, u5, u6) @@ -958,20 +958,22 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let p2 = prf.add_premise(p("(~~A | B) & ~A")); let p3 = prf.add_premise(p("(B & ~A) | A")); let p4 = prf.add_premise(p("~B | (A & ~~B)")); - let p5 = prf.add_premise(p("(forall A (A & (~A | B))) | (~(forall A (A & (~A | B))) & C)")); + // let p5 = prf.add_premise(p("(forall A (A & (~A | B))) | (~(forall A (A & (~A | B))) & C)")); let p6 = prf.add_premise(p("B & (C | (~C & ~A))")); let p7 = prf.add_premise(p("A | (~A & (~~A | B))")); let p8 = prf.add_premise(p("D | (~A & (~~A | B))")); let p9 = prf.add_premise(p("P & M & (~P | Q)")); let p10 = prf.add_premise(p("P | M | (~P & Q)")); - // let p11 = prf.add_premise(p("~P & (P | Q)")); + + let p11 = prf.add_premise(p("~P & (P | Q)")); + let p12 = prf.add_premise(p("P & M & (~(P & M) | Q)")); + let p13 = prf.add_premise(p("(forall A (A & B)) | (~(forall A (A & B)) & C)")); let r1 = prf.add_step(Justification(p("A & B"), RuleM::Reduction, vec![i(p1.clone())], vec![])); let r2 = prf.add_step(Justification(p("~A & B"), RuleM::Reduction, vec![i(p2.clone())], vec![])); let r3 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p3.clone())], vec![])); let r4 = prf.add_step(Justification(p("~B | A"), RuleM::Reduction, vec![i(p4.clone())], vec![])); - // let r18 = prf.add_step(Justification(p("¬P ∧ Q"), RuleM::Reduction, vec![i(p11.clone())], vec![])); - let r5 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p5)], vec![])); + // let r5 = prf.add_step(Justification(p("(forall A (A & B)) | (~(forall A (A & B)) & C)"), RuleM::Reduction, vec![i(p5)], vec![])); let r6 = prf.add_step(Justification(p("A"), RuleM::Reduction, vec![i(p1)], vec![])); let r7 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p2)], vec![])); @@ -988,7 +990,11 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let r16 = prf.add_step(Justification(p("P | M | Q"), RuleM::Reduction, vec![i(p10.clone())], vec![])); let r17 = prf.add_step(Justification(p("(P | M) & Q"), RuleM::Reduction, vec![i(p10)], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r10), i(r12), i(r13), i(r14), i(r16)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) + let r18 = prf.add_step(Justification(p("~P & Q"), RuleM::Reduction, vec![i(p11.clone())], vec![])); + let r19 = prf.add_step(Justification(p("P & M & Q"), RuleM::Reduction, vec![i(p12.clone())], vec![])); + let r20 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p13)], vec![])); + + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r19), i(r18), i(r10), i(r12), i(r13), i(r14), i(r16), i(r20)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) } pub fn test_adjacency() -> (P, Vec>, Vec>) { @@ -998,6 +1004,10 @@ pub fn test_adjacency() -> (P, Vec>, Vec>) { let p1 = prf.add_premise(p("(A & B) | (A & ~B)")); let p2 = prf.add_premise(p("(A | B) & (A | ~B)")); + let p3 = prf.add_premise(p("(¬(P∧M) ∨ Q) ∧ ((P∧M) ∨ Q)")); + let p4 = prf.add_premise(p("(¬(P∧M) ∨ Q) ∧ ((P) ∨ Q)")); + let p5 = prf.add_premise(p("(A | B) & M & (A | ~B)")); + let p6 = prf.add_premise(p("(M ∨ (P ∧ Q ∧ W) ∨ (P ∧ W ∧ ¬Q))")); let r1 = prf.add_step(Justification(p("A"), RuleM::Adjacency, vec![i(p1.clone())], vec![])); let r2 = prf.add_step(Justification(p("A"), RuleM::Adjacency, vec![i(p2.clone())], vec![])); @@ -1007,7 +1017,12 @@ pub fn test_adjacency() -> (P, Vec>, Vec>) { let r5 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p1)], vec![])); let r6 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p2)], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4)], vec![i(r5), i(r6)]) + let r7 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p3)], vec![])); + let r8 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p4)], vec![])); + let r9 = prf.add_step(Justification(p("A & M"), RuleM::Adjacency, vec![i(p5.clone())], vec![])); + + let r10 = prf.add_step(Justification(p("(P & W) | M"), RuleM::Adjacency, vec![i(p6.clone())], vec![])); + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r7), i(r9), i(r10)], vec![i(r5), i(r6), i(r8)]) } pub fn test_resolution() -> (P, Vec>, Vec>) { @@ -1202,9 +1217,9 @@ pub fn test_weak_induction() -> (P, Vec>, Vec>) { use crate::parser::parse_unwrap as p; let mut prf = P::new(); let r1 = prf.add_premise(p("~LessThan(0,0)")); - let r2 = prf.add_premise(p("forall x ~LessThan(x,x) -> ~LessThan(s(x),s(x))")); + let r2 = prf.add_premise(p("forall x (~LessThan(x,x) -> ~LessThan(s(x),s(x)))")); let r3 = prf.add_premise(p("Equals(0,0)")); - let r4 = prf.add_premise(p("forall 0 Equals(0,0) -> Equals(s(0),s(0))")); + let r4 = prf.add_premise(p("forall 0 (Equals(0,0) -> Equals(s(0),s(0)))")); let r5 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); let r6 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r2.clone()), i(r1.clone())], vec![])); let r7 = prf.add_step(Justification(p("forall n ~LessThan(n,n)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); @@ -1217,8 +1232,8 @@ pub fn test_strong_induction() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); - let r1 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x)) -> P(n)")); - let r2 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x,n)) -> P(n,n)")); + let r1 = prf.add_premise(p("forall n (forall x (LessThan(x, n) -> P(x)) -> P(n))")); + let r2 = prf.add_premise(p("forall n (forall x (LessThan(x, n) -> P(x,n)) -> P(n,n))")); let r3 = prf.add_step(Justification(p("forall x P(x)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); let r4 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); let r5 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![])); diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 771d9b9d..89a618d2 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -165,6 +165,7 @@ pub enum RedundantPrepositionalInference { ExcludedMiddle, ConstructiveDilemma, HalfDeMorgan, + QuantifierInference, } #[allow(missing_docs)] @@ -321,6 +322,7 @@ pub mod RuleM { [ExcludedMiddle, "EXCLUDED_MIDDLE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ExcludedMiddle))))))))], [ConstructiveDilemma, "CONSTRUCTIVE_DILEMMA", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ConstructiveDilemma))))))))], [HalfDeMorgan, "HALF_DE_MORGAN", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::HalfDeMorgan))))))))], + [QuantifierInference, "QUANTIFIER_INFERENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::QuantifierInference))))))))], [Resolution, "RESOLUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::Resolution)))))))))], [TruthFunctionalConsequence, "TRUTHFUNCTIONAL_CONSEQUENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::TruthFunctionalConsequence)))))))))], @@ -536,7 +538,6 @@ impl RuleT for PrepositionalInference { fn check(self, p: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { use PrepositionalInference::*; use ProofCheckError::*; - match self { Reit => { let prem = p.lookup_expr_or_die(&deps[0])?; @@ -547,6 +548,12 @@ impl RuleT for PrepositionalInference { } } AndIntro => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } if let Expr::Assoc { op: Op::And, ref exprs } = conclusion { // ensure each dep appears in exprs for d in deps.iter() { @@ -567,6 +574,12 @@ impl RuleT for PrepositionalInference { } } AndElim => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::And, ref exprs } = prem { let premise_set: HashSet<_> = exprs.iter().collect(); @@ -592,6 +605,12 @@ impl RuleT for PrepositionalInference { } } OrIntro => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::Or, ref exprs } = conclusion { if !exprs.iter().any(|e| e == &prem) { @@ -603,6 +622,12 @@ impl RuleT for PrepositionalInference { } } OrElim => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::Or, ref exprs } = prem { let sproofs = sdeps.into_iter().map(|r| p.lookup_subproof_or_die(&r)).collect::, _>>()?; @@ -1020,11 +1045,13 @@ where F: Fn(Expr) -> Expr, { let mut premise = p.lookup_expr_or_die(&deps[0])?; + let mut conclusion_mut = conclusion; if commutative { premise = premise.sort_commutative_ops(restriction); + conclusion_mut = conclusion_mut.sort_commutative_ops(restriction); } let mut p = normalize_fn(premise.clone()); - let mut q = normalize_fn(conclusion); + let mut q = normalize_fn(conclusion_mut); if commutative { p = p.sort_commutative_ops(restriction); q = q.sort_commutative_ops(restriction); @@ -1036,6 +1063,19 @@ where } } +fn check_by_normalize_first_expr_one_way(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> +where + F: Fn(Expr) -> Expr, +{ + let premise = p.lookup_expr_or_die(&deps[0])?; + let p = normalize_fn(premise.clone()); + if p == conclusion.clone() { + Ok(()) + } else { + Err(ProofCheckError::Other(format!("{p} and {conclusion} are not equal. {:?}", premise))) + } +} + fn check_by_normalize_multiple_possibilities(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> where F: Fn(Expr) -> Vec, @@ -1128,7 +1168,7 @@ impl RuleT for BooleanEquivalence { Inverse => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::INVERSE, "none"), Absorption => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_absorption(), "none"), Reduction => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_reduction(), "none"), - Adjacency => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::ADJACENCY, "none"), + Adjacency => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_adjacency(), "none"), } } } @@ -1229,6 +1269,7 @@ impl RuleT for RedundantPrepositionalInference { ExcludedMiddle => "Excluded Middle", ConstructiveDilemma => "Constructive Dilemma", HalfDeMorgan => "Half DeMorgan", + QuantifierInference => "Quantifier Inference", } .into() } @@ -1241,7 +1282,7 @@ impl RuleT for RedundantPrepositionalInference { ModusTollens | HypotheticalSyllogism | DisjunctiveSyllogism => Some(2), ExcludedMiddle => Some(0), ConstructiveDilemma => Some(3), - HalfDeMorgan => Some(1), + HalfDeMorgan | QuantifierInference => Some(1), } } fn num_subdeps(&self) -> Option { @@ -1414,6 +1455,7 @@ impl RuleT for RedundantPrepositionalInference { ) } HalfDeMorgan => check_by_normalize_multiple_possibilities(proof, deps, conclusion, |e| e.normalize_halfdemorgans()), + QuantifierInference => check_by_normalize_first_expr_one_way(proof, deps, conclusion, |e| e.quantifier_inference()), } } } diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs index ff65423c..3aea749d 100644 --- a/web-app/src/components/proof_widget/mod.rs +++ b/web-app/src/components/proof_widget/mod.rs @@ -166,90 +166,44 @@ impl ProofWidget { /// /// [lib]: https://github.com/vsn4ik/bootstrap-submenu fn render_rules_menu(&self, ctx: &Context, jref:

::JustificationReference, cur_rule_name: &str) -> Html { - let menu = RuleClassification::iter() - .map(|rule_class| { - let rules = rule_class - .rules() - .map(|rule| { - let pjref = Coproduct::inject(jref); - - // Determine the folder for the current theme - let get_folder = || { - if theme() == "dark" { - "proofImages_dark" - } else { - "proofImages_light" - } - }; - let image_src = format!("{}/{}.png", get_folder(), rule.get_name()); - - html! { -

- - {rule.get_name()} -
- } - }) - .collect::>(); + let equivalence_classes = [RuleClassification::BooleanEquivalence, RuleClassification::ConditionalEquivalence, RuleClassification::BiconditionalEquivalence, RuleClassification::QuantifierEquivalence]; + + let render_rules = |rules: Vec| { + rules + .into_iter() + .map(|rule| { + let pjref = Coproduct::inject(jref); + let image_src = format!("{}/{}.png", if theme() == "dark" { "proofImages_dark" } else { "proofImages_light" }, rule.get_name()); + html! { + + } + }) + .collect::>() + }; - let rules = yew::virtual_dom::VList::with_children(rules, None); + let render_class = |rule_class: RuleClassification| { + let rules = render_rules(rule_class.rules().collect()); + html! { +
+ +
{ rules }
+
+ } + }; - html! { -
- -
{ rules }
-
- } - }) - .collect::>(); - let menu = yew::virtual_dom::VList::with_children(menu, None); + let equivalence_submenu = equivalence_classes.iter().map(|&class| render_class(class)).collect::>(); + let non_equivalence_menu = RuleClassification::iter().filter(|class| !equivalence_classes.contains(class)).map(render_class).collect::>(); html! {
@@ -257,7 +211,11 @@ impl ProofWidget { { cur_rule_name }
- { menu } + { non_equivalence_menu } +
+ +
{ equivalence_submenu }
+
} @@ -266,8 +224,7 @@ impl ProofWidget { fn render_justification_widget(&self, ctx: &Context, jref:

::JustificationReference) -> Html { let just = self.prf.lookup_justification_or_die(&jref).expect("proofref should exist in self.prf"); - // Iterator over line dependency badges, for rendering list of - // dependencies + // Iterator over line dependency badges, for rendering list of dependencies let dep_badges = just.2.iter().map(|dep| { let (dep_line, _) = self.pud.ref_to_line_depth[dep]; html! { @@ -275,8 +232,7 @@ impl ProofWidget { } }); - // Iterator over subproof dependency badges, for rendering list of - // dependencies + // Iterator over subproof dependency badges, for rendering list of dependencies let sdep_badges = just.3.iter().filter_map(|sdep| self.prf.lookup_subproof(sdep)).map(|sub| { let (mut lo, mut hi) = (usize::MAX, usize::MIN); for line in sub.premises().into_iter().map(Coproduct::inject).chain(sub.direct_lines().into_iter().map(Coproduct::inject)) { @@ -897,26 +853,7 @@ impl Component for ProofWidget { } } - fn rendered(&mut self, _: &Context, first_render: bool) { + fn rendered(&mut self, _: &Context, _: bool) { js_sys::eval("$('[data-submenu]').submenupicker(); $('[data-toggle=popover]').popover()").unwrap_throw(); - if !first_render { - let js = r#" - document.querySelectorAll('.dropdown-item').forEach(item => { - const imgId = `tooltip-img-${item.innerText.trim().replace(/\s+/g, '_')}`; - const imgElem = document.getElementById(imgId); - item.addEventListener('mouseover', function() { - if (imgElem) { - imgElem.style.display = 'block'; - } - }); - item.addEventListener('mouseout', function() { - if (imgElem) { - imgElem.style.display = 'none'; - } - }); - }); - "#; - js_sys::eval(js).unwrap_throw(); - } } } diff --git a/web-app/static/dark-theme.css b/web-app/static/dark-theme.css index ccf7397f..415a59da 100644 --- a/web-app/static/dark-theme.css +++ b/web-app/static/dark-theme.css @@ -163,3 +163,28 @@ background-color: black; } +[theme="dark"] .tooltip { + overflow: visible; +} + +[theme="dark"] .tooltip-inner { + border: 3px solid white; + padding: 4px; +} + +/* Tooltip Arrow Colors in Dark Mode */ +[theme="dark"] .bs-tooltip-bottom .arrow::before { + border-bottom-color: white; +} + +[theme="dark"] .bs-tooltip-top .arrow::before { + border-top-color: white; +} + +[theme="dark"] .bs-tooltip-left .arrow::before { + border-left-color: white; +} + +[theme="dark"] .bs-tooltip-right .arrow::before { + border-right-color: white; +} \ No newline at end of file diff --git a/web-app/static/proofImages_dark/Disjunctive Syllogism.png b/web-app/static/proofImages_dark/Disjunctive Syllogism.png index b95af5dc..58533cc3 100644 Binary files a/web-app/static/proofImages_dark/Disjunctive Syllogism.png and b/web-app/static/proofImages_dark/Disjunctive Syllogism.png differ diff --git a/web-app/static/proofImages_dark/Quantifier Distribution.png b/web-app/static/proofImages_dark/Quantifier Distribution.png index 2c69b19b..635041c8 100644 Binary files a/web-app/static/proofImages_dark/Quantifier Distribution.png and b/web-app/static/proofImages_dark/Quantifier Distribution.png differ diff --git a/web-app/static/proofImages_dark/Quantifier Inference.png b/web-app/static/proofImages_dark/Quantifier Inference.png new file mode 100644 index 00000000..b3f94158 Binary files /dev/null and b/web-app/static/proofImages_dark/Quantifier Inference.png differ diff --git "a/web-app/static/proofImages_dark/\342\211\241 Introduction.png" "b/web-app/static/proofImages_dark/\342\211\241 Introduction.png" index 7abf8bdb..8d4e6ea7 100644 Binary files "a/web-app/static/proofImages_dark/\342\211\241 Introduction.png" and "b/web-app/static/proofImages_dark/\342\211\241 Introduction.png" differ diff --git a/web-app/static/proofImages_light/Disjunctive Syllogism.png b/web-app/static/proofImages_light/Disjunctive Syllogism.png index 6dfdc11f..83414494 100644 Binary files a/web-app/static/proofImages_light/Disjunctive Syllogism.png and b/web-app/static/proofImages_light/Disjunctive Syllogism.png differ diff --git a/web-app/static/proofImages_light/Quantifier Distribution.png b/web-app/static/proofImages_light/Quantifier Distribution.png index 9cb0373d..ca17c0ed 100644 Binary files a/web-app/static/proofImages_light/Quantifier Distribution.png and b/web-app/static/proofImages_light/Quantifier Distribution.png differ diff --git a/web-app/static/proofImages_light/Quantifier Inference.png b/web-app/static/proofImages_light/Quantifier Inference.png new file mode 100644 index 00000000..b85bc64c Binary files /dev/null and b/web-app/static/proofImages_light/Quantifier Inference.png differ diff --git "a/web-app/static/proofImages_light/\342\211\241 Introduction.png" "b/web-app/static/proofImages_light/\342\211\241 Introduction.png" index 2d1aacfa..77a99f25 100644 Binary files "a/web-app/static/proofImages_light/\342\211\241 Introduction.png" and "b/web-app/static/proofImages_light/\342\211\241 Introduction.png" differ diff --git a/web-app/static/styles.css b/web-app/static/styles.css index dbe4cc6f..afddb198 100644 --- a/web-app/static/styles.css +++ b/web-app/static/styles.css @@ -54,9 +54,15 @@ html, body { margin-top: 10px; } +.tooltip { + overflow: visible; +} + .tooltip-inner { - max-width: 100%; - background-color: #0062cc; + border: 1px solid black; /* Set uniform border width and color */ + padding: 3px; /* Add consistent padding around the image */ + width: auto; /* Ensure tooltip width adjusts to content */ + max-width: none; } .tooltip.show { @@ -64,14 +70,14 @@ html, body { } .bs-tooltip-bottom .arrow::before{ - border-bottom-color: #0062cc; + border-bottom-color: black; } .bs-tooltip-top .arrow::before{ - border-top-color: #0062cc; + border-top-color: black; } .bs-tooltip-left .arrow::before{ - border-left-color: #0062cc; + border-left-color: black; } .bs-tooltip-right .arrow::before{ - border-right-color: #0062cc; + border-right-color: black; }