902 lines
26 KiB
Rust
902 lines
26 KiB
Rust
use nom::
|
|
{
|
|
IResult,
|
|
branch::alt,
|
|
bytes::complete::{escaped_transform, tag},
|
|
character::complete::{digit1, multispace0, none_of},
|
|
combinator::{map, map_res, opt, recognize},
|
|
multi::{many1, separated_list},
|
|
sequence::{delimited, pair, preceded, terminated},
|
|
};
|
|
|
|
use super::{Declarations, function_or_predicate_name, word_boundary, variable_name};
|
|
|
|
fn true_(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
terminated
|
|
(
|
|
tag("true"),
|
|
word_boundary,
|
|
),
|
|
|_| crate::Term::true_(),
|
|
)(i)
|
|
}
|
|
|
|
fn false_(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
terminated
|
|
(
|
|
tag("false"),
|
|
word_boundary,
|
|
),
|
|
|_| crate::Term::false_(),
|
|
)(i)
|
|
}
|
|
|
|
fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
preceded
|
|
(
|
|
terminated
|
|
(
|
|
tag("-"),
|
|
multispace0,
|
|
),
|
|
|i| term_precedence_0(i, d),
|
|
),
|
|
|x| crate::Term::negative(Box::new(x)),
|
|
)(i)
|
|
}
|
|
|
|
pub fn boolean(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
true_,
|
|
false_,
|
|
))(i)
|
|
}
|
|
|
|
pub fn integer(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
map_res
|
|
(
|
|
recognize
|
|
(
|
|
terminated
|
|
(
|
|
pair
|
|
(
|
|
opt
|
|
(
|
|
alt
|
|
((
|
|
tag("-"),
|
|
tag("+"),
|
|
))
|
|
),
|
|
digit1,
|
|
),
|
|
word_boundary,
|
|
)
|
|
),
|
|
std::str::FromStr::from_str,
|
|
),
|
|
crate::Term::integer,
|
|
)(i)
|
|
}
|
|
|
|
fn infimum(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
terminated
|
|
(
|
|
tag("#inf"),
|
|
word_boundary,
|
|
),
|
|
|_| crate::Term::infimum(),
|
|
)(i)
|
|
}
|
|
|
|
fn supremum(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
terminated
|
|
(
|
|
tag("#sup"),
|
|
word_boundary,
|
|
),
|
|
|_| crate::Term::supremum(),
|
|
)(i)
|
|
}
|
|
|
|
pub fn special_integer(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
infimum,
|
|
supremum,
|
|
))(i)
|
|
}
|
|
|
|
pub fn string(i: &str) -> IResult<&str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
terminated
|
|
(
|
|
delimited
|
|
(
|
|
tag("\""),
|
|
escaped_transform
|
|
(
|
|
none_of("\"\\"),
|
|
'\\',
|
|
alt
|
|
((
|
|
tag("\""),
|
|
tag("\\"),
|
|
map
|
|
(
|
|
tag("n"),
|
|
|_| "\n",
|
|
),
|
|
map
|
|
(
|
|
tag("t"),
|
|
|_| "\t",
|
|
),
|
|
)),
|
|
),
|
|
tag("\""),
|
|
),
|
|
word_boundary,
|
|
),
|
|
crate::Term::string,
|
|
)(i)
|
|
}
|
|
|
|
fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
|
|
-> IResult<&'i str, (&'i str, Option<Vec<Box<crate::Term>>>)>
|
|
{
|
|
pair
|
|
(
|
|
function_or_predicate_name,
|
|
opt
|
|
(
|
|
delimited
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
tag("("),
|
|
multispace0,
|
|
),
|
|
separated_list
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
tag(","),
|
|
multispace0,
|
|
),
|
|
map
|
|
(
|
|
|i| term(i, d),
|
|
Box::new,
|
|
),
|
|
),
|
|
preceded
|
|
(
|
|
multispace0,
|
|
tag(")"),
|
|
),
|
|
)
|
|
),
|
|
)(i)
|
|
}
|
|
|
|
pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
|
|
{
|
|
map
|
|
(
|
|
|i| function_or_predicate(i, d),
|
|
|(name, arguments)|
|
|
{
|
|
let arguments = match arguments
|
|
{
|
|
Some(arguments) => arguments,
|
|
None => vec![],
|
|
};
|
|
|
|
let mut function_declarations = d.function_declarations.borrow_mut();
|
|
|
|
let declaration = match function_declarations.iter()
|
|
.find(|x| x.name == name && x.arity == arguments.len())
|
|
{
|
|
Some(declaration) => std::rc::Rc::clone(&declaration),
|
|
None =>
|
|
{
|
|
let declaration = crate::FunctionDeclaration
|
|
{
|
|
name: name.to_string(),
|
|
arity: arguments.len(),
|
|
};
|
|
let declaration = std::rc::Rc::new(declaration);
|
|
|
|
function_declarations.insert(std::rc::Rc::clone(&declaration));
|
|
|
|
declaration
|
|
},
|
|
};
|
|
|
|
crate::Function::new(declaration, arguments)
|
|
},
|
|
)(i)
|
|
}
|
|
|
|
pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate>
|
|
{
|
|
map
|
|
(
|
|
|i| function_or_predicate(i, d),
|
|
|(name, arguments)|
|
|
{
|
|
let arguments = match arguments
|
|
{
|
|
Some(arguments) => arguments,
|
|
None => vec![],
|
|
};
|
|
|
|
let mut predicate_declarations = d.predicate_declarations.borrow_mut();
|
|
|
|
let declaration = match predicate_declarations.iter()
|
|
.find(|x| x.name == name && x.arity == arguments.len())
|
|
{
|
|
Some(declaration) => std::rc::Rc::clone(&declaration),
|
|
None =>
|
|
{
|
|
let declaration = crate::PredicateDeclaration
|
|
{
|
|
name: name.to_string(),
|
|
arity: arguments.len(),
|
|
};
|
|
let declaration = std::rc::Rc::new(declaration);
|
|
|
|
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
|
|
|
|
declaration
|
|
},
|
|
};
|
|
|
|
crate::Predicate::new(declaration, arguments)
|
|
},
|
|
)(i)
|
|
}
|
|
|
|
pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
|
|
{
|
|
map
|
|
(
|
|
variable_name,
|
|
|name| crate::VariableDeclaration::new(name.to_string())
|
|
)(i)
|
|
}
|
|
|
|
pub fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
|
|
{
|
|
map
|
|
(
|
|
variable_name,
|
|
|name|
|
|
{
|
|
let mut variable_declaration_stack = d.variable_declaration_stack.borrow_mut();
|
|
|
|
let declaration = variable_declaration_stack.find_or_create(name);
|
|
|
|
crate::Variable::new(declaration)
|
|
},
|
|
)(i)
|
|
}
|
|
|
|
fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
delimited
|
|
(
|
|
terminated
|
|
(
|
|
tag("("),
|
|
multispace0,
|
|
),
|
|
|i| term(i, d),
|
|
preceded
|
|
(
|
|
multispace0,
|
|
tag(")"),
|
|
),
|
|
)(i)
|
|
}
|
|
|
|
fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
special_integer,
|
|
integer,
|
|
map
|
|
(
|
|
|i| function(i, d),
|
|
crate::Term::Function,
|
|
),
|
|
string,
|
|
map
|
|
(
|
|
|i| variable(i, d),
|
|
crate::Term::Variable,
|
|
),
|
|
|i| term_parenthesized(i, d),
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
|i| negative(i, d),
|
|
|i| term_precedence_0(i, d),
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
many1
|
|
(
|
|
terminated
|
|
(
|
|
|i| term_precedence_1(i, d),
|
|
delimited
|
|
(
|
|
multispace0,
|
|
tag("**"),
|
|
multispace0,
|
|
),
|
|
)
|
|
),
|
|
|i| term_precedence_1(i, d),
|
|
),
|
|
|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
|
|
|accumulator, argument|
|
|
crate::Term::exponentiate(Box::new(argument), Box::new(accumulator))),
|
|
),
|
|
|i| term_precedence_1(i, d),
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
|i| term_precedence_2(i, d),
|
|
many1
|
|
(
|
|
pair
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
alt
|
|
((
|
|
tag("*"),
|
|
tag("/"),
|
|
tag("%"),
|
|
)),
|
|
multispace0,
|
|
),
|
|
|i| term_precedence_2(i, d),
|
|
)
|
|
),
|
|
),
|
|
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
|
|accumulator, (operator, argument)|
|
|
match operator
|
|
{
|
|
"*" => crate::Term::multiply(Box::new(accumulator), Box::new(argument)),
|
|
"/" => crate::Term::divide(Box::new(accumulator), Box::new(argument)),
|
|
"%" => crate::Term::modulo(Box::new(accumulator), Box::new(argument)),
|
|
// TODO: handle appropriately
|
|
_ => panic!("test"),
|
|
})
|
|
),
|
|
|i| term_precedence_2(i, d),
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
|i| term_precedence_3(i, d),
|
|
many1
|
|
(
|
|
pair
|
|
(
|
|
delimited
|
|
(
|
|
multispace0,
|
|
alt
|
|
((
|
|
tag("+"),
|
|
tag("-"),
|
|
)),
|
|
multispace0,
|
|
),
|
|
|i| term_precedence_3(i, d),
|
|
)
|
|
),
|
|
),
|
|
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
|
|accumulator, (operator, argument)|
|
|
match operator
|
|
{
|
|
"+" => crate::Term::add(Box::new(accumulator), Box::new(argument)),
|
|
"-" => crate::Term::subtract(Box::new(accumulator), Box::new(argument)),
|
|
// TODO: handle appropriately
|
|
_ => panic!("test"),
|
|
})
|
|
),
|
|
|i| term_precedence_3(i, d),
|
|
))(i)
|
|
}
|
|
|
|
fn term_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
alt
|
|
((
|
|
map
|
|
(
|
|
delimited
|
|
(
|
|
terminated
|
|
(
|
|
tag("|"),
|
|
multispace0,
|
|
),
|
|
|i| term_precedence_4(i, d),
|
|
preceded
|
|
(
|
|
multispace0,
|
|
tag("|"),
|
|
),
|
|
),
|
|
|argument| crate::Term::absolute_value(Box::new(argument)),
|
|
),
|
|
|i| term_precedence_4(i, d),
|
|
))(i)
|
|
}
|
|
|
|
pub fn term<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
term_precedence_5(i, d)
|
|
}
|
|
|
|
#[cfg(test)]
|
|
mod tests
|
|
{
|
|
use crate::parse::*;
|
|
use crate::{Term, VariableDeclaration, VariableDeclarationStack};
|
|
|
|
/*#[test]
|
|
fn parse_binary_operator()
|
|
{
|
|
assert!(binary_operator("+") == Ok(("", BinaryOperator::Add)));
|
|
assert!(binary_operator("+ ") == Ok((" ", BinaryOperator::Add)));
|
|
assert!(binary_operator("+3") == Ok(("3", BinaryOperator::Add)));
|
|
assert!(binary_operator("+ 3") == Ok((" 3", BinaryOperator::Add)));
|
|
assert!(binary_operator("+(rest") == Ok(("(rest", BinaryOperator::Add)));
|
|
assert!(binary_operator("+ (rest") == Ok((" (rest", BinaryOperator::Add)));
|
|
assert!(binary_operator("-") == Ok(("", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("- ") == Ok((" ", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("-3") == Ok(("3", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("- 3") == Ok((" 3", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("-(rest") == Ok(("(rest", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("- (rest") == Ok((" (rest", BinaryOperator::Subtract)));
|
|
assert!(binary_operator("*") == Ok(("", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("* ") == Ok((" ", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("*3") == Ok(("3", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("* 3") == Ok((" 3", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("*(rest") == Ok(("(rest", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("* (rest") == Ok((" (rest", BinaryOperator::Multiply)));
|
|
assert!(binary_operator("/") == Ok(("", BinaryOperator::Divide)));
|
|
assert!(binary_operator("/ ") == Ok((" ", BinaryOperator::Divide)));
|
|
assert!(binary_operator("/3") == Ok(("3", BinaryOperator::Divide)));
|
|
assert!(binary_operator("/ 3") == Ok((" 3", BinaryOperator::Divide)));
|
|
assert!(binary_operator("/(rest") == Ok(("(rest", BinaryOperator::Divide)));
|
|
assert!(binary_operator("/ (rest") == Ok((" (rest", BinaryOperator::Divide)));
|
|
assert!(binary_operator("%") == Ok(("", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("% ") == Ok((" ", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("%3") == Ok(("3", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("% 3") == Ok((" 3", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("%(rest") == Ok(("(rest", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("% (rest") == Ok((" (rest", BinaryOperator::Modulo)));
|
|
assert!(binary_operator("**") == Ok(("", BinaryOperator::Exponentiate)));
|
|
assert!(binary_operator("** ") == Ok((" ", BinaryOperator::Exponentiate)));
|
|
assert!(binary_operator("**3") == Ok(("3", BinaryOperator::Exponentiate)));
|
|
assert!(binary_operator("** 3") == Ok((" 3", BinaryOperator::Exponentiate)));
|
|
assert!(binary_operator("**(rest") == Ok(("(rest", BinaryOperator::Exponentiate)));
|
|
assert!(binary_operator("** (rest") == Ok((" (rest", BinaryOperator::Exponentiate)));
|
|
}*/
|
|
|
|
/*#[test]
|
|
fn parse_binary_operation()
|
|
{
|
|
assert_eq!(binary_operation("4 + 5", Declarations::new()),
|
|
Ok(("", Term::add(Box::new(Term::integer(4)), Box::new(Term::integer(5))))));
|
|
assert_eq!(binary_operation("4 + 5 + 7", Declarations::new()),
|
|
Ok(("", Term::add(Box::new(Term::integer(4)), Box::new(Term::integer(5))))));
|
|
}*/
|
|
|
|
#[test]
|
|
fn parse_term()
|
|
{
|
|
let (rest, e1) = term("1 ** 2 ** 3 ** 4 ** 5, rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", e1), "1 ** 2 ** 3 ** 4 ** 5");
|
|
|
|
let (rest, e2) = term("1 ** (2 ** (3 ** (4 ** 5))), rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", e2), "1 ** 2 ** 3 ** 4 ** 5");
|
|
|
|
let (rest, e3) = term("(((1 ** 2) ** 3) ** 4) ** 5, rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", e3), "(((1 ** 2) ** 3) ** 4) ** 5");
|
|
|
|
assert_eq!(e1, e2);
|
|
assert_ne!(e1, e3);
|
|
|
|
let (rest, m1) = term("1 * 2 * 3 * 4 * 5, rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", m1), "1 * 2 * 3 * 4 * 5");
|
|
|
|
let (rest, m2) = term("1 * (2 * (3 * (4 * 5))), rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", m2), "1 * 2 * 3 * 4 * 5");
|
|
|
|
let (rest, m3) = term("(((1 * 2) * 3) * 4) * 5, rest", &Declarations::new()).unwrap();
|
|
assert_eq!(rest, ", rest");
|
|
assert_eq!(format!("{}", m3), "1 * 2 * 3 * 4 * 5");
|
|
|
|
assert_eq!(m1, m2);
|
|
assert_ne!(m1, m3);
|
|
}
|
|
|
|
#[test]
|
|
fn parse_term_precedence_3()
|
|
{
|
|
assert_eq!(
|
|
crate::parse::terms::term_precedence_3("1 * 2 / 3 % 4 * 5", &Declarations::new()),
|
|
Ok(("", Term::multiply(
|
|
Box::new(Term::modulo(
|
|
Box::new(Term::divide(
|
|
Box::new(Term::multiply(
|
|
Box::new(Term::integer(1)),
|
|
Box::new(Term::integer(2)))),
|
|
Box::new(Term::integer(3)))),
|
|
Box::new(Term::integer(4)))),
|
|
Box::new(Term::integer(5))))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_term_precedence_4()
|
|
{
|
|
assert_eq!(
|
|
crate::parse::terms::term_precedence_4("1 + 2 - 3 + 4 - 5", &Declarations::new()),
|
|
Ok(("", Term::subtract(
|
|
Box::new(Term::add(
|
|
Box::new(Term::subtract(
|
|
Box::new(Term::add(
|
|
Box::new(Term::integer(1)),
|
|
Box::new(Term::integer(2)))),
|
|
Box::new(Term::integer(3)))),
|
|
Box::new(Term::integer(4)))),
|
|
Box::new(Term::integer(5))))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_term_precedence_5()
|
|
{
|
|
assert_eq!(
|
|
crate::parse::terms::term_precedence_5("|1 + 2|", &Declarations::new()),
|
|
Ok(("", Term::absolute_value(
|
|
Box::new(Term::add(
|
|
Box::new(Term::integer(1)),
|
|
Box::new(Term::integer(2))))))));
|
|
}
|
|
|
|
#[test]
|
|
fn parse_boolean()
|
|
{
|
|
assert_eq!(boolean("true"), Ok(("", Term::true_())));
|
|
assert_eq!(boolean("false"), Ok(("", Term::false_())));
|
|
assert_eq!(boolean("true false"), Ok((" false", Term::true_())));
|
|
assert_eq!(boolean("false true"), Ok((" true", Term::false_())));
|
|
assert_eq!(boolean("true,"), Ok((",", Term::true_())));
|
|
assert_eq!(boolean("false,"), Ok((",", Term::false_())));
|
|
assert!(boolean("truefalse").is_err());
|
|
assert!(boolean("falsetrue").is_err());
|
|
assert!(boolean("truea").is_err());
|
|
assert!(boolean("falsea").is_err());
|
|
assert!(boolean("a").is_err());
|
|
assert!(boolean("-").is_err());
|
|
assert!(boolean(" ").is_err());
|
|
}
|
|
|
|
#[test]
|
|
fn parse_integer()
|
|
{
|
|
assert_eq!(integer("0"), Ok(("", Term::integer(0))));
|
|
assert_eq!(integer("10000"), Ok(("", Term::integer(10000))));
|
|
assert_eq!(integer("+10000"), Ok(("", Term::integer(10000))));
|
|
assert_eq!(integer("-10000"), Ok(("", Term::integer(-10000))));
|
|
assert_eq!(integer("0 42"), Ok((" 42", Term::integer(0))));
|
|
assert_eq!(integer("10000 42"), Ok((" 42", Term::integer(10000))));
|
|
assert_eq!(integer("+10000 42"), Ok((" 42", Term::integer(10000))));
|
|
assert_eq!(integer("-10000 42"), Ok((" 42", Term::integer(-10000))));
|
|
assert_eq!(integer("10000,"), Ok((",", Term::integer(10000))));
|
|
assert_eq!(integer("+10000,"), Ok((",", Term::integer(10000))));
|
|
assert_eq!(integer("-10000,"), Ok((",", Term::integer(-10000))));
|
|
assert!(integer("10000a").is_err());
|
|
assert!(integer("+10000a").is_err());
|
|
assert!(integer("-10000a").is_err());
|
|
assert!(integer("1.5").is_err());
|
|
assert!(integer("a").is_err());
|
|
assert!(integer("-").is_err());
|
|
assert!(integer(" ").is_err());
|
|
}
|
|
|
|
#[test]
|
|
fn parse_special_integer()
|
|
{
|
|
assert_eq!(special_integer("#inf"), Ok(("", Term::infimum())));
|
|
assert_eq!(special_integer("#sup"), Ok(("", Term::supremum())));
|
|
assert_eq!(special_integer("#inf #sup"), Ok((" #sup", Term::infimum())));
|
|
assert_eq!(special_integer("#sup #inf"), Ok((" #inf", Term::supremum())));
|
|
assert_eq!(special_integer("#inf,"), Ok((",", Term::infimum())));
|
|
assert_eq!(special_integer("#sup,"), Ok((",", Term::supremum())));
|
|
assert!(special_integer("#inf0").is_err());
|
|
assert!(special_integer("#sup0").is_err());
|
|
assert!(special_integer("#infimum").is_err());
|
|
assert!(special_integer("#supremum").is_err());
|
|
assert!(special_integer("inf").is_err());
|
|
assert!(special_integer("sup").is_err());
|
|
assert!(special_integer("0").is_err());
|
|
assert!(special_integer("10000").is_err());
|
|
assert!(special_integer("-10000").is_err());
|
|
assert!(special_integer("-").is_err());
|
|
assert!(special_integer("+").is_err());
|
|
assert!(special_integer("a").is_err());
|
|
assert!(special_integer(" ").is_err());
|
|
}
|
|
|
|
#[test]
|
|
fn parse_string()
|
|
{
|
|
assert_eq!(string("\"test 123\""), Ok(("", Term::string("test 123".to_string()))));
|
|
assert_eq!(string("\"123 test\""), Ok(("", Term::string("123 test".to_string()))));
|
|
assert_eq!(string("\" test 123 \""), Ok(("", Term::string(" test 123 ".to_string()))));
|
|
assert_eq!(string("\"test 123\" \"rest"), Ok((" \"rest", Term::string("test 123".to_string()))));
|
|
assert_eq!(string("\"test 123\", \"rest"), Ok((", \"rest", Term::string("test 123".to_string()))));
|
|
assert_eq!(string("\"test\n123\""), Ok(("", Term::string("test\n123".to_string()))));
|
|
assert_eq!(string("\"test\\\"123\""), Ok(("", Term::string("test\"123".to_string()))));
|
|
assert_eq!(string("\"test\\\"123\\\"\""), Ok(("", Term::string("test\"123\"".to_string()))));
|
|
assert_eq!(string("\"\\\"test 123\\\"\""), Ok(("", Term::string("\"test 123\"".to_string()))));
|
|
assert_eq!(string("\"test\\\\123\""), Ok(("", Term::string("test\\123".to_string()))));
|
|
assert_eq!(string("\"test\\\\123\\\\\""), Ok(("", Term::string("test\\123\\".to_string()))));
|
|
assert_eq!(string("\"\\\\test 123\\\\\""), Ok(("", Term::string("\\test 123\\".to_string()))));
|
|
assert_eq!(string("\"test\\n123\""), Ok(("", Term::string("test\n123".to_string()))));
|
|
assert_eq!(string("\"test\\n123\\n\""), Ok(("", Term::string("test\n123\n".to_string()))));
|
|
assert_eq!(string("\"\\ntest 123\\n\""), Ok(("", Term::string("\ntest 123\n".to_string()))));
|
|
assert_eq!(string("\"test\\t123\""), Ok(("", Term::string("test\t123".to_string()))));
|
|
assert_eq!(string("\"test\\t123\\t\""), Ok(("", Term::string("test\t123\t".to_string()))));
|
|
assert_eq!(string("\"\\ttest 123\\t\""), Ok(("", Term::string("\ttest 123\t".to_string()))));
|
|
assert_eq!(string("\"test 🙂 123\""), Ok(("", Term::string("test 🙂 123".to_string()))));
|
|
assert!(string("\"test 123\"a").is_err());
|
|
assert!(string("\"test\\i123\"").is_err());
|
|
assert!(string("\"test").is_err());
|
|
assert!(string("test").is_err());
|
|
assert!(string("-").is_err());
|
|
assert!(string(" ").is_err());
|
|
}
|
|
|
|
#[test]
|
|
fn parse_function()
|
|
{
|
|
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)));
|
|
}
|
|
|
|
#[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())));
|
|
// 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!(variable_declaration("0 Rest").is_err());
|
|
assert!(variable_declaration("123_Asd Rest").is_err());
|
|
assert!(variable_declaration("x Rest").is_err());
|
|
assert!(variable_declaration("variable_123 Rest").is_err());
|
|
assert!(variable_declaration("_ Rest").is_err());
|
|
assert!(variable_declaration("_variable_123 Rest").is_err());
|
|
assert!(variable_declaration(" ").is_err());
|
|
}
|
|
|
|
#[test]
|
|
fn parse_variable()
|
|
{
|
|
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 new_variable_declarations = |names: &[&str]| std::rc::Rc::new(names.iter()
|
|
.map(|name| std::rc::Rc::new(VariableDeclaration::new(name.to_string())))
|
|
.collect());
|
|
|
|
let layer_1 = new_variable_declarations(&["A", "B", "X"]);
|
|
let layer_2 = new_variable_declarations(&["C", "D", "X"]);
|
|
let layer_3 = new_variable_declarations(&["E", "F", "Y"]);
|
|
let layer_4 = new_variable_declarations(&["G", "H", "X"]);
|
|
|
|
let variable_declaration_stack = VariableDeclarationStack::new();
|
|
|
|
let mut declarations = Declarations::new();
|
|
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);
|
|
assert_eq!(x1.declaration, x2.declaration);
|
|
let (_, y1) = variable("Y", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 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);
|
|
assert_ne!(x1.declaration, x3.declaration);
|
|
let (_, x4) = variable("X", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 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);
|
|
assert_ne!(x3.declaration, a1.declaration);
|
|
let (_, y2) = variable("Y", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 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);
|
|
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);
|
|
assert_eq!(x5.declaration, x6.declaration);
|
|
let (_, a2) = variable("A", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 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);
|
|
assert_eq!(x5.declaration, x7.declaration);
|
|
let (_, y3) = variable("Y", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 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);
|
|
assert_ne!(x7.declaration, x8.declaration);
|
|
let (_, y4) = variable("Y", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 2);
|
|
assert_eq!(y3.declaration, y4.declaration);
|
|
let _ = variable("I", &declarations).unwrap();
|
|
assert_eq!(declarations.variable_declaration_stack.borrow()
|
|
.free_variable_declarations.len(), 3);
|
|
}
|
|
}
|