Support comments
This commit is contained in:
parent
5070965bfe
commit
8a7bd651b2
@ -1,6 +1,6 @@
|
|||||||
mod ast;
|
mod ast;
|
||||||
pub mod format;
|
pub mod format;
|
||||||
mod parse;
|
pub mod parse;
|
||||||
|
|
||||||
pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term};
|
pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term};
|
||||||
pub use parse::{formula, formulas, term};
|
pub use parse::{formula, formulas, term};
|
||||||
|
122
src/parse.rs
122
src/parse.rs
@ -2,10 +2,10 @@ use nom::
|
|||||||
{
|
{
|
||||||
IResult,
|
IResult,
|
||||||
bytes::complete::{take_while, take_while_m_n, is_not},
|
bytes::complete::{take_while, take_while_m_n, is_not},
|
||||||
character::complete::{digit1, multispace0},
|
character::complete::{digit1, multispace0, space1, not_line_ending, line_ending},
|
||||||
sequence::{preceded, delimited, pair},
|
sequence::{preceded, delimited, pair, terminated},
|
||||||
combinator::{map, map_res},
|
combinator::{map, map_res},
|
||||||
multi::{many0, separated_list},
|
multi::{many0, many0_count, separated_list},
|
||||||
branch::alt,
|
branch::alt,
|
||||||
bytes::complete::tag,
|
bytes::complete::tag,
|
||||||
};
|
};
|
||||||
@ -17,11 +17,53 @@ enum TermOperator
|
|||||||
Multiply,
|
Multiply,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn comment(i: &str) -> IResult<&str, &str>
|
||||||
|
{
|
||||||
|
terminated
|
||||||
|
(
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
tag("%"),
|
||||||
|
not_line_ending,
|
||||||
|
),
|
||||||
|
line_ending,
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn whitespace0(i: &str) -> IResult<&str, ()>
|
||||||
|
{
|
||||||
|
let (i, _) = preceded
|
||||||
|
(
|
||||||
|
multispace0,
|
||||||
|
many0_count
|
||||||
|
(
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
comment,
|
||||||
|
multispace0,
|
||||||
|
)
|
||||||
|
),
|
||||||
|
)(i)?;
|
||||||
|
|
||||||
|
Ok((i, ()))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn whitespace_single(i: &str) -> IResult<&str, ()>
|
||||||
|
{
|
||||||
|
let (i, _) = alt
|
||||||
|
((
|
||||||
|
space1,
|
||||||
|
line_ending,
|
||||||
|
))(i)?;
|
||||||
|
|
||||||
|
Ok((i, ()))
|
||||||
|
}
|
||||||
|
|
||||||
fn infimum(i: &str) -> IResult<&str, crate::Term>
|
fn infimum(i: &str) -> IResult<&str, crate::Term>
|
||||||
{
|
{
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
delimited(multispace0, tag("#inf"), multispace0),
|
delimited(whitespace0, tag("#inf"), whitespace0),
|
||||||
|_| crate::Term::Infimum
|
|_| crate::Term::Infimum
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
@ -30,7 +72,7 @@ fn supremum(i: &str) -> IResult<&str, crate::Term>
|
|||||||
{
|
{
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
delimited(multispace0, tag("#sup"), multispace0),
|
delimited(whitespace0, tag("#sup"), whitespace0),
|
||||||
|_| crate::Term::Supremum
|
|_| crate::Term::Supremum
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
@ -41,7 +83,7 @@ fn integer(i: &str) -> IResult<&str, crate::Term>
|
|||||||
(
|
(
|
||||||
map_res
|
map_res
|
||||||
(
|
(
|
||||||
delimited(multispace0, digit1, multispace0),
|
delimited(whitespace0, digit1, whitespace0),
|
||||||
std::str::FromStr::from_str
|
std::str::FromStr::from_str
|
||||||
),
|
),
|
||||||
crate::Term::Integer
|
crate::Term::Integer
|
||||||
@ -72,7 +114,7 @@ fn symbolic(i: &str) -> IResult<&str, crate::Term>
|
|||||||
{
|
{
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
delimited(multispace0, symbolic_identifier, multispace0),
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
||||||
crate::Term::Symbolic
|
crate::Term::Symbolic
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
@ -83,14 +125,14 @@ fn string(i: &str) -> IResult<&str, crate::Term>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
tag("\""),
|
tag("\""),
|
||||||
is_not("\""),
|
is_not("\""),
|
||||||
tag("\""),
|
tag("\""),
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|s: &str| crate::Term::String(s.to_string())
|
|s: &str| crate::Term::String(s.to_string())
|
||||||
)(i)
|
)(i)
|
||||||
@ -102,13 +144,13 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
tag("X"),
|
tag("X"),
|
||||||
take_while(char::is_alphanumeric)
|
take_while(char::is_alphanumeric)
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|s: &str| s.to_string()
|
|s: &str| s.to_string()
|
||||||
)(i)
|
)(i)
|
||||||
@ -120,13 +162,13 @@ fn integer_variable_identifier(i: &str) -> IResult<&str, String>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
tag("N"),
|
tag("N"),
|
||||||
take_while(char::is_alphanumeric)
|
take_while(char::is_alphanumeric)
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|s: &str| s.to_string()
|
|s: &str| s.to_string()
|
||||||
)(i)
|
)(i)
|
||||||
@ -190,7 +232,7 @@ fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
{
|
{
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
delimited(multispace0, symbolic_identifier, multispace0),
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
||||||
|name| crate::Formula::Predicate(
|
|name| crate::Formula::Predicate(
|
||||||
crate::Predicate
|
crate::Predicate
|
||||||
{
|
{
|
||||||
@ -211,17 +253,17 @@ fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
(
|
(
|
||||||
pair
|
pair
|
||||||
(
|
(
|
||||||
delimited(multispace0, symbolic_identifier, multispace0),
|
delimited(whitespace0, symbolic_identifier, whitespace0),
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
tag("("),
|
tag("("),
|
||||||
separated_list(tag(","), term),
|
separated_list(tag(","), term),
|
||||||
tag(")")
|
tag(")")
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
)
|
)
|
||||||
),
|
),
|
||||||
|(name, arguments)| crate::Formula::Predicate(
|
|(name, arguments)| crate::Formula::Predicate(
|
||||||
@ -253,13 +295,13 @@ fn boolean(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
alt
|
alt
|
||||||
((
|
((
|
||||||
map(tag("#true"), |_| true),
|
map(tag("#true"), |_| true),
|
||||||
map(tag("#false"), |_| false)
|
map(tag("#false"), |_| false)
|
||||||
)),
|
)),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|value| crate::Formula::Boolean(value)
|
|value| crate::Formula::Boolean(value)
|
||||||
)(i)
|
)(i)
|
||||||
@ -360,14 +402,14 @@ fn term_parenthesized(i: &str) -> IResult<&str, crate::Term>
|
|||||||
{
|
{
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
tag("("),
|
tag("("),
|
||||||
term,
|
term,
|
||||||
tag(")")
|
tag(")")
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -409,9 +451,9 @@ fn term_precedence_1(i: &str) -> IResult<&str, crate::Term>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded(tag("-"), term_precedence_0),
|
preceded(tag("-"), term_precedence_0),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|term| crate::Term::Negative(Box::new(term))
|
|term| crate::Term::Negative(Box::new(term))
|
||||||
),
|
),
|
||||||
@ -468,14 +510,14 @@ fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
{
|
{
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
tag("("),
|
tag("("),
|
||||||
formula,
|
formula,
|
||||||
tag(")")
|
tag(")")
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -496,10 +538,14 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded
|
preceded
|
||||||
|
(
|
||||||
|
terminated
|
||||||
(
|
(
|
||||||
tag("exists"),
|
tag("exists"),
|
||||||
|
whitespace_single,
|
||||||
|
),
|
||||||
pair
|
pair
|
||||||
(
|
(
|
||||||
separated_list
|
separated_list
|
||||||
@ -510,7 +556,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
formula_precedence_1
|
formula_precedence_1
|
||||||
)
|
)
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|(parameters, argument)| crate::Formula::Exists(
|
|(parameters, argument)| crate::Formula::Exists(
|
||||||
crate::Exists
|
crate::Exists
|
||||||
@ -527,10 +573,14 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded
|
preceded
|
||||||
|
(
|
||||||
|
terminated
|
||||||
(
|
(
|
||||||
tag("forall"),
|
tag("forall"),
|
||||||
|
whitespace_single,
|
||||||
|
),
|
||||||
pair
|
pair
|
||||||
(
|
(
|
||||||
separated_list
|
separated_list
|
||||||
@ -541,7 +591,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
formula_precedence_1
|
formula_precedence_1
|
||||||
)
|
)
|
||||||
),
|
),
|
||||||
multispace0
|
whitespace0
|
||||||
),
|
),
|
||||||
|(parameters, argument)| crate::Formula::ForAll(
|
|(parameters, argument)| crate::Formula::ForAll(
|
||||||
crate::ForAll
|
crate::ForAll
|
||||||
@ -570,9 +620,17 @@ fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula>
|
|||||||
(
|
(
|
||||||
delimited
|
delimited
|
||||||
(
|
(
|
||||||
multispace0,
|
whitespace0,
|
||||||
preceded(tag("not "), formula_precedence_1),
|
preceded
|
||||||
multispace0
|
(
|
||||||
|
terminated
|
||||||
|
(
|
||||||
|
tag("not"),
|
||||||
|
whitespace_single,
|
||||||
|
),
|
||||||
|
formula_precedence_1
|
||||||
|
),
|
||||||
|
whitespace0
|
||||||
),
|
),
|
||||||
|argument| crate::Formula::Not(Box::new(argument))
|
|argument| crate::Formula::Not(Box::new(argument))
|
||||||
),
|
),
|
||||||
|
Loading…
Reference in New Issue
Block a user