248 lines
6.1 KiB
Rust
248 lines
6.1 KiB
Rust
use nom::
|
|
{
|
|
IResult,
|
|
branch::alt,
|
|
bytes::complete::{escaped_transform, tag},
|
|
character::complete::{digit1, none_of},
|
|
combinator::{map, map_res, opt, recognize},
|
|
sequence::{delimited, pair, terminated},
|
|
};
|
|
|
|
use super::word_boundary;
|
|
|
|
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<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
|
|
{
|
|
alt
|
|
((
|
|
function_n_ary,
|
|
function_0_ary
|
|
))(i)
|
|
}
|
|
|
|
fn function_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
delimited(multispace0, function_identifier, multispace0),
|
|
|name| crate::Formula::function(
|
|
crate::FunctionDeclaration
|
|
{
|
|
name: name,
|
|
arity: 0,
|
|
},
|
|
vec![])
|
|
)(i)
|
|
}
|
|
|
|
fn function_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
|
|
{
|
|
map
|
|
(
|
|
pair
|
|
(
|
|
delimited(multispace0, function_identifier, multispace0),
|
|
delimited
|
|
(
|
|
multispace0,
|
|
delimited
|
|
(
|
|
tag("("),
|
|
separated_list(tag(","), term),
|
|
tag(")")
|
|
),
|
|
multispace0
|
|
)
|
|
),
|
|
|(name, arguments)| crate::Formula::function(
|
|
crate::PredicateDeclaration
|
|
{
|
|
name: name,
|
|
arity: arguments.len(),
|
|
},
|
|
arguments)
|
|
)(i)
|
|
}
|
|
|
|
*/
|
|
|
|
#[cfg(test)]
|
|
mod tests
|
|
{
|
|
use crate::parse::*;
|
|
use crate::Term;
|
|
|
|
#[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());
|
|
}
|
|
|
|
#[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());
|
|
}
|
|
}
|