Add support for comments
This commit is contained in:
parent
ae46634d67
commit
0216f90929
@ -192,7 +192,7 @@ where
|
|||||||
pub fn parse(&self, level: usize) -> Result<crate::Formula, crate::parse::Error>
|
pub fn parse(&self, level: usize) -> Result<crate::Formula, crate::parse::Error>
|
||||||
{
|
{
|
||||||
let indentation = " ".repeat(level);
|
let indentation = " ".repeat(level);
|
||||||
let input = self.input.trim_start();
|
let input = trim_start(self.input);
|
||||||
|
|
||||||
log::trace!("{}- parsing formula: {}", indentation, input);
|
log::trace!("{}- parsing formula: {}", indentation, input);
|
||||||
|
|
||||||
@ -258,7 +258,7 @@ where
|
|||||||
{
|
{
|
||||||
"not" =>
|
"not" =>
|
||||||
{
|
{
|
||||||
let input = input.trim_start();
|
let input = trim_start(input);
|
||||||
log::trace!("{} parsing “not” formula body: {}", indentation, input);
|
log::trace!("{} parsing “not” formula body: {}", indentation, input);
|
||||||
|
|
||||||
let argument = FormulaStr::new(input, self.declarations, self.variable_declaration_stack).parse(level + 1)?;
|
let argument = FormulaStr::new(input, self.declarations, self.variable_declaration_stack).parse(level + 1)?;
|
||||||
@ -297,7 +297,7 @@ where
|
|||||||
|
|
||||||
if let Some(quantifier) = quantifier
|
if let Some(quantifier) = quantifier
|
||||||
{
|
{
|
||||||
let input = input.trim_start();
|
let input = trim_start(input);
|
||||||
log::trace!("{} parsing “{:?}” formula body: {}", indentation, quantifier, input);
|
log::trace!("{} parsing “{:?}” formula body: {}", indentation, quantifier, input);
|
||||||
|
|
||||||
return self.quantified_formula(input, quantifier, level + 1);
|
return self.quantified_formula(input, quantifier, level + 1);
|
||||||
@ -347,7 +347,7 @@ where
|
|||||||
{
|
{
|
||||||
log::trace!("{} parsing predicate {}", indentation, predicate_name);
|
log::trace!("{} parsing predicate {}", indentation, predicate_name);
|
||||||
|
|
||||||
let input = input.trim_start();
|
let input = trim_start(input);
|
||||||
|
|
||||||
// Parse arguments if there are any
|
// Parse arguments if there are any
|
||||||
let (arguments, input) = match parenthesized_expression(input)?
|
let (arguments, input) = match parenthesized_expression(input)?
|
||||||
|
@ -104,7 +104,7 @@ pub(crate) fn variable_declarations(input: &str)
|
|||||||
|
|
||||||
loop
|
loop
|
||||||
{
|
{
|
||||||
input = input.trim_start();
|
input = trim_start(input);
|
||||||
|
|
||||||
input = match symbol(input)
|
input = match symbol(input)
|
||||||
{
|
{
|
||||||
@ -113,7 +113,7 @@ pub(crate) fn variable_declarations(input: &str)
|
|||||||
_ => return Ok(Some((variable_declarations, input))),
|
_ => return Ok(Some((variable_declarations, input))),
|
||||||
};
|
};
|
||||||
|
|
||||||
input = input.trim_start();
|
input = trim_start(input);
|
||||||
|
|
||||||
let (variable_declaration, remaining_input) = match variable_declaration(input)
|
let (variable_declaration, remaining_input) = match variable_declaration(input)
|
||||||
{
|
{
|
||||||
@ -304,7 +304,7 @@ where
|
|||||||
let indentation = " ".repeat(level);
|
let indentation = " ".repeat(level);
|
||||||
log::trace!("{}- parsing term: {}", indentation, self.input);
|
log::trace!("{}- parsing term: {}", indentation, self.input);
|
||||||
|
|
||||||
let input = self.input.trim_start();
|
let input = trim_start(self.input);
|
||||||
|
|
||||||
match input.chars().next()
|
match input.chars().next()
|
||||||
{
|
{
|
||||||
@ -442,7 +442,7 @@ where
|
|||||||
let function_name = identifier;
|
let function_name = identifier;
|
||||||
log::trace!("{} parsing function {}", indentation, function_name);
|
log::trace!("{} parsing function {}", indentation, function_name);
|
||||||
|
|
||||||
let input = input.trim_start();
|
let input = trim_start(input);
|
||||||
|
|
||||||
// Parse arguments if there are any
|
// Parse arguments if there are any
|
||||||
let (arguments, input) = match parenthesized_expression(input)?
|
let (arguments, input) = match parenthesized_expression(input)?
|
||||||
|
@ -3,6 +3,42 @@ fn substring_offset(substring: &str, string: &str) -> usize
|
|||||||
substring.as_ptr() as usize - string.as_ptr() as usize
|
substring.as_ptr() as usize - string.as_ptr() as usize
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn trim_start(mut input: &str) -> &str
|
||||||
|
{
|
||||||
|
loop
|
||||||
|
{
|
||||||
|
let original_input = input;
|
||||||
|
|
||||||
|
input = input.trim_start();
|
||||||
|
|
||||||
|
let mut input_characters = input.chars();
|
||||||
|
|
||||||
|
if let Some('#') = input_characters.next()
|
||||||
|
{
|
||||||
|
input = input_characters.as_str();
|
||||||
|
|
||||||
|
match (input.find('\n'), input.find('\r'))
|
||||||
|
{
|
||||||
|
(Some(newline_index), Some(carriage_return_index)) =>
|
||||||
|
{
|
||||||
|
let split_index = std::cmp::min(newline_index, carriage_return_index);
|
||||||
|
input = input.split_at(split_index).1;
|
||||||
|
},
|
||||||
|
(Some(split_index), _)
|
||||||
|
| (_, Some(split_index)) => input = input.split_at(split_index).1,
|
||||||
|
_ => input = &input[..input.len()],
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if input.is_empty() || input == original_input
|
||||||
|
{
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
input
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Clone, Copy, Eq, PartialEq)]
|
#[derive(Clone, Copy, Eq, PartialEq)]
|
||||||
pub(crate) enum Keyword
|
pub(crate) enum Keyword
|
||||||
{
|
{
|
||||||
@ -366,7 +402,7 @@ impl<'i, F> Tokens<'i, F>
|
|||||||
|
|
||||||
fn next_token(&mut self) -> Option<Result<(usize, usize, Token<'i>), crate::parse::Error>>
|
fn next_token(&mut self) -> Option<Result<(usize, usize, Token<'i>), crate::parse::Error>>
|
||||||
{
|
{
|
||||||
self.input = self.input.trim_start();
|
self.input = trim_start(self.input);
|
||||||
let index_left = substring_offset(self.input, self.original_input);
|
let index_left = substring_offset(self.input, self.original_input);
|
||||||
|
|
||||||
let first_character = match self.input.chars().next()
|
let first_character = match self.input.chars().next()
|
||||||
|
Loading…
Reference in New Issue
Block a user