diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs index 8b3d51d..e531c70 100644 --- a/src/formatting/fol/default.rs +++ b/src/formatting/fol/default.rs @@ -438,11 +438,81 @@ mod tests { formatting::fol::default::Format, syntax_tree::fol::{ AnnotatedFormula, Atom, AtomicFormula, BinaryConnective, BinaryOperator, Comparison, - Direction, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, - Relation, Role, Sort, Specification, SymbolicTerm, UnaryConnective, Variable, + Direction, Formula, GeneralTerm, Guard, IntegerTerm, PlaceholderDeclaration, Predicate, + Quantification, Quantifier, Relation, Role, Sort, Specification, SymbolicTerm, Theory, + UnaryConnective, UnaryOperator, UserGuide, UserGuideEntry, Variable, }, }; + #[test] + fn format_unary_operator() { + assert_eq!(Format(&UnaryOperator::Negative).to_string(), "-"); + } + + #[test] + fn format_binary_operator() { + for (left, right) in [ + (BinaryOperator::Add, "+"), + (BinaryOperator::Subtract, "-"), + (BinaryOperator::Multiply, "*"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_relation() { + for (left, right) in [ + (Relation::Less, "<"), + (Relation::Greater, ">"), + (Relation::LessEqual, "<="), + (Relation::GreaterEqual, ">="), + (Relation::Equal, "="), + (Relation::NotEqual, "!="), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_unary_connective() { + assert_eq!(Format(&UnaryConnective::Negation).to_string(), "not"); + } + + #[test] + fn format_binary_connective() { + for (left, right) in [ + (BinaryConnective::Conjunction, "and"), + (BinaryConnective::Disjunction, "or"), + (BinaryConnective::Implication, "->"), + (BinaryConnective::ReverseImplication, "<-"), + (BinaryConnective::Equivalence, "<->"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_quantifier() { + for (left, right) in [ + (Quantifier::Forall, "forall"), + (Quantifier::Exists, "exists"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_sort() { + for (left, right) in [ + (Sort::General, "g"), + (Sort::Integer, "i"), + (Sort::Symbol, "s"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + #[test] fn format_integer_term() { assert_eq!(Format(&IntegerTerm::Numeral(-1)).to_string(), "-1"); @@ -832,6 +902,89 @@ mod tests { ); } + #[test] + fn format_theory() { + assert_eq!( + Format(&Theory { + formulas: vec![ + Formula::AtomicFormula(AtomicFormula::Truth).into(), + Formula::BinaryFormula { + connective: BinaryConnective::Equivalence, + lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "p".to_string(), + terms: vec![] + })) + .into(), + rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "q".to_string(), + terms: vec![] + })) + .into() + } + ], + }) + .to_string(), + "#true.\np <-> q.\n" + ); + } + + #[test] + fn format_role() { + for (left, right) in [ + (Role::Assumption, "assumption"), + (Role::Spec, "spec"), + (Role::Lemma, "lemma"), + (Role::Definition, "definition"), + (Role::InductiveLemma, "inductive-lemma"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_direction() { + for (left, right) in [ + (Direction::Universal, "universal"), + (Direction::Forward, "forward"), + (Direction::Backward, "backward"), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_annotated_formula() { + for (left, right) in [ + ( + AnnotatedFormula { + role: Role::Lemma, + direction: Direction::Universal, + name: "lemma_p".to_string(), + formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "p".to_string(), + terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Numeral(1))], + })), + }, + "lemma[lemma_p]: p(1)", + ), + ( + AnnotatedFormula { + role: Role::Assumption, + direction: Direction::Forward, + name: String::default(), + formula: Formula::BinaryFormula { + connective: BinaryConnective::Disjunction, + lhs: Formula::AtomicFormula(AtomicFormula::Truth).into(), + rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(), + }, + }, + "assumption(forward): #true or #false", + ), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + #[test] fn format_specification() { let left = Format(&Specification { @@ -901,4 +1054,81 @@ mod tests { let right = "spec(forward)[about_p_0]: not p(0).\nassumption: p(5).\ninductive-lemma(backward)[il1]: forall X (p(X) <-> q(X) or t).\n".to_string(); assert_eq!(left, right, "\n{left}!=\n{right}"); } + + #[test] + fn format_placeholder_declaration() { + assert_eq!( + Format(&PlaceholderDeclaration { + name: "n".to_string(), + sort: Sort::Integer, + }) + .to_string(), + "n -> i" + ); + } + + #[test] + fn format_user_guide_entry() { + for (left, right) in [ + ( + UserGuideEntry::InputPredicate(Predicate { + symbol: "p".to_string(), + arity: 0, + }), + "input: p/0", + ), + ( + UserGuideEntry::OutputPredicate(Predicate { + symbol: "q".to_string(), + arity: 1, + }), + "output: q/1", + ), + ( + UserGuideEntry::PlaceholderDeclaration(PlaceholderDeclaration { + name: "a".to_string(), + sort: Sort::Symbol, + }), + "input: a -> s", + ), + ( + UserGuideEntry::AnnotatedFormula(AnnotatedFormula { + role: Role::Lemma, + direction: Direction::Backward, + name: String::default(), + formula: Formula::UnaryFormula { + connective: UnaryConnective::Negation, + formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "p".to_string(), + terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Numeral(1))], + })) + .into(), + }, + }), + "lemma(backward): not p(1)", + ), + ] { + assert_eq!(Format(&left).to_string(), right); + } + } + + #[test] + fn format_user_guide() { + assert_eq!( + Format(&UserGuide { + entries: vec![ + UserGuideEntry::PlaceholderDeclaration(PlaceholderDeclaration { + name: "n".to_string(), + sort: Sort::Integer, + }), + UserGuideEntry::OutputPredicate(Predicate { + symbol: "q".to_string(), + arity: 2, + }), + ], + }) + .to_string(), + "input: n -> i.\noutput: q/2.\n", + ); + } } diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs index baa88c9..1c8be66 100644 --- a/src/parsing/fol/pest.rs +++ b/src/parsing/fol/pest.rs @@ -818,10 +818,11 @@ mod tests { use { super::{ AnnotatedFormulaParser, AtomParser, AtomicFormulaParser, BinaryConnectiveParser, - BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser, - IntegerTermParser, PredicateParser, QuantificationParser, QuantifierParser, - RelationParser, SortParser, SpecificationParser, SymbolicTermParser, TheoryParser, - UnaryConnectiveParser, UnaryOperatorParser, UserGuideParser, VariableParser, + BinaryOperatorParser, ComparisonParser, DirectionParser, FormulaParser, + GeneralTermParser, GuardParser, IntegerTermParser, PredicateParser, + QuantificationParser, QuantifierParser, RelationParser, RoleParser, SortParser, + SpecificationParser, SymbolicTermParser, TheoryParser, UnaryConnectiveParser, + UnaryOperatorParser, UserGuideEntryParser, UserGuideParser, VariableParser, }, crate::{ parsing::TestedParser, @@ -1632,6 +1633,36 @@ mod tests { ]); } + #[test] + fn parse_role() { + RoleParser + .should_parse_into([ + ("assumption", Role::Assumption), + ("spec", Role::Spec), + ("lemma", Role::Lemma), + ("definition", Role::Definition), + ("inductive-lemma", Role::InductiveLemma), + ]) + .should_reject([ + "assume", + "specification", + "inductive_lemma", + "inductive lemma", + "def", + ]); + } + + #[test] + fn parse_direction() { + DirectionParser + .should_parse_into([ + ("universal", Direction::Universal), + ("forward", Direction::Forward), + ("backward", Direction::Backward), + ]) + .should_reject(["backwards", "forwards"]); + } + #[test] fn parse_annotated_formula() { AnnotatedFormulaParser @@ -1738,6 +1769,44 @@ mod tests { .should_reject(["lemma: X"]); } + #[test] + fn parse_user_guide_entry() { + UserGuideEntryParser + .should_parse_into([ + ( + "input: n -> integer", + UserGuideEntry::PlaceholderDeclaration(PlaceholderDeclaration { + name: "n".to_string(), + sort: Sort::Integer, + }), + ), + ( + "input: a/0", + UserGuideEntry::InputPredicate(Predicate { + symbol: "a".to_string(), + arity: 0, + }), + ), + ( + "output: a/1", + UserGuideEntry::OutputPredicate(Predicate { + symbol: "a".to_string(), + arity: 1, + }), + ), + ( + "spec: #true", + UserGuideEntry::AnnotatedFormula(AnnotatedFormula { + role: Role::Spec, + direction: Direction::Universal, + name: String::default(), + formula: Formula::AtomicFormula(AtomicFormula::Truth), + }), + ), + ]) + .should_reject(["output: p", "input: p(X)", "#false"]); + } + #[test] fn parse_user_guide() { UserGuideParser