Retrieve declarations using traits and not objects

This commit is contained in:
Patrick Lühne 2020-04-17 04:06:22 +02:00
parent 0e78e4ea57
commit 0d5971cad7
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 185 additions and 124 deletions

View File

@ -9,23 +9,3 @@ pub(crate) use literals::{boolean, integer, special_integer, string};
pub(crate) use names::{function_or_predicate_name, variable_name};
pub use terms::term;
pub use formulas::formula;
pub struct Declarations
{
function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
free_variable_declarations: std::cell::RefCell<crate::VariableDeclarations>,
}
impl Declarations
{
pub fn new() -> Self
{
Self
{
function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
free_variable_declarations: std::cell::RefCell::new(vec![]),
}
}
}

View File

@ -9,10 +9,12 @@ use nom::
sequence::{delimited, pair, preceded, terminated, tuple},
};
use super::{Declarations, boolean, word_boundary};
use super::{boolean, word_boundary};
pub fn predicate<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
pub fn predicate<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Predicate>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -25,34 +27,17 @@ pub fn predicate<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDec
None => vec![],
};
let mut predicate_declarations = d.predicate_declarations.borrow_mut();
let declaration = match predicate_declarations.iter()
.find(|x| x.name == name && x.arity == arguments.len())
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::PredicateDeclaration
{
name: name.to_string(),
arity: arguments.len(),
};
let declaration = std::rc::Rc::new(declaration);
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
};
let declaration = d.find_or_create_predicate_declaration(name, arguments.len());
crate::Predicate::new(declaration, arguments)
},
)(i)
}
fn not<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn not<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -69,8 +54,10 @@ fn not<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSt
)(i)
}
fn and<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn and<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formulas>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map_res
(
@ -102,8 +89,10 @@ fn and<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSt
)(i)
}
fn or<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn or<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formulas>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map_res
(
@ -135,9 +124,10 @@ fn or<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSta
)(i)
}
fn implies_left_to_right<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn implies_left_to_right<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -165,9 +155,10 @@ fn implies_left_to_right<'i, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn implies_right_to_left<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn implies_right_to_left<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -195,8 +186,10 @@ fn implies_right_to_left<'i, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn if_and_only_if<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn if_and_only_if<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formulas>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map_res
(
@ -224,9 +217,11 @@ fn if_and_only_if<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDe
)(i)
}
fn quantified_formula<'i, 'b, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer, keyword: &'b str)
fn quantified_formula<'i, 'b, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer,
keyword: &'b str)
-> IResult<&'i str, crate::QuantifiedFormula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
preceded
(
@ -280,8 +275,10 @@ fn quantified_formula<'i, 'b, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn compare<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn compare<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Compare>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -335,21 +332,26 @@ fn compare<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarati
)(i)
}
fn exists<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn exists<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::QuantifiedFormula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
quantified_formula(i, d, v, "exists")
}
fn for_all<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn for_all<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::QuantifiedFormula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
quantified_formula(i, d, v, "forall")
}
fn formula_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_parenthesized<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
delimited
(
@ -367,9 +369,10 @@ fn formula_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn formula_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_0<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -392,9 +395,10 @@ fn formula_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_1<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -412,9 +416,10 @@ fn formula_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_2<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -423,9 +428,10 @@ fn formula_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_3<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -438,9 +444,10 @@ fn formula_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_4<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -453,9 +460,10 @@ fn formula_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_5<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_5<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -465,9 +473,10 @@ fn formula_precedence_5<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn formula_precedence_6<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn formula_precedence_6<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -480,8 +489,10 @@ fn formula_precedence_6<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
pub fn formula<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
pub fn formula<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Formula>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
formula_precedence_6(i, d, v)
}
@ -489,9 +500,9 @@ pub fn formula<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDecla
#[cfg(test)]
mod tests
{
use crate::parse::formulas::*;
use crate::parse::formulas as original;
use crate::{Formula, ImplicationDirection, Term, VariableDeclarationStackLayer};
use crate::parse::formulas as original;
use crate::utils::*;
fn formula(i: &str) -> Formula
{

View File

@ -9,11 +9,12 @@ use nom::
sequence::{delimited, pair, preceded, terminated},
};
use super::{Declarations, boolean, function_or_predicate_name, integer, special_integer, string,
variable_name};
use super::{boolean, function_or_predicate_name, integer, special_integer, string, variable_name};
fn negative<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn negative<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -37,8 +38,10 @@ fn negative<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
)(i)
}
fn absolute_value<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn absolute_value<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -60,9 +63,11 @@ fn absolute_value<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDe
)(i)
}
pub(crate) fn function_or_predicate<'i, 'v>(i: &'i str, d: &Declarations,
pub(crate) fn function_or_predicate<'i, 'v, D>(i: &'i str, d: &D,
v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, (&'i str, Option<crate::Terms>)>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
pair
(
@ -97,8 +102,10 @@ pub(crate) fn function_or_predicate<'i, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn function<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
fn function<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Function>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
map
(
@ -111,26 +118,7 @@ fn function<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
None => vec![],
};
let mut function_declarations = d.function_declarations.borrow_mut();
let declaration = match function_declarations.iter()
.find(|x| x.name == name && x.arity == arguments.len())
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::FunctionDeclaration
{
name: name.to_string(),
arity: arguments.len(),
};
let declaration = std::rc::Rc::new(declaration);
function_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
};
let declaration = d.find_or_create_function_declaration(name, arguments.len());
crate::Function::new(declaration, arguments)
},
@ -161,9 +149,10 @@ fn variable<'i, 'v>(i: &'i str, v: &'v crate::VariableDeclarationStackLayer)
)(i)
}
fn term_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn term_parenthesized<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
delimited
(
@ -181,9 +170,10 @@ fn term_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
)(i)
}
fn term_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn term_precedence_0<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -222,9 +212,10 @@ fn term_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn term_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn term_precedence_1<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -233,9 +224,10 @@ fn term_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn term_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn term_precedence_2<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -266,9 +258,10 @@ fn term_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn term_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer)
fn term_precedence_3<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -311,8 +304,10 @@ fn term_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
fn term_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
v: &'v crate::VariableDeclarationStackLayer) -> IResult<&'i str, crate::Term>
fn term_precedence_4<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
alt
((
@ -353,8 +348,10 @@ fn term_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
))(i)
}
pub fn term<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
pub fn term<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
-> IResult<&'i str, crate::Term>
where
D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
{
term_precedence_4(i, d, v)
}
@ -362,9 +359,9 @@ pub fn term<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
#[cfg(test)]
mod tests
{
use crate::parse::terms::*;
use crate::parse::terms as original;
use crate::{Term, VariableDeclaration, VariableDeclarationStackLayer};
use crate::parse::terms as original;
use crate::utils::*;
fn term(i: &str) -> Term
{

View File

@ -1,20 +1,15 @@
pub trait FindFunctionDeclaration
pub trait FindOrCreateFunctionDeclaration
{
fn find_function_declaration(&self, name: &str, arity: usize)
fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<crate::FunctionDeclaration>;
}
pub trait FindPredicateDeclaration
pub trait FindOrCreatePredicateDeclaration
{
fn find_predicate_declaration(&self, name: &str, arity: usize)
fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<crate::PredicateDeclaration>;
}
pub trait FindVariableDeclaration
{
fn find_variable_declaration(&self, name: &str) -> std::rc::Rc<crate::VariableDeclaration>;
}
pub struct BoundVariableDeclarations<'p>
{
parent: &'p VariableDeclarationStackLayer<'p>,
@ -144,3 +139,81 @@ impl<'p> VariableDeclarationStackLayer<'p>
}
}
}
#[cfg(test)]
pub struct Declarations
{
function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
//free_variable_declarations: std::cell::RefCell<crate::VariableDeclarations>,
}
#[cfg(test)]
impl Declarations
{
pub fn new() -> Self
{
Self
{
function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
//free_variable_declarations: std::cell::RefCell::new(vec![]),
}
}
}
#[cfg(test)]
impl FindOrCreateFunctionDeclaration for Declarations
{
fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<crate::FunctionDeclaration>
{
let mut function_declarations = self.function_declarations.borrow_mut();
match function_declarations.iter().find(|x| x.name == name && x.arity == arity)
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::FunctionDeclaration
{
name: name.to_string(),
arity,
};
let declaration = std::rc::Rc::new(declaration);
function_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
}
}
}
#[cfg(test)]
impl FindOrCreatePredicateDeclaration for Declarations
{
fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<crate::PredicateDeclaration>
{
let mut predicate_declarations = self.predicate_declarations.borrow_mut();
match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity)
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::PredicateDeclaration
{
name: name.to_string(),
arity,
};
let declaration = std::rc::Rc::new(declaration);
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
}
}
}