From 8a7bd651b217a37f6d95faaa2d4bc1221631e88b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 5 Nov 2019 12:43:03 -0600 Subject: [PATCH] Support comments --- src/lib.rs | 2 +- src/parse.rs | 126 +++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 93 insertions(+), 35 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index be744e7..1954948 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,6 @@ mod ast; pub mod format; -mod parse; +pub mod parse; pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term}; pub use parse::{formula, formulas, term}; diff --git a/src/parse.rs b/src/parse.rs index 0cc40c4..0ab696f 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -2,10 +2,10 @@ use nom:: { IResult, bytes::complete::{take_while, take_while_m_n, is_not}, - character::complete::{digit1, multispace0}, - sequence::{preceded, delimited, pair}, + character::complete::{digit1, multispace0, space1, not_line_ending, line_ending}, + sequence::{preceded, delimited, pair, terminated}, combinator::{map, map_res}, - multi::{many0, separated_list}, + multi::{many0, many0_count, separated_list}, branch::alt, bytes::complete::tag, }; @@ -17,11 +17,53 @@ enum TermOperator 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> { map ( - delimited(multispace0, tag("#inf"), multispace0), + delimited(whitespace0, tag("#inf"), whitespace0), |_| crate::Term::Infimum )(i) } @@ -30,7 +72,7 @@ fn supremum(i: &str) -> IResult<&str, crate::Term> { map ( - delimited(multispace0, tag("#sup"), multispace0), + delimited(whitespace0, tag("#sup"), whitespace0), |_| crate::Term::Supremum )(i) } @@ -41,7 +83,7 @@ fn integer(i: &str) -> IResult<&str, crate::Term> ( map_res ( - delimited(multispace0, digit1, multispace0), + delimited(whitespace0, digit1, whitespace0), std::str::FromStr::from_str ), crate::Term::Integer @@ -72,7 +114,7 @@ fn symbolic(i: &str) -> IResult<&str, crate::Term> { map ( - delimited(multispace0, symbolic_identifier, multispace0), + delimited(whitespace0, symbolic_identifier, whitespace0), crate::Term::Symbolic )(i) } @@ -83,14 +125,14 @@ fn string(i: &str) -> IResult<&str, crate::Term> ( delimited ( - multispace0, + whitespace0, delimited ( tag("\""), is_not("\""), tag("\""), ), - multispace0 + whitespace0 ), |s: &str| crate::Term::String(s.to_string()) )(i) @@ -102,13 +144,13 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String> ( delimited ( - multispace0, + whitespace0, preceded ( tag("X"), take_while(char::is_alphanumeric) ), - multispace0 + whitespace0 ), |s: &str| s.to_string() )(i) @@ -120,13 +162,13 @@ fn integer_variable_identifier(i: &str) -> IResult<&str, String> ( delimited ( - multispace0, + whitespace0, preceded ( tag("N"), take_while(char::is_alphanumeric) ), - multispace0 + whitespace0 ), |s: &str| s.to_string() )(i) @@ -190,7 +232,7 @@ fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula> { map ( - delimited(multispace0, symbolic_identifier, multispace0), + delimited(whitespace0, symbolic_identifier, whitespace0), |name| crate::Formula::Predicate( crate::Predicate { @@ -211,17 +253,17 @@ fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula> ( pair ( - delimited(multispace0, symbolic_identifier, multispace0), + delimited(whitespace0, symbolic_identifier, whitespace0), delimited ( - multispace0, + whitespace0, delimited ( tag("("), separated_list(tag(","), term), tag(")") ), - multispace0 + whitespace0 ) ), |(name, arguments)| crate::Formula::Predicate( @@ -253,13 +295,13 @@ fn boolean(i: &str) -> IResult<&str, crate::Formula> ( delimited ( - multispace0, + whitespace0, alt (( map(tag("#true"), |_| true), map(tag("#false"), |_| false) )), - multispace0 + whitespace0 ), |value| crate::Formula::Boolean(value) )(i) @@ -360,14 +402,14 @@ fn term_parenthesized(i: &str) -> IResult<&str, crate::Term> { delimited ( - multispace0, + whitespace0, delimited ( tag("("), term, tag(")") ), - multispace0 + whitespace0 )(i) } @@ -409,9 +451,9 @@ fn term_precedence_1(i: &str) -> IResult<&str, crate::Term> ( delimited ( - multispace0, + whitespace0, preceded(tag("-"), term_precedence_0), - multispace0 + whitespace0 ), |term| crate::Term::Negative(Box::new(term)) ), @@ -468,14 +510,14 @@ fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula> { delimited ( - multispace0, + whitespace0, delimited ( tag("("), formula, tag(")") ), - multispace0 + whitespace0 )(i) } @@ -496,10 +538,14 @@ fn exists(i: &str) -> IResult<&str, crate::Formula> ( delimited ( - multispace0, + whitespace0, preceded ( - tag("exists "), + terminated + ( + tag("exists"), + whitespace_single, + ), pair ( separated_list @@ -510,7 +556,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula> formula_precedence_1 ) ), - multispace0 + whitespace0 ), |(parameters, argument)| crate::Formula::Exists( crate::Exists @@ -527,10 +573,14 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula> ( delimited ( - multispace0, + whitespace0, preceded ( - tag("forall "), + terminated + ( + tag("forall"), + whitespace_single, + ), pair ( separated_list @@ -541,7 +591,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula> formula_precedence_1 ) ), - multispace0 + whitespace0 ), |(parameters, argument)| crate::Formula::ForAll( crate::ForAll @@ -570,9 +620,17 @@ fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula> ( delimited ( - multispace0, - preceded(tag("not "), formula_precedence_1), - multispace0 + whitespace0, + preceded + ( + terminated + ( + tag("not"), + whitespace_single, + ), + formula_precedence_1 + ), + whitespace0 ), |argument| crate::Formula::Not(Box::new(argument)) ),