Improve interface for declaration types
This commit is contained in:
parent
036544d3c7
commit
a0fefe9b6a
@ -2,8 +2,9 @@ pub trait FunctionDeclaration
|
||||
{
|
||||
fn new(name: String, arity: usize) -> Self;
|
||||
|
||||
fn name(&self) -> &str;
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
|
||||
fn arity(&self) -> usize;
|
||||
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
|
||||
}
|
||||
|
||||
impl FunctionDeclaration for crate::FunctionDeclaration
|
||||
@ -17,23 +18,29 @@ impl FunctionDeclaration for crate::FunctionDeclaration
|
||||
}
|
||||
}
|
||||
|
||||
fn name(&self) -> &str
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
&self.name
|
||||
write!(formatter, "{}", self.name)
|
||||
}
|
||||
|
||||
fn arity(&self) -> usize
|
||||
{
|
||||
self.arity
|
||||
}
|
||||
|
||||
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
|
||||
{
|
||||
self.name == other_name && self.arity == other_arity
|
||||
}
|
||||
}
|
||||
|
||||
pub trait PredicateDeclaration
|
||||
{
|
||||
fn new(name: String, arity: usize) -> Self;
|
||||
|
||||
fn name(&self) -> &str;
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
|
||||
fn arity(&self) -> usize;
|
||||
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
|
||||
}
|
||||
|
||||
impl PredicateDeclaration for crate::PredicateDeclaration
|
||||
@ -47,22 +54,28 @@ impl PredicateDeclaration for crate::PredicateDeclaration
|
||||
}
|
||||
}
|
||||
|
||||
fn name(&self) -> &str
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
&self.name
|
||||
write!(formatter, "{}", self.name)
|
||||
}
|
||||
|
||||
fn arity(&self) -> usize
|
||||
{
|
||||
self.arity
|
||||
}
|
||||
|
||||
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
|
||||
{
|
||||
self.name == other_name && self.arity == other_arity
|
||||
}
|
||||
}
|
||||
|
||||
pub trait VariableDeclaration
|
||||
{
|
||||
fn new(name: String) -> Self;
|
||||
|
||||
fn name(&self) -> &str;
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
|
||||
fn matches_name(&self, other_name: &str) -> bool;
|
||||
}
|
||||
|
||||
impl VariableDeclaration for crate::VariableDeclaration
|
||||
@ -75,9 +88,14 @@ impl VariableDeclaration for crate::VariableDeclaration
|
||||
}
|
||||
}
|
||||
|
||||
fn name(&self) -> &str
|
||||
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
&self.name
|
||||
write!(formatter, "{}", self.name)
|
||||
}
|
||||
|
||||
fn matches_name(&self, other_name: &str) -> bool
|
||||
{
|
||||
self.name == other_name
|
||||
}
|
||||
}
|
||||
|
||||
@ -86,8 +104,7 @@ pub trait Flavor
|
||||
type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
|
||||
type PredicateDeclaration:
|
||||
PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
|
||||
type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash
|
||||
+ std::fmt::Display;
|
||||
type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
|
||||
}
|
||||
|
||||
pub struct DefaultFlavor;
|
||||
|
@ -1,4 +1,4 @@
|
||||
use crate::flavor::PredicateDeclaration as _;
|
||||
use crate::flavor::{PredicateDeclaration as _, VariableDeclaration as _};
|
||||
use super::terms::*;
|
||||
|
||||
impl std::fmt::Debug for crate::ComparisonOperator
|
||||
@ -180,7 +180,8 @@ where
|
||||
|
||||
for parameter in exists.parameters.iter()
|
||||
{
|
||||
write!(formatter, "{}{}", separator, parameter)?;
|
||||
write!(formatter, "{}", separator)?;
|
||||
parameter.display_name(formatter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
@ -204,7 +205,8 @@ where
|
||||
|
||||
for parameter in for_all.parameters.iter()
|
||||
{
|
||||
write!(formatter, "{}{}", separator, parameter)?;
|
||||
write!(formatter, "{}", separator)?;
|
||||
parameter.display_name(formatter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
@ -341,7 +343,7 @@ where
|
||||
crate::Formula::Boolean(false) => write!(formatter, "false")?,
|
||||
crate::Formula::Predicate(predicate) =>
|
||||
{
|
||||
write!(formatter, "{}", predicate.declaration.name())?;
|
||||
predicate.declaration.display_name(formatter)?;
|
||||
|
||||
if !predicate.arguments.is_empty()
|
||||
{
|
||||
|
@ -1,4 +1,4 @@
|
||||
use crate::flavor::FunctionDeclaration as _;
|
||||
use crate::flavor::{FunctionDeclaration as _, VariableDeclaration as _};
|
||||
|
||||
impl std::fmt::Debug for crate::SpecialInteger
|
||||
{
|
||||
@ -190,10 +190,10 @@ where
|
||||
crate::Term::Integer(value) => write!(formatter, "{}", value)?,
|
||||
crate::Term::String(value) => write!(formatter, "\"{}\"",
|
||||
value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?,
|
||||
crate::Term::Variable(variable) => write!(formatter, "{}", variable.declaration)?,
|
||||
crate::Term::Variable(variable) => variable.declaration.display_name(formatter)?,
|
||||
crate::Term::Function(function) =>
|
||||
{
|
||||
write!(formatter, "{}", function.declaration.name())?;
|
||||
function.declaration.display_name(formatter)?;
|
||||
|
||||
assert!(function.declaration.arity() == function.arguments.len(),
|
||||
"number of function arguments differs from declaration (expected {}, got {})",
|
||||
|
12
src/utils.rs
12
src/utils.rs
@ -70,7 +70,7 @@ where
|
||||
VariableDeclarationStackLayer::Free(free_variable_declarations) =>
|
||||
{
|
||||
if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
|
||||
.find(|x| x.name() == variable_name)
|
||||
.find(|x| x.matches_name(variable_name))
|
||||
{
|
||||
return Some(std::rc::Rc::clone(&variable_declaration));
|
||||
}
|
||||
@ -81,7 +81,7 @@ where
|
||||
{
|
||||
if let Some(variable_declaration) = bound_variable_declarations
|
||||
.variable_declarations.iter()
|
||||
.find(|x| x.name() == variable_name)
|
||||
.find(|x| x.matches_name(variable_name))
|
||||
{
|
||||
return Some(std::rc::Rc::clone(&variable_declaration));
|
||||
}
|
||||
@ -98,7 +98,7 @@ where
|
||||
VariableDeclarationStackLayer::Free(free_variable_declarations) =>
|
||||
{
|
||||
if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
|
||||
.find(|x| x.name() == variable_name)
|
||||
.find(|x| x.matches_name(variable_name))
|
||||
{
|
||||
return std::rc::Rc::clone(&variable_declaration);
|
||||
}
|
||||
@ -115,7 +115,7 @@ where
|
||||
{
|
||||
if let Some(variable_declaration) = bound_variable_declarations
|
||||
.variable_declarations.iter()
|
||||
.find(|x| x.name() == variable_name)
|
||||
.find(|x| x.matches_name(variable_name))
|
||||
{
|
||||
return std::rc::Rc::clone(&variable_declaration);
|
||||
}
|
||||
@ -184,7 +184,7 @@ where
|
||||
{
|
||||
let mut function_declarations = self.function_declarations.borrow_mut();
|
||||
|
||||
match function_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
|
||||
match function_declarations.iter().find(|x| x.matches_signature(name, arity))
|
||||
{
|
||||
Some(declaration) => std::rc::Rc::clone(&declaration),
|
||||
None =>
|
||||
@ -209,7 +209,7 @@ where
|
||||
{
|
||||
let mut predicate_declarations = self.predicate_declarations.borrow_mut();
|
||||
|
||||
match predicate_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
|
||||
match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
|
||||
{
|
||||
Some(declaration) => std::rc::Rc::clone(&declaration),
|
||||
None =>
|
||||
|
Loading…
x
Reference in New Issue
Block a user