use super::terms::*;
use super::tokens::*;
pub fn formula
(input: &str, parser: &P)
-> Result, crate::parse::Error>
where
P: super::Parser,
{
let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
let formula_str = FormulaStr::new(input, parser, &variable_declaration_stack);
let formula = formula_str.parse(0)?;
let free_variable_declarations = match variable_declaration_stack
{
crate::VariableDeclarationStackLayer::Free(free_variable_declarations) =>
std::rc::Rc::new(free_variable_declarations.into_inner()),
_ => unreachable!(),
};
Ok(crate::OpenFormula
{
formula,
free_variable_declarations,
})
}
pub(crate) fn predicate_name(identifier: &str) -> Option<(&str, &str)>
{
function_name(identifier)
}
#[derive(Clone, Copy, Eq, PartialEq)]
enum LogicalConnective
{
And,
IfAndOnlyIf,
ImpliesLeftToRight,
ImpliesRightToLeft,
Or,
}
impl LogicalConnective
{
fn level(&self) -> usize
{
match self
{
Self::And => 1,
Self::Or => 2,
Self::ImpliesLeftToRight
| Self::ImpliesRightToLeft => 3,
Self::IfAndOnlyIf => 4,
}
}
}
impl std::fmt::Debug for LogicalConnective
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::And => write!(formatter, "and"),
Self::IfAndOnlyIf => write!(formatter, "<->"),
Self::ImpliesLeftToRight => write!(formatter, "->"),
Self::ImpliesRightToLeft => write!(formatter, "<-"),
Self::Or => write!(formatter, "or"),
}
}
}
struct FormulaStr<'i, 'd, 'p, 'v, P>
where
P: super::Parser,
{
input: &'i str,
parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>,
}
impl<'i, 'd, 'p, 'v, P> FormulaStr<'i, 'd, 'p, 'v, P>
where
P: super::Parser,
{
pub fn new(input: &'i str, parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>)
-> Self
{
Self
{
input,
parser,
variable_declaration_stack,
}
}
fn logical_connectives(&self) -> Tokens<'i, impl FnMut(Token<'i>) -> Option>
{
let functor = |token| match token
{
Token::Identifier("and") => Some(LogicalConnective::And),
Token::Identifier("or") => Some(LogicalConnective::Or),
Token::Symbol(Symbol::ArrowLeft) => Some(LogicalConnective::ImpliesRightToLeft),
Token::Symbol(Symbol::ArrowLeftAndRight) => Some(LogicalConnective::IfAndOnlyIf),
Token::Symbol(Symbol::ArrowRight) => Some(LogicalConnective::ImpliesLeftToRight),
_ => None,
};
Tokens::new_filter_map(self.input, functor)
}
fn split_at_logical_connective(&self, logical_connective: LogicalConnective)
-> TokenSplit) -> Option>>>
{
let predicate = move |token: &_| match token
{
Token::Identifier("and") => logical_connective == LogicalConnective::And,
Token::Identifier("or") => logical_connective == LogicalConnective::Or,
Token::Symbol(Symbol::ArrowLeft) =>
logical_connective == LogicalConnective::ImpliesRightToLeft,
Token::Symbol(Symbol::ArrowLeftAndRight) =>
logical_connective == LogicalConnective::IfAndOnlyIf,
Token::Symbol(Symbol::ArrowRight) =>
logical_connective == LogicalConnective::ImpliesLeftToRight,
_ => false,
};
Tokens::new_filter(self.input, predicate).split()
}
pub fn top_level_logical_connective(&self)
-> Result