Refactor term parser tests
This commit is contained in:
parent
95677bae34
commit
cb616eba87
@ -468,7 +468,7 @@ mod tests
|
||||
use crate::parse::formulas::*;
|
||||
use crate::{Formula, Term};
|
||||
|
||||
/*fn formula(i: &str) -> Formula
|
||||
fn formula(i: &str) -> Formula
|
||||
{
|
||||
crate::parse::formula(i, &Declarations::new()).unwrap().1
|
||||
}
|
||||
@ -479,11 +479,11 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_formula_boolean()
|
||||
fn parse_boolean()
|
||||
{
|
||||
assert_eq!(formula("true"), Formula::true_());
|
||||
assert_eq!(formula("false"), Formula::false_());
|
||||
}*/
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_predicate()
|
||||
@ -545,6 +545,6 @@ mod tests
|
||||
#[test]
|
||||
fn parse_formula()
|
||||
{
|
||||
assert!(formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest", &Declarations::new()).is_ok());
|
||||
formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest");
|
||||
}
|
||||
}
|
||||
|
@ -352,11 +352,12 @@ pub fn term<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
mod tests
|
||||
{
|
||||
use crate::parse::terms::*;
|
||||
use crate::parse::terms as original;
|
||||
use crate::{Term, VariableDeclaration, VariableDeclarationStack};
|
||||
|
||||
fn term(i: &str) -> Term
|
||||
{
|
||||
crate::parse::term(i, &Declarations::new()).unwrap().1
|
||||
original::term(i, &Declarations::new()).unwrap().1
|
||||
}
|
||||
|
||||
fn format_term(i: &str) -> String
|
||||
@ -365,7 +366,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_parenthesized()
|
||||
fn parse_parenthesized()
|
||||
{
|
||||
assert_eq!(format_term("(1)"), format_term("1"));
|
||||
assert_eq!(format_term("((1))"), format_term("1"));
|
||||
@ -429,14 +430,14 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_boolean()
|
||||
fn parse_boolean()
|
||||
{
|
||||
assert_eq!(term("true"), Term::true_());
|
||||
assert_eq!(term("false"), Term::false_());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_integer()
|
||||
fn parse_integer()
|
||||
{
|
||||
assert_eq!(term("0"), Term::integer(0));
|
||||
assert_eq!(term("10000"), Term::integer(10000));
|
||||
@ -445,14 +446,14 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_special_integer()
|
||||
fn parse_special_integer()
|
||||
{
|
||||
assert_eq!(term("#inf"), Term::infimum());
|
||||
assert_eq!(term("#sup"), Term::supremum());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_string()
|
||||
fn parse_string()
|
||||
{
|
||||
assert_eq!(term("\"test 123\""), Term::string("test 123".to_string()));
|
||||
assert_eq!(term("\"123 test\""), Term::string("123 test".to_string()));
|
||||
@ -476,7 +477,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_function()
|
||||
fn parse_function()
|
||||
{
|
||||
let term_as_function = |i| match term(i)
|
||||
{
|
||||
@ -495,7 +496,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_variable()
|
||||
fn parse_variable()
|
||||
{
|
||||
let term_as_variable = |i| match term(i)
|
||||
{
|
||||
@ -508,7 +509,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_unary()
|
||||
fn parse_unary()
|
||||
{
|
||||
assert_eq!(format_term("|a|"), "|a|");
|
||||
assert_eq!(format_term("||a||"), "||a||");
|
||||
@ -538,7 +539,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_exponentiate()
|
||||
fn parse_exponentiate()
|
||||
{
|
||||
assert_eq!(term("1 ** (2 ** (3 ** (4 ** 5)))"), term("1 ** 2 ** 3 ** 4 ** 5"));
|
||||
assert_eq!(format_term("1 ** 2 ** 3 ** 4 ** 5"), "1 ** 2 ** 3 ** 4 ** 5");
|
||||
@ -549,7 +550,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_multiplicative()
|
||||
fn parse_multiplicative()
|
||||
{
|
||||
assert_eq!(format_term("(a * b) * (c * d)"), "a * b * c * d");
|
||||
assert_eq!(format_term("(a * b) * (c / d)"), "a * b * c / d");
|
||||
@ -581,7 +582,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_additive()
|
||||
fn parse_additive()
|
||||
{
|
||||
assert_eq!(format_term("(a + b) + (c + d)"), "a + b + c + d");
|
||||
assert_eq!(format_term("(a + b) + (c - d)"), "a + b + c - d");
|
||||
@ -594,7 +595,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_precedence()
|
||||
fn parse_precedence()
|
||||
{
|
||||
assert_eq!(term("-a + b"), term("(-a) + b"));
|
||||
assert_eq!(term("-a + -b"), term("(-a) + (-b)"));
|
||||
@ -655,9 +656,9 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_bounds()
|
||||
fn parse_bounds()
|
||||
{
|
||||
let term = |i| crate::parse::term(i, &Declarations::new()).unwrap().0;
|
||||
let term = |i| original::term(i, &Declarations::new()).unwrap().0;
|
||||
|
||||
assert_eq!(term("1 ** 2 ** 3, rest"), ", rest");
|
||||
assert_eq!(term("1 * 2 * 3, rest"), ", rest");
|
||||
@ -688,7 +689,7 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_term_whitespace()
|
||||
fn parse_whitespace()
|
||||
{
|
||||
assert_eq!(format_term("(a+b)*(c+d)"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("( a + b ) * ( c + d )"), "(a + b) * (c + d)");
|
||||
@ -704,57 +705,48 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_function()
|
||||
fn parse_function_primitive()
|
||||
{
|
||||
assert_eq!(function("s", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok(("", "s".to_string())));
|
||||
assert_eq!(function("s", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.arity)),
|
||||
Ok(("", 0)));
|
||||
assert_eq!(function("s ( )", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok(("", "s".to_string())));
|
||||
assert_eq!(function("s ( )", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.arity)),
|
||||
Ok(("", 0)));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok(("", "s".to_string())));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.arity)),
|
||||
Ok(("", 3)));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )", &Declarations::new())
|
||||
.map(|(i, mut x)| (i, x.arguments.remove(0))),
|
||||
Ok(("", Box::new(Term::integer(1)))));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )", &Declarations::new())
|
||||
.map(|(i, mut x)| (i, x.arguments.remove(2))),
|
||||
Ok(("", Box::new(Term::integer(3)))));
|
||||
assert_eq!(function("s ( ), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok((", rest", "s".to_string())));
|
||||
assert_eq!(function("s ( ), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.arity)),
|
||||
Ok((", rest", 0)));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok((", rest", "s".to_string())));
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.arity)),
|
||||
Ok((", rest", 3)));
|
||||
let function_remainder = |i| original::function(i, &Declarations::new()).unwrap().0;
|
||||
let function = |i| original::function(i, &Declarations::new()).unwrap().1;
|
||||
|
||||
assert_eq!(function("s").declaration.name, "s");
|
||||
assert_eq!(function("s").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s"), "");
|
||||
assert_eq!(function("s ( )").declaration.name, "s");
|
||||
assert_eq!(function("s ( )").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s ( )"), "");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )").declaration.name, "s");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )").declaration.arity, 3);
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
|
||||
assert_eq!(function_remainder("s ( 1 , 2 , 3 )"), "");
|
||||
assert_eq!(function("s ( ), rest").declaration.name, "s");
|
||||
assert_eq!(function("s ( ), rest").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s ( ), rest"), ", rest");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
|
||||
assert_eq!(function_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_variable_declaration()
|
||||
{
|
||||
assert_eq!(variable_declaration("X Rest")
|
||||
.map(|(i, x)| (i, x.name.clone())), Ok((" Rest", "X".to_string())));
|
||||
assert_eq!(variable_declaration("X, Rest")
|
||||
.map(|(i, x)| (i, x.name.clone())), Ok((", Rest", "X".to_string())));
|
||||
let variable_declaration_remainder = |i| variable_declaration(i).unwrap().0;
|
||||
let variable_declaration = |i| variable_declaration(i).unwrap().1;
|
||||
|
||||
assert_eq!(variable_declaration("X Rest").name, "X");
|
||||
assert_eq!(variable_declaration_remainder("X Rest"), " Rest");
|
||||
assert_eq!(variable_declaration("X, Rest").name, "X");
|
||||
assert_eq!(variable_declaration_remainder("X, Rest"), ", Rest");
|
||||
// Variable declarations parsed at different locations should not be considered equal
|
||||
assert_ne!(variable_declaration("X"), variable_declaration("X"));
|
||||
assert_eq!(variable_declaration("Variable_123 Rest")
|
||||
.map(|(i, x)| (i, x.name.clone())), Ok((" Rest", "Variable_123".to_string())));
|
||||
assert_eq!(variable_declaration("Variable_123 Rest").name, "Variable_123");
|
||||
assert_eq!(variable_declaration_remainder("Variable_123 Rest"), " Rest");
|
||||
|
||||
let variable_declaration = original::variable_declaration;
|
||||
|
||||
assert!(variable_declaration("0 Rest").is_err());
|
||||
assert!(variable_declaration("123_Asd Rest").is_err());
|
||||
assert!(variable_declaration("x Rest").is_err());
|
||||
@ -765,22 +757,27 @@ mod tests
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_variable()
|
||||
fn parse_variable_primitive()
|
||||
{
|
||||
assert_eq!(variable("X Rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())), Ok((" Rest", "X".to_string())));
|
||||
assert_eq!(variable("X, Rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())), Ok((", Rest", "X".to_string())));
|
||||
assert_eq!(variable("Variable_123 Rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.declaration.name.clone())),
|
||||
Ok((" Rest", "Variable_123".to_string())));
|
||||
assert!(variable("0 Rest", &Declarations::new()).is_err());
|
||||
assert!(variable("123_Asd Rest", &Declarations::new()).is_err());
|
||||
assert!(variable("x Rest", &Declarations::new()).is_err());
|
||||
assert!(variable("variable_123 Rest", &Declarations::new()).is_err());
|
||||
assert!(variable("_ Rest", &Declarations::new()).is_err());
|
||||
assert!(variable("_variable_123 Rest", &Declarations::new()).is_err());
|
||||
assert!(variable(" ", &Declarations::new()).is_err());
|
||||
let variable_remainder = |i| original::variable(i, &Declarations::new()).unwrap().0;
|
||||
let variable = |i| original::variable(i, &Declarations::new()).unwrap().1;
|
||||
|
||||
assert_eq!(variable("X Rest").declaration.name, "X");
|
||||
assert_eq!(variable_remainder("X Rest"), " Rest");
|
||||
assert_eq!(variable("X, Rest").declaration.name, "X");
|
||||
assert_eq!(variable_remainder("X, Rest"), ", Rest");
|
||||
assert_eq!(variable("Variable_123 Rest").declaration.name, "Variable_123");
|
||||
assert_eq!(variable_remainder("Variable_123 Rest"), " Rest");
|
||||
|
||||
let variable = |i| original::variable(i, &Declarations::new());
|
||||
|
||||
assert!(variable("0 Rest").is_err());
|
||||
assert!(variable("123_Asd Rest").is_err());
|
||||
assert!(variable("x Rest").is_err());
|
||||
assert!(variable("variable_123 Rest").is_err());
|
||||
assert!(variable("_ Rest").is_err());
|
||||
assert!(variable("_variable_123 Rest").is_err());
|
||||
assert!(variable(" ").is_err());
|
||||
|
||||
let new_variable_declarations = |names: &[&str]| std::rc::Rc::new(names.iter()
|
||||
.map(|name| std::rc::Rc::new(VariableDeclaration::new(name.to_string())))
|
||||
@ -797,77 +794,66 @@ mod tests
|
||||
declarations.variable_declaration_stack =
|
||||
std::cell::RefCell::new(variable_declaration_stack);
|
||||
|
||||
let (_, x1) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 1);
|
||||
let (_, x2) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 1);
|
||||
let variable = |i| original::variable(i, &declarations).unwrap().1;
|
||||
let number_of_free_variable_declarations =
|
||||
|| declarations.variable_declaration_stack.borrow().free_variable_declarations.len();
|
||||
|
||||
let x1 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 1);
|
||||
let x2 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 1);
|
||||
assert_eq!(x1.declaration, x2.declaration);
|
||||
let (_, y1) = variable("Y", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let y1 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, y1.declaration);
|
||||
assert_ne!(x2.declaration, y1.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_1);
|
||||
|
||||
let (_, x3) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x3 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, x3.declaration);
|
||||
let (_, x4) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x4 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x3.declaration, x4.declaration);
|
||||
let (_, a1) = variable("A", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let a1 = variable("A");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x3.declaration, a1.declaration);
|
||||
let (_, y2) = variable("Y", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let y2 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(y1.declaration, y2.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_2);
|
||||
|
||||
let (_, x5) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x5 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, x5.declaration);
|
||||
assert_ne!(x3.declaration, x5.declaration);
|
||||
let (_, x6) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x6 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x5.declaration, x6.declaration);
|
||||
let (_, a2) = variable("A", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let a2 = variable("A");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(a1.declaration, a2.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_3);
|
||||
|
||||
let (_, x7) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x7 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x5.declaration, x7.declaration);
|
||||
let (_, y3) = variable("Y", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let y3 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(y2.declaration, y3.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_4);
|
||||
|
||||
let (_, x8) = variable("X", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let x8 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x7.declaration, x8.declaration);
|
||||
let (_, y4) = variable("Y", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 2);
|
||||
let y4 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(y3.declaration, y4.declaration);
|
||||
let _ = variable("I", &declarations).unwrap();
|
||||
assert_eq!(declarations.variable_declaration_stack.borrow()
|
||||
.free_variable_declarations.len(), 3);
|
||||
let _ = variable("I");
|
||||
assert_eq!(number_of_free_variable_declarations(), 3);
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user