Simplify representation of quantified formulas
This commit is contained in:
parent
903993dbec
commit
80636b447a
31
src/ast.rs
31
src/ast.rs
|
@ -263,32 +263,13 @@ impl Compare
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||||
pub struct Exists
|
pub struct QuantifiedFormula
|
||||||
{
|
{
|
||||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
pub parameters: std::rc::Rc<VariableDeclarations>,
|
||||||
pub argument: Box<Formula>,
|
pub argument: Box<Formula>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Exists
|
impl QuantifiedFormula
|
||||||
{
|
|
||||||
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
|
||||||
{
|
|
||||||
Self
|
|
||||||
{
|
|
||||||
parameters,
|
|
||||||
argument,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
|
||||||
pub struct ForAll
|
|
||||||
{
|
|
||||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
|
||||||
pub argument: Box<Formula>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl ForAll
|
|
||||||
{
|
{
|
||||||
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||||
{
|
{
|
||||||
|
@ -471,8 +452,8 @@ pub enum Formula
|
||||||
And(Formulas),
|
And(Formulas),
|
||||||
Boolean(bool),
|
Boolean(bool),
|
||||||
Compare(Compare),
|
Compare(Compare),
|
||||||
Exists(Exists),
|
Exists(QuantifiedFormula),
|
||||||
ForAll(ForAll),
|
ForAll(QuantifiedFormula),
|
||||||
IfAndOnlyIf(Formulas),
|
IfAndOnlyIf(Formulas),
|
||||||
Implies(Implies),
|
Implies(Implies),
|
||||||
Not(Box<Formula>),
|
Not(Box<Formula>),
|
||||||
|
@ -501,7 +482,7 @@ impl Formula
|
||||||
|
|
||||||
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||||
{
|
{
|
||||||
Self::Exists(Exists::new(parameters, argument))
|
Self::Exists(QuantifiedFormula::new(parameters, argument))
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
|
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
|
||||||
|
@ -516,7 +497,7 @@ impl Formula
|
||||||
|
|
||||||
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||||
{
|
{
|
||||||
Self::ForAll(ForAll::new(parameters, argument))
|
Self::ForAll(QuantifiedFormula::new(parameters, argument))
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
|
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
|
||||||
|
|
|
@ -215,11 +215,8 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn quantified_expression<'a, 'b, T, N>(i: &'a str, d: &Declarations, keyword: &'b str,
|
fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
|
||||||
new_functor: N)
|
-> IResult<&'a str, crate::QuantifiedFormula>
|
||||||
-> IResult<&'a str, T>
|
|
||||||
where
|
|
||||||
N: Fn(std::rc::Rc<crate::VariableDeclarations>, Box<crate::Formula>) -> T
|
|
||||||
{
|
{
|
||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
|
@ -230,7 +227,7 @@ where
|
||||||
),
|
),
|
||||||
cut
|
cut
|
||||||
(
|
(
|
||||||
|i| -> IResult<&'a str, T>
|
|i|
|
||||||
{
|
{
|
||||||
let (i, variable_declarations) =
|
let (i, variable_declarations) =
|
||||||
map
|
map
|
||||||
|
@ -270,7 +267,7 @@ where
|
||||||
d.variable_declaration_stack.borrow_mut().pop()
|
d.variable_declaration_stack.borrow_mut().pop()
|
||||||
.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;
|
.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;
|
||||||
|
|
||||||
Ok((i, new_functor(variable_declarations, Box::new(argument))))
|
Ok((i, crate::QuantifiedFormula::new(variable_declarations, Box::new(argument))))
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
)(i)
|
)(i)
|
||||||
|
@ -330,14 +327,14 @@ fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists>
|
fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
|
||||||
{
|
{
|
||||||
quantified_expression::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
|
quantified_formula(i, d, "exists")
|
||||||
}
|
}
|
||||||
|
|
||||||
fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
|
fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
|
||||||
{
|
{
|
||||||
quantified_expression::<crate::ForAll, _>(i, d, "forall", crate::ForAll::new)
|
quantified_formula(i, d, "forall")
|
||||||
}
|
}
|
||||||
|
|
||||||
fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||||
|
|
Loading…
Reference in New Issue