2020-02-04 23:33:59 +01:00
|
|
|
mod arithmetic_terms;
|
|
|
|
|
|
|
|
pub(crate) use arithmetic_terms::*;
|
|
|
|
|
|
|
|
#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
|
|
|
|
pub(crate) enum OperatorNotation
|
|
|
|
{
|
|
|
|
Prefix,
|
|
|
|
Infix,
|
|
|
|
}
|
|
|
|
|
2020-02-05 19:40:21 +01:00
|
|
|
#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
|
|
|
|
pub enum Domain
|
2020-02-04 16:42:50 +01:00
|
|
|
{
|
|
|
|
Program,
|
|
|
|
Integer,
|
|
|
|
}
|
|
|
|
|
2020-02-05 19:40:21 +01:00
|
|
|
impl std::fmt::Debug for Domain
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
match self
|
|
|
|
{
|
|
|
|
Domain::Program => write!(formatter, "program"),
|
|
|
|
Domain::Integer => write!(formatter, "integer"),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl std::fmt::Display for Domain
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
write!(formatter, "{:?}", self)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-05-05 19:40:57 +02:00
|
|
|
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
|
|
|
|
pub enum ProofDirection
|
|
|
|
{
|
|
|
|
Forward,
|
|
|
|
Backward,
|
|
|
|
Both,
|
|
|
|
}
|
|
|
|
|
2020-05-07 02:53:48 +02:00
|
|
|
impl std::fmt::Debug for ProofDirection
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
match self
|
|
|
|
{
|
|
|
|
ProofDirection::Forward => write!(formatter, "forward"),
|
|
|
|
ProofDirection::Backward => write!(formatter, "backward"),
|
|
|
|
ProofDirection::Both => write!(formatter, "both"),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl std::fmt::Display for ProofDirection
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
write!(formatter, "{:?}", self)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
pub struct InvalidProofDirectionError;
|
|
|
|
|
|
|
|
impl std::fmt::Debug for InvalidProofDirectionError
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
write!(formatter, "invalid proof direction")
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl std::fmt::Display for InvalidProofDirectionError
|
|
|
|
{
|
|
|
|
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
{
|
|
|
|
write!(formatter, "{:?}", self)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl std::str::FromStr for ProofDirection
|
|
|
|
{
|
|
|
|
type Err = InvalidProofDirectionError;
|
|
|
|
|
|
|
|
fn from_str(s: &str) -> Result<Self, Self::Err>
|
|
|
|
{
|
|
|
|
match s
|
|
|
|
{
|
|
|
|
"forward" => Ok(ProofDirection::Forward),
|
|
|
|
"backward" => Ok(ProofDirection::Backward),
|
|
|
|
"both" => Ok(ProofDirection::Both),
|
|
|
|
_ => Err(InvalidProofDirectionError),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-02-04 16:42:50 +01:00
|
|
|
pub(crate) struct ScopedFormula
|
|
|
|
{
|
|
|
|
pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
|
2020-04-17 03:37:53 +02:00
|
|
|
pub formula: foliage::Formula,
|
2020-02-04 16:42:50 +01:00
|
|
|
}
|
2020-02-05 01:10:33 +01:00
|
|
|
|
2020-04-17 00:09:44 +02:00
|
|
|
pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
|
2020-02-09 04:26:24 +01:00
|
|
|
{
|
|
|
|
match scoped_formula.free_variable_declarations.is_empty()
|
|
|
|
{
|
2020-04-17 03:37:53 +02:00
|
|
|
true => scoped_formula.formula,
|
2020-04-17 00:09:44 +02:00
|
|
|
false => foliage::Formula::exists(scoped_formula.free_variable_declarations,
|
2020-04-17 03:37:53 +02:00
|
|
|
Box::new(scoped_formula.formula)),
|
2020-02-09 04:26:24 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-04-17 00:09:44 +02:00
|
|
|
pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
|
2020-02-09 04:26:24 +01:00
|
|
|
{
|
|
|
|
match scoped_formula.free_variable_declarations.is_empty()
|
|
|
|
{
|
2020-04-17 03:37:53 +02:00
|
|
|
true => scoped_formula.formula,
|
2020-04-17 00:09:44 +02:00
|
|
|
false => foliage::Formula::for_all(scoped_formula.free_variable_declarations,
|
2020-04-17 03:37:53 +02:00
|
|
|
Box::new(scoped_formula.formula)),
|
2020-02-09 04:26:24 +01:00
|
|
|
}
|
|
|
|
}
|
2020-02-05 19:40:21 +01:00
|
|
|
|
2020-05-05 19:40:57 +02:00
|
|
|
/*pub fn parse_predicate_declaration(input: &str)
|
2020-02-05 01:10:33 +01:00
|
|
|
-> Result<std::rc::Rc<foliage::PredicateDeclaration>, crate::Error>
|
|
|
|
{
|
|
|
|
let mut parts = input.split("/");
|
|
|
|
|
2020-02-05 19:42:53 +01:00
|
|
|
let name = parts.next().ok_or(crate::Error::new_parse_predicate_declaration())?;
|
2020-02-05 01:10:33 +01:00
|
|
|
|
|
|
|
use std::str::FromStr;
|
|
|
|
|
|
|
|
let arity = match parts.next()
|
|
|
|
{
|
|
|
|
Some(arity)
|
|
|
|
=> usize::from_str(arity).map_err(|_| crate::Error::new_parse_predicate_declaration())?,
|
2020-02-05 19:42:53 +01:00
|
|
|
None => 0,
|
2020-02-05 01:10:33 +01:00
|
|
|
};
|
|
|
|
|
|
|
|
if parts.next().is_some()
|
|
|
|
{
|
|
|
|
return Err(crate::Error::new_parse_predicate_declaration());
|
|
|
|
}
|
|
|
|
|
|
|
|
Ok(std::rc::Rc::new(foliage::PredicateDeclaration
|
|
|
|
{
|
2020-02-05 19:42:53 +01:00
|
|
|
name: name.to_string(),
|
2020-02-05 01:10:33 +01:00
|
|
|
arity,
|
|
|
|
}))
|
2020-05-05 19:40:57 +02:00
|
|
|
}*/
|
2020-02-05 19:40:21 +01:00
|
|
|
|
2020-02-09 04:26:24 +01:00
|
|
|
pub type InputConstantDeclarationDomains
|
|
|
|
= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, Domain>;
|
|
|
|
|
2020-05-05 19:40:57 +02:00
|
|
|
/*pub fn parse_constant_declaration(input: &str)
|
2020-02-05 19:40:21 +01:00
|
|
|
-> Result<(std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain), crate::Error>
|
|
|
|
{
|
|
|
|
let mut parts = input.split(":");
|
|
|
|
|
|
|
|
let name = parts.next().ok_or(crate::Error::new_parse_constant_declaration())?.trim();
|
|
|
|
|
|
|
|
let domain = match parts.next()
|
|
|
|
{
|
|
|
|
None => crate::Domain::Program,
|
|
|
|
Some(value) => match value.trim()
|
|
|
|
{
|
|
|
|
"program" => crate::Domain::Program,
|
|
|
|
"integer" => crate::Domain::Integer,
|
|
|
|
_ => return Err(crate::Error::new_parse_constant_declaration()),
|
|
|
|
},
|
|
|
|
};
|
|
|
|
|
|
|
|
if parts.next().is_some()
|
|
|
|
{
|
|
|
|
return Err(crate::Error::new_parse_constant_declaration());
|
|
|
|
}
|
|
|
|
|
|
|
|
let constant_declaration = std::rc::Rc::new(foliage::FunctionDeclaration
|
|
|
|
{
|
|
|
|
name: name.to_string(),
|
|
|
|
arity: 0,
|
|
|
|
});
|
|
|
|
|
|
|
|
Ok((constant_declaration, domain))
|
2020-05-05 19:40:57 +02:00
|
|
|
}*/
|