#[cfg(feature = "serde")]
use serde::{Deserialize, Serialize};
use std::borrow::Cow;
use std::convert::AsRef;
use std::fmt;
use std::path::PathBuf;
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum Name<'a> {
LowerWord(Cow<'a, str>),
SingleQuoted(Cow<'a, str>),
Integer(Cow<'a, str>),
}
impl<'a> AsRef<str> for Name<'a> {
fn as_ref(&self) -> &str {
use self::Name::*;
match self {
LowerWord(name) => name,
SingleQuoted(name) => name,
Integer(name) => name,
}
}
}
impl<'a> fmt::Display for Name<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}", self.as_ref())
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct Variable<'a>(pub Cow<'a, str>);
impl<'a> AsRef<str> for Variable<'a> {
fn as_ref(&self) -> &str {
self.0.as_ref()
}
}
impl<'a> fmt::Display for Variable<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}", self.as_ref())
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum FofTerm<'a> {
Variable(Variable<'a>),
Constant(Name<'a>),
Functor(Name<'a>, Vec<FofTerm<'a>>),
}
fn fmt_args(f: &mut fmt::Formatter, args: &[FofTerm]) -> fmt::Result {
if args.is_empty() {
return Ok(());
}
write!(f, "(")?;
let mut args = args.iter();
write!(f, "{}", args.next().unwrap())?;
for arg in args {
write!(f, ",{}", arg)?;
}
write!(f, ")")
}
impl<'a> fmt::Display for FofTerm<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::FofTerm::*;
match self {
Variable(x) => write!(f, "{}", x),
Constant(c) => write!(f, "{}", c),
Functor(name, args) => {
write!(f, "{}", name)?;
fmt_args(f, args)
}
}
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum UnaryConnective {
Not,
}
impl fmt::Display for UnaryConnective {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::UnaryConnective::*;
match self {
Not => write!(f, "~"),
}
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum InfixEquality {
Equal,
NotEqual,
}
impl fmt::Display for InfixEquality {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::InfixEquality::*;
match self {
Equal => write!(f, "="),
NotEqual => write!(f, "!="),
}
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum NonAssocConnective {
LRImplies,
RLImplies,
Equivalent,
NotEquivalent,
NotOr,
NotAnd,
}
impl fmt::Display for NonAssocConnective {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::NonAssocConnective::*;
match self {
LRImplies => write!(f, "=>"),
RLImplies => write!(f, "<="),
Equivalent => write!(f, "<=>"),
NotEquivalent => write!(f, "<~>"),
NotOr => write!(f, "~|"),
NotAnd => write!(f, "~&"),
}
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum AssocConnective {
And,
Or,
}
impl fmt::Display for AssocConnective {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::AssocConnective::*;
match self {
And => write!(f, "&"),
Or => write!(f, "|"),
}
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum FofQuantifier {
Forall,
Exists,
}
impl fmt::Display for FofQuantifier {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::FofQuantifier::*;
match self {
Forall => write!(f, "!"),
Exists => write!(f, "?"),
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum FofFormula<'a> {
Boolean(bool),
Infix(InfixEquality, FofTerm<'a>, FofTerm<'a>),
Proposition(Name<'a>),
Predicate(Name<'a>, Vec<FofTerm<'a>>),
Unary(UnaryConnective, Box<FofFormula<'a>>),
NonAssoc(NonAssocConnective, Box<FofFormula<'a>>, Box<FofFormula<'a>>),
Assoc(AssocConnective, Vec<FofFormula<'a>>),
Quantified(FofQuantifier, Vec<Variable<'a>>, Box<FofFormula<'a>>),
}
impl<'a> fmt::Display for FofFormula<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::FofFormula::*;
match self {
Boolean(b) => write!(f, "${}", b),
Infix(op, left, right) => write!(f, "{}{}{}", left, op, right),
Proposition(name) => write!(f, "{}", name),
Predicate(name, args) => {
write!(f, "{}", name)?;
fmt_args(f, args)
}
Unary(op, sub) => write!(f, "{}({})", op, sub),
NonAssoc(op, left, right) => write!(f, "({}{}{})", left, op, right),
Assoc(op, args) => {
if args.is_empty() {
panic!("displaying empty associative formula");
}
let mut args = args.iter();
write!(f, "({}", args.next().unwrap())?;
for arg in args {
write!(f, "{}{}", op, arg)?;
}
write!(f, ")")
}
Quantified(op, bound, sub) => {
if bound.is_empty() {
panic!("displaying empty quantifier");
}
write!(f, "{}[", op)?;
let mut bound = bound.iter();
write!(f, "{}", bound.next().unwrap())?;
for x in bound {
write!(f, ",{}", x)?;
}
write!(f, "]:{}", sub)
}
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum Literal<'a> {
Literal(FofFormula<'a>),
NegatedLiteral(FofFormula<'a>),
EqualityLiteral(FofFormula<'a>),
}
impl<'a> fmt::Display for Literal<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::Literal::*;
match self {
Literal(fof) => write!(f, "{}", fof),
NegatedLiteral(fof) => write!(f, "~{}", fof),
EqualityLiteral(fof) => write!(f, "{}", fof),
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct CnfFormula<'a>(pub Vec<Literal<'a>>);
impl<'a> fmt::Display for CnfFormula<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let mut literals = self.0.iter();
write!(f, "{}", literals.next().unwrap())?;
for literal in literals {
write!(f, "|{}", literal)?;
}
Ok(())
}
}
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum FormulaRole {
Axiom,
Hypothesis,
Definition,
Assumption,
Lemma,
Theorem,
Corollary,
Conjecture,
NegatedConjecture,
Plain,
Unknown,
}
impl fmt::Display for FormulaRole {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::FormulaRole::*;
match self {
Axiom => write!(f, "axiom"),
Hypothesis => write!(f, "hypothesis"),
Definition => write!(f, "definition"),
Assumption => write!(f, "assumption"),
Lemma => write!(f, "lemma"),
Theorem => write!(f, "theorem"),
Corollary => write!(f, "corollary"),
Conjecture => write!(f, "conjecture"),
NegatedConjecture => write!(f, "negated_conjecture"),
Plain => write!(f, "plain"),
Unknown => write!(f, "unknown"),
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum DagSource<'a> {
Name(Name<'a>),
Inference(Cow<'a, str>, Vec<Source<'a>>),
}
impl<'a> fmt::Display for DagSource<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::DagSource::*;
match self {
Name(ref name) => write!(f, "{}", name),
Inference(ref rule, ref parents) => {
write!(f, "inference({},[],[", rule)?;
if !parents.is_empty() {
let mut parents = parents.iter();
write!(f, "{}", parents.next().unwrap())?;
for parent in parents {
write!(f, ",{}", parent)?;
}
}
write!(f, "])")
}
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum InternalSource {}
impl fmt::Display for InternalSource {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "")
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum ExternalSource<'a> {
File(Cow<'a, str>, Option<Name<'a>>),
}
impl<'a> fmt::Display for ExternalSource<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::ExternalSource::*;
match self {
File(ref name, None) => write!(f, "file('{}')", name),
File(ref name, Some(info)) => {
write!(f, "file('{}',{})", name, info)
}
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum Source<'a> {
Unknown,
Dag(DagSource<'a>),
Internal(InternalSource),
External(ExternalSource<'a>),
Sources(Vec<Source<'a>>),
}
impl<'a> fmt::Display for Source<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::Source::*;
match self {
Unknown => write!(f, "unknown"),
Dag(ref dag) => write!(f, "{}", dag),
Internal(ref internal) => write!(f, "{}", internal),
External(ref external) => write!(f, "{}", external),
Sources(ref sources) => {
write!(f, "[",)?;
if !sources.is_empty() {
let mut sources = sources.iter();
write!(f, "{}", sources.next().unwrap())?;
for source in sources {
write!(f, ",{}", source)?;
}
}
write!(f, "]")
}
}
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct Annotations<'a> {
pub source: Source<'a>,
}
impl<'a> fmt::Display for Annotations<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}", self.source)
}
}
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct Included<'a>(pub Cow<'a, str>);
impl<'a> fmt::Display for Included<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
self.0.fmt(f)
}
}
impl<'a> From<Included<'a>> for PathBuf {
fn from(included: Included<'a>) -> Self {
included.0.replace("\\\\", "\\").replace("\\'", "'").into()
}
}
#[allow(clippy::large_enum_variant)]
#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum Statement<'a> {
Include(Included<'a>, Option<Vec<Name<'a>>>),
Cnf(
Name<'a>,
FormulaRole,
CnfFormula<'a>,
Option<Annotations<'a>>,
),
Fof(
Name<'a>,
FormulaRole,
FofFormula<'a>,
Option<Annotations<'a>>,
),
}
impl<'a> fmt::Display for Statement<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::Statement::*;
match self {
Include(include, None) => write!(f, "include({}).", include),
Include(include, Some(names)) => {
write!(f, "include({},[", include)?;
let mut names = names.iter();
write!(f, "{}", names.next().unwrap())?;
for name in names {
write!(f, ",{}", name)?;
}
write!(f, ").")
}
Cnf(name, role, formula, None) => {
write!(f, "cnf({},{},{}).", name, role, formula)
}
Cnf(name, role, formula, Some(annotations)) => {
write!(f, "cnf({},{},{},{}).", name, role, formula, annotations)
}
Fof(name, role, formula, None) => {
write!(f, "fof({},{},{}).", name, role, formula)
}
Fof(name, role, formula, Some(annotations)) => {
write!(f, "fof({},{},{},{}).", name, role, formula, annotations)
}
}
}
}