diff --git a/foliage b/foliage index 9076ecd..8870cee 160000 --- a/foliage +++ b/foliage @@ -1 +1 @@ -Subproject commit 9076ecd95ddd0e0244a8d3782d43b4708f0f05b0 +Subproject commit 8870cee1793571a313ac4f0948e4d73c5589e671 diff --git a/src/format_tptp.rs b/src/format_tptp.rs index b2de09d..a6e1cc2 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -62,7 +62,7 @@ fn collect_predicate_declarations_in_formula<'a>( { collect_predicate_declarations_in_formula(predicate_declarations, argument); }, - foliage::Formula::Implies(ref left, ref right) => + foliage::Formula::Implies(ref left, ref right, _) => { collect_predicate_declarations_in_formula(predicate_declarations, left); collect_predicate_declarations_in_formula(predicate_declarations, right); @@ -162,7 +162,7 @@ fn collect_symbolic_constants_in_formula<'a>( { collect_symbolic_constants_in_formula(symbolic_constants, argument); }, - foliage::Formula::Implies(ref left, ref right) => + foliage::Formula::Implies(ref left, ref right, _) => { collect_symbolic_constants_in_formula(symbolic_constants, left); collect_symbolic_constants_in_formula(symbolic_constants, right); @@ -515,7 +515,11 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a> write!(format, ")") }, - foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction + { + foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), + foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", left.display_tptp(), right.display_tptp()), + }, foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()), foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", Some("p__less__"), left, right), foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", Some("p__less_equal__"), left, right),