Skip to content

Commit

Permalink
Merge branch 'master' into tobias/dependencies
Browse files Browse the repository at this point in the history
  • Loading branch information
@ZachJHansen
ZachJHansen authored Jan 31, 2025
2 parents 3c268ac + c6a7a2b commit 8c8d20b
Show file tree
Hide file tree
Showing 2 changed files with 305 additions and 6 deletions.
234 changes: 232 additions & 2 deletions src/formatting/fol/default.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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",
);
}
}
77 changes: 73 additions & 4 deletions src/parsing/fol/pest.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 8c8d20b

Please sign in to comment.